1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 well_sorted.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2007-12-29.
15
16 Revision History:
17
18 --*/
19
20 #include<sstream>
21 #include "ast/for_each_expr.h"
22 #include "ast/well_sorted.h"
23 #include "ast/ast_ll_pp.h"
24 #include "ast/ast_pp.h"
25 #include "util/warning.h"
26 #include "ast/ast_smt2_pp.h"
27
28 namespace {
29
30 struct well_sorted_proc {
31 ast_manager & m_manager;
32 bool m_error;
33
well_sorted_proc__anon71551d310111::well_sorted_proc34 well_sorted_proc(ast_manager & m):m_manager(m), m_error(false) {}
35
operator ()__anon71551d310111::well_sorted_proc36 void operator()(var * v) {}
37
operator ()__anon71551d310111::well_sorted_proc38 void operator()(quantifier * n) {
39 expr const * e = n->get_expr();
40 if (!is_lambda(n) && !m_manager.is_bool(e)) {
41 warning_msg("quantifier's body must be a boolean.");
42 m_error = true;
43 UNREACHABLE();
44 }
45 }
46
operator ()__anon71551d310111::well_sorted_proc47 void operator()(app * n) {
48 unsigned num_args = n->get_num_args();
49 func_decl * decl = n->get_decl();
50 if (num_args != decl->get_arity() && !decl->is_associative() &&
51 !decl->is_right_associative() && !decl->is_left_associative()) {
52 TRACE("ws", tout << "unexpected number of arguments.\n" << mk_ismt2_pp(n, m_manager););
53 warning_msg("unexpected number of arguments.");
54 m_error = true;
55 return;
56 }
57
58 for (unsigned i = 0; i < num_args; i++) {
59 sort * actual_sort = n->get_arg(i)->get_sort();
60 sort * expected_sort = decl->is_associative() ? decl->get_domain(0) : decl->get_domain(i);
61 if (expected_sort != actual_sort) {
62 TRACE("tc", tout << "sort mismatch on argument #" << i << ".\n" << mk_ismt2_pp(n, m_manager);
63 tout << "Sort mismatch for argument " << i+1 << " of " << mk_ismt2_pp(n, m_manager, false) << "\n";
64 tout << "Expected sort: " << mk_pp(expected_sort, m_manager) << "\n";
65 tout << "Actual sort: " << mk_pp(actual_sort, m_manager) << "\n";
66 tout << "Function sort: " << mk_pp(decl, m_manager) << ".";
67 );
68 std::ostringstream strm;
69 strm << "Sort mismatch for argument " << i+1 << " of " << mk_ll_pp(n, m_manager, false) << "\n";
70 strm << "Expected sort: " << mk_pp(expected_sort, m_manager) << '\n';
71 strm << "Actual sort: " << mk_pp(actual_sort, m_manager) << '\n';
72 strm << "Function sort: " << mk_pp(decl, m_manager) << '.';
73 auto str = strm.str();
74 warning_msg("%s", str.c_str());
75 m_error = true;
76 return;
77 }
78 }
79 }
80 };
81
82 }
83
is_well_sorted(ast_manager const & m,expr * n)84 bool is_well_sorted(ast_manager const & m, expr * n) {
85 well_sorted_proc p(const_cast<ast_manager&>(m));
86 for_each_expr(p, n);
87 return !p.m_error;
88 }
89
90
91