From 20cfbcd66b680bad0973c88963b1b19ed2264920 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jan 2016 13:29:44 -0800 Subject: [PATCH 01/10] dealing with issues #402 #399 #258 Signed-off-by: Nikolaj Bjorner --- src/api/api_quant.cpp | 5 +++++ src/api/python/z3.py | 2 ++ src/smt/theory_arith.h | 2 ++ src/smt/theory_arith_aux.h | 3 ++- src/smt/theory_arith_core.h | 41 +++++++++++++++++++++++++++++++++---- src/smt/theory_arith_eq.h | 3 +++ 6 files changed, 51 insertions(+), 5 deletions(-) diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index cfaf5b6df..73215580e 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -162,6 +162,11 @@ extern "C" { ptr_vector bound_asts; if (num_patterns > 0 && num_no_patterns > 0) { SET_ERROR_CODE(Z3_INVALID_USAGE); + RETURN_Z3(0); + } + if (num_bound == 0) { + SET_ERROR_CODE(Z3_INVALID_USAGE); + RETURN_Z3(0); } for (unsigned i = 0; i < num_bound; ++i) { app* a = to_app(bound[i]); diff --git a/src/api/python/z3.py b/src/api/python/z3.py index b8ec74d18..686d838b2 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1815,6 +1815,8 @@ def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], if is_app(vs): vs = [vs] num_vars = len(vs) + if num_vars == 0: + raise Z3Exception("Quantification requires a non-empty list of variables.") _vs = (Ast * num_vars)() for i in range(num_vars): ## TODO: Check if is constant diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 7b56f19e5..703e19f1d 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -544,6 +544,8 @@ namespace smt { void set_var_kind(theory_var v, var_kind k) { m_data[v].m_kind = k; } unsigned get_var_row(theory_var v) const { SASSERT(!is_non_base(v)); return m_data[v].m_row_id; } void set_var_row(theory_var v, unsigned r_id) { m_data[v].m_row_id = r_id; } + ptr_vector m_todo; + bool is_int_expr(expr* e); bool is_int(theory_var v) const { return m_data[v].m_is_int; } bool is_real(theory_var v) const { return !is_int(v); } bool get_implied_old_value(theory_var v, inf_numeral & r) const; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 4291590c6..72004f8b0 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -838,8 +838,9 @@ namespace smt { template typename theory_arith::inf_numeral theory_arith::normalize_bound(theory_var v, inf_numeral const & k, bound_kind kind) { - if (is_real(v)) + if (is_real(v)) { return k; + } if (kind == B_LOWER) return inf_numeral(ceil(k)); SASSERT(kind == B_UPPER); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 4561e1ced..6f245d1c6 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -64,12 +64,44 @@ namespace smt { return f >= adaptive_assertion_threshold(); } + template + bool theory_arith::is_int_expr(expr* e) { + if (m_util.is_int(e)) return true; + if (is_uninterp(e)) return false; + m_todo.reset(); + m_todo.push_back(e); + rational r; + unsigned i = 0; + while (!m_todo.empty()) { + ++i; + if (i > 100) { + return false; + } + e = m_todo.back(); + m_todo.pop_back(); + if (m_util.is_to_real(e)) { + // pass + } + else if (m_util.is_numeral(e, r) && r.is_int()) { + // pass + } + else if (m_util.is_add(e) || m_util.is_mul(e)) { + m_todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else { + return false; + } + } + return true; + } + + template theory_var theory_arith::mk_var(enode * n) { theory_var r = theory::mk_var(n); SASSERT(r == static_cast(m_columns.size())); SASSERT(check_vector_sizes()); - bool is_int = m_util.is_int(n->get_owner()); + bool is_int = is_int_expr(n->get_owner()); TRACE("mk_arith_var", tout << mk_pp(n->get_owner(), get_manager()) << " is_int: " << is_int << "\n";); m_columns .push_back(column()); m_data .push_back(var_data(is_int)); @@ -835,7 +867,6 @@ namespace smt { void theory_arith::mk_bound_axioms(atom * a1) { theory_var v = a1->get_var(); atoms & occs = m_var_occs[v]; - //SASSERT(v != 15); TRACE("mk_bound_axioms", tout << "add bound axioms for v" << v << " " << a1 << "\n";); if (!get_context().is_searching()) { // @@ -974,9 +1005,9 @@ namespace smt { --i; } } - TRACE("arith", + CTRACE("arith", !atoms.empty(), for (unsigned i = 0; i < atoms.size(); ++i) { - atoms[i]->display(*this, tout); + atoms[i]->display(*this, tout); tout << "\n"; }); ptr_vector occs(m_var_occs[v]); @@ -1106,6 +1137,8 @@ namespace smt { kind = A_LOWER; app * lhs = to_app(n->get_arg(0)); app * rhs = to_app(n->get_arg(1)); + expr * rhs2; + if (m_util.is_to_real(rhs, rhs2) && is_app(rhs2)) { rhs = to_app(rhs2); } SASSERT(m_util.is_numeral(rhs)); theory_var v = internalize_term_core(lhs); if (v == null_theory_var) { diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index 7e61b968e..7ed6cfe50 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -328,6 +328,9 @@ namespace smt { // Ignore equality if variables are already known to be equal. if (is_equal(x, y)) return; + if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) { + return; + } context & ctx = get_context(); region & r = ctx.get_region(); enode * _x = get_enode(x); From 0df4931c4b5cfc42358d7063806309a219fee03a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jan 2016 15:43:47 -0800 Subject: [PATCH 02/10] dealing with issue #402 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 2 +- src/smt/smt_internalizer.cpp | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 686d838b2..2670dfa9a 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1816,7 +1816,7 @@ def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], vs = [vs] num_vars = len(vs) if num_vars == 0: - raise Z3Exception("Quantification requires a non-empty list of variables.") + return body _vs = (Ast * num_vars)() for i in range(num_vars): ## TODO: Check if is constant diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 13999222f..18e8879e9 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -322,6 +322,9 @@ namespace smt { TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m_manager) << "\n";); TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m_manager) << "\n";); if (m_manager.is_bool(n)) { + if (is_var(n)) { + throw default_exception("Formulas should not contain unbound variables"); + } SASSERT(is_quantifier(n) || is_app(n)); internalize_formula(n, gate_ctx); } From fce286db918d2568a571b485d44a40d80d865fa0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Jan 2016 17:11:12 -0800 Subject: [PATCH 03/10] Issue #354. Fix unsoundness in Array theory based on missing propagation of selects over ite expressions Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/proto_model.cpp | 11 ++++++-- src/smt/proto_model/proto_model.h | 3 ++- src/smt/smt_context.cpp | 1 + src/smt/smt_context.h | 2 ++ src/smt/smt_context_inv.cpp | 39 +++++++++++++++++++++++++++ src/smt/smt_context_pp.cpp | 1 + src/smt/smt_model_checker.cpp | 10 ++++++- src/smt/smt_model_finder.cpp | 2 +- src/smt/theory_array.cpp | 41 +++++++++++++++++++++++++---- src/smt/theory_array_base.cpp | 12 +++++++++ 10 files changed, 112 insertions(+), 10 deletions(-) diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 26ff0136c..024de9f15 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -174,6 +174,13 @@ bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & resu return true; } +bool proto_model::is_select_of_model_value(expr* e) const { + return + is_app_of(e, m_afid, OP_SELECT) && + is_as_array(to_app(e)->get_arg(0)) && + has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0)))); +} + /** \brief Evaluate the expression e in the current model, and store the result in \c result. It returns \c true if succeeded, and false otherwise. If the evaluation fails, @@ -257,7 +264,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t); TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";); trail.push_back(new_t); - if (!is_app(new_t) || to_app(new_t)->get_decl() != f) { + if (!is_app(new_t) || to_app(new_t)->get_decl() != f || is_select_of_model_value(new_t)) { // if the result is not of the form (f ...), then assume we must simplify it. expr * new_new_t = 0; if (!eval_cache.find(new_t.get(), new_new_t)) { @@ -588,7 +595,7 @@ void proto_model::register_value(expr * n) { } } -bool proto_model::is_array_value(expr * v) const { +bool proto_model::is_as_array(expr * v) const { return is_app_of(v, m_afid, OP_AS_ARRAY); } diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h index 578880459..d26f4d70d 100644 --- a/src/smt/proto_model/proto_model.h +++ b/src/smt/proto_model/proto_model.h @@ -59,6 +59,7 @@ class proto_model : public model_core { void remove_aux_decls_not_in_set(ptr_vector & decls, func_decl_set const & s); void cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs); + bool is_select_of_model_value(expr* e) const; public: proto_model(ast_manager & m, simplifier & s, params_ref const & p = params_ref()); @@ -68,7 +69,7 @@ public: bool eval(expr * e, expr_ref & result, bool model_completion = false); - bool is_array_value(expr * v) const; + bool is_as_array(expr * v) const; value_factory * get_factory(family_id fid); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 04b7ce234..9b9fdf841 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4126,6 +4126,7 @@ namespace smt { if (m_fparams.m_model_compact) m_proto_model->compress(); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); + SASSERT(validate_model()); } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index fd1049626..38463abe2 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1415,6 +1415,8 @@ namespace smt { bool update_model(bool refinalize); void get_proto_model(proto_model_ref & m) const; + + bool validate_model(); unsigned get_num_asserted_formulas() const { return m_asserted_formulas.get_num_formulas(); } diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index dabeab401..50814b686 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -399,6 +399,45 @@ namespace smt { #endif + bool context::validate_model() { + if (!m_proto_model) { + return true; + } + ast_manager& m = m_manager; + literal_vector::const_iterator it = m_assigned_literals.begin(); + literal_vector::const_iterator end = m_assigned_literals.end(); + for (; it != end; ++it) { + literal lit = *it; + if (!is_relevant(lit)) { + continue; + } + expr_ref n(m), res(m); + literal2expr(lit, n); + if (!is_ground(n)) { + continue; + } + switch (get_assignment(*it)) { + case l_undef: + break; + case l_true: + m_proto_model->eval(n, res, false); + CTRACE("mbqi_bug", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); + if (m.is_false(res)) { + return false; + } + break; + case l_false: + m_proto_model->eval(n, res, false); + CTRACE("mbqi_bug", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); + if (m.is_true(res)) { + return false; + } + break; + } + } + return true; + } + /** \brief validate unsat core returned by */ diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 79684570e..695c71eea 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -239,6 +239,7 @@ namespace smt { first = false; } out << "#" << n->get_id() << " -> #" << r->get_id() << "\n"; + out << mk_pp(n, m_manager) << " -> " << mk_pp(r, m_manager) << "\n"; } } } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 09b8fe4b6..b294bf4c9 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -346,6 +346,10 @@ namespace smt { for (; it != end; ++it) { quantifier * q = *it; if(!m_qm->mbqi_enabled(q)) continue; + TRACE("model_checker", + tout << "Check: " << mk_pp(q, m_manager) << "\n"; + tout << m_context->get_assignment(q) << "\n";); + if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) { if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) { verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n"; @@ -364,8 +368,12 @@ namespace smt { m_iteration_idx++; TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md);); - TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); + TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); m_max_cexs += m_params.m_mbqi_max_cexs; + + if (num_failures == 0 && !m_context->validate_model()) { + num_failures = 1; + } if (num_failures == 0) m_curr_model->cleanup(); if (m_params.m_mbqi_trace) { diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 2e260cbca..d7dc4d806 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1418,7 +1418,7 @@ namespace smt { func_decl * get_array_func_decl(app * ground_array, auf_solver & s) { expr * ground_array_interp = s.eval(ground_array, false); - if (ground_array_interp != 0 && s.get_model()->is_array_value(ground_array_interp)) + if (ground_array_interp != 0 && s.get_model()->is_as_array(ground_array_interp)) return to_func_decl(to_app(ground_array_interp)->get_decl()->get_parameter(0).get_ast()); return 0; } diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 7ba94d9cb..960218dff 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -44,7 +44,9 @@ namespace smt { void theory_array::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) { // v1 is the new root - TRACE("array", tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1);); + TRACE("array", + tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1); + tout << mk_pp(get_enode(v1)->get_owner(), get_manager()) << " <- " << mk_pp(get_enode(v2)->get_owner(), get_manager()) << "\n";); SASSERT(v1 == find(v1)); var_data * d1 = m_var_data[v1]; var_data * d2 = m_var_data[v2]; @@ -70,21 +72,41 @@ namespace smt { } theory_var theory_array::mk_var(enode * n) { + ast_manager& m = get_manager(); + context& ctx = get_context(); theory_var r = theory_array_base::mk_var(n); theory_var r2 = m_find.mk_var(); SASSERT(r == r2); SASSERT(r == static_cast(m_var_data.size())); m_var_data.push_back(alloc(var_data)); var_data * d = m_var_data[r]; - TRACE("array", tout << mk_bounded_pp(n->get_owner(), get_manager()) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) << + TRACE("array", tout << mk_bounded_pp(n->get_owner(), m) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) << ", is_store: " << is_store(n) << "\n";); d->m_is_array = is_array_sort(n); if (d->m_is_array) - register_sort(get_manager().get_sort(n->get_owner())); + register_sort(m.get_sort(n->get_owner())); d->m_is_select = is_select(n); + + expr* e1, *e2, *e3; if (is_store(n)) d->m_stores.push_back(n); - get_context().attach_th_var(n, this, r); + else if (m.is_ite(n->get_owner(), e1, e2, e3)) { + ptr_vector todo; + todo.push_back(e2); + todo.push_back(e3); + while (!todo.empty()) { + e1 = todo.back(); + todo.pop_back(); + if (is_app(e1) && is_store(to_app(e1))) { + d->m_stores.push_back(ctx.get_enode(e1)); + } + else if (m.is_ite(e1, e1, e2, e3)) { + todo.push_back(e2); + todo.push_back(e3); + } + } + } + ctx.attach_th_var(n, this, r); if (m_params.m_array_laziness <= 1 && is_store(n)) instantiate_axiom1(n); return r; @@ -97,6 +119,7 @@ namespace smt { v = find(v); var_data * d = m_var_data[v]; d->m_parent_selects.push_back(s); + TRACE("array", tout << mk_pp(s->get_owner(), get_manager()) << " " << mk_pp(get_enode(v)->get_owner(), get_manager()) << "\n";); m_trail_stack.push(push_back_trail(d->m_parent_selects)); ptr_vector::iterator it = d->m_stores.begin(); ptr_vector::iterator end = d->m_stores.end(); @@ -109,8 +132,13 @@ namespace smt { for (; it != end; ++it) { enode * store = *it; SASSERT(is_store(store)); - if (!m_params.m_array_cg || store->is_cgr()) + std::cout << mk_pp(store->get_owner(), get_manager()) << " " << mk_pp(s->get_owner(), get_manager()) << "\n"; + if (!m_params.m_array_cg || store->is_cgr()) { instantiate_axiom2b(s, store); + } + else { + std::cout << mk_pp(store->get_owner(), get_manager()) << "\n"; + } } } } @@ -331,6 +359,9 @@ namespace smt { void theory_array::relevant_eh(app * n) { if (m_params.m_array_laziness == 0) return; + if (get_manager().is_ite(n)) { + TRACE("array", tout << "relevant ite " << mk_pp(n, get_manager()) << "\n";); + } if (!is_store(n) && !is_select(n)) return; context & ctx = get_context(); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 4526b283a..498f8aeec 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -943,6 +943,18 @@ namespace smt { result->add_entry(args.size(), args.c_ptr(), select); } } + TRACE("array", + tout << mk_pp(n->get_root()->get_owner(), get_manager()) << "\n"; + if (sel_set) { + select_set::iterator it = sel_set->begin(); + select_set::iterator end = sel_set->end(); + for (; it != end; ++it) { + tout << "#" << (*it)->get_root()->get_owner()->get_id() << " " << mk_pp((*it)->get_owner(), get_manager()) << "\n"; + } + } + if (else_val_n) { + tout << "else: " << mk_pp(else_val_n->get_owner(), get_manager()) << "\n"; + }); return result; } From 082dcda7f7e2e5850fc6b7a9b4452c493b280a05 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Jan 2016 19:16:59 -0800 Subject: [PATCH 04/10] Fix Issue #405: Horn normal form ignores implication Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_rule.cpp | 4 ++++ src/muz/base/hnf.cpp | 11 ++++++++++- src/smt/smt_context.cpp | 2 +- 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index aa010ab5a..693391bef 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -282,6 +282,8 @@ namespace datalog { func_decl* rule_manager::mk_query(expr* query, rule_set& rules) { + TRACE("dl", tout << mk_pp(query, m) << "\n";); + ptr_vector vars; svector names; app_ref_vector body(m); @@ -290,6 +292,7 @@ namespace datalog { // Add implicit variables. // Remove existential prefix. bind_variables(query, false, q); + quantifier_hoister qh(m); qh.pull_quantifier(false, q, 0, &names); // retrieve free variables. @@ -358,6 +361,7 @@ namespace datalog { if (!vars.empty()) { rule_expr = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), impl); } + TRACE("dl", tout << rule_expr << "\n";); scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED); proof_ref pr(m); diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp index 6c1e917c3..6d1c19a13 100644 --- a/src/muz/base/hnf.cpp +++ b/src/muz/base/hnf.cpp @@ -325,9 +325,10 @@ private: void eliminate_disjunctions(expr_ref_vector::element_ref& body, proof_ref_vector& proofs) { expr* b = body.get(); - expr* e1; + expr* e1, *e2; bool negate_args = false; bool is_disj = false; + expr_ref_vector _body(m); unsigned num_disj = 0; expr* const* disjs = 0; if (!contains_predicate(b)) { @@ -346,6 +347,14 @@ private: num_disj = to_app(e1)->get_num_args(); disjs = to_app(e1)->get_args(); } + if (m.is_implies(b, e1, e2)) { + is_disj = true; + _body.push_back(mk_not(m, e1)); + _body.push_back(e2); + disjs = _body.c_ptr(); + num_disj = 2; + negate_args = false; + } if (is_disj) { app* old_head = 0; if (m_memoize_disj.find(b, old_head)) { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 9b9fdf841..f12708150 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4126,7 +4126,7 @@ namespace smt { if (m_fparams.m_model_compact) m_proto_model->compress(); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); - SASSERT(validate_model()); + //SASSERT(validate_model()); } } From 131f9e22478a8a1a361d5cfe0ab388acdee1eef9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Jan 2016 20:43:41 -0800 Subject: [PATCH 05/10] change queries to take function names instead of arbitrary predicates. This allows to bypass issues with having arbitrary query expressions compiled in arbitrary ways to auxiliary predicates where names of bound variables are reshuffled. See also Stackoverflow http://stackoverflow.com/questions/34693719/bug-in-z3-datalog Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 1 + src/muz/fp/dl_cmds.cpp | 25 ++++++++++++++++--------- src/parsers/smt2/smt2parser.cpp | 12 ++++++------ 3 files changed, 23 insertions(+), 15 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 8566482c4..e2b078bcd 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -891,6 +891,7 @@ namespace datalog { } lbool context::rel_query(unsigned num_rels, func_decl * const* rels) { + m_last_answer = 0; ensure_engine(); return m_engine->query(num_rels, rels); } diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 2ce96c15e..f8e97d95d 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -114,9 +114,16 @@ struct dl_context { } } - bool collect_query(expr* q) { + bool collect_query(func_decl* q) { if (m_collected_cmds) { - expr_ref qr = m_context->bind_vars(q, false); + ast_manager& m = m_cmd.m(); + expr_ref qr(m); + expr_ref_vector args(m); + for (unsigned i = 0; i < q->get_arity(); ++i) { + args.push_back(m.mk_var(i, q->get_domain(i))); + } + qr = m.mk_app(q, args.size(), args.c_ptr()); + qr = m_context->bind_vars(qr, false); m_collected_cmds->m_queries.push_back(qr); m_trail.push(push_back_vector(m_collected_cmds->m_queries)); return true; @@ -187,30 +194,30 @@ public: virtual void finalize(cmd_context & ctx) { } virtual void execute(cmd_context & ctx) { - m_dl_ctx->add_rule(m_t, m_name, m_bound); + m_dl_ctx->add_rule(m_t, m_name, m_bound); } }; class dl_query_cmd : public parametric_cmd { ref m_dl_ctx; - expr* m_target; + func_decl* m_target; public: dl_query_cmd(dl_context * dl_ctx): parametric_cmd("query"), m_dl_ctx(dl_ctx), m_target(0) { } - virtual char const * get_usage() const { return "(exists (q) (and body))"; } + virtual char const * get_usage() const { return "predicate"; } virtual char const * get_main_descr() const { - return "pose a query based on the Horn rules."; + return "pose a query to a predicate based on the Horn rules."; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { - if (m_target == 0) return CPK_EXPR; + if (m_target == 0) return CPK_FUNC_DECL; return parametric_cmd::next_arg_kind(ctx); } - virtual void set_next_arg(cmd_context & ctx, expr * t) { + virtual void set_next_arg(cmd_context & ctx, func_decl* t) { m_target = t; } @@ -239,7 +246,7 @@ public: scoped_timer timer(timeout, &eh); cmd_context::scoped_watch sw(ctx); try { - status = dlctx.query(m_target); + status = dlctx.rel_query(1, &m_target); } catch (z3_error & ex) { ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl; diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index c6736c1e0..b6350ed28 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -719,9 +719,9 @@ namespace smt2 { SASSERT(sort_stack().size() == stack_pos + 1); } - unsigned parse_sorts() { - unsigned sz = 0; - check_lparen_next("invalid list of sorts, '(' expected"); + unsigned parse_sorts(char const* context) { + unsigned sz = 0; + check_lparen_next(context); while (!curr_is_rparen()) { parse_sort(); sz++; @@ -2019,7 +2019,7 @@ namespace smt2 { symbol id = curr_id(); next(); unsigned spos = sort_stack().size(); - unsigned num_params = parse_sorts(); + unsigned num_params = parse_sorts("Parsing function declaration. Expecting sort list '('"); parse_sort(); func_decl_ref f(m()); f = m().mk_func_decl(id, num_params, sort_stack().c_ptr() + spos, sort_stack().back()); @@ -2300,7 +2300,7 @@ namespace smt2 { next(); } unsigned spos = sort_stack().size(); - parse_sorts(); + parse_sorts("Parsing function name. Expecting sort list startig with '(' to disambiguate function name"); unsigned domain_size = sort_stack().size() - spos; parse_sort(); func_decl * d = m_ctx.find_func_decl(id, indices.size(), indices.c_ptr(), domain_size, sort_stack().c_ptr() + spos, sort_stack().back()); @@ -2380,7 +2380,7 @@ namespace smt2 { return; case CPK_SORT_LIST: { unsigned spos = sort_stack().size(); - unsigned num = parse_sorts(); + unsigned num = parse_sorts("expecting sort list starting with '('"); m_curr_cmd->set_next_arg(m_ctx, num, sort_stack().c_ptr() + spos); break; } From d4c98c1ab45392d7d7632e0ab0287b3315569123 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Jan 2016 09:38:05 -0800 Subject: [PATCH 06/10] Corrected fix to #354: The parameters got shared between the MBQI checker and main context, overriding m_array_laziness to 0 which caused missing propagations Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array.cpp | 20 +------------------- src/smt/theory_array.h | 4 ++-- 2 files changed, 3 insertions(+), 21 deletions(-) diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 960218dff..1bc3ea8b8 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -85,27 +85,9 @@ namespace smt { d->m_is_array = is_array_sort(n); if (d->m_is_array) register_sort(m.get_sort(n->get_owner())); - d->m_is_select = is_select(n); - - expr* e1, *e2, *e3; + d->m_is_select = is_select(n); if (is_store(n)) d->m_stores.push_back(n); - else if (m.is_ite(n->get_owner(), e1, e2, e3)) { - ptr_vector todo; - todo.push_back(e2); - todo.push_back(e3); - while (!todo.empty()) { - e1 = todo.back(); - todo.pop_back(); - if (is_app(e1) && is_store(to_app(e1))) { - d->m_stores.push_back(ctx.get_enode(e1)); - } - else if (m.is_ite(e1, e1, e2, e3)) { - todo.push_back(e2); - todo.push_back(e3); - } - } - } ctx.attach_th_var(n, this, r); if (m_params.m_array_laziness <= 1 && is_store(n)) instantiate_axiom1(n); diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h index 9cc833d31..4e45f77f2 100644 --- a/src/smt/theory_array.h +++ b/src/smt/theory_array.h @@ -49,7 +49,7 @@ namespace smt { var_data():m_prop_upward(false), m_is_array(false), m_is_select(false) {} }; ptr_vector m_var_data; - theory_array_params & m_params; + theory_array_params& m_params; theory_array_stats m_stats; th_union_find m_find; th_trail_stack m_trail_stack; @@ -98,7 +98,7 @@ namespace smt { theory_array(ast_manager & m, theory_array_params & params); virtual ~theory_array(); - virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, new_ctx->get_manager(), m_params); } + virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, new_ctx->get_manager(), new_ctx->get_fparams()); } virtual char const * get_name() const { return "array"; } From a156028d82d062d719644b90f3b72cfbe67ba6a1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Jan 2016 09:46:10 -0800 Subject: [PATCH 07/10] pin expressions per Sarah Winkler's memory leak report Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 18e8879e9..21a3ef86c 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -291,15 +291,15 @@ namespace smt { return; } sort * s = m_manager.get_sort(n->get_arg(0)); - sort * u = m_manager.mk_fresh_sort("distinct-elems"); - func_decl * f = m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u); + sort_ref u(m_manager.mk_fresh_sort("distinct-elems"), m_manager); + func_decl_ref f(m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m_manager); for (unsigned i = 0; i < num_args; i++) { expr * arg = n->get_arg(i); - app * fapp = m_manager.mk_app(f, arg); - app * val = m_manager.mk_fresh_const("unique-value", u); + app_ref fapp(m_manager.mk_app(f, arg), m_manager); + app_ref val(m_manager.mk_fresh_const("unique-value", u), m_manager); enode * e = mk_enode(val, false, false, true); e->mark_as_interpreted(); - app * eq = m_manager.mk_eq(fapp, val); + app_ref eq(m_manager.mk_eq(fapp, val), m_manager); TRACE("assert_distinct", tout << "eq: " << mk_pp(eq, m_manager) << "\n";); assert_default(eq, 0); mark_as_relevant(eq); @@ -435,7 +435,7 @@ namespace smt { TRACE("distinct", tout << "internalizing distinct: " << mk_pp(n, m_manager) << "\n";); SASSERT(!b_internalized(n)); SASSERT(m_manager.is_distinct(n)); - expr * def = m_manager.mk_distinct_expanded(n->get_num_args(), n->get_args()); + expr_ref def(m_manager.mk_distinct_expanded(n->get_num_args(), n->get_args()), m_manager); internalize(def, true); bool_var v = mk_bool_var(n); literal l(v); @@ -753,8 +753,8 @@ namespace smt { expr * c = n->get_arg(0); expr * t = n->get_arg(1); expr * e = n->get_arg(2); - app * eq1 = mk_eq_atom(n, t); - app * eq2 = mk_eq_atom(n, e); + app_ref eq1(mk_eq_atom(n, t), m_manager); + app_ref eq2(mk_eq_atom(n, e), m_manager); mk_enode(n, true /* supress arguments, I don't want to apply CC on ite terms */, false /* it is a term, so it should not be merged with true/false */, From 79a5b133d796f267563ddcc80e75475f78bac896 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Jan 2016 11:04:44 -0800 Subject: [PATCH 08/10] fix debugging code in ast.cpp to take into account that literals may be repeated Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index ab1a5a5af..a74ab90c1 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2866,22 +2866,24 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro svector found; #endif for (unsigned i = 0; i < num_args; i++) { + bool found_complement = false; expr * lit = cls->get_arg(i); - unsigned j = 1; - for (; j < num_proofs; j++) { + for (unsigned j = 1; j < num_proofs; j++) { expr const * _fact = get_fact(proofs[j]); if (is_complement(lit, _fact)) { - DEBUG_CODE(found.setx(j, true, false);); + found_complement = true; + DEBUG_CODE(found.setx(j, true, false); continue;); break; } } - if (j == num_proofs) + if (!found_complement) new_lits.push_back(lit); } DEBUG_CODE({ for (unsigned i = 1; m_proof_mode == PGM_FINE && i < num_proofs; i++) { CTRACE("mk_unit_resolution_bug", !found.get(i, false), for (unsigned j = 0; j < num_proofs; j++) { + if (j == i) tout << "Index " << i << " was not found:\n"; tout << mk_ll_pp(get_fact(proofs[j]), *this); }); SASSERT(found.get(i, false)); From e22ac712b05f75f84477d5e3e354861a94394f56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Jan 2016 16:53:29 -0800 Subject: [PATCH 09/10] add model construction for disequations Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 24 ++++++++++++++++++++---- src/smt/theory_seq.h | 1 + src/smt/theory_seq_empty.h | 8 ++++---- 3 files changed, 25 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index f06afce71..c1083ea25 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -551,9 +551,6 @@ bool theory_seq::is_solved() { IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";); return false; } - if (!m_nqs.empty()) { - return false; - } for (unsigned i = 0; i < m_automata.size(); ++i) { if (!m_automata[i]) { IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";); @@ -1252,9 +1249,28 @@ void theory_seq::collect_statistics(::statistics & st) const { st.update("seq add axiom", m_stats.m_add_axiom); } +void theory_seq::init_model(expr_ref_vector const& es) { + expr_ref new_s(m); + for (unsigned i = 0; i < es.size(); ++i) { + dependency* eqs = 0; + expr_ref s = canonize(es[i], eqs); + if (is_var(s)) { + new_s = m_factory->get_fresh_value(m.get_sort(s)); + m_rep.update(s, new_s, eqs); + } + } +} + void theory_seq::init_model(model_generator & mg) { m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); mg.register_factory(m_factory); + for (unsigned j = 0; j < m_nqs.size(); ++j) { + ne const& n = m_nqs[j]; + for (unsigned i = 0; i < n.ls().size(); ++i) { + init_model(n.ls(i)); + init_model(n.rs(i)); + } + } } @@ -2182,7 +2198,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { m_rewrite(eq); if (!m.is_false(eq)) { literal lit = ~mk_eq(e1, e2, false); - SASSERT(get_context().get_assignment(lit) == l_true); + //SASSERT(get_context().get_assignment(lit) == l_true); dependency* dep = m_dm.mk_leaf(assumption(lit)); m_nqs.push_back(ne(e1, e2, dep)); solve_nqs(m_nqs.size() - 1); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index d14dbba6d..927cec537 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -301,6 +301,7 @@ namespace smt { virtual model_value_proc * mk_value(enode * n, model_generator & mg); virtual void init_model(model_generator & mg); + void init_model(expr_ref_vector const& es); // final check bool simplify_and_solve_eqs(); // solve unitary equalities bool branch_variable(); // branch on a variable diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 5065c733d..9c8f15a7a 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -31,7 +31,7 @@ namespace smt { symbol_set m_strings; unsigned m_next; char m_char; - std::string m_unique_prefix; + std::string m_unique_delim; obj_map m_unique_sequences; expr_ref_vector m_trail; public: @@ -43,7 +43,7 @@ namespace smt { u(m), m_next(0), m_char(0), - m_unique_prefix("#B"), + m_unique_delim("!"), m_trail(m) { m_strings.insert(symbol("")); @@ -56,7 +56,7 @@ namespace smt { } void set_prefix(char const* p) { - m_unique_prefix = p; + m_unique_delim = p; } // generic method for setting unique sequences @@ -89,7 +89,7 @@ namespace smt { if (u.is_string(s)) { while (true) { std::ostringstream strm; - strm << m_unique_prefix << m_next++; + strm << m_unique_delim << std::hex << m_next++ << std::dec << m_unique_delim; symbol sym(strm.str().c_str()); if (m_strings.contains(sym)) continue; m_strings.insert(sym); From 3bf8b17b96bd16bf3539db905c3c98d4912c2004 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Jan 2016 19:22:11 -0800 Subject: [PATCH 10/10] remove std::cout Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 1bc3ea8b8..c60efe1b1 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -114,13 +114,9 @@ namespace smt { for (; it != end; ++it) { enode * store = *it; SASSERT(is_store(store)); - std::cout << mk_pp(store->get_owner(), get_manager()) << " " << mk_pp(s->get_owner(), get_manager()) << "\n"; if (!m_params.m_array_cg || store->is_cgr()) { instantiate_axiom2b(s, store); } - else { - std::cout << mk_pp(store->get_owner(), get_manager()) << "\n"; - } } } }