From b10f79a941c0114e37d8daa9a30b1b84d1cf5e08 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 27 May 2015 17:07:18 +0100 Subject: [PATCH 01/48] dl_compiler: minor simplifications Signed-off-by: Nuno Lopes --- src/muz/rel/dl_compiler.cpp | 14 ++++++++------ src/muz/rel/dl_compiler.h | 8 ++++---- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 9e8ead241..59ba260a4 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -85,7 +85,7 @@ namespace datalog { removed_cols.size(), removed_cols.c_ptr(), result)); } - void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, + void compiler::make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col, reg_idx & result, bool reuse, instruction_block & acc) { relation_signature res_sig; relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig); @@ -139,7 +139,7 @@ namespace datalog { return r; } - compiler::reg_idx compiler::get_single_column_register(const relation_sort & s) { + compiler::reg_idx compiler::get_single_column_register(const relation_sort s) { relation_signature singl_sig; singl_sig.push_back(s); return get_fresh_register(singl_sig); @@ -165,7 +165,7 @@ namespace datalog { } } - void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort & s, const relation_element & val, + void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort s, const relation_element val, reg_idx & result, bool & dealloc, instruction_block & acc) { reg_idx singleton_table; if(!m_constant_registers.find(s, val, singleton_table)) { @@ -185,7 +185,7 @@ namespace datalog { } } - void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, + void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result, bool & dealloc, instruction_block & acc) { TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";); @@ -862,9 +862,11 @@ namespace datalog { ast_manager& m = m_context.get_manager(); unsigned pt_len = r->get_positive_tail_size(); unsigned ut_len = r->get_uninterpreted_tail_size(); - if (pt_len == ut_len) { + + // no negated predicates + if (pt_len == ut_len) return; - } + // populate negative variables: for (unsigned i = pt_len; i < ut_len; ++i) { app * neg_tail = r->get_tail(i); diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h index 8c33f987c..4902b9387 100644 --- a/src/muz/rel/dl_compiler.h +++ b/src/muz/rel/dl_compiler.h @@ -135,7 +135,7 @@ namespace datalog { reg_idx get_fresh_register(const relation_signature & sig); reg_idx get_register(const relation_signature & sig, bool reuse, reg_idx r); - reg_idx get_single_column_register(const relation_sort & s); + reg_idx get_single_column_register(const relation_sort s); /** \brief Allocate registers for predicates in \c pred and add them into the \c regs map. @@ -150,7 +150,7 @@ namespace datalog { const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc); void make_filter_interpreted_and_project(reg_idx src, app_ref & cond, const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc); - void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, + void make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col, reg_idx & result, bool reuse, instruction_block & acc); /** \brief Create add an union or widen operation and put it into \c acc. @@ -174,10 +174,10 @@ namespace datalog { void make_dealloc_non_void(reg_idx r, instruction_block & acc); - void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort & s, const relation_element & val, + void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort s, const relation_element val, reg_idx & result, bool & dealloc, instruction_block & acc); - void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, + void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result, bool & dealloc, instruction_block & acc); void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, instruction_block & acc); From cb0055563582b80d96907cad9863d63b22c115e9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 May 2015 09:18:52 -0700 Subject: [PATCH 02/48] local changes Signed-off-by: Nikolaj Bjorner --- src/api/java/InterpolationContext.java | 11 ++++++++--- src/math/euclid/euclidean_solver.cpp | 1 + src/smt/smt_internalizer.cpp | 6 ++++-- src/smt/theory_arith_core.h | 2 ++ src/smt/theory_arith_int.h | 4 +++- 5 files changed, 18 insertions(+), 6 deletions(-) diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 667c91a53..5ce5a584a 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -90,7 +90,7 @@ public class InterpolationContext extends Context public class ComputeInterpolantResult { public Z3_lbool status = Z3_lbool.Z3_L_UNDEF; - public ASTVector interp = null; + public BoolExpr[] interp = null; public Model model = null; }; @@ -109,8 +109,13 @@ public class InterpolationContext extends Context ComputeInterpolantResult res = new ComputeInterpolantResult(); Native.LongPtr n_i = new Native.LongPtr(); Native.LongPtr n_m = new Native.LongPtr(); - res.status =Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); - if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value); + res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); + if (res.status == Z3_lbool.Z3_L_FALSE) {xx + res.interp = new BoolExpr[Native.astVectorSize(nCtx(), n_i.value)]; + for (int i = 0; i < res.interp.Length; ++i) { + res.interp[i] = new BoolExpr(this, Native.astVectorGet(nCtx(), i)); + } + } if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; } diff --git a/src/math/euclid/euclidean_solver.cpp b/src/math/euclid/euclidean_solver.cpp index 02ff1591e..9225a87ee 100644 --- a/src/math/euclid/euclidean_solver.cpp +++ b/src/math/euclid/euclidean_solver.cpp @@ -609,6 +609,7 @@ struct euclidean_solver::imp { // neg coeffs... to make sure that m_next_x is -1 neg_coeffs(eq.m_as); neg_coeffs(eq.m_bs); + m().neg(eq.m_c); } unsigned sz = eq.size(); for (unsigned i = 0; i < sz; i++) { diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 74f2e09fa..4f810727a 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1411,6 +1411,10 @@ namespace smt { void context::mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params) { justification * js = 0; + TRACE("mk_th_axiom", + display_literals_verbose(tout, num_lits, lits); + tout << "\n";); + if (m_manager.proofs_enabled()) { js = mk_justification(theory_axiom_justification(tid, m_region, num_lits, lits, num_params, params)); } @@ -1425,13 +1429,11 @@ namespace smt { void context::mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params, parameter * params) { literal ls[2] = { l1, l2 }; - TRACE("mk_th_axiom", display_literal(tout, l1); tout << " "; display_literal(tout, l2); tout << "\n";); mk_th_axiom(tid, 2, ls, num_params, params); } void context::mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params, parameter * params) { literal ls[3] = { l1, l2, l3 }; - TRACE("mk_th_axiom", display_literal(tout, l1); tout << " "; display_literal(tout, l2); tout << " "; display_literal(tout, l3); tout << "\n";); mk_th_axiom(tid, 3, ls, num_params, params); } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index f481e35d0..d0c9953c2 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -439,6 +439,7 @@ namespace smt { j += rational(1); } ctx.mk_th_axiom(get_id(), lits.size(), lits.begin()); + #else // performs slightly worse. literal_buffer lits; @@ -2788,6 +2789,7 @@ namespace smt { tout << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";); + SASSERT(false); if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) { literal_vector & lits = m_tmp_literal_vector2; lits.reset(); diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 45c615e0c..d34b02a27 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -1061,6 +1061,7 @@ namespace smt { } if (!failed) { m_solver.assert_eq(as.size(), as.c_ptr(), xs.c_ptr(), c, j); + TRACE("euclidean_solver", tout << "add definition: v" << v << " := " << mk_ismt2_pp(n, t.get_manager()) << "\n";); } else { TRACE("euclidean_solver", tout << "failed for:\n" << mk_ismt2_pp(n, t.get_manager()) << "\n";); @@ -1191,7 +1192,8 @@ namespace smt { if (l != 0) { rational l_old = l->get_value().get_rational().to_rational(); rational l_new = g*ceil((l_old - c2)/g) + c2; - TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n";); + TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n"; + tout << "c: " << c2 << " ceil((l_old - c2)/g): " << (ceil((l_old - c2)/g)) << "\n";); if (l_new > l_old) { propagated = true; mk_lower(v, l_new, l, m_js); From 562ed61a2415273e88f149113b8a1cc348e6d7da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 May 2015 09:30:37 -0700 Subject: [PATCH 03/48] add shorthands for creating uninterpreted sorts to context API Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 0c5b34fb1..3c2053a5c 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -203,7 +203,12 @@ namespace z3 { and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration. */ sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts); - + /** + \brief create an uninterpreted sort with the name given by the string or symbol. + */ + sort uninterpreted_sort(char const* name); + sort uninterpreted_sort(symbol const& name); + func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range); func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range); func_decl function(symbol const& name, sort_vector const& domain, sort const& range); @@ -1637,6 +1642,13 @@ namespace z3 { for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); } return s; } + inline sort context::uninterpreted_sort(char const* name) { + Z3_symbol _name = Z3_mk_string_symbol(*this, name); + return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name)); + } + inline sort context::uninterpreted_sort(symbol const& name) { + return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name)); + } inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) { array args(arity); From 4f02d380aa9d0fc95fd24975357fbff5825176b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 May 2015 09:34:47 -0700 Subject: [PATCH 04/48] make use of uninterpreted_sort shorthand Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index d40aa93e9..63971a7d9 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -1089,12 +1089,11 @@ class env { } z3::sort mk_sort(char const* s) { - z3::symbol sym = symbol(s); - return mk_sort(sym); + return m_context.uninterpreted_sort(s); } z3::sort mk_sort(z3::symbol& s) { - return z3::sort(m_context, Z3_mk_uninterpreted_sort(m_context, s)); + return m_context.uninterpreted_sort(s); } public: From e3b1ce1fdc24baf10be47ef760393c384c518c23 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 May 2015 10:07:09 -0700 Subject: [PATCH 05/48] also allw n-ary distrinct Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index 63971a7d9..3b8d2364d 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -809,8 +809,12 @@ class env { r = terms[0] / terms[1]; } else if (!strcmp(ch,"$distinct")) { - check_arity(terms.size(), 2); - r = terms[0] != terms[1]; + if (terms.size() == 2) { + r = terms[0] != terms[1]; + } + else { + r = distinct(terms); + } } else if (!strcmp(ch,"$floor") || !strcmp(ch,"$to_int")) { check_arity(terms.size(), 1); From 534271db08fbf0217dc44e99f3b5e837f9d29ccf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 May 2015 14:48:51 -0700 Subject: [PATCH 06/48] adding parameters to gomory cut axioms Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 2 ++ src/smt/theory_arith_int.h | 21 ++++++++++++--------- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 660a11faa..db4b01395 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -245,6 +245,8 @@ namespace smt { parameter* params(char const* name); }; + class gomory_cut_justification; + class bound { protected: theory_var m_var; diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 8993d6c84..cc69bb533 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -460,13 +460,16 @@ namespace smt { SASSERT(is_well_sorted(get_manager(), result)); } - class gomory_cut_justification : public ext_theory_propagation_justification { + template + class theory_arith::gomory_cut_justification : public ext_theory_propagation_justification { public: - gomory_cut_justification(family_id fid, region & r, + gomory_cut_justification(family_id fid, region & r, unsigned num_lits, literal const * lits, unsigned num_eqs, enode_pair const * eqs, + antecedents& bounds, literal consequent): - ext_theory_propagation_justification(fid, r, num_lits, lits, num_eqs, eqs, consequent) { + ext_theory_propagation_justification(fid, r, num_lits, lits, num_eqs, eqs, consequent, + bounds.num_params(), bounds.params("gomory-cut")) { } // Remark: the assignment must be propagated back to arith virtual theory_id get_from_theory() const { return null_theory_id; } @@ -530,7 +533,7 @@ namespace smt { } // k += new_a_ij * lower_bound(x_j).get_rational(); k.addmul(new_a_ij, lower_bound(x_j).get_rational()); - lower(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled()); + lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled()); } else { SASSERT(at_upper(x_j)); @@ -546,7 +549,7 @@ namespace smt { } // k += new_a_ij * upper_bound(x_j).get_rational(); k.addmul(new_a_ij, upper_bound(x_j).get_rational()); - upper(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled()); + upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled()); } pol.push_back(row_entry(new_a_ij, x_j)); } @@ -571,7 +574,7 @@ namespace smt { } // k += new_a_ij * lower_bound(x_j).get_rational(); k.addmul(new_a_ij, lower_bound(x_j).get_rational()); - lower(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled()); + lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled()); } else { SASSERT(at_upper(x_j)); @@ -584,7 +587,7 @@ namespace smt { new_a_ij.neg(); // the upper terms are inverted // k += new_a_ij * upper_bound(x_j).get_rational(); k.addmul(new_a_ij, upper_bound(x_j).get_rational()); - upper(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled()); + upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled()); } TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << "\n";); pol.push_back(row_entry(new_a_ij, x_j)); @@ -600,7 +603,7 @@ namespace smt { if (pol.empty()) { SASSERT(k.is_pos()); // conflict 0 >= k where k is positive - set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, true, "gomory_cut"); + set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, true, "gomory-cut"); return true; } else if (pol.size() == 1) { @@ -652,7 +655,7 @@ namespace smt { gomory_cut_justification( get_id(), ctx.get_region(), ante.lits().size(), ante.lits().c_ptr(), - ante.eqs().size(), ante.eqs().c_ptr(), l))); + ante.eqs().size(), ante.eqs().c_ptr(), ante, l))); return true; } From 3d2ef8bb4a3698c7617a2ddcb3175e1c7223c459 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 27 May 2015 16:05:40 -0700 Subject: [PATCH 07/48] fix for issue #109 --- src/interp/iz3mgr.cpp | 24 ++++++++++++++++++++++++ src/interp/iz3mgr.h | 8 +++++++- src/interp/iz3translate.cpp | 32 ++++++++++++++++++++++++++++++++ 3 files changed, 63 insertions(+), 1 deletion(-) diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 78dd6f174..268085090 100755 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -616,6 +616,30 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& r extract_lcd(rats); } +void iz3mgr::get_gomory_cut_coeffs(const ast &proof, std::vector& coeffs){ + std::vector rats; + get_gomory_cut_coeffs(proof,rats); + coeffs.resize(rats.size()); + for(unsigned i = 0; i < rats.size(); i++){ + coeffs[i] = make_int(rats[i]); + } +} + +void iz3mgr::get_gomory_cut_coeffs(const ast &proof, std::vector& rats){ + symb s = sym(proof); + int numps = s->get_num_parameters(); + rats.resize(numps-2); + for(int i = 2; i < numps; i++){ + rational r; + bool ok = s->get_parameter(i).is_rational(r); + if(!ok) + throw "Bad Farkas coefficient"; + rats[i-2] = r; + } + abs_rat(rats); + extract_lcd(rats); +} + void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector& coeffs){ std::vector rats; get_assign_bounds_rule_coeffs(proof,rats); diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 8d4479f8f..dcbe08817 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -396,7 +396,7 @@ class iz3mgr { return UnknownTheory; } - enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,ArithMysteryKind,UnknownKind}; + enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,GomoryCutKind,ArithMysteryKind,UnknownKind}; lemma_kind get_theory_lemma_kind(const ast &proof){ symb s = sym(proof); @@ -417,6 +417,8 @@ class iz3mgr { return AssignBoundsKind; if(foo == "eq-propagate") return EqPropagateKind; + if(foo == "gomory-cut") + return GomoryCutKind; return UnknownKind; } @@ -434,6 +436,10 @@ class iz3mgr { void get_assign_bounds_rule_coeffs(const ast &proof, std::vector& rats); + void get_gomory_cut_coeffs(const ast &proof, std::vector& rats); + + void get_gomory_cut_coeffs(const ast &proof, std::vector& rats); + bool is_farkas_coefficient_negative(const ast &proof, int n); bool is_true(ast t){ diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 2debdaf42..3620f0ad1 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1182,6 +1182,31 @@ public: return res; } + ast GomoryCutRule2Farkas(const ast &proof, const ast &con, std::vector prems){ + std::vector my_prems = prems; + std::vector my_coeffs; + std::vector my_prem_cons; + get_gomory_cut_coeffs(proof,my_coeffs); + int nargs = num_prems(proof); + if(nargs != (int)(my_coeffs.size())) + throw "bad gomory-cut theory lemma"; + for(int i = 0; i < nargs; i++) + my_prem_cons.push_back(conc(prem(proof,i))); + ast my_con = normalize_inequality(sum_inequalities(my_coeffs,my_prem_cons)); + Iproof::node hyp = iproof->make_hypothesis(mk_not(my_con)); + my_prems.push_back(hyp); + my_coeffs.push_back(make_int("1")); + my_prem_cons.push_back(mk_not(my_con)); + Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_prem_cons,my_coeffs); + ast t = arg(my_con,0); + ast c = arg(my_con,1); + ast d = gcd_of_coefficients(t); + t = z3_simplify(mk_idiv(t,d)); + c = z3_simplify(mk_idiv(c,d)); + ast cut_con = make(op(my_con),t,c); + return iproof->make_cut_rule(my_con,d,cut_con,res); + } + Iproof::node RewriteClause(Iproof::node clause, const ast &rew){ if(pr(rew) == PR_MONOTONICITY){ int nequivs = num_prems(rew); @@ -1912,6 +1937,13 @@ public: res = AssignBounds2Farkas(proof,conc(proof)); break; } + case GomoryCutKind: { + if(args.size() > 0) + res = GomoryCutRule2Farkas(proof, conc(proof), args); + else + throw unsupported(); + break; + } case EqPropagateKind: { std::vector prems(nprems); for(unsigned i = 0; i < nprems; i++) From 713126225b6e729d41ad6a246af58f79342b10dd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 28 May 2015 12:19:55 +0100 Subject: [PATCH 08/48] FPA min/max -+0.0 special cases changed to +0.0 instead of second argument. --- src/ast/fpa/fpa2bv_converter.cpp | 12 ++++++++++-- src/ast/rewriter/fpa_rewriter.cpp | 19 +++++++++++++++---- 2 files changed, 25 insertions(+), 6 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 2c32e7f1a..d2d2c6a3f 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1071,7 +1071,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, split_fp(x, x_sgn, x_exp, x_sig); split_fp(y, y_sgn, y_exp, y_sig); - expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m); + expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m); mk_is_zero(x, x_is_zero); mk_is_zero(y, y_is_zero); m_simp.mk_and(x_is_zero, y_is_zero, both_zero); @@ -1079,12 +1079,16 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, mk_is_nan(y, y_is_nan); mk_pzero(f, pzero); + expr_ref sgn_diff(m); + sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn)); + expr_ref lt(m); mk_float_lt(f, num, args, lt); result = y; mk_ite(lt, x, result, result); mk_ite(both_zero, y, result, result); + mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0 mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); @@ -1109,12 +1113,16 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, mk_is_nan(y, y_is_nan); mk_pzero(f, pzero); + expr_ref sgn_diff(m); + sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn)); + expr_ref gt(m); mk_float_gt(f, num, args, gt); result = y; mk_ite(gt, x, result, result); - mk_ite(both_zero, y, result, result); + mk_ite(both_zero, y, result, result); + mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0 mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 37c42b494..738e8ec29 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -243,7 +243,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const !m_util.au().is_numeral(args[2], r2)) return BR_FAILED; - TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); + TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator()); result = m_util.mk_value(v); return BR_DONE; @@ -420,11 +420,15 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { arg2, m().mk_ite(mk_eq_nan(arg2), arg1, + // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0 + m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2), + m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))), + m_util.mk_pzero(m().get_sort(arg1)), m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), arg2, m().mk_ite(m_util.mk_lt(arg1, arg2), arg1, - arg2)))); + arg2))))); return BR_REWRITE_FULL; } @@ -445,12 +449,16 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { result = m().mk_ite(mk_eq_nan(arg1), arg2, m().mk_ite(mk_eq_nan(arg2), - arg1, + arg1, + // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0 + m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2), + m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))), + m_util.mk_pzero(m().get_sort(arg1)), m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), arg2, m().mk_ite(m_util.mk_gt(arg1, arg2), arg1, - arg2)))); + arg2))))); return BR_REWRITE_FULL; } @@ -583,6 +591,7 @@ br_status fpa_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_zero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; @@ -593,6 +602,7 @@ br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_nzero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; @@ -603,6 +613,7 @@ br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_pzero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; From 7619d609f925539ae985b525bfb70c726060d1b8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 28 May 2015 12:19:55 +0100 Subject: [PATCH 09/48] FPA min/max -+0.0 special cases changed to +0.0 instead of second argument. Fixes #68 --- src/ast/fpa/fpa2bv_converter.cpp | 12 ++++++++++-- src/ast/rewriter/fpa_rewriter.cpp | 19 +++++++++++++++---- 2 files changed, 25 insertions(+), 6 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 2c32e7f1a..d2d2c6a3f 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1071,7 +1071,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, split_fp(x, x_sgn, x_exp, x_sig); split_fp(y, y_sgn, y_exp, y_sig); - expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m); + expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m); mk_is_zero(x, x_is_zero); mk_is_zero(y, y_is_zero); m_simp.mk_and(x_is_zero, y_is_zero, both_zero); @@ -1079,12 +1079,16 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, mk_is_nan(y, y_is_nan); mk_pzero(f, pzero); + expr_ref sgn_diff(m); + sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn)); + expr_ref lt(m); mk_float_lt(f, num, args, lt); result = y; mk_ite(lt, x, result, result); mk_ite(both_zero, y, result, result); + mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0 mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); @@ -1109,12 +1113,16 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, mk_is_nan(y, y_is_nan); mk_pzero(f, pzero); + expr_ref sgn_diff(m); + sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn)); + expr_ref gt(m); mk_float_gt(f, num, args, gt); result = y; mk_ite(gt, x, result, result); - mk_ite(both_zero, y, result, result); + mk_ite(both_zero, y, result, result); + mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0 mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 37c42b494..738e8ec29 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -243,7 +243,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const !m_util.au().is_numeral(args[2], r2)) return BR_FAILED; - TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); + TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator()); result = m_util.mk_value(v); return BR_DONE; @@ -420,11 +420,15 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { arg2, m().mk_ite(mk_eq_nan(arg2), arg1, + // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0 + m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2), + m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))), + m_util.mk_pzero(m().get_sort(arg1)), m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), arg2, m().mk_ite(m_util.mk_lt(arg1, arg2), arg1, - arg2)))); + arg2))))); return BR_REWRITE_FULL; } @@ -445,12 +449,16 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { result = m().mk_ite(mk_eq_nan(arg1), arg2, m().mk_ite(mk_eq_nan(arg2), - arg1, + arg1, + // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0 + m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2), + m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))), + m_util.mk_pzero(m().get_sort(arg1)), m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), arg2, m().mk_ite(m_util.mk_gt(arg1, arg2), arg1, - arg2)))); + arg2))))); return BR_REWRITE_FULL; } @@ -583,6 +591,7 @@ br_status fpa_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_zero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; @@ -593,6 +602,7 @@ br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_nzero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; @@ -603,6 +613,7 @@ br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_pzero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; From 49a4df0de144fb87b23d8af01be4816a428da25b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 28 May 2015 12:54:57 +0100 Subject: [PATCH 10/48] MPF min/max -+0.0 special cases changed to +0.0 instead of second argument. Another piece of fix #68 --- src/util/mpf.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 1521a8f87..57e5b56b5 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1229,7 +1229,11 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { } void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) { - if (is_nan(x) || (is_zero(x) && is_zero(y))) + if (is_nan(x)) + set(o, y); + else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y)) + mk_pzero(x.ebits, x.sbits, o); + else if (is_zero(x) && is_zero(y)) set(o, y); else if (is_nan(y)) set(o, x); @@ -1240,7 +1244,11 @@ void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) { } void mpf_manager::minimum(mpf const & x, mpf const & y, mpf & o) { - if (is_nan(x) || (is_zero(x) && is_zero(y))) + if (is_nan(x)) + set(o, y); + else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y)) + mk_pzero(x.ebits, x.sbits, o); + else if (is_zero(x) && is_zero(y)) set(o, y); else if (is_nan(y)) set(o, x); From 23a6138d81799947b25e614c8bb115090e9e3321 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 May 2015 14:55:37 -0700 Subject: [PATCH 11/48] initialize potentially unused variables. Fixes issue #112 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 3c2053a5c..cd47d6900 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -683,7 +683,7 @@ namespace z3 { friend expr operator+(expr const & a, expr const & b) { check_context(a, b); - Z3_ast r; + Z3_ast r = 0; if (a.is_arith() && b.is_arith()) { Z3_ast args[2] = { a, b }; r = Z3_mk_add(a.ctx(), 2, args); @@ -703,7 +703,7 @@ namespace z3 { friend expr operator*(expr const & a, expr const & b) { check_context(a, b); - Z3_ast r; + Z3_ast r = 0; if (a.is_arith() && b.is_arith()) { Z3_ast args[2] = { a, b }; r = Z3_mk_mul(a.ctx(), 2, args); @@ -730,7 +730,7 @@ namespace z3 { friend expr operator/(expr const & a, expr const & b) { check_context(a, b); - Z3_ast r; + Z3_ast r = 0; if (a.is_arith() && b.is_arith()) { r = Z3_mk_div(a.ctx(), a, b); } @@ -748,7 +748,7 @@ namespace z3 { friend expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; } friend expr operator-(expr const & a) { - Z3_ast r; + Z3_ast r = 0; if (a.is_arith()) { r = Z3_mk_unary_minus(a.ctx(), a); } @@ -765,7 +765,7 @@ namespace z3 { friend expr operator-(expr const & a, expr const & b) { check_context(a, b); - Z3_ast r; + Z3_ast r = 0; if (a.is_arith() && b.is_arith()) { Z3_ast args[2] = { a, b }; r = Z3_mk_sub(a.ctx(), 2, args); @@ -785,7 +785,7 @@ namespace z3 { friend expr operator<=(expr const & a, expr const & b) { check_context(a, b); - Z3_ast r; + Z3_ast r = 0; if (a.is_arith() && b.is_arith()) { r = Z3_mk_le(a.ctx(), a, b); } @@ -804,7 +804,7 @@ namespace z3 { friend expr operator>=(expr const & a, expr const & b) { check_context(a, b); - Z3_ast r; + Z3_ast r = 0; if (a.is_arith() && b.is_arith()) { r = Z3_mk_ge(a.ctx(), a, b); } @@ -823,7 +823,7 @@ namespace z3 { friend expr operator<(expr const & a, expr const & b) { check_context(a, b); - Z3_ast r; + Z3_ast r = 0; if (a.is_arith() && b.is_arith()) { r = Z3_mk_lt(a.ctx(), a, b); } @@ -842,7 +842,7 @@ namespace z3 { friend expr operator>(expr const & a, expr const & b) { check_context(a, b); - Z3_ast r; + Z3_ast r = 0; if (a.is_arith() && b.is_arith()) { r = Z3_mk_gt(a.ctx(), a, b); } @@ -1189,7 +1189,7 @@ namespace z3 { expr eval(expr const & n, bool model_completion=false) const { check_context(*this, n); - Z3_ast r; + Z3_ast r = 0; Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r); check_error(); if (status == Z3_FALSE) From ac732a500cb90d255f7bf4cee992a04fb5a97ef3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 May 2015 15:20:25 -0700 Subject: [PATCH 12/48] add first file Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.h | 51 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 src/qe/qe_mbp.h diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h new file mode 100644 index 000000000..b8a73a890 --- /dev/null +++ b/src/qe/qe_mbp.h @@ -0,0 +1,51 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qe_mbp.h + +Abstract: + + Model-based projection utilities + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-28 + +Revision History: + + +--*/ + +#ifndef __QE_MBP_H__ +#define __QE_MBP_H__ + +#include "ast.h" +#include "params.h" + +class qe_mbp { + class impl; + impl * m_impl; +public: + qe_mbp(ast_manager& m); + + ~qe_mbp(); + + /** + \brief + Apply model-based qe on constants provided as vector of variables. + Return the updated formula and updated set of variables that were not eliminated. + + */ + void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml); + + /** + \brief full rewriting based light-weight quantifier elimination round. + */ + void operator()(expr_ref& fml, proof_ref& pr); + + void set_cancel(bool f); +}; + +#endif From e47eea2c610e19e1afde2ac3df5565aca755a4d4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 May 2015 17:22:34 -0700 Subject: [PATCH 13/48] n/a Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.h | 43 +++++------ src/qe/qsat.cpp | 200 ++++++++++++++++++++++++++++++++++++++++++++++++ src/qe/qsat.h | 52 +++++++++++++ 3 files changed, 272 insertions(+), 23 deletions(-) create mode 100644 src/qe/qsat.cpp create mode 100644 src/qe/qsat.h diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h index b8a73a890..11bceef0b 100644 --- a/src/qe/qe_mbp.h +++ b/src/qe/qe_mbp.h @@ -24,28 +24,25 @@ Revision History: #include "ast.h" #include "params.h" -class qe_mbp { - class impl; - impl * m_impl; -public: - qe_mbp(ast_manager& m); - - ~qe_mbp(); - - /** - \brief - Apply model-based qe on constants provided as vector of variables. - Return the updated formula and updated set of variables that were not eliminated. - - */ - void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml); - - /** - \brief full rewriting based light-weight quantifier elimination round. - */ - void operator()(expr_ref& fml, proof_ref& pr); - - void set_cancel(bool f); -}; +namespace qe { + class mbp { + class impl; + impl * m_impl; + public: + mbp(ast_manager& m); + + ~mbp(); + + /** + \brief + Apply model-based qe on constants provided as vector of variables. + Return the updated formula and updated set of variables that were not eliminated. + + */ + void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml); + + void set_cancel(bool f); + }; +} #endif diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp new file mode 100644 index 000000000..6a59b40cd --- /dev/null +++ b/src/qe/qsat.cpp @@ -0,0 +1,200 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qsat.cpp + +Abstract: + + Quantifier Satisfiability Solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-28 + +Revision History: + + +--*/ + +#include "qsat.h" +#include "smt_kernel.h" +#include "qe_mbp.h" + +namespace qe; + +sturct qdef_t { + expr_ref m_pred; + expr_ref m_expr; + expr_ref_vector m_vars; + bool m_is_forall; + qdef_t(expr_ref& p, expr_ref& e, expr_ref_vector const& vars, bool is_forall): + m_pred(p), + m_expr(e), + m_vars(vars), + m_is_forall(is_forall) {} +}; + +typedef vector qdefs_t; + +struct pdef_t { + expr_ref m_pred; + expr_ref m_atom; + pdef_t(expr_ref& p, expr_ref& a): + m_pred(p), + m_atom(a) + {} +}; + +class qsat::impl { + ast_manager& m; + mbp mbp; + + /** + \brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate. + */ + void remove_quantifiers(expr_ref_vector& fmls, qdefs_t& defs) { + + } + + /** + \brief create propositional abstration of formula by replacing atomic sub-formulas by fresh + propositional variables, and adding definitions for each propositional formula on the side. + Assumption is that the formula is quantifier-free. + */ + void mk_abstract(expr_ref_vector& fmls, vector& pdefs) { + expr_ref_vector todo(fmls), trail(m); + obj_map cache; + ptr_vector args; + expr_ref r(m); + while (!todo.empty()) { + expr* e = todo.back(); + if (cache.contains(e)) { + todo.pop_back(); + continue; + } + SASSERT(is_app(e)); + app* a = to_app(e); + if (a->get_family_id() == m.get_basic_family_id()) { + unsigned sz = a->get_num_args(); + args.reset(); + for (unsigned i = 0; i < sz; ++i) { + expr* f = a->get_arg(i); + if (cache.find(f, f)) { + args.push_back(f); + } + else { + todo.push_back(f); + } + } + if (args.size() == sz) { + r = m.mk_app(a->get_decl(), sz, args.c_ptr()); + cache.insert(e, r); + trail.push_back(r); + todo.pop_back(e); + } + } + else if (is_uninterpreted_const(a)) { + cache.insert(e, e); + } + else { + // TBD: nested Booleans. + r = m.mk_fresh_const("p",m.mk_bool_sort()); + trail.push_back(r); + cache.insert(e, r); + pdefs.push_back(pdef_t(e, r)); + } + } + + for (unsigned i = 0; i < fmls.size(); ++i) { + fmls[i] = cache.find(fmls[i].get()); + } + } + + /** + \brief use dual propagation to minimize model. + */ + void minimize_assignment(app_ref_vector& assignment) { + + } + +public: + impl(ast_manager& m): + m(m), + mbp(m) {} + + void updt_params(params_ref const & p) { + } + void collect_param_descrs(param_descrs & r) { + } + void operator()(/* in */ goal_ref const & in, + /* out */ goal_ref_buffer & result, + /* out */ model_converter_ref & mc, + /* out */ proof_converter_ref & pc, + /* out */ expr_dependency_ref & core) { + + } + + void collect_statistics(statistics & st) const { + + } + void reset_statistics() { + } + void cleanup() { + } + void set_logic(symbol const & l) { + } + void set_progress_callback(progress_callback * callback) { + } + tactic * translate(ast_manager & m) { + return 0; + } + +}; + +qsat::qsat(ast_manager& m) { + m_impl = alloc(impl, m); +} + +qsat::~qsat() { + dealloc(m_impl); +} + +void qsat::updt_params(params_ref const & p) { + m_impl->updt_params(p); +} +void qsat::collect_param_descrs(param_descrs & r) { + m_impl->collect_param_descrs(r); +} +void qsat::operator()(/* in */ goal_ref const & in, + /* out */ goal_ref_buffer & result, + /* out */ model_converter_ref & mc, + /* out */ proof_converter_ref & pc, + /* out */ expr_dependency_ref & core) { + (*m_impl)(in, result, mc, pc, core); +} + +void qsat::collect_statistics(statistics & st) const { + m_impl->collect_statistics(st); +} +void qsat::reset_statistics() { + m_impl->reset_statistics(); +} +void qsat::cleanup() { + m_impl->cleanup(); +} +void qsat::set_logic(symbol const & l) { + m_impl->set_logic(l); +} +void qsat::set_progress_callback(progress_callback * callback) { + m_impl->set_progress_callback(callback); +} +tactic * qsat::translate(ast_manager & m) { + return m_impl->translate(m); +} + + +}; + +#endif diff --git a/src/qe/qsat.h b/src/qe/qsat.h new file mode 100644 index 000000000..23d506294 --- /dev/null +++ b/src/qe/qsat.h @@ -0,0 +1,52 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qsat.h + +Abstract: + + Quantifier Satisfiability Solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-28 + +Revision History: + + +--*/ + +#ifndef __QE_MBP_H__ +#define __QE_MBP_H__ + +#include "tactic.h" + +namespace qe { + class qsat : public tactic { + class impl; + impl * m_impl; + public: + qsat(ast_manager& m); + ~qsat(); + + virtual void updt_params(params_ref const & p); + virtual void collect_param_descrs(param_descrs & r); + virtual void operator()(/* in */ goal_ref const & in, + /* out */ goal_ref_buffer & result, + /* out */ model_converter_ref & mc, + /* out */ proof_converter_ref & pc, + /* out */ expr_dependency_ref & core); + + virtual void collect_statistics(statistics & st) const; + virtual void reset_statistics(); + virtual void cleanup() = 0; + virtual void set_logic(symbol const & l); + virtual void set_progress_callback(progress_callback * callback); + virtual tactic * translate(ast_manager & m); + + }; +}; + +#endif From ed7e0e11a80a2d6cad4c8a11eaa0e2fbdc5ee3e8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 May 2015 20:55:13 -0700 Subject: [PATCH 14/48] n/a Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 4 ++ src/muz/base/dl_context.cpp | 4 ++ src/opt/opt_cmds.cpp | 6 +- src/opt/opt_context.cpp | 4 ++ src/qe/qsat.cpp | 131 +++++++++++++++++++++++++++------- src/qe/qsat.h | 4 +- src/smt/theory_array_full.cpp | 37 +++++----- src/smt/theory_array_full.h | 7 +- 8 files changed, 142 insertions(+), 55 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index e57050e82..ca15762f5 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -355,6 +355,10 @@ extern "C" { init_solver(c, s); Z3_stats_ref * st = alloc(Z3_stats_ref); to_solver_ref(s)->collect_statistics(st->m_stats); + unsigned long long max_mem = memory::get_max_used_memory(); + unsigned long long mem = memory::get_allocation_size(); + st->m_stats.update("max memory", static_cast(max_mem)/(1024.0*1024.0)); + st->m_stats.update("memory", static_cast(mem)/(1024.0*1024.0)); mk_c(c)->save_object(st); Z3_stats r = of_stats(st); RETURN_Z3(r); diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index bd70c06ef..3555e5bdc 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -945,6 +945,10 @@ namespace datalog { if (m_engine) { m_engine->collect_statistics(st); } + unsigned long long max_mem = memory::get_max_used_memory(); + unsigned long long mem = memory::get_allocation_size(); + st.update("max memory", static_cast(max_mem)/(1024.0*1024.0)); + st.update("memory", static_cast(mem)/(1024.0*1024.0)); } diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 537f4bf22..01324fc67 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -323,12 +323,8 @@ private: void display_statistics(cmd_context& ctx) { statistics stats; - unsigned long long max_mem = memory::get_max_used_memory(); - unsigned long long mem = memory::get_allocation_size(); - stats.update("time", ctx.get_seconds()); - stats.update("memory", static_cast(mem)/static_cast(1024*1024)); - stats.update("max memory", static_cast(max_mem)/static_cast(1024*1024)); get_opt(ctx).collect_statistics(stats); + stats.update("time", ctx.get_seconds()); stats.display_smt2(ctx.regular_stream()); } }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 857b57296..5353d9b53 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1179,6 +1179,10 @@ namespace opt { for (; it != end; ++it) { it->m_value->collect_statistics(stats); } + unsigned long long max_mem = memory::get_max_used_memory(); + unsigned long long mem = memory::get_allocation_size(); + stats.update("memory", static_cast(mem)/static_cast(1024*1024)); + stats.update("max memory", static_cast(max_mem)/static_cast(1024*1024)); } void context::collect_param_descrs(param_descrs & r) { diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 6a59b40cd..4c736bc31 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -21,10 +21,12 @@ Revision History: #include "qsat.h" #include "smt_kernel.h" #include "qe_mbp.h" +#include "smt_params.h" +#include "ast_util.h" -namespace qe; +using namespace qe; -sturct qdef_t { +struct qdef_t { expr_ref m_pred; expr_ref m_expr; expr_ref_vector m_vars; @@ -41,15 +43,25 @@ typedef vector qdefs_t; struct pdef_t { expr_ref m_pred; expr_ref m_atom; - pdef_t(expr_ref& p, expr_ref& a): - m_pred(p), - m_atom(a) + pdef_t(expr_ref& p, expr* a): + m_pred(p), + m_atom(a, p.get_manager()) {} }; class qsat::impl { - ast_manager& m; - mbp mbp; + ast_manager& m; + qe::mbp mbp; + smt_params m_smtp; + smt::kernel m_kernel; + expr_ref m_fml_pred; // predicate that encodes top-level formula + expr_ref_vector m_atoms; // predicates that encode atomic subformulas + + + lbool check_sat() { + // TBD main procedure goes here. + return l_undef; + } /** \brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate. @@ -63,11 +75,12 @@ class qsat::impl { propositional variables, and adding definitions for each propositional formula on the side. Assumption is that the formula is quantifier-free. */ - void mk_abstract(expr_ref_vector& fmls, vector& pdefs) { - expr_ref_vector todo(fmls), trail(m); + void mk_abstract(expr_ref& fml, vector& pdefs) { + expr_ref_vector todo(m), trail(m); obj_map cache; ptr_vector args; expr_ref r(m); + todo.push_back(fml); while (!todo.empty()) { expr* e = todo.back(); if (cache.contains(e)) { @@ -87,47 +100,114 @@ class qsat::impl { else { todo.push_back(f); } - } + } if (args.size() == sz) { r = m.mk_app(a->get_decl(), sz, args.c_ptr()); cache.insert(e, r); trail.push_back(r); - todo.pop_back(e); + todo.pop_back(); } } - else if (is_uninterpreted_const(a)) { + else if (is_uninterp_const(a)) { cache.insert(e, e); } else { - // TBD: nested Booleans. + // TBD: nested Booleans. + r = m.mk_fresh_const("p",m.mk_bool_sort()); trail.push_back(r); cache.insert(e, r); - pdefs.push_back(pdef_t(e, r)); + pdefs.push_back(pdef_t(r, e)); } } - - for (unsigned i = 0; i < fmls.size(); ++i) { - fmls[i] = cache.find(fmls[i].get()); - } + fml = cache.find(fml); } /** \brief use dual propagation to minimize model. */ - void minimize_assignment(app_ref_vector& assignment) { - + bool minimize_assignment(expr_ref_vector& assignment, expr* not_fml) { + bool result = false; + assignment.push_back(not_fml); + lbool res = m_kernel.check(assignment.size(), assignment.c_ptr()); + switch (res) { + case l_true: + UNREACHABLE(); + break; + case l_undef: + break; + case l_false: + result = true; + get_core(assignment, not_fml); + break; + } + return result; + } + + lbool check_sat(expr_ref_vector& assignment, expr* fml) { + assignment.push_back(fml); + lbool res = m_kernel.check(assignment.size(), assignment.c_ptr()); + switch (res) { + case l_true: { + model_ref mdl; + expr_ref tmp(m); + assignment.reset(); + m_kernel.get_model(mdl); + for (unsigned i = 0; i < m_atoms.size(); ++i) { + expr* p = m_atoms[i].get(); + if (mdl->eval(p, tmp)) { + if (m.is_true(tmp)) { + assignment.push_back(p); + } + else if (m.is_false(tmp)) { + assignment.push_back(m.mk_not(p)); + } + } + } + expr_ref not_fml = mk_not(fml); + if (!minimize_assignment(assignment, not_fml)) { + res = l_undef; + } + break; + } + case l_undef: + break; + case l_false: + get_core(assignment, fml); + break; + } + return res; + } + + void get_core(expr_ref_vector& core, expr* exclude) { + unsigned sz = m_kernel.get_unsat_core_size(); + core.reset(); + for (unsigned i = 0; i < sz; ++i) { + expr* e = m_kernel.get_unsat_core_expr(i); + if (e != exclude) { + core.push_back(e); + } + } + } + + expr_ref mk_not(expr* e) { + return expr_ref(::mk_not(m, e), m); } public: impl(ast_manager& m): m(m), - mbp(m) {} - + mbp(m), + m_kernel(m, m_smtp), + m_fml_pred(m), + m_atoms(m) {} + void updt_params(params_ref const & p) { } + void collect_param_descrs(param_descrs & r) { } + void operator()(/* in */ goal_ref const & in, /* out */ goal_ref_buffer & result, /* out */ model_converter_ref & mc, @@ -141,12 +221,16 @@ public: } void reset_statistics() { } + void cleanup() { } + void set_logic(symbol const & l) { } + void set_progress_callback(progress_callback * callback) { } + tactic * translate(ast_manager & m) { return 0; } @@ -195,6 +279,3 @@ tactic * qsat::translate(ast_manager & m) { } -}; - -#endif diff --git a/src/qe/qsat.h b/src/qe/qsat.h index 23d506294..2fc071c76 100644 --- a/src/qe/qsat.h +++ b/src/qe/qsat.h @@ -18,8 +18,8 @@ Revision History: --*/ -#ifndef __QE_MBP_H__ -#define __QE_MBP_H__ +#ifndef __QE_QSAT_H__ +#define __QE_QSAT_H__ #include "tactic.h" diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 28314c421..dd74f2871 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -208,6 +208,8 @@ namespace smt { theory_array::reset_eh(); std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc()); m_var_data_full.reset(); + m_eqs.reset(); + m_eqsv.reset(); } void theory_array_full::display_var(std::ostream & out, theory_var v) const { @@ -223,7 +225,6 @@ namespace smt { } theory_var theory_array_full::mk_var(enode * n) { - theory_var r = theory_array::mk_var(n); SASSERT(r == static_cast(m_var_data_full.size())); m_var_data_full.push_back(alloc(var_data_full)); @@ -512,7 +513,7 @@ namespace smt { TRACE("array_map_bug", tout << "select-map axiom\n" << mk_ismt2_pp(sel1, m) << "\n=\n" << mk_ismt2_pp(sel2,m) << "\n";); - + return try_assign_eq(sel1, sel2); } @@ -760,36 +761,30 @@ namespace smt { r = FC_CONTINUE; } } + while (!m_eqsv.empty()) { + literal eq = m_eqsv.back(); + m_eqsv.pop_back(); + get_context().mark_as_relevant(eq); + assert_axiom(eq); + r = FC_CONTINUE; + } if (r == FC_DONE && m_found_unsupported_op) r = FC_GIVEUP; return r; } + bool theory_array_full::try_assign_eq(expr* v1, expr* v2) { context& ctx = get_context(); - enode* n1 = ctx.get_enode(v1); - enode* n2 = ctx.get_enode(v2); - if (n1->get_root() == n2->get_root()) { + if (m_eqs.contains(v1, v2)) { return false; } + m_eqs.insert(v1, v2, true); TRACE("array", tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" << mk_bounded_pp(v2, get_manager()) << "\n";); - -#if 0 - if (m.proofs_enabled()) { -#endif - literal eq(mk_eq(v1,v2,true)); - ctx.mark_as_relevant(eq); - assert_axiom(eq); -#if 0 - } - else { - ctx.mark_as_relevant(n1); - ctx.mark_as_relevant(n2); - ctx.assign_eq(n1, n2, eq_justification::mk_axiom()); - } -#endif + literal eq(mk_eq(v1, v2, true)); + m_eqsv.push_back(eq); return true; } @@ -798,6 +793,8 @@ namespace smt { theory_array::pop_scope_eh(num_scopes); std::for_each(m_var_data_full.begin() + num_old_vars, m_var_data_full.end(), delete_proc()); m_var_data_full.shrink(num_old_vars); + m_eqs.reset(); + m_eqsv.reset(); } void theory_array_full::collect_statistics(::statistics & st) const { diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h index 7c066f765..bbbf35408 100644 --- a/src/smt/theory_array_full.h +++ b/src/smt/theory_array_full.h @@ -38,12 +38,12 @@ namespace smt { ast2ast_trailmap m_sort2epsilon; simplifier* m_simp; + obj_pair_map m_eqs; + svector m_eqsv; protected: -#if 0 - virtual final_check_status final_check_eh(); -#endif + //virtual final_check_status final_check_eh(); virtual void reset_eh(); virtual void set_prop_upward(theory_var v); @@ -84,6 +84,7 @@ namespace smt { bool try_assign_eq(expr* n1, expr* n2); + void assign_eqs(); public: From 3f22201ba3e1518d9b6cb9cc18752bcd997e8fe8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 29 May 2015 12:25:44 +0100 Subject: [PATCH 15/48] Bugfix for dll/so name resolution in Java. --- scripts/update_api.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 051e8fced..0d57a29ac 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -568,10 +568,12 @@ def mk_java(): java_native.write(' public static class ObjArrayPtr { public long[] value; }\n') java_native.write(' public static class UIntArrayPtr { public int[] value; }\n') java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n') - if IS_WINDOWS or os.uname()[0]=="CYGWIN": - java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name) - else: - java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name + + java_native.write(' static {\n') + java_native.write(' try { System.loadLibrary("z3java"); }\n') + java_native.write(' catch (UnsatisfiedLinkError ex) { System.loadLibrary("libz3java"); }\n') + java_native.write(' }\n') + java_native.write('\n') for name, result, params in _dotnet_decls: java_native.write(' protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name))) From d8d0b21e4212e24c2acbea64d43bc1f018efbebe Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 29 May 2015 12:25:44 +0100 Subject: [PATCH 16/48] Bugfix for dll/so name resolution in Java. Fixes #111 --- scripts/update_api.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 051e8fced..0d57a29ac 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -568,10 +568,12 @@ def mk_java(): java_native.write(' public static class ObjArrayPtr { public long[] value; }\n') java_native.write(' public static class UIntArrayPtr { public int[] value; }\n') java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n') - if IS_WINDOWS or os.uname()[0]=="CYGWIN": - java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name) - else: - java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name + + java_native.write(' static {\n') + java_native.write(' try { System.loadLibrary("z3java"); }\n') + java_native.write(' catch (UnsatisfiedLinkError ex) { System.loadLibrary("libz3java"); }\n') + java_native.write(' }\n') + java_native.write('\n') for name, result, params in _dotnet_decls: java_native.write(' protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name))) From f2f6fc1994fcbfaa1c4191f51e75babf7f67544e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 29 May 2015 13:58:23 +0100 Subject: [PATCH 17/48] Added QF_BVFP logic alias for QF_FPBV --- src/cmd_context/cmd_context.cpp | 2 ++ src/smt/smt_setup.cpp | 2 +- src/tactic/portfolio/smt_strategic_solver.cpp | 2 +- 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 80aa10cde..9aa089096 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -528,6 +528,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "LRA" || s == "QF_FP" || s == "QF_FPBV" || + s == "QF_BVFP" || s == "HORN"; } @@ -547,6 +548,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const { s == "QF_AUFBV" || s == "QF_BVRE" || s == "QF_FPBV" || + s == "QF_BVFP" || s == "HORN"; } diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index d4c0e1efb..98ad5e51a 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -116,7 +116,7 @@ namespace smt { setup_LRA(); else if (m_logic == "QF_FP") setup_QF_FP(); - else if (m_logic == "QF_FPBV") + else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP") setup_QF_FPBV(); else setup_unknown(); diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index b28c8cf3d..687771a30 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -81,7 +81,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_ufbv_tactic(m, p); else if (logic=="QF_FP") return mk_qffp_tactic(m, p); - else if (logic == "QF_FPBV") + else if (logic == "QF_FPBV" || logic == "QF_BVFP") return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p); From 9428acd578459edcec0936259d00b3c002378ef2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 29 May 2015 13:58:33 +0100 Subject: [PATCH 18/48] Bugfix for FPA rewriter. --- src/ast/rewriter/fpa_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 738e8ec29..07a39bcae 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -143,9 +143,9 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) { if (m_hi_fp_unspecified) - result = m_util.au().mk_numeral(0, false); - else // The "hardware interpretation" is 0. + result = m_util.au().mk_numeral(rational(0), false); + else result = m_util.mk_internal_to_real_unspecified(); return BR_DONE; From 85419ca503496b0cd873234320ef195199ac3093 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 29 May 2015 14:21:27 +0100 Subject: [PATCH 19/48] Added branch into QF_NRA from QF_FP problems containing to_real terms. --- scripts/mk_project.py | 2 +- src/tactic/fpa/qffp_tactic.cpp | 9 +++++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 4bccdf6bb..b9641c869 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -55,7 +55,6 @@ def init_project_def(): add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv') add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('smt_tactic', ['smt'], 'smt/tactic') - add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic'], 'tactic/fpa') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') add_lib('qe', ['smt','sat'], 'qe') add_lib('duality', ['smt', 'interp', 'qe']) @@ -71,6 +70,7 @@ def init_project_def(): add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp') add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt') add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics') + add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 4854b3c07..12c127a37 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -23,6 +23,8 @@ Notes: #include"fpa2bv_tactic.h" #include"smt_tactic.h" #include"propagate_values_tactic.h" +#include"probe_arith.h" +#include"qfnra_tactic.h" #include"qffp_tactic.h" @@ -40,10 +42,13 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { mk_propagate_values_tactic(m, p), using_params(mk_simplify_tactic(m, p), simp_p), mk_bit_blaster_tactic(m, p), - using_params(mk_simplify_tactic(m, p), simp_p), + using_params(mk_simplify_tactic(m, p), simp_p), cond(mk_is_propositional_probe(), mk_sat_tactic(m, p), - mk_smt_tactic(p)), + cond(mk_is_qfnra_probe(), + mk_qfnra_tactic(m, p), + mk_smt_tactic(p)) + ), mk_fail_if_undecided_tactic()))); st->updt_params(p); From d35ebd6e57564815a8c89ca52fb57c15ecd1d4d5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 29 May 2015 14:49:26 +0100 Subject: [PATCH 20/48] Bugfix for FP to_fp from non-numeral reals. --- src/ast/fpa/fpa2bv_converter.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d2d2c6a3f..16b7cc1da 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2312,7 +2312,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * mk_ite(rm_nta, v1, result, result); } } - else { + else { + SASSERT(!m_arith_util.is_numeral(x)); bv_util & bu = m_bv_util; arith_util & au = m_arith_util; @@ -2330,12 +2331,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * expr_ref rme(rm, m); round(s, rme, sgn, sig, exp, result); - expr_ref c0(m); - mk_is_zero(x, c0); - mk_ite(c0, x, result, result); - expr * e = m.mk_eq(m_util.mk_to_real(result), x); - m_extra_assertions.push_back(e); + m_extra_assertions.push_back(e); } SASSERT(is_well_sorted(m, result)); From ba8864846816603742a06d60ab9191604fd1b6bd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 29 May 2015 14:49:53 +0100 Subject: [PATCH 21/48] Added has_fp_to_real probe to detect when QF_FP need QF_NRA. --- src/tactic/fpa/qffp_tactic.cpp | 38 +++++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 12c127a37..3bee224b3 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -28,6 +28,42 @@ Notes: #include"qffp_tactic.h" + +struct has_fp_to_real_predicate { + struct found {}; + ast_manager & m; + bv_util bu; + fpa_util fu; + arith_util au; + + has_fp_to_real_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (au.is_real(s) && n->get_family_id() == fu.get_family_id() && + is_app(n) && to_app(n)->get_kind() == OP_FPA_TO_REAL) + throw found(); + } +}; + +class has_fp_to_real_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } + + virtual ~has_fp_to_real_probe() {} +}; + +probe * mk_has_fp_to_real_probe() { + return alloc(has_fp_to_real_probe); +} + + tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { params_ref simp_p = p; simp_p.set_bool("arith_lhs", true); @@ -45,7 +81,7 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { using_params(mk_simplify_tactic(m, p), simp_p), cond(mk_is_propositional_probe(), mk_sat_tactic(m, p), - cond(mk_is_qfnra_probe(), + cond(mk_has_fp_to_real_probe(), mk_qfnra_tactic(m, p), mk_smt_tactic(p)) ), From a2448be0cde41a774f8321d94521373563285608 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 May 2015 08:55:44 -0700 Subject: [PATCH 22/48] print pareto model in check-sat too Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 10 ++++++++++ src/cmd_context/cmd_context.h | 1 + src/opt/opt_context.cpp | 6 ++++++ src/opt/opt_context.h | 1 + 4 files changed, 18 insertions(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 80aa10cde..187c7ba63 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -40,6 +40,7 @@ Notes: #include"for_each_expr.h" #include"scoped_timer.h" #include"interpolant_cmds.h" +#include"model_smt2_pp.h" func_decls::func_decls(ast_manager & m, func_decl * f): m_decls(TAG(func_decl*, f, 0)) { @@ -1402,6 +1403,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions was_pareto = true; get_opt()->display_assignment(regular_stream()); regular_stream() << "\n"; + if (get_opt()->print_model()) { + model_ref mdl; + get_opt()->get_model(mdl); + if (mdl) { + regular_stream() << "(model " << std::endl; + model_smt2_pp(regular_stream(), *this, *(mdl.get()), 2); + regular_stream() << ")" << std::endl; + } + } r = get_opt()->optimize(); } } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 148bb61d9..795b3a65a 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -124,6 +124,7 @@ public: virtual void display_assignment(std::ostream& out) = 0; virtual bool is_pareto() = 0; virtual void set_logic(symbol const& s) = 0; + virtual bool print_model() const = 0; }; class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 857b57296..f5a3b5c67 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -254,6 +254,12 @@ namespace opt { } } + + bool context::print_model() const { + opt_params optp(m_params); + return optp.print_model(); + } + void context::get_base_model(model_ref& mdl) { mdl = m_model; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 59868dd1e..eabc2550f 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -180,6 +180,7 @@ namespace opt { virtual void cancel() { set_cancel(true); } virtual void set_hard_constraints(ptr_vector & hard); virtual lbool optimize(); + virtual bool print_model() const; virtual void get_model(model_ref& _m); virtual void set_model(model_ref& _m); virtual void fix_model(model_ref& _m); From fec815b41ef66c5dc28a04aeabd933fca59e4d37 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 29 May 2015 18:13:39 +0100 Subject: [PATCH 23/48] Various variable renamings to avoid conflicts with previously defined local variables, function parameters, or members (Visual Studio 2015 warnings). --- src/ast/ast_smt2_pp.cpp | 8 +-- src/ast/ast_util.cpp | 6 +- src/ast/datatype_decl_plugin.cpp | 14 ++--- src/ast/expr2polynomial.cpp | 10 ++-- src/ast/fpa/fpa2bv_converter.cpp | 58 +++++++++---------- src/ast/func_decl_dependencies.cpp | 16 ++--- .../bit_blaster/bit_blaster_tpl_def.h | 12 ++-- src/ast/rewriter/rewriter_def.h | 2 +- src/ast/shared_occs.h | 2 +- src/tactic/arith/arith_bounds_tactic.cpp | 4 +- src/tactic/tactical.cpp | 2 - 11 files changed, 65 insertions(+), 69 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 0d319af39..c74b4f185 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -341,22 +341,22 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d } else { SASSERT(u.is_irrational_algebraic_numeral(t)); - anum const & val = u.to_irrational_algebraic_numeral(t); + anum const & val2 = u.to_irrational_algebraic_numeral(t); algebraic_numbers::manager & am = u.am(); format * vf; std::ostringstream buffer; bool is_neg = false; if (decimal) { scoped_anum abs_val(am); - am.set(abs_val, val); - if (am.is_neg(val)) { + am.set(abs_val, val2); + if (am.is_neg(val2)) { is_neg = true; am.neg(abs_val); } am.display_decimal(buffer, abs_val, decimal_prec); } else { - am.display_root_smt2(buffer, val); + am.display_root_smt2(buffer, val2); } vf = mk_string(get_manager(), buffer.str().c_str()); return is_neg ? mk_neg(vf) : vf; diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index d77deca01..79f8f740e 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -44,12 +44,12 @@ app * mk_list_assoc_app(ast_manager & m, family_id fid, decl_kind k, unsigned nu return mk_list_assoc_app(m, decl, num_args, args); } -bool is_well_formed_vars(ptr_vector& bound, expr* e) { +bool is_well_formed_vars(ptr_vector& bound, expr * top) { ptr_vector todo; ast_mark mark; - todo.push_back(e); + todo.push_back(top); while (!todo.empty()) { - expr* e = todo.back(); + expr * e = todo.back(); todo.pop_back(); if (mark.is_marked(e)) { continue; diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index d707f0178..c185540b7 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -149,10 +149,10 @@ enum status { */ static bool is_recursive_datatype(parameter const * parameters) { unsigned num_types = parameters[0].get_int(); - unsigned tid = parameters[1].get_int(); + unsigned top_tid = parameters[1].get_int(); buffer already_found(num_types, WHITE); buffer todo; - todo.push_back(tid); + todo.push_back(top_tid); while (!todo.empty()) { unsigned tid = todo.back(); if (already_found[tid] == BLACK) { @@ -198,11 +198,11 @@ static bool is_recursive_datatype(parameter const * parameters) { */ static sort_size get_datatype_size(parameter const * parameters) { unsigned num_types = parameters[0].get_int(); - unsigned tid = parameters[1].get_int(); + unsigned top_tid = parameters[1].get_int(); buffer szs(num_types, sort_size()); buffer already_found(num_types, WHITE); buffer todo; - todo.push_back(tid); + todo.push_back(top_tid); while (!todo.empty()) { unsigned tid = todo.back(); if (already_found[tid] == BLACK) { @@ -280,7 +280,7 @@ static sort_size get_datatype_size(parameter const * parameters) { } } } - return szs[tid]; + return szs[top_tid]; } /** @@ -657,8 +657,8 @@ bool datatype_decl_plugin::is_fully_interp(sort const * s) const { for (unsigned tid = 0; tid < num_types; tid++) { unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset unsigned num_constructors = parameters[o].get_int(); - for (unsigned s = 1; s <= num_constructors; s++) { - unsigned k_i = parameters[o + s].get_int(); + for (unsigned si = 1; si <= num_constructors; si++) { + unsigned k_i = parameters[o + si].get_int(); unsigned num_accessors = parameters[k_i + 2].get_int(); unsigned r = 0; for (; r < num_accessors; r++) { diff --git a/src/ast/expr2polynomial.cpp b/src/ast/expr2polynomial.cpp index fbabcb150..097d77cbc 100644 --- a/src/ast/expr2polynomial.cpp +++ b/src/ast/expr2polynomial.cpp @@ -367,16 +367,16 @@ struct expr2polynomial::imp { begin_loop: checkpoint(); frame & fr = m_frame_stack.back(); - app * t = fr.m_curr; - TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(t, m()) << "\n";); - unsigned num_args = t->get_num_args(); + app * a = fr.m_curr; + TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(a, m()) << "\n";); + unsigned num_args = a->get_num_args(); while (fr.m_idx < num_args) { - expr * arg = t->get_arg(fr.m_idx); + expr * arg = a->get_arg(fr.m_idx); fr.m_idx++; if (!visit(arg)) goto begin_loop; } - process_app(t); + process_app(a); m_frame_stack.pop_back(); } } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 16b7cc1da..75e8dfd99 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2219,13 +2219,13 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * SASSERT(sz == 3); BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned(); - mpf_rounding_mode rm; + mpf_rounding_mode mrm; switch (bv_rm) { - case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break; - case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break; - case BV_RM_TO_NEGATIVE: rm = MPF_ROUND_TOWARD_NEGATIVE; break; - case BV_RM_TO_POSITIVE: rm = MPF_ROUND_TOWARD_POSITIVE; break; - case BV_RM_TO_ZERO: rm = MPF_ROUND_TOWARD_ZERO; break; + case BV_RM_TIES_TO_AWAY: mrm = MPF_ROUND_NEAREST_TAWAY; break; + case BV_RM_TIES_TO_EVEN: mrm = MPF_ROUND_NEAREST_TEVEN; break; + case BV_RM_TO_NEGATIVE: mrm = MPF_ROUND_TOWARD_NEGATIVE; break; + case BV_RM_TO_POSITIVE: mrm = MPF_ROUND_TOWARD_POSITIVE; break; + case BV_RM_TO_ZERO: mrm = MPF_ROUND_TOWARD_ZERO; break; default: UNREACHABLE(); } @@ -2237,17 +2237,15 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * return mk_pzero(f, result); else { scoped_mpf v(m_mpf_manager); - m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); + m_util.fm().set(v, ebits, sbits, mrm, q.to_mpq()); - - - expr_ref sgn(m), s(m), e(m), unbiased_exp(m); + expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits); - mk_bias(unbiased_exp, e); + mk_bias(unbiased_exp, exp); - mk_fp(sgn, e, s, result); + mk_fp(sgn, exp, sig, result); } } else if (m_util.au().is_numeral(x)) { @@ -2275,37 +2273,37 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * expr_ref v1(m), v2(m), v3(m), v4(m); - expr_ref sgn(m), s(m), e(m), unbiased_exp(m); + expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v1); + mk_bias(unbiased_exp, exp); + mk_fp(sgn, exp, sig, v1); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v2); + mk_bias(unbiased_exp, exp); + mk_fp(sgn, exp, sig, v2); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v3); + mk_bias(unbiased_exp, exp); + mk_fp(sgn, exp, sig, v3); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v4); + mk_bias(unbiased_exp, exp); + mk_fp(sgn, exp, sig, v4); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits); - mk_bias(unbiased_exp, e); + mk_bias(unbiased_exp, exp); - mk_fp(sgn, e, s, result); + mk_fp(sgn, exp, sig, result); mk_ite(rm_tn, v4, result, result); mk_ite(rm_tp, v3, result, result); mk_ite(rm_nte, v2, result, result); @@ -3350,7 +3348,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref // the maximum shift is `sbits', because after that the mantissa // would be zero anyways. So we can safely cut the shift variable down, // as long as we check the higher bits. - expr_ref sh(m), is_sh_zero(m), sl(m), zero_s(m), sbits_s(m), short_shift(m); + expr_ref sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m); zero_s = m_bv_util.mk_numeral(0, sbits-1); sbits_s = m_bv_util.mk_numeral(sbits, sbits); sh = m_bv_util.mk_extract(ebits-1, sbits, shift); diff --git a/src/ast/func_decl_dependencies.cpp b/src/ast/func_decl_dependencies.cpp index 162efb0dd..76f1e3889 100644 --- a/src/ast/func_decl_dependencies.cpp +++ b/src/ast/func_decl_dependencies.cpp @@ -145,24 +145,24 @@ class func_decl_dependencies::top_sort { return false; m_todo.push_back(f); while (!m_todo.empty()) { - func_decl * f = m_todo.back(); + func_decl * cf = m_todo.back(); - switch (get_color(f)) { + switch (get_color(cf)) { case CLOSED: m_todo.pop_back(); break; case OPEN: - set_color(f, IN_PROGRESS); - if (visit_children(f)) { + set_color(cf, IN_PROGRESS); + if (visit_children(cf)) { SASSERT(m_todo.back() == f); m_todo.pop_back(); - set_color(f, CLOSED); + set_color(cf, CLOSED); } break; case IN_PROGRESS: - if (all_children_closed(f)) { - SASSERT(m_todo.back() == f); - set_color(f, CLOSED); + if (all_children_closed(cf)) { + SASSERT(m_todo.back() == cf); + set_color(cf, CLOSED); } else { m_todo.reset(); return true; diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index e97933921..9284ff420 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -464,18 +464,18 @@ void bit_blaster_tpl::mk_udiv_urem(unsigned sz, expr * const * a_bits, expr // update p if (i < sz - 1) { for (unsigned j = sz - 1; j > 0; j--) { - expr_ref i(m()); - mk_ite(q, t.get(j-1), p.get(j-1), i); - p.set(j, i); + expr_ref ie(m()); + mk_ite(q, t.get(j-1), p.get(j-1), ie); + p.set(j, ie); } p.set(0, a_bits[sz - i - 2]); } else { // last step: p contains the remainder for (unsigned j = 0; j < sz; j++) { - expr_ref i(m()); - mk_ite(q, t.get(j), p.get(j), i); - p.set(j, i); + expr_ref ie(m()); + mk_ite(q, t.get(j), p.get(j), ie); + p.set(j, ie); } } } diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 92f06679d..be3bfbd0a 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -324,7 +324,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { } result_stack().push_back(def); TRACE("get_macro", tout << "bindings:\n"; - for (unsigned i = 0; i < m_bindings.size(); i++) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";); + for (unsigned j = 0; j < m_bindings.size(); j++) tout << j << ": " << mk_ismt2_pp(m_bindings[j], m()) << "\n";); begin_scope(); m_num_qvars = 0; m_root = def; diff --git a/src/ast/shared_occs.h b/src/ast/shared_occs.h index e135fea84..b522f4a4d 100644 --- a/src/ast/shared_occs.h +++ b/src/ast/shared_occs.h @@ -75,7 +75,7 @@ public: iterator end_shared() const { return m_shared.end(); } void reset(); void cleanup(); - void display(std::ostream & out, ast_manager & m) const; + void display(std::ostream & out, ast_manager & mgr) const; }; #endif diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp index 0de507183..dc24a625b 100644 --- a/src/tactic/arith/arith_bounds_tactic.cpp +++ b/src/tactic/arith/arith_bounds_tactic.cpp @@ -34,8 +34,8 @@ struct arith_bounds_tactic : public tactic { bounds_arith_subsumption(in, result); } - virtual tactic* translate(ast_manager& m) { - return alloc(arith_bounds_tactic, m); + virtual tactic* translate(ast_manager & mgr) { + return alloc(arith_bounds_tactic, mgr); } void checkpoint() { diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 9765bced5..149cbc272 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -709,8 +709,6 @@ public: tactic_ref_vector ts2; goal_ref_vector g_copies; - ast_manager & m = in->m(); - for (unsigned i = 0; i < r1_size; i++) { ast_manager * new_m = alloc(ast_manager, m, !m.proof_mode()); managers.push_back(new_m); From f8e2fa03379d752fc400376f312a5d8115e173fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 May 2015 11:11:13 -0700 Subject: [PATCH 24/48] fixes issue #93 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array_full.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index dd74f2871..f2d1527c0 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -775,17 +775,19 @@ namespace smt { bool theory_array_full::try_assign_eq(expr* v1, expr* v2) { + TRACE("array", + tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" + << mk_bounded_pp(v2, get_manager()) << "\n";); context& ctx = get_context(); if (m_eqs.contains(v1, v2)) { return false; } - m_eqs.insert(v1, v2, true); - TRACE("array", - tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" - << mk_bounded_pp(v2, get_manager()) << "\n";); - literal eq(mk_eq(v1, v2, true)); - m_eqsv.push_back(eq); - return true; + else { + m_eqs.insert(v1, v2, true); + literal eq(mk_eq(v1, v2, true)); + m_eqsv.push_back(eq); + return true; + } } void theory_array_full::pop_scope_eh(unsigned num_scopes) { From 894d6cb11b4be3750d32ca42218f8f379f7b9e25 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 May 2015 13:38:54 -0700 Subject: [PATCH 25/48] fix build break to support new statistics items Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 16d2eb6ba..6d0c5bad0 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -5617,7 +5617,7 @@ class Statistics: sat >>> st = s.statistics() >>> len(st) - 2 + 4 """ return int(Z3_stats_size(self.ctx.ref(), self.stats)) @@ -5631,7 +5631,7 @@ class Statistics: sat >>> st = s.statistics() >>> len(st) - 2 + 4 >>> st[0] ('nlsat propagations', 2) >>> st[1] @@ -5655,7 +5655,7 @@ class Statistics: sat >>> st = s.statistics() >>> st.keys() - ['nlsat propagations', 'nlsat stages'] + ['nlsat propagations', 'nlsat stages', 'max memory', 'memory'] """ return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))] @@ -5692,7 +5692,7 @@ class Statistics: sat >>> st = s.statistics() >>> st.keys() - ['nlsat propagations', 'nlsat stages'] + ['nlsat propagations', 'nlsat stages', 'max memory', 'memory'] >>> st.nlsat_propagations 2 >>> st.nlsat_stages From 2d409c6042318e74d6d1b8adfc5c36225b53a691 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 May 2015 14:32:24 -0700 Subject: [PATCH 26/48] revert bug introduced to avoid stack overflow in arrays Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array_full.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index f2d1527c0..4e169a8be 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -785,7 +785,10 @@ namespace smt { else { m_eqs.insert(v1, v2, true); literal eq(mk_eq(v1, v2, true)); - m_eqsv.push_back(eq); + get_context().mark_as_relevant(eq); + assert_axiom(eq); + + // m_eqsv.push_back(eq); return true; } } From e240e6c4300aad2b6cd64bef92cf9d8e165b5bfb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 30 May 2015 12:12:23 +0100 Subject: [PATCH 27/48] Bugfix for variable renamings (fec815b41ef66c5dc28a04aeabd933fca59e4d37) --- src/ast/func_decl_dependencies.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/func_decl_dependencies.cpp b/src/ast/func_decl_dependencies.cpp index 76f1e3889..d53c2d9b1 100644 --- a/src/ast/func_decl_dependencies.cpp +++ b/src/ast/func_decl_dependencies.cpp @@ -154,7 +154,7 @@ class func_decl_dependencies::top_sort { case OPEN: set_color(cf, IN_PROGRESS); if (visit_children(cf)) { - SASSERT(m_todo.back() == f); + SASSERT(m_todo.back() == cf); m_todo.pop_back(); set_color(cf, CLOSED); } From fde873ac09c0e183b28d9b27809ec05a416467e4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 30 May 2015 14:50:15 +0100 Subject: [PATCH 28/48] Bugfix for rounding in FP to_sbv. Fixes #113 --- src/ast/fpa/fpa2bv_converter.cpp | 50 ++++++++++++++++++++++---------- 1 file changed, 35 insertions(+), 15 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 75e8dfd99..ef11a4f1e 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2953,9 +2953,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift); SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2); SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2); - SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2); - dbg_decouple("fpa2bv_to_sbv_shift", shift); - dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs); + SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2); + dbg_decouple("fpa2bv_to_sbv_shift", shift); // sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long // [1][ ... sig ... ][r][g][ ... s ...] @@ -2964,34 +2963,48 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz); shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs); SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz); + dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs); expr_ref c_in_limits(m); c_in_limits = m_bv_util.mk_sle(shift, m_bv_util.mk_numeral(0, ebits + 2)); dbg_decouple("fpa2bv_to_sbv_in_limits", c_in_limits); - expr_ref shifted_sig(m); - shifted_sig = m_bv_util.mk_bv_lshr(sig, shift_abs); - dbg_decouple("fpa2bv_to_sbv_shifted_sig", shifted_sig); + expr_ref huge_sig(m), huge_shift(m), huge_shifted_sig(m); + huge_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_sz)); + huge_shift = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sig_sz), shift_abs); + huge_shifted_sig = m_bv_util.mk_bv_lshr(huge_sig, huge_shift); + dbg_decouple("fpa2bv_to_sbv_huge_shifted_sig", huge_shifted_sig); + SASSERT(m_bv_util.get_bv_size(huge_shifted_sig) == 2 * sig_sz); + + expr_ref upper_hss(m), lower_hss(m); + upper_hss = m_bv_util.mk_extract(2 * sig_sz - 1, sig_sz + 1, huge_shifted_sig); + lower_hss = m_bv_util.mk_extract(sig_sz, 0, huge_shifted_sig); + SASSERT(m_bv_util.get_bv_size(upper_hss) == sig_sz - 1); + SASSERT(m_bv_util.get_bv_size(lower_hss) == sig_sz + 1); + dbg_decouple("fpa2bv_to_sbv_upper_hss", upper_hss); + dbg_decouple("fpa2bv_to_sbv_lower_hss", lower_hss); expr_ref last(m), round(m), sticky(m); - last = m_bv_util.mk_extract(sig_sz - bv_sz - 0, sig_sz - bv_sz - 0, shifted_sig); - round = m_bv_util.mk_extract(sig_sz - bv_sz - 1, sig_sz - bv_sz - 1, shifted_sig); - sticky = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(sig_sz - bv_sz - 2, 0, shifted_sig), - m_bv_util.mk_numeral(0, sig_sz - (bv_sz + 3) + 2)), - bv0, - bv1); + last = m_bv_util.mk_extract(1, 1, upper_hss); + round = m_bv_util.mk_extract(0, 0, upper_hss); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lower_hss); dbg_decouple("fpa2bv_to_sbv_last", last); dbg_decouple("fpa2bv_to_sbv_round", round); dbg_decouple("fpa2bv_to_sbv_sticky", sticky); + expr_ref upper_hss_w_sticky(m); + upper_hss_w_sticky = m_bv_util.mk_concat(upper_hss, sticky); + dbg_decouple("fpa2bv_to_sbv_upper_hss_w_sticky", upper_hss_w_sticky); + SASSERT(m_bv_util.get_bv_size(upper_hss_w_sticky) == sig_sz); + expr_ref rounding_decision(m); rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky); SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1); dbg_decouple("fpa2bv_to_sbv_rounding_decision", rounding_decision); expr_ref unrounded_sig(m), pre_rounded(m), inc(m); - unrounded_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz, shifted_sig)); - inc = m_bv_util.mk_zero_extend(1, m_bv_util.mk_zero_extend(bv_sz - 1, rounding_decision)); + unrounded_sig = m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz - 1, upper_hss_w_sticky); + inc = m_bv_util.mk_zero_extend(bv_sz, rounding_decision); pre_rounded = m_bv_util.mk_bv_add(unrounded_sig, inc); dbg_decouple("fpa2bv_to_sbv_inc", inc); dbg_decouple("fpa2bv_to_sbv_unrounded_sig", unrounded_sig); @@ -3399,7 +3412,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #ifdef Z3DEBUG - return; + // return; // CMW: This works only for quantifier-free formulas. expr_ref new_e(m); new_e = m.mk_fresh_const(prefix, m.get_sort(e)); @@ -3409,6 +3422,12 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { } expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky) { + dbg_decouple("fpa2bv_rnd_dec_rm", expr_ref(rm, m)); + dbg_decouple("fpa2bv_rnd_dec_sgn", expr_ref(sgn, m)); + dbg_decouple("fpa2bv_rnd_dec_last", expr_ref(last, m)); + dbg_decouple("fpa2bv_rnd_dec_round", expr_ref(round, m)); + dbg_decouple("fpa2bv_rnd_dec_sticky", expr_ref(sticky, m)); + expr_ref last_or_sticky(m), round_or_sticky(m), not_last(m), not_round(m), not_sticky(m), not_lors(m), not_rors(m), not_sgn(m); expr * last_sticky[2] = { last, sticky }; expr * round_sticky[2] = { round, sticky }; @@ -3446,6 +3465,7 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * la m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2); m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, res); + dbg_decouple("fpa2bv_rnd_dec_res", res); return res; } From 5ae2dd9c747946535f1f05771161b19d0e03ccf6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 30 May 2015 15:20:07 +0100 Subject: [PATCH 29/48] Bugfix for QF_FP default tactic. --- src/tactic/fpa/qffp_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 3bee224b3..fbce1668e 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -45,7 +45,7 @@ struct has_fp_to_real_predicate { void operator()(app * n) { sort * s = get_sort(n); if (au.is_real(s) && n->get_family_id() == fu.get_family_id() && - is_app(n) && to_app(n)->get_kind() == OP_FPA_TO_REAL) + is_app(n) && to_app(n)->get_decl_kind() == OP_FPA_TO_REAL) throw found(); } }; From 8d55159dc85a6d353c0f5d5b8ec45de04c73cded Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 30 May 2015 15:23:30 +0100 Subject: [PATCH 30/48] Proper declaration of locals to make clang happy. --- src/ast/fpa/fpa2bv_converter.cpp | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index ef11a4f1e..11c6f8bf6 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2987,7 +2987,7 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg expr_ref last(m), round(m), sticky(m); last = m_bv_util.mk_extract(1, 1, upper_hss); round = m_bv_util.mk_extract(0, 0, upper_hss); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lower_hss); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lower_hss.get()); dbg_decouple("fpa2bv_to_sbv_last", last); dbg_decouple("fpa2bv_to_sbv_round", round); dbg_decouple("fpa2bv_to_sbv_sticky", sticky); @@ -3412,7 +3412,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #ifdef Z3DEBUG - // return; + return; // CMW: This works only for quantifier-free formulas. expr_ref new_e(m); new_e = m.mk_fresh_const(prefix, m.get_sort(e)); @@ -3422,11 +3422,16 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { } expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky) { - dbg_decouple("fpa2bv_rnd_dec_rm", expr_ref(rm, m)); - dbg_decouple("fpa2bv_rnd_dec_sgn", expr_ref(sgn, m)); - dbg_decouple("fpa2bv_rnd_dec_last", expr_ref(last, m)); - dbg_decouple("fpa2bv_rnd_dec_round", expr_ref(round, m)); - dbg_decouple("fpa2bv_rnd_dec_sticky", expr_ref(sticky, m)); + expr_ref rmr(rm, m); + expr_ref sgnr(sgn, m); + expr_ref lastr(last, m); + expr_ref roundr(round, m); + expr_ref stickyr(sticky, m); + dbg_decouple("fpa2bv_rnd_dec_rm", rmr); + dbg_decouple("fpa2bv_rnd_dec_sgn", sgnr); + dbg_decouple("fpa2bv_rnd_dec_last", lastr); + dbg_decouple("fpa2bv_rnd_dec_round", roundr); + dbg_decouple("fpa2bv_rnd_dec_sticky", stickyr); expr_ref last_or_sticky(m), round_or_sticky(m), not_last(m), not_round(m), not_sticky(m), not_lors(m), not_rors(m), not_sgn(m); expr * last_sticky[2] = { last, sticky }; From 6f42cbd325f6d9474d58720e3d7e7d5e84c3fc4b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2015 09:22:19 -0700 Subject: [PATCH 31/48] remove std-out Signed-off-by: Nikolaj Bjorner --- src/muz/base/rule_properties.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 5d1aff44e..455e02e45 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -194,7 +194,6 @@ void rule_properties::operator()(app* n) { } } else { - std::cout << mk_pp(n, m) << "\n"; } } From 46a5aeaef1c0ed393c4595b72fb7805ff3056585 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2015 14:10:22 -0700 Subject: [PATCH 32/48] improve type checking and reporting, fixes issue #116 Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index b056ded36..37b339ddb 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -594,6 +594,18 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p } func_decl * r = mk_func_decl(k, bv_size); if (r != 0) { + if (num_args != r->get_arity()) { + m.raise_exception("declared arity mismatches supplied arity"); + return 0; + } + for (unsigned i = 0; i < num_args; ++i) { + if (m.get_sort(args[i]) != r->get_domain(i)) { + std::ostringstream buffer; + buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m); + m.raise_exception(buffer.str().c_str()); + return 0; + } + } return r; } return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range); From d4dd608badd15221cd95da57ddc044f19e239fab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2015 14:11:31 -0700 Subject: [PATCH 33/48] improve type checking and reporting, fixes issue #116 Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 37b339ddb..d01b8371b 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -566,6 +566,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range) { + ast_manager& m = *m_manager; int bv_size; if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) { // bv_size is filled in. @@ -589,7 +590,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range); } else if (num_args == 0 || !get_bv_size(args[0], bv_size)) { - m_manager->raise_exception("operator is applied to arguments of the wrong sort"); + m.raise_exception("operator is applied to arguments of the wrong sort"); return 0; } func_decl * r = mk_func_decl(k, bv_size); From aee18130568812d06f3a02e8aa075eb540fc803a Mon Sep 17 00:00:00 2001 From: Matthias Schlaipfer Date: Tue, 2 Jun 2015 09:49:08 +0100 Subject: [PATCH 34/48] Added missing input format option "-dl" Signed-off-by: Matthias Schlaipfer --- src/shell/main.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 5a47d0d16..609f5d47b 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -163,6 +163,9 @@ void parse_cmd_line_args(int argc, char ** argv) { else if (strcmp(opt_name, "smt2") == 0) { g_input_kind = IN_SMTLIB_2; } + else if (strcmp(opt_name, "dl") == 0) { + g_input_kind = IN_DATALOG; + } else if (strcmp(opt_name, "in") == 0) { g_standard_input = true; } From d6398c4fdc7eb625c3d20f709fc3691d14214b1a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jun 2015 11:59:55 +0100 Subject: [PATCH 35/48] Fixed FPA Python doctest --- src/api/python/z3.py | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 6d0c5bad0..9ac9da3e8 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8194,21 +8194,21 @@ def FP(name, fpsort, ctx=None): >>> eq(x, x2) True """ - ctx = fpsort.ctx + if isinstance(fpsort, FPSortRef): + ctx = fpsort.ctx + else: + ctx = _get_ctx(ctx) return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx) def FPs(names, fpsort, ctx=None): """Return an array of floating-point constants. - >>> x, y, z = BitVecs('x y z', 16) - >>> x.size() - 16 + >>> x, y, z = FPs('x y z', FPSort(8, 24)) >>> x.sort() - BitVec(16) - >>> Sum(x, y, z) - 0 + x + y + z - >>> Product(x, y, z) - 1*x*y*z + >>> x.sbits() + 24 + >>> x.ebits() + 8 >>> simplify(Product(x, y, z)) x*y*z """ From c7fd74e8adc6be5eca0f153ddb781927f98210e0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jun 2015 12:45:55 +0100 Subject: [PATCH 36/48] Fixed FPA Python doctest --- src/api/python/z3.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 9ac9da3e8..f6a617317 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8205,12 +8205,13 @@ def FPs(names, fpsort, ctx=None): >>> x, y, z = FPs('x y z', FPSort(8, 24)) >>> x.sort() + FPSort(8, 24) >>> x.sbits() 24 >>> x.ebits() 8 - >>> simplify(Product(x, y, z)) - x*y*z + >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) + fpMul(RNE(), fpAdd(RNE(), x, y), z) """ ctx = z3._get_ctx(ctx) if isinstance(names, str): From 17c06199a89ae28ec605d7d47e6274a4c43da0da Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jun 2015 12:46:30 +0100 Subject: [PATCH 37/48] Relaxed BV type checking, follow up to issue #116 --- src/ast/bv_decl_plugin.cpp | 28 ++++++++++++++++++++++------ 1 file changed, 22 insertions(+), 6 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index d01b8371b..f65462d1b 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -501,13 +501,17 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p func_decl * r = mk_func_decl(k, bv_size); if (r != 0) { if (arity != r->get_arity()) { - m_manager->raise_exception("declared arity mismatches supplied arity"); - return 0; + if (r->get_info()->is_associative()) + arity = r->get_arity(); + else { + m_manager->raise_exception("declared arity mismatches supplied arity"); + return 0; + } } for (unsigned i = 0; i < arity; ++i) { if (domain[i] != r->get_domain(i)) { m_manager->raise_exception("declared sorts do not match supplied sorts"); - return 0; + return 0; } } return r; @@ -596,15 +600,27 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p func_decl * r = mk_func_decl(k, bv_size); if (r != 0) { if (num_args != r->get_arity()) { - m.raise_exception("declared arity mismatches supplied arity"); - return 0; + if (r->get_info()->is_associative()) { + sort * fs = r->get_domain(0); + for (unsigned i = 0; i < num_args; ++i) { + if (m.get_sort(args[i]) != fs) { + m_manager->raise_exception("declared sorts do not match supplied sorts"); + return 0; + } + } + return r; + } + else { + m.raise_exception("declared arity mismatches supplied arity"); + return 0; + } } for (unsigned i = 0; i < num_args; ++i) { if (m.get_sort(args[i]) != r->get_domain(i)) { std::ostringstream buffer; buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m); m.raise_exception(buffer.str().c_str()); - return 0; + return 0; } } return r; From bc94007207e62a5e56c8660263d50552c880ab92 Mon Sep 17 00:00:00 2001 From: Matthias Schlaipfer Date: Tue, 2 Jun 2015 14:58:31 +0100 Subject: [PATCH 38/48] Fixed non-deterministic behaviour in relation_map Use of ptr_hash and subsequent iteration led to non-deterministic behaviour in Datalog engine. Signed-off-by: Matthias Schlaipfer --- src/muz/rel/dl_relation_manager.cpp | 2 +- src/muz/rel/dl_relation_manager.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index b92c9f796..6a9bb7f2a 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -108,7 +108,7 @@ namespace datalog { void relation_manager::store_relation(func_decl * pred, relation_base * rel) { SASSERT(rel); - relation_map::entry * e = m_relations.insert_if_not_there2(pred, 0); + relation_map::obj_map_entry * e = m_relations.insert_if_not_there2(pred, 0); if (e->get_data().m_value) { e->get_data().m_value->deallocate(); } diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h index 530538df5..53d7f21e2 100644 --- a/src/muz/rel/dl_relation_manager.h +++ b/src/muz/rel/dl_relation_manager.h @@ -73,7 +73,7 @@ namespace datalog { typedef map, ptr_eq > rp2fprp_map; - typedef map, ptr_eq > relation_map; + typedef obj_map relation_map; typedef ptr_vector table_plugin_vector; typedef ptr_vector relation_plugin_vector; From 7161d6c1503eea13e7bde7ae17333b0f5ddf1aaa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2015 08:48:37 -0700 Subject: [PATCH 39/48] fixes crash from issue #119 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/card2bv_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 933b687b4..7c715e6e7 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -488,7 +488,7 @@ public: unsigned size = g->size(); expr_ref new_f1(m), new_f2(m); proof_ref new_pr1(m), new_pr2(m); - for (unsigned idx = 0; idx < size; idx++) { + for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) { m_rw1(g->form(idx), new_f1, new_pr1); TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;); m_rw2.rewrite(new_f1, new_f2); From a07cba72bccf568486f0aaf701912222827a39d3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jun 2015 17:15:07 +0100 Subject: [PATCH 40/48] eliminated unused variables --- src/tactic/fpa/fpa2bv_approx_tactic.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_approx_tactic.cpp b/src/tactic/fpa/fpa2bv_approx_tactic.cpp index 4670883e1..9d5873f12 100644 --- a/src/tactic/fpa/fpa2bv_approx_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_approx_tactic.cpp @@ -147,7 +147,6 @@ class fpa2bv_approx_tactic: public tactic { while (to_traverse.size() > 0) { cur = to_app(to_traverse.front()); - mpf_rounding_mode rm; #ifdef Z3DEBUG std::cout<<"Analyze - traversing: "<::iterator itp = ranked_terms.begin(); itp != ranked_terms.end(); itp++) { From ffff006945611126334728fd0640f38a808da729 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2015 09:15:08 -0700 Subject: [PATCH 41/48] remove old files Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 16 ++- src/opt/opt_solver.h | 2 +- src/qe/qe_mbp.h | 48 ------- src/qe/qsat.cpp | 281 ----------------------------------------- src/qe/qsat.h | 52 -------- 5 files changed, 10 insertions(+), 389 deletions(-) delete mode 100644 src/qe/qe_mbp.h delete mode 100644 src/qe/qsat.cpp delete mode 100644 src/qe/qsat.h diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index d505a9ffb..dcbbc3fae 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -42,7 +42,7 @@ namespace opt { m_context(mgr, m_params), m(mgr), m_fm(fm), - m_objective_sorts(m), + m_objective_terms(m), m_dump_benchmarks(false), m_first(true) { m_params.updt_params(p); @@ -213,11 +213,13 @@ namespace opt { } else { SASSERT(has_shared); - decrement_value(i, val); + decrement_value(i, val); } m_objective_values[i] = val; - TRACE("opt", { tout << val << "\n"; - tout << blocker << "\n"; + TRACE("opt", { + tout << "objective: " << mk_pp(m_objective_terms[i].get(), m) << "\n"; + tout << "maximal value: " << val << "\n"; + tout << "new condition: " << blocker << "\n"; model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); }); } @@ -240,7 +242,7 @@ namespace opt { TRACE("opt", tout << is_sat << "\n";); if (is_sat != l_true) { // cop-out approximation - if (arith_util(m).is_real(m_objective_sorts[i].get())) { + if (arith_util(m).is_real(m_objective_terms[i].get())) { val -= inf_eps(inf_rational(rational(0), true)); } else { @@ -304,7 +306,7 @@ namespace opt { smt::theory_var v = get_optimizer().add_objective(term); m_objective_vars.push_back(v); m_objective_values.push_back(inf_eps(rational(-1), inf_rational())); - m_objective_sorts.push_back(m.get_sort(term)); + m_objective_terms.push_back(term); m_valid_objectives.push_back(true); m_models.push_back(0); return v; @@ -363,7 +365,7 @@ namespace opt { void opt_solver::reset_objectives() { m_objective_vars.reset(); m_objective_values.reset(); - m_objective_sorts.reset(); + m_objective_terms.reset(); m_valid_objectives.reset(); } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 19205ddd9..a18ad9540 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -76,7 +76,7 @@ namespace opt { svector m_objective_vars; vector m_objective_values; sref_vector m_models; - sort_ref_vector m_objective_sorts; + expr_ref_vector m_objective_terms; svector m_valid_objectives; bool m_dump_benchmarks; static unsigned m_dump_count; diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h deleted file mode 100644 index 11bceef0b..000000000 --- a/src/qe/qe_mbp.h +++ /dev/null @@ -1,48 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - - qe_mbp.h - -Abstract: - - Model-based projection utilities - -Author: - - Nikolaj Bjorner (nbjorner) 2015-5-28 - -Revision History: - - ---*/ - -#ifndef __QE_MBP_H__ -#define __QE_MBP_H__ - -#include "ast.h" -#include "params.h" - -namespace qe { - class mbp { - class impl; - impl * m_impl; - public: - mbp(ast_manager& m); - - ~mbp(); - - /** - \brief - Apply model-based qe on constants provided as vector of variables. - Return the updated formula and updated set of variables that were not eliminated. - - */ - void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml); - - void set_cancel(bool f); - }; -} - -#endif diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp deleted file mode 100644 index 4c736bc31..000000000 --- a/src/qe/qsat.cpp +++ /dev/null @@ -1,281 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - - qsat.cpp - -Abstract: - - Quantifier Satisfiability Solver. - -Author: - - Nikolaj Bjorner (nbjorner) 2015-5-28 - -Revision History: - - ---*/ - -#include "qsat.h" -#include "smt_kernel.h" -#include "qe_mbp.h" -#include "smt_params.h" -#include "ast_util.h" - -using namespace qe; - -struct qdef_t { - expr_ref m_pred; - expr_ref m_expr; - expr_ref_vector m_vars; - bool m_is_forall; - qdef_t(expr_ref& p, expr_ref& e, expr_ref_vector const& vars, bool is_forall): - m_pred(p), - m_expr(e), - m_vars(vars), - m_is_forall(is_forall) {} -}; - -typedef vector qdefs_t; - -struct pdef_t { - expr_ref m_pred; - expr_ref m_atom; - pdef_t(expr_ref& p, expr* a): - m_pred(p), - m_atom(a, p.get_manager()) - {} -}; - -class qsat::impl { - ast_manager& m; - qe::mbp mbp; - smt_params m_smtp; - smt::kernel m_kernel; - expr_ref m_fml_pred; // predicate that encodes top-level formula - expr_ref_vector m_atoms; // predicates that encode atomic subformulas - - - lbool check_sat() { - // TBD main procedure goes here. - return l_undef; - } - - /** - \brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate. - */ - void remove_quantifiers(expr_ref_vector& fmls, qdefs_t& defs) { - - } - - /** - \brief create propositional abstration of formula by replacing atomic sub-formulas by fresh - propositional variables, and adding definitions for each propositional formula on the side. - Assumption is that the formula is quantifier-free. - */ - void mk_abstract(expr_ref& fml, vector& pdefs) { - expr_ref_vector todo(m), trail(m); - obj_map cache; - ptr_vector args; - expr_ref r(m); - todo.push_back(fml); - while (!todo.empty()) { - expr* e = todo.back(); - if (cache.contains(e)) { - todo.pop_back(); - continue; - } - SASSERT(is_app(e)); - app* a = to_app(e); - if (a->get_family_id() == m.get_basic_family_id()) { - unsigned sz = a->get_num_args(); - args.reset(); - for (unsigned i = 0; i < sz; ++i) { - expr* f = a->get_arg(i); - if (cache.find(f, f)) { - args.push_back(f); - } - else { - todo.push_back(f); - } - } - if (args.size() == sz) { - r = m.mk_app(a->get_decl(), sz, args.c_ptr()); - cache.insert(e, r); - trail.push_back(r); - todo.pop_back(); - } - } - else if (is_uninterp_const(a)) { - cache.insert(e, e); - } - else { - // TBD: nested Booleans. - - r = m.mk_fresh_const("p",m.mk_bool_sort()); - trail.push_back(r); - cache.insert(e, r); - pdefs.push_back(pdef_t(r, e)); - } - } - fml = cache.find(fml); - } - - /** - \brief use dual propagation to minimize model. - */ - bool minimize_assignment(expr_ref_vector& assignment, expr* not_fml) { - bool result = false; - assignment.push_back(not_fml); - lbool res = m_kernel.check(assignment.size(), assignment.c_ptr()); - switch (res) { - case l_true: - UNREACHABLE(); - break; - case l_undef: - break; - case l_false: - result = true; - get_core(assignment, not_fml); - break; - } - return result; - } - - lbool check_sat(expr_ref_vector& assignment, expr* fml) { - assignment.push_back(fml); - lbool res = m_kernel.check(assignment.size(), assignment.c_ptr()); - switch (res) { - case l_true: { - model_ref mdl; - expr_ref tmp(m); - assignment.reset(); - m_kernel.get_model(mdl); - for (unsigned i = 0; i < m_atoms.size(); ++i) { - expr* p = m_atoms[i].get(); - if (mdl->eval(p, tmp)) { - if (m.is_true(tmp)) { - assignment.push_back(p); - } - else if (m.is_false(tmp)) { - assignment.push_back(m.mk_not(p)); - } - } - } - expr_ref not_fml = mk_not(fml); - if (!minimize_assignment(assignment, not_fml)) { - res = l_undef; - } - break; - } - case l_undef: - break; - case l_false: - get_core(assignment, fml); - break; - } - return res; - } - - void get_core(expr_ref_vector& core, expr* exclude) { - unsigned sz = m_kernel.get_unsat_core_size(); - core.reset(); - for (unsigned i = 0; i < sz; ++i) { - expr* e = m_kernel.get_unsat_core_expr(i); - if (e != exclude) { - core.push_back(e); - } - } - } - - expr_ref mk_not(expr* e) { - return expr_ref(::mk_not(m, e), m); - } - -public: - impl(ast_manager& m): - m(m), - mbp(m), - m_kernel(m, m_smtp), - m_fml_pred(m), - m_atoms(m) {} - - void updt_params(params_ref const & p) { - } - - void collect_param_descrs(param_descrs & r) { - } - - void operator()(/* in */ goal_ref const & in, - /* out */ goal_ref_buffer & result, - /* out */ model_converter_ref & mc, - /* out */ proof_converter_ref & pc, - /* out */ expr_dependency_ref & core) { - - } - - void collect_statistics(statistics & st) const { - - } - void reset_statistics() { - } - - void cleanup() { - } - - void set_logic(symbol const & l) { - } - - void set_progress_callback(progress_callback * callback) { - } - - tactic * translate(ast_manager & m) { - return 0; - } - -}; - -qsat::qsat(ast_manager& m) { - m_impl = alloc(impl, m); -} - -qsat::~qsat() { - dealloc(m_impl); -} - -void qsat::updt_params(params_ref const & p) { - m_impl->updt_params(p); -} -void qsat::collect_param_descrs(param_descrs & r) { - m_impl->collect_param_descrs(r); -} -void qsat::operator()(/* in */ goal_ref const & in, - /* out */ goal_ref_buffer & result, - /* out */ model_converter_ref & mc, - /* out */ proof_converter_ref & pc, - /* out */ expr_dependency_ref & core) { - (*m_impl)(in, result, mc, pc, core); -} - -void qsat::collect_statistics(statistics & st) const { - m_impl->collect_statistics(st); -} -void qsat::reset_statistics() { - m_impl->reset_statistics(); -} -void qsat::cleanup() { - m_impl->cleanup(); -} -void qsat::set_logic(symbol const & l) { - m_impl->set_logic(l); -} -void qsat::set_progress_callback(progress_callback * callback) { - m_impl->set_progress_callback(callback); -} -tactic * qsat::translate(ast_manager & m) { - return m_impl->translate(m); -} - - diff --git a/src/qe/qsat.h b/src/qe/qsat.h deleted file mode 100644 index 2fc071c76..000000000 --- a/src/qe/qsat.h +++ /dev/null @@ -1,52 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - - qsat.h - -Abstract: - - Quantifier Satisfiability Solver. - -Author: - - Nikolaj Bjorner (nbjorner) 2015-5-28 - -Revision History: - - ---*/ - -#ifndef __QE_QSAT_H__ -#define __QE_QSAT_H__ - -#include "tactic.h" - -namespace qe { - class qsat : public tactic { - class impl; - impl * m_impl; - public: - qsat(ast_manager& m); - ~qsat(); - - virtual void updt_params(params_ref const & p); - virtual void collect_param_descrs(param_descrs & r); - virtual void operator()(/* in */ goal_ref const & in, - /* out */ goal_ref_buffer & result, - /* out */ model_converter_ref & mc, - /* out */ proof_converter_ref & pc, - /* out */ expr_dependency_ref & core); - - virtual void collect_statistics(statistics & st) const; - virtual void reset_statistics(); - virtual void cleanup() = 0; - virtual void set_logic(symbol const & l); - virtual void set_progress_callback(progress_callback * callback); - virtual tactic * translate(ast_manager & m); - - }; -}; - -#endif From 65a6845945670c01b420e3eb2bece65ce9a03a66 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jun 2015 17:19:31 +0100 Subject: [PATCH 42/48] Bugfix for fpa2bv_converter_prec --- src/tactic/fpa/fpa2bv_converter_prec.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter_prec.cpp b/src/tactic/fpa/fpa2bv_converter_prec.cpp index ff627f7e4..b60a58968 100644 --- a/src/tactic/fpa/fpa2bv_converter_prec.cpp +++ b/src/tactic/fpa/fpa2bv_converter_prec.cpp @@ -35,8 +35,8 @@ fpa2bv_converter_prec::fpa2bv_converter_prec(ast_manager & m, fpa_approximation_ void fpa2bv_converter_prec::fix_bits(unsigned prec, expr_ref rounded, unsigned sbits, unsigned ebits)//expr_ref& fixed, { //AZ: TODO: revise! minimal number of legal bits is 3!!!! Remove magic numbers - unsigned szeroes=((sbits-2)*(MAX_PRECISION - prec +0.0)/MAX_PRECISION);//3 bits are minimum for the significand - unsigned ezeroes=((ebits-2)*(MAX_PRECISION - prec+0.0)/MAX_PRECISION);//2 bits are minimum for the exponent + unsigned szeroes = (unsigned) ((sbits-2)*(MAX_PRECISION - prec +0.0) / MAX_PRECISION);//3 bits are minimum for the significand + unsigned ezeroes = (unsigned) ((ebits - 2)*(MAX_PRECISION - prec + 0.0) / MAX_PRECISION);//2 bits are minimum for the exponent expr_ref fix_sig(m), fix_exp(m); expr * sgn, *sig, *expn; @@ -226,8 +226,8 @@ void fpa2bv_converter_prec::mk_cast_small_to_big(unsigned sbits, unsigned ebits, void fpa2bv_converter_prec::match_sorts(expr * a, expr * b, expr_ref & n_a, expr_ref & n_b) { //Check if the sorts of lhs and rhs match, otherwise cast them to appropriate size? - SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_TO_FP)); - SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_TO_FP)); + SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP)); + SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP)); func_decl * a_decl = to_app(a)->get_decl(); func_decl * b_decl = to_app(b)->get_decl(); From 610c549104770d4c9cecb1bc5b23d6c3ea424865 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jun 2015 18:17:49 +0100 Subject: [PATCH 43/48] fpa2bv_approx: added fp.abs, fixed rounding mode model extraction --- src/tactic/fpa/fpa2bv_approx_tactic.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/tactic/fpa/fpa2bv_approx_tactic.cpp b/src/tactic/fpa/fpa2bv_approx_tactic.cpp index 9d5873f12..bc0b5d39a 100644 --- a/src/tactic/fpa/fpa2bv_approx_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_approx_tactic.cpp @@ -272,8 +272,12 @@ class fpa2bv_approx_tactic: public tactic { expr_ref arg_e[] = { expr_ref(m), expr_ref(m), expr_ref(m), expr_ref(m) }; unsigned i=0; //Set rounding mode - if (rhs->get_num_args() > 0 && m_float_util.is_rm(rhs->get_arg(0))) + if (rhs->get_num_args() > 0 && m_float_util.is_rm(rhs->get_arg(0))) { + expr_ref rm_val(m); + mdl->eval(rhs->get_arg(0), rm_val, true); + m_float_util.is_rm_numeral(rm_val, rm); i = 1; + } //Collect argument values for (; i < rhs->get_num_args(); i++) { expr * arg = rhs->get_arg(i); @@ -372,6 +376,11 @@ class fpa2bv_approx_tactic: public tactic { mpf_mngr.set(est_rhs_value, ebits, sbits, rm, est_arg_val[1]); break; } + case OP_FPA_ABS: + { + mpf_mngr.abs(arg_val[0], rhs_value); + break; + } default: NOT_IMPLEMENTED_YET(); break; From a7b12e6321d7f511e0940a31ae1e08995980884d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jun 2015 18:31:09 +0100 Subject: [PATCH 44/48] Bugfix for fp.fma with sbits <= 3 --- src/ast/fpa/fpa2bv_converter.cpp | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 11c6f8bf6..ca6aa4858 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1403,9 +1403,19 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); - sticky_raw = m_bv_util.mk_extract(sbits-5, 0, sig_abs); - sticky = m_bv_util.mk_zero_extend(sbits+3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get())); + if (sbits > 5) { + sticky_raw = m_bv_util.mk_extract(sbits - 5, 0, sig_abs); + sticky = m_bv_util.mk_zero_extend(sbits + 3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get())); + expr * res_or_args[2] = { m_bv_util.mk_extract(2 * sbits - 1, sbits - 4, sig_abs), sticky }; + res_sig = m_bv_util.mk_bv_or(2, res_or_args); + } + else { + unsigned too_short = 6 - sbits; + sig_abs = m_bv_util.mk_concat(sig_abs, m_bv_util.mk_numeral(0, too_short)); + res_sig = m_bv_util.mk_extract(sbits + 3, 0, sig_abs); + } dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky); + SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4); expr * res_or_args[2] = { m_bv_util.mk_extract(2*sbits-1, sbits-4, sig_abs), sticky }; res_sig = m_bv_util.mk_bv_or(2, res_or_args); From 81218c098343a13a561a6c1ad54c4213cdea6253 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jun 2015 18:36:19 +0100 Subject: [PATCH 45/48] Bugfix for fp.fma --- src/ast/fpa/fpa2bv_converter.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index ca6aa4858..13f406aeb 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1417,10 +1417,6 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky); SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4); - expr * res_or_args[2] = { m_bv_util.mk_extract(2*sbits-1, sbits-4, sig_abs), sticky }; - res_sig = m_bv_util.mk_bv_or(2, res_or_args); - SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4); - expr_ref is_zero_sig(m), nil_sbits4(m); nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4); m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig); From d06207f072c4989cde037b40cdd420249451507a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2015 10:38:22 -0700 Subject: [PATCH 46/48] remove ite terms from objectives to synchronize values in tableau with objective value. Fixes part of (three repros) from issue #120 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 7 +++++-- src/opt/optsmt.cpp | 3 +++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index bf8a9dd7f..6fb4ef542 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -31,6 +31,7 @@ Notes: #include "propagate_values_tactic.h" #include "solve_eqs_tactic.h" #include "elim_uncnstr_tactic.h" +#include "elim_term_ite_tactic.h" #include "tactical.h" #include "model_smt2_pp.h" #include "card2bv_tactic.h" @@ -650,17 +651,19 @@ namespace opt { and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), mk_solve_eqs_tactic(m), + mk_elim_term_ite_tactic(m), // NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints mk_simplify_tactic(m)); opt_params optp(m_params); - tactic_ref tac2, tac3; + tactic_ref tac2, tac3, tac4; if (optp.elim_01()) { tac2 = mk_elim01_tactic(m); tac3 = mk_lia2card_tactic(m); + tac4 = mk_elim_term_ite_tactic(m); params_ref lia_p; lia_p.set_bool("compile_equality", optp.pb_compile_equality()); tac3->updt_params(lia_p); - set_simplify(and_then(tac0.get(), tac2.get(), tac3.get())); + set_simplify(and_then(tac0.get(), tac2.get(), tac3.get(), tac4.get())); } else { set_simplify(tac0.get()); diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 6b061f9cd..02effa337 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -141,6 +141,7 @@ namespace opt { ors.push_back(m_s->mk_ge(i, m_upper[i])); } + fml = m.mk_or(ors.size(), ors.c_ptr()); tmp = m.mk_fresh_const("b", m.mk_bool_sort()); fml = m.mk_implies(tmp, fml); @@ -150,6 +151,7 @@ namespace opt { solver::scoped_push _push(*m_s); while (!m_cancel) { m_s->assert_expr(fml); + TRACE("opt", tout << fml << "\n";); is_sat = m_s->check_sat(1,vars); if (is_sat == l_true) { disj.reset(); @@ -343,6 +345,7 @@ namespace opt { m_lower[i] = m_s->saved_objective_value(i); } } + TRACE("opt", tout << "strengthen bound: " << block << "\n";); m_s->assert_expr(block); // TBD: only works for simplex From c910ed2eae2588bd10092f4e878fb2a187d4121e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jun 2015 18:40:11 +0100 Subject: [PATCH 47/48] fpa2bv_approx: bugfix for fp.abs --- src/tactic/fpa/fpa2bv_approx_tactic.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tactic/fpa/fpa2bv_approx_tactic.cpp b/src/tactic/fpa/fpa2bv_approx_tactic.cpp index bc0b5d39a..02c5ab8bd 100644 --- a/src/tactic/fpa/fpa2bv_approx_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_approx_tactic.cpp @@ -379,6 +379,7 @@ class fpa2bv_approx_tactic: public tactic { case OP_FPA_ABS: { mpf_mngr.abs(arg_val[0], rhs_value); + mpf_mngr.abs(est_arg_val[0], est_rhs_value); break; } default: From c09ac5422ba5132b8739dfa44328db1527cd35cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2015 10:42:03 -0700 Subject: [PATCH 48/48] fix by anomaly detection, issue #118 Signed-off-by: Nikolaj Bjorner --- src/math/realclosure/realclosure.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 84ba606fd..1ca8823a1 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -4075,7 +4075,7 @@ namespace realclosure { void refine_rational_interval(rational_value * v, unsigned prec) { mpbqi & i = interval(v); - if (!i.lower_is_open() && !i.lower_is_open()) { + if (!i.lower_is_open() && !i.upper_is_open()) { SASSERT(bqm().eq(i.lower(), i.upper())); return; }