From 20cfbcd66b680bad0973c88963b1b19ed2264920 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jan 2016 13:29:44 -0800 Subject: [PATCH 01/15] 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/15] 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/15] 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/15] 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/15] 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/15] 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/15] 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 d4efa3753c05719d5d64f6decb97dcf373b92b9b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 11 Jan 2016 18:54:07 +0000 Subject: [PATCH 08/15] Optimization for real to float conversion. Relates to #383. --- src/util/mpf.cpp | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 1601d7fe3..24aa253a4 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -244,32 +244,35 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode m_mpq_manager.abs(sig); m_mpz_manager.set(exp, exponent); - // Normalize - while (m_mpq_manager.ge(sig, 2)) { - m_mpq_manager.div(sig, mpq(2), sig); - m_mpz_manager.inc(exp); + // Normalize such that 1.0 <= sig < 2.0 + if (m_mpq_manager.ge(sig, mpq(2))) { + unsigned int pp = m_mpq_manager.prev_power_of_two(sig); + scoped_mpz p2(m_mpz_manager); + m_mpq_manager.power(2, pp, p2); + m_mpq_manager.div(sig, p2, sig); + m_mpz_manager.add(exp, mpz(pp), exp); } + SASSERT(m_mpq_manager.lt(sig, mpq(2))); while (m_mpq_manager.lt(sig, 1)) { m_mpq_manager.mul(sig, 2, sig); m_mpz_manager.dec(exp); } - // 1.0 <= sig < 2.0 + // Check that 1.0 <= sig < 2.0 SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2))); - TRACE("mpf_dbg", tout << "sig = " << m_mpq_manager.to_string(sig) << + TRACE("mpf_dbg", tout << "Normalized: sig = " << m_mpq_manager.to_string(sig) << " exp = " << m_mpz_manager.to_string(exp) << std::endl;); - m_mpz_manager.set(o.significand, 0); - for (unsigned i = 0; i < (sbits+3); i++) { - m_mpz_manager.mul2k(o.significand, 1); - if (m_mpq_manager.ge(sig, 1)) { - m_mpz_manager.inc(o.significand); - m_mpq_manager.dec(sig); - } - m_mpq_manager.mul(sig, mpq(2), sig); - } + scoped_mpz p(m_mpq_manager); + scoped_mpq t(m_mpq_manager), sq(m_mpq_manager); + m_mpz_manager.power(2, sbits + 3 - 1, p); + m_mpq_manager.mul(p, sig, t); + m_mpq_manager.floor(t, o.significand); + m_mpq_manager.set(sq, o.significand); + m_mpq_manager.div(sq, p, t); + m_mpq_manager.sub(sig, t, sig); // sticky if (!m_mpq_manager.is_zero(sig) && m_mpz_manager.is_even(o.significand)) From 79a5b133d796f267563ddcc80e75475f78bac896 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Jan 2016 11:04:44 -0800 Subject: [PATCH 09/15] 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 8ae60d300e39b469ad6165c74badb563616a0fa1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 11 Jan 2016 22:45:57 +0000 Subject: [PATCH 10/15] Update information in ``README.md`` on ".NET" bindings. Since 942b6ba5eca408baefb9e31118db969425bed07f ``--dotnet`` needs to be passed to enable the bindings. --- README.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 7d2fc5a24..32de3d2f2 100644 --- a/README.md +++ b/README.md @@ -105,17 +105,16 @@ Z3 has bindings for various programming languages. ### ``.NET`` -These bindings are enabled by default on Windows and are enabled on other -platforms if [mono](http://www.mono-project.com/) is detected. On these +Use the ``--dotnet`` command line flag with ``mk_make.py`` to enable building these. + +On non-windows platforms [mono](http://www.mono-project.com/) is required. On these platforms the location of the C# compiler and gac utility need to be known. You can set these as follows if they aren't detected automatically. For example: ```bash -CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py +CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py --dotnet ``` -To disable building these bindings pass ``--nodotnet`` to ``mk_make.py``. - Note for very old versions of Mono (e.g. ``2.10``) you may need to set ``CSC`` to ``/usr/bin/dmcs``. From 7cc12bf59f8c9f70b15d6eac6eebb7501b2ecc87 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 11 Jan 2016 23:35:12 +0000 Subject: [PATCH 11/15] Update information in ``README.md`` on Python bindings. Since e9ea687bb9e4848a6205cf7e0b07f73f349f7c36 they aren't on by default. Now ``--python`` needs to passed. Also give better documentation on how install the Python bindings outside the install prefix. --- README.md | 55 +++++++++++++++++++++++++++++-------------------------- 1 file changed, 29 insertions(+), 26 deletions(-) diff --git a/README.md b/README.md index 32de3d2f2..6ab4f7d20 100644 --- a/README.md +++ b/README.md @@ -66,31 +66,6 @@ make make install ``` -Note the above will typically disable the installation of the Python bindings -because the Python ``site-packages`` directory (e.g. -``/usr/lib/python3.5/site-packages/``) is not rooted in the install prefix and -installing outside of the install prefix is dangerous and misleading. - -To avoid this issue you can use the ``DESTDIR`` makefile variable and leave the -install prefix as the default. The ``DESTDIR`` variable is prepended to the -install locations during ``make install`` and ``make uninstall`` and is intended -to allow ["staged installs"](https://www.gnu.org/prep/standards/html_node/DESTDIR.html). -Therefore it must always contain a trailing slash. - -For example: - -```bash -python scripts/mk_make.py -cd build -make -make install DESTDIR=/home/leo/ -``` - -In this example, the Z3 Python bindings will be stored at -``/home/leo/lib/pythonX.Y/site-packages`` -(``/home/leo/lib/pythonX.Y/dist-packages`` on Debian based Linux -distributions) where X.Y corresponds to the python version in your system. - To uninstall Z3, use ```bash @@ -155,6 +130,34 @@ See [``examples/ml``](examples/ml) for examples. ### ``Python`` -These bindings are always enabled. +Use the ``--python`` command line flag with ``mk_make.py`` to enable building these. + +Note that is required on certain platforms that the Python package directory +(``site-packages`` on most distributions and ``dist-packages`` on Debian based +distributions) live under the install prefix. If you use a non standard prefix +you can use the ``--pypkgdir`` option to change the Python package directory +used for installation. For example: + +```bash +python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages +``` + +If you do need to install to a non standard prefix a better approach is to use +a [Python virtual environment](https://virtualenv.readthedocs.org/en/latest/) +and install Z3 there. + +```bash +virtualenv venv +source venv/bin/active +python scripts/mk_make.py --python +cd build +make +make install +# You will find Z3 and the Python bindings installed in the virtual environment +venv/bin/z3 -h +... +python -c 'import z3; print(z3.get_version_string())' +... +``` See [``examples/python``](examples/python) for examples. From e22ac712b05f75f84477d5e3e354861a94394f56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Jan 2016 16:53:29 -0800 Subject: [PATCH 12/15] 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 13/15] 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"; - } } } } From 08139d1ab1c4b8e933c397c52fbabe6574ced17d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 12 Jan 2016 08:48:41 +0000 Subject: [PATCH 14/15] fix build with gcc --- src/smt/smt_internalizer.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 21a3ef86c..78a6b85cb 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -302,7 +302,7 @@ namespace smt { 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); + mark_as_relevant(eq.get()); // TODO: we may want to hide the auxiliary values val and the function f from the model. } } From 55ea75d0a9cfbc9bdd3f6791fab236351648f50b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 12 Jan 2016 11:25:30 +0000 Subject: [PATCH 15/15] Fix minor typo in ``README.md`` --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 6ab4f7d20..534c6c378 100644 --- a/README.md +++ b/README.md @@ -148,7 +148,7 @@ and install Z3 there. ```bash virtualenv venv -source venv/bin/active +source venv/bin/activate python scripts/mk_make.py --python cd build make