From 41c9e2b1a47e23959f66fc655e3e142fd2864919 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Sep 2013 11:27:52 -0700 Subject: [PATCH 1/5] check equalities with unknown evaluations Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_util.cpp | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp index d021d5fb1..f122f1e2c 100644 --- a/src/muz/pdr/pdr_util.cpp +++ b/src/muz/pdr/pdr_util.cpp @@ -112,8 +112,8 @@ namespace pdr { set_value(e, val); } else { - IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";); - TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";); + IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";); + TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";); set_x(e); } } @@ -672,7 +672,19 @@ namespace pdr { eval_array_eq(e, arg1, arg2); } else if (is_x(arg1) || is_x(arg2)) { - set_x(e); + expr_ref eq(m), vl(m); + eq = m.mk_eq(arg1, arg2); + m_model->eval(eq, vl); + if (m.is_true(vl)) { + set_bool(e, true); + } + else if (m.is_false(vl)) { + set_bool(e, false); + } + else { + TRACE("pdr", tout << "cannot evaluate: " << mk_pp(vl, m) << "\n";); + set_x(e); + } } else if (m.is_bool(arg1)) { bool val = is_true(arg1) == is_true(arg2); From 0a964c324eba0b511c11b14f76c253d55b8d0e0c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Sep 2013 12:32:16 -0700 Subject: [PATCH 2/5] test for undetermined accessor for PDR Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 2 +- src/muz/base/dl_rule.cpp | 19 ++++++++++++++++--- src/muz/base/dl_rule.h | 2 +- 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index f08efb00a..8183744b5 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -576,7 +576,7 @@ namespace datalog { void context::check_uninterpreted_free(rule_ref& r) { func_decl* f = 0; - if (r->has_uninterpreted_non_predicates(f)) { + if (r->has_uninterpreted_non_predicates(m, f)) { std::stringstream stm; stm << "Uninterpreted '" << f->get_name() diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 96e2b163a..184a5fa02 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -43,6 +43,7 @@ Revision History: #include"expr_safe_replace.h" #include"filter_model_converter.h" #include"scoped_proof.h" +#include"datatype_decl_plugin.h" namespace datalog { @@ -881,9 +882,12 @@ namespace datalog { } struct uninterpreted_function_finder_proc { + ast_manager& m; + datatype_util m_dt; bool m_found; func_decl* m_func; - uninterpreted_function_finder_proc() : m_found(false), m_func(0) {} + uninterpreted_function_finder_proc(ast_manager& m): + m(m), m_dt(m), m_found(false), m_func(0) {} void operator()(var * n) { } void operator()(quantifier * n) { } void operator()(app * n) { @@ -891,6 +895,14 @@ namespace datalog { m_found = true; m_func = n->get_decl(); } + else if (m_dt.is_accessor(n)) { + sort* s = m.get_sort(n->get_arg(0)); + SASSERT(m_dt.is_datatype(s)); + if (m_dt.get_datatype_constructors(s)->size() > 1) { + m_found = true; + m_func = n->get_decl(); + } + } } bool found(func_decl*& f) const { f = m_func; return m_found; } @@ -900,9 +912,9 @@ namespace datalog { // non-predicates may appear only in the interpreted tail, it is therefore // sufficient only to check the tail. // - bool rule::has_uninterpreted_non_predicates(func_decl*& f) const { + bool rule::has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const { unsigned sz = get_tail_size(); - uninterpreted_function_finder_proc proc; + uninterpreted_function_finder_proc proc(m); expr_mark visited; for (unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) { for_each_expr(proc, visited, get_tail(i)); @@ -910,6 +922,7 @@ namespace datalog { return proc.found(f); } + struct quantifier_finder_proc { bool m_exist; bool m_univ; diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 77bf9ac74..1c31dc6b4 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -293,7 +293,7 @@ namespace datalog { */ bool is_in_tail(const func_decl * p, bool only_positive=false) const; - bool has_uninterpreted_non_predicates(func_decl*& f) const; + bool has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const; void has_quantifiers(bool& existential, bool& universal) const; bool has_quantifiers() const; bool has_negation() const; From fd1f4b91911cb9628e3419244fcb3646540bad97 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Sep 2013 04:07:08 +0300 Subject: [PATCH 3/5] fix bugs reported by Anvesh Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 2 +- src/smt/diff_logic.h | 7 +++++++ src/smt/theory_utvpi_def.h | 3 ++- 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 739a9e61a..f68457383 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6449,7 +6449,7 @@ class Tactic: def _to_goal(a): if isinstance(a, BoolRef): - goal = Goal() + goal = Goal(a.ctx) goal.add(a) return goal else: diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 6fd156e41..2717e4a92 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -820,6 +820,7 @@ public: } } +private: // Update the assignment of variable v, that is, // m_assignment[v] += inc // This method also stores the old value of v in the assignment stack. @@ -829,6 +830,12 @@ public: m_assignment[v] += inc; } +public: + + void inc_assignment(dl_var v, numeral const& inc) { + m_assignment[v] += inc; + } + struct every_var_proc { bool operator()(dl_var v) const { diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 8463eb17f..6039b208a 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -752,7 +752,8 @@ namespace smt { for (unsigned j = 0; j < zero_v.size(); ++j) { int v = zero_v[j]; - m_graph.acc_assignment(v, numeral(-1)); + + m_graph.inc_assignment(v, numeral(-1)); th_var k = from_var(v); if (!is_parity_ok(k)) { todo.push_back(k); From 2e7f5303ebfe9fe7e77da8af34d97bf7063b0844 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Sep 2013 04:56:38 +0300 Subject: [PATCH 4/5] address incompleteness bug in axiomatization of int2bv Signed-off-by: Nikolaj Bjorner --- src/smt/theory_bv.cpp | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 559ce155b..a338be50a 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -581,10 +581,13 @@ namespace smt { void theory_bv::assert_int2bv_axiom(app* n) { // // create the axiom: - // bv2int(n) = e mod 2^bit_width - // + // bv2int(n) = e mod 2^bit_width // where n = int2bv(e) // + // Create the axioms: + // bit2bool(i,n) == ((e div 2^i) mod 2 != 0) + // for i = 0,.., sz-1 + // SASSERT(get_context().e_internalized(n)); SASSERT(m_util.is_int2bv(n)); ast_manager & m = get_manager(); @@ -592,10 +595,12 @@ namespace smt { parameter param(m_autil.mk_int()); expr* n_expr = n; - expr* lhs = m.mk_app(get_id(), OP_BV2INT, 1, ¶m, 1, &n_expr); + expr* e = n->get_arg(0); + expr_ref lhs(m), rhs(m); + lhs = m.mk_app(get_id(), OP_BV2INT, 1, ¶m, 1, &n_expr); unsigned sz = m_util.get_bv_size(n); numeral mod = power(numeral(2), sz); - expr* rhs = m_autil.mk_mod(n->get_arg(0), m_autil.mk_numeral(mod, true)); + rhs = m_autil.mk_mod(e, m_autil.mk_numeral(mod, true)); literal l(mk_eq(lhs, rhs, false)); ctx.mark_as_relevant(l); @@ -605,6 +610,24 @@ namespace smt { tout << mk_pp(lhs, m) << " == \n"; tout << mk_pp(rhs, m) << "\n"; ); + + expr_ref_vector n_bits(m); + enode * n_enode = mk_enode(n); + get_bits(n_enode, n_bits); + + for (unsigned i = 0; i < sz; ++i) { + numeral div = power(numeral(2), i); + mod = numeral(2); + rhs = m_autil.mk_idiv(e, m_autil.mk_numeral(div,true)); + rhs = m_autil.mk_mod(rhs, m_autil.mk_numeral(mod, true)); + rhs = m.mk_eq(rhs, m_autil.mk_numeral(rational(1), true)); + lhs = n_bits.get(i); + TRACE("bv", tout << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";); + l = literal(mk_eq(lhs, rhs, false)); + ctx.mark_as_relevant(l); + ctx.mk_th_axiom(get_id(), 1, &l); + + } } From c1384095f356a478d91ec08759ed86d053d06b9c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Sep 2013 21:44:24 +0300 Subject: [PATCH 5/5] fix default argument identification Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index f68457383..aaad24256 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6449,7 +6449,7 @@ class Tactic: def _to_goal(a): if isinstance(a, BoolRef): - goal = Goal(a.ctx) + goal = Goal(ctx = a.ctx) goal.add(a) return goal else: