diff --git a/src/api/python/z3.py b/src/api/python/z3.py index a71db82c5..84724e51e 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -635,7 +635,7 @@ class FuncDeclRef(AstRef): args = _get_args(args) num = len(args) if __debug__: - _z3_assert(num == self.arity(), "Incorrect number of arguments") + _z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self) _args = (Ast * num)() saved = [] for i in range(num): @@ -1735,7 +1735,7 @@ class ArithSortRef(SortRef): """Real and Integer sorts.""" def is_real(self): - """Return `True` if `self` is the integer sort. + """Return `True` if `self` is of the sort Real. >>> x = Real('x') >>> x.is_real() @@ -1749,7 +1749,7 @@ class ArithSortRef(SortRef): return self.kind() == Z3_REAL_SORT def is_int(self): - """Return `True` if `self` is the real sort. + """Return `True` if `self` is of the sort Integer. >>> x = Int('x') >>> x.is_int() diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 713727f05..f18e6a78e 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -949,6 +949,10 @@ public: mark.mark(s, true); } + void operator()(sort* s) { + ast_mark mark; + pp_sort_decl(mark, s); + } void operator()(func_decl* d) { if (m_is_smt2) { @@ -962,7 +966,6 @@ public: m_out << ") "; visit_sort(d->get_range()); m_out << ")"; - newline(); } else { m_out << "("; @@ -1021,6 +1024,22 @@ void ast_smt_pp::display_expr_smt2(std::ostream& strm, expr* n, unsigned indent, p(n); } +void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, unsigned num_var_names, char const* const* var_names) { + ptr_vector ql; + smt_renaming rn; + smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, indent, num_var_names, var_names); + if (is_expr(a)) { + p(to_expr(a)); + } + else if (is_func_decl(a)) { + p(to_func_decl(a)); + } + else { + SASSERT(is_sort(a)); + p(to_sort(a)); + } +} + void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { ptr_vector ql; @@ -1071,6 +1090,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { if (!(*m_is_declared)(d)) { smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0); p(d); + strm << "\n"; } } @@ -1079,6 +1099,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { if (!(*m_is_declared)(d)) { smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0); p(d); + strm << "\n"; } } diff --git a/src/ast/ast_smt_pp.h b/src/ast/ast_smt_pp.h index 36d4ced2e..97527759a 100644 --- a/src/ast/ast_smt_pp.h +++ b/src/ast/ast_smt_pp.h @@ -79,22 +79,23 @@ public: void display_smt2(std::ostream& strm, expr* n); void display_expr(std::ostream& strm, expr* n); void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0); + void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0); }; struct mk_smt_pp { - expr * m_expr; + ast* m_ast; ast_manager& m_manager; unsigned m_indent; unsigned m_num_var_names; char const* const* m_var_names; - mk_smt_pp(expr* e, ast_manager & m, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0) : - m_expr(e), m_manager(m), m_indent(indent), m_num_var_names(num_var_names), m_var_names(var_names) {} + mk_smt_pp(ast* e, ast_manager & m, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0) : + m_ast(e), m_manager(m), m_indent(indent), m_num_var_names(num_var_names), m_var_names(var_names) {} }; inline std::ostream& operator<<(std::ostream& out, const mk_smt_pp & p) { ast_smt_pp pp(p.m_manager); - pp.display_expr_smt2(out, p.m_expr, p.m_indent, p.m_num_var_names, p.m_var_names); + pp.display_ast_smt2(out, p.m_ast, p.m_indent, p.m_num_var_names, p.m_var_names); return out; } diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 77b391ef7..f11c9852d 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -994,6 +994,7 @@ namespace datalog { p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"); p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"); + p.insert(":print-low-level-smt2", CPK_BOOL, "(default true) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"); PRIVATE_PARAMS( p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL, @@ -1650,6 +1651,9 @@ namespace datalog { expr_ref_vector rules(m); svector names; bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true); + bool print_low_level = m_params.get_bool(":print-low-level-smt2", true); + +#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params); get_rules_as_formulas(rules, names); @@ -1684,18 +1688,18 @@ namespace datalog { obj_hashtable& sorts = visitor.sorts(); obj_hashtable::iterator sit = sorts.begin(), send = sorts.end(); for (; sit != send; ++sit) { - ast_smt2_pp(out, *sit, env, params); + PP(*sit); } for (; it != end; ++it) { func_decl* f = *it; - ast_smt2_pp(out, f, env, params); + PP(f); out << "\n"; } it = rels.begin(); end = rels.end(); for (; it != end; ++it) { func_decl* f = *it; out << "(declare-rel " << f->get_name() << " ("; - for (unsigned i = 0; i < f->get_arity(); ++i) { + for (unsigned i = 0; i < f->get_arity(); ++i) { ast_smt2_pp(out, f->get_domain(i), env, params); if (i + 1 < f->get_arity()) { out << " "; @@ -1714,7 +1718,7 @@ namespace datalog { for (unsigned i = 0; i < num_axioms; ++i) { out << "(assert "; - ast_smt2_pp(out, axioms[i], env, params); + PP(axioms[i]); out << ")\n"; } for (unsigned i = 0; i < rules.size(); ++i) { @@ -1724,12 +1728,7 @@ namespace datalog { if (symbol::null != nm) { out << "(! "; } - if (use_fixedpoint_extensions) { - ast_smt2_pp(out, r, env, params); - } - else { - out << mk_smt_pp(r, m); - } + PP(r); if (symbol::null != nm) { while (fresh_names.contains(nm)) { std::ostringstream s; @@ -1744,7 +1743,7 @@ namespace datalog { if (use_fixedpoint_extensions) { for (unsigned i = 0; i < num_queries; ++i) { out << "(query "; - ast_smt2_pp(out, queries[i], env, params); + PP(queries[i]); out << ")\n"; } } @@ -1754,7 +1753,7 @@ namespace datalog { out << "(assert "; expr_ref q(m); q = m.mk_not(queries[i]); - ast_smt2_pp(out, q, env, params); + PP(q); out << ")\n"; out << "(check-sat)\n"; if (num_queries > 1) out << "(pop)\n"; diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 909a42625..227b1aee7 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -43,6 +43,7 @@ Notes: #include "qe_lite.h" #include "ast_ll_pp.h" #include "proof_checker.h" +#include "smt_value_sort.h" namespace pdr { @@ -1827,14 +1828,14 @@ namespace pdr { if (!vars.empty()) { // also fresh names for auxiliary variables in body? expr_substitution sub(m); - expr_ref_vector refs(m); expr_ref tmp(m); proof_ref pr(m); pr = m.mk_asserted(m.mk_true()); - for (unsigned i = 0; i < vars.size(); ++i) { - VERIFY (M->eval(vars[i].get(), tmp, true)); - refs.push_back(tmp); - sub.insert(vars[i].get(), tmp, pr); + for (unsigned i = 0; i < vars.size(); ++i) { + if (smt::is_value_sort(m, vars[i].get())) { + VERIFY (M->eval(vars[i].get(), tmp, true)); + sub.insert(vars[i].get(), tmp, pr); + } } if (!rep) rep = mk_expr_simp_replacer(m); rep->set_substitution(&sub); diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index 2c009dc25..0fcb6c7c2 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -903,6 +903,7 @@ namespace pdr { return !has_x; } + void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) { ast_manager& m = fml.get_manager(); expr_ref_vector conjs(m); diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index ef8d27e2f..91784f5f5 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -29,6 +29,7 @@ Revision History: #include "array_decl_plugin.h" #include "uint_set.h" #include "model_v2_pp.h" +#include "smt_value_sort.h" namespace smt { @@ -134,44 +135,7 @@ namespace smt { } } } - } - - bool is_simple_type(sort* s) { - arith_util arith(m); - datatype_util data(m); - - ptr_vector sorts; - ast_mark mark; - sorts.push_back(s); - - while (!sorts.empty()) { - s = sorts.back(); - sorts.pop_back(); - if (mark.is_marked(s)) { - continue; - } - mark.mark(s, true); - if (arith.is_int_real(s)) { - // simple - } - else if (m.is_bool(s)) { - // simple - } - else if (data.is_datatype(s)) { - ptr_vector const& cs = *data.get_datatype_constructors(s); - for (unsigned i = 0; i < cs.size(); ++i) { - func_decl* f = cs[i]; - for (unsigned j = 0; j < f->get_arity(); ++j) { - sorts.push_back(f->get_domain(j)); - } - } - } - else { - return false; - } - } - return true; - } + } /** \brief Extract implied equalities for a collection of terms in the current context. @@ -216,7 +180,7 @@ namespace smt { uint_set non_values; - if (!is_simple_type(srt)) { + if (!is_value_sort(m, srt)) { for (unsigned i = 0; i < terms.size(); ++i) { non_values.insert(i); } diff --git a/src/smt/smt_value_sort.cpp b/src/smt/smt_value_sort.cpp new file mode 100644 index 000000000..a840b77b7 --- /dev/null +++ b/src/smt/smt_value_sort.cpp @@ -0,0 +1,74 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + smt_value_sort.cpp + +Abstract: + + Determine if elements of a given sort can be values. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-25 + +Revision History: + + +--*/ + +#include "smt_value_sort.h" +#include "bv_decl_plugin.h" +#include "arith_decl_plugin.h" +#include "datatype_decl_plugin.h" + +namespace smt { + + + bool is_value_sort(ast_manager& m, sort* s) { + arith_util arith(m); + datatype_util data(m); + bv_util bv(m); + + ptr_vector sorts; + ast_mark mark; + sorts.push_back(s); + + while (!sorts.empty()) { + s = sorts.back(); + sorts.pop_back(); + if (mark.is_marked(s)) { + continue; + } + mark.mark(s, true); + if (arith.is_int_real(s)) { + // simple + } + else if (m.is_bool(s)) { + // simple + } + else if (bv.is_bv_sort(s)) { + // simple + } + else if (data.is_datatype(s)) { + ptr_vector const& cs = *data.get_datatype_constructors(s); + for (unsigned i = 0; i < cs.size(); ++i) { + func_decl* f = cs[i]; + for (unsigned j = 0; j < f->get_arity(); ++j) { + sorts.push_back(f->get_domain(j)); + } + } + } + else { + return false; + } + } + return true; + } + + bool is_value_sort(ast_manager& m, expr* e) { + return is_value_sort(m, m.get_sort(e)); + } + +} diff --git a/src/smt/smt_value_sort.h b/src/smt/smt_value_sort.h new file mode 100644 index 000000000..ae32be62a --- /dev/null +++ b/src/smt/smt_value_sort.h @@ -0,0 +1,37 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + smt_value_sort.h + +Abstract: + + Determine if elements of a given sort can be values. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-25 + +Revision History: + + +--*/ + + +#ifndef __SMT_VALUE_SORT_H__ +#define __SMT_VALUE_SORT_H__ + +#include "ast.h" + + +namespace smt { + + bool is_value_sort(ast_manager& m, sort* s); + + bool is_value_sort(ast_manager& m, expr* e); + +}; + + +#endif