From d757c342d59edf29d0ba9af57adc4fa492f9e65e Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 7 Jan 2019 23:13:09 +0700 Subject: [PATCH 1/6] Define NO_Z3_DEBUGGER for emscripten builds. --- src/util/debug.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/util/debug.h b/src/util/debug.h index ea702e8a7..613328013 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -51,6 +51,10 @@ bool assertions_enabled(); #endif #endif +#ifdef __EMSCRIPTEN__ +#define NO_Z3_DEBUGGER +#endif + #ifdef NO_Z3_DEBUGGER #define INVOKE_DEBUGGER() exit(ERR_INTERNAL_FATAL) #else From 9c318ed304579b6101207cf52535fc2a1128a76c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Jan 2019 15:43:45 -0800 Subject: [PATCH 2/6] fix #2076, add option to handle .cnf files into dimacs parser Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 2 +- src/smt/theory_pb.cpp | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index a5ad7b525..8f92d5bb4 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -181,7 +181,7 @@ extern "C" { if (!is) { SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr); } - else if (ext && std::string("dimacs") == ext) { + else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) { ast_manager& m = to_solver_ref(s)->get_manager(); std::stringstream err; sat::solver solver(to_solver_ref(s)->get_params(), m.limit()); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 671184633..182324832 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1197,8 +1197,11 @@ namespace smt { literal_vector& lits = get_unhelpful_literals(c, true); lits.push_back(c.lit()); for (unsigned i = 0; i < sz; ++i) { - DEBUG_CODE(validate_assign(c, lits, c.lit(i));); - add_assign(c, lits, c.lit(i)); + literal lit = c.lit(i); + if (ctx.get_assignment(lit) == l_undef) { + DEBUG_CODE(validate_assign(c, lits, lit);); + add_assign(c, lits, c.lit(i)); + } } } } From efaab6d8fd9e2166b3497233c1bad7637e253c7b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Jan 2019 11:38:35 -0800 Subject: [PATCH 3/6] have sat cleaner use a fixed-point Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 31 +++---------- src/ast/datatype_decl_plugin.cpp | 74 +++++++++++++++++++++++++++++++- src/ast/datatype_decl_plugin.h | 57 +++--------------------- src/sat/sat_cleaner.cpp | 12 ++++-- 4 files changed, 94 insertions(+), 80 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 523d40842..65f634b6b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -482,6 +482,7 @@ def _to_ast_ref(a, ctx): else: return _to_expr_ref(a, ctx) + ######################################### # # Sorts @@ -6664,17 +6665,11 @@ class Solver(Z3PPObject): def from_file(self, filename): """Parse assertions from a file""" - try: - Z3_solver_from_file(self.ctx.ref(), self.solver, filename) - except Z3Exception as e: - _handle_parse_error(e, self.ctx) + Z3_solver_from_file(self.ctx.ref(), self.solver, filename) def from_string(self, s): """Parse assertions from a string""" - try: - Z3_solver_from_string(self.ctx.ref(), self.solver, s) - except Z3Exception as e: - _handle_parse_error(e, self.ctx) + Z3_solver_from_string(self.ctx.ref(), self.solver, s) def cube(self, vars = None): """Get set of cubes @@ -7063,17 +7058,11 @@ class Fixedpoint(Z3PPObject): def parse_string(self, s): """Parse rules and queries from a string""" - try: - return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx) - except Z3Exception as e: - _handle_parse_error(e, self.ctx) + return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx) def parse_file(self, f): """Parse rules and queries from a file""" - try: - return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx) - except Z3Exception as e: - _handle_parse_error(e, self.ctx) + return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx) def get_rules(self): """retrieve rules that have been added to fixedpoint context""" @@ -7410,17 +7399,11 @@ class Optimize(Z3PPObject): def from_file(self, filename): """Parse assertions and objectives from a file""" - try: - Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename) - except Z3Exception as e: - _handle_parse_error(e, self.ctx) + Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename) def from_string(self, s): """Parse assertions and objectives from a string""" - try: - Z3_optimize_from_string(self.ctx.ref(), self.optimize, s) - except Z3Exception as e: - _handle_parse_error(e, self.ctx) + Z3_optimize_from_string(self.ctx.ref(), self.optimize, s) def assertions(self): """Return an AST vector containing all added constraints.""" diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 0271d8311..a7f6fb07b 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -143,7 +143,77 @@ namespace datatype { } return r; } - size* size::mk_power(size* a1, size* a2) { return alloc(power, a1, a2); } + + size* size::mk_power(size* a1, size* a2) { + return alloc(power, a1, a2); + } + + + sort_size plus::eval(obj_map const& S) { + rational r(0); + ptr_vector todo; + todo.push_back(m_arg1); + todo.push_back(m_arg2); + while (!todo.empty()) { + size* s = todo.back(); + todo.pop_back(); + plus* p = dynamic_cast(s); + if (p) { + todo.push_back(p->m_arg1); + todo.push_back(p->m_arg2); + } + else { + sort_size sz = s->eval(S); + if (sz.is_infinite()) return sz; + if (sz.is_very_big()) return sz; + r += rational(sz.size(), rational::ui64()); + } + } + return sort_size(r); + } + + size* plus::subst(obj_map& S) { + return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); + } + + sort_size times::eval(obj_map const& S) { + sort_size s1 = m_arg1->eval(S); + sort_size s2 = m_arg2->eval(S); + if (s1.is_infinite()) return s1; + if (s2.is_infinite()) return s2; + if (s1.is_very_big()) return s1; + if (s2.is_very_big()) return s2; + rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64()); + return sort_size(r); + } + + size* times::subst(obj_map& S) { + return mk_times(m_arg1->subst(S), m_arg2->subst(S)); + } + + sort_size power::eval(obj_map const& S) { + sort_size s1 = m_arg1->eval(S); + sort_size s2 = m_arg2->eval(S); + // s1^s2 + if (s1.is_infinite()) return s1; + if (s2.is_infinite()) return s2; + if (s1.is_very_big()) return s1; + if (s2.is_very_big()) return s2; + if (s1.size() == 1) return s1; + if (s2.size() == 1) return s1; + if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big(); + rational r = ::power(rational(s1.size(), rational::ui64()), static_cast(s2.size())); + return sort_size(r); + } + + size* power::subst(obj_map& S) { + return mk_power(m_arg1->subst(S), m_arg2->subst(S)); + } + + size* sparam::subst(obj_map& S) { + return S[m_param]; + } + } namespace decl { @@ -667,7 +737,7 @@ namespace datatype { continue; } - ptr_vector s_add; + ptr_vector s_add; for (constructor const* c : d) { ptr_vector s_mul; for (accessor const* a : *c) { diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index fc98c97e7..16d1f74c0 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -132,71 +132,28 @@ namespace datatype { size* m_arg1, *m_arg2; plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();} ~plus() override { m_arg1->dec_ref(); m_arg2->dec_ref(); } - size* subst(obj_map& S) override { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); } - sort_size eval(obj_map const& S) override { - rational r(0); - ptr_vector todo; - todo.push_back(m_arg1); - todo.push_back(m_arg2); - while (!todo.empty()) { - size* s = todo.back(); - todo.pop_back(); - plus* p = dynamic_cast(s); - if (p) { - todo.push_back(p->m_arg1); - todo.push_back(p->m_arg2); - } - else { - sort_size sz = s->eval(S); - if (sz.is_infinite()) return sz; - if (sz.is_very_big()) return sz; - r += rational(sz.size(), rational::ui64()); - } - } - return sort_size(r); - } + size* subst(obj_map& S) override; + sort_size eval(obj_map const& S) override; }; struct times : public size { size* m_arg1, *m_arg2; times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); } ~times() override { m_arg1->dec_ref(); m_arg2->dec_ref(); } - size* subst(obj_map& S) override { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); } - sort_size eval(obj_map const& S) override { - sort_size s1 = m_arg1->eval(S); - sort_size s2 = m_arg2->eval(S); - if (s1.is_infinite()) return s1; - if (s2.is_infinite()) return s2; - if (s1.is_very_big()) return s1; - if (s2.is_very_big()) return s2; - rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64()); - return sort_size(r); - } + size* subst(obj_map& S) override; + sort_size eval(obj_map const& S) override; }; struct power : public size { size* m_arg1, *m_arg2; power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); } ~power() override { m_arg1->dec_ref(); m_arg2->dec_ref(); } - size* subst(obj_map& S) override { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); } - sort_size eval(obj_map const& S) override { - sort_size s1 = m_arg1->eval(S); - sort_size s2 = m_arg2->eval(S); - // s1^s2 - if (s1.is_infinite()) return s1; - if (s2.is_infinite()) return s2; - if (s1.is_very_big()) return s1; - if (s2.is_very_big()) return s2; - if (s1.size() == 1) return s1; - if (s2.size() == 1) return s1; - if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big(); - rational r = ::power(rational(s1.size(), rational::ui64()), static_cast(s2.size())); - return sort_size(r); - } + size* subst(obj_map& S) override; + sort_size eval(obj_map const& S) override; }; struct sparam : public size { sort_ref m_param; sparam(sort_ref& p): m_param(p) {} ~sparam() override {} - size* subst(obj_map& S) override { return S[m_param]; } + size* subst(obj_map& S) override; sort_size eval(obj_map const& S) override { return S[m_param]; } }; }; diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index c0c6fabe4..e13a117fd 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -192,10 +192,14 @@ namespace sat { report rpt(*this); m_last_num_units = trail_sz; m_cleanup_counter = 0; - cleanup_watches(); - cleanup_clauses(s.m_clauses); - cleanup_clauses(s.m_learned); - s.propagate(false); + do { + trail_sz = s.m_trail.size(); + cleanup_watches(); + cleanup_clauses(s.m_clauses); + cleanup_clauses(s.m_learned); + s.propagate(false); + } + while (trail_sz < s.m_trail.size()); CASSERT("cleaner_bug", s.check_invariant()); return true; } From 59b0b56b421af33ba02e9662a19c3d69ef4bf371 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Jan 2019 12:08:38 -0800 Subject: [PATCH 4/6] add checkpoints to blocked clause elimination to handle timeouts, #2080 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_simplifier.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 21d264af5..ca29a8501 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1527,6 +1527,7 @@ namespace sat { block_covered_binary(w, l, blocked, k); break; } + s.checkpoint(); } } @@ -1552,6 +1553,7 @@ namespace sat { s.set_learned(c); break; } + s.checkpoint(); } } From b12c1b1cbac974efb27298a7c9d0123ea2714082 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Jan 2019 13:38:45 -0800 Subject: [PATCH 5/6] set a throttle on ala Signed-off-by: Nikolaj Bjorner --- src/sat/sat_simplifier.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index ca29a8501..ca9b71a2d 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1272,7 +1272,8 @@ namespace sat { * unless C contains lit, and it is a tautology. */ bool add_ala() { - for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) { + unsigned init_size = m_covered_clause.size(); + for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size; ++m_ala_qhead) { literal l = m_covered_clause[m_ala_qhead]; for (watched & w : s.get_wlist(~l)) { if (w.is_binary_non_learned_clause()) { @@ -1282,7 +1283,6 @@ namespace sat { return true; } if (!s.is_marked(~lit)) { - // if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << l << " " << lit << "\n"); m_covered_clause.push_back(~lit); m_covered_antecedent.push_back(clause_ante(l, false)); s.mark_visited(~lit); @@ -1312,7 +1312,6 @@ namespace sat { if (lit1 == null_literal) { return true; } - // if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << c << " " << lit1 << "\n"); m_covered_clause.push_back(~lit1); m_covered_antecedent.push_back(clause_ante(c)); s.mark_visited(~lit1); From 6e60926cc38361f411b6a709a1c36c902aeb7ded Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Jan 2019 15:25:10 -0800 Subject: [PATCH 6/6] fix drat output for elim_eqs Signed-off-by: Nikolaj Bjorner --- src/sat/sat_elim_eqs.cpp | 77 +++++++++++++++++++++++++++------------- src/sat/sat_elim_eqs.h | 4 +++ src/sat/sat_solver.cpp | 4 +-- src/sat/sat_solver.h | 2 +- 4 files changed, 60 insertions(+), 27 deletions(-) diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index 870aa7fe2..8633f04d3 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -23,9 +23,15 @@ Revision History: namespace sat { elim_eqs::elim_eqs(solver & s): - m_solver(s) { + m_solver(s), + m_to_delete(nullptr) { } + elim_eqs::~elim_eqs() { + dealloc(m_to_delete); + } + + inline literal norm(literal_vector const & roots, literal l) { if (l.sign()) return ~roots[l.var()]; @@ -86,6 +92,12 @@ namespace sat { m_new_bin.reset(); } + void elim_eqs::drat_delete_clause() { + if (m_solver.m_config.m_drat) { + m_solver.m_drat.del(*m_to_delete->get()); + } + } + void elim_eqs::cleanup_clauses(literal_vector const & roots, clause_vector & cs) { clause_vector::iterator it = cs.begin(); clause_vector::iterator it2 = it; @@ -107,8 +119,16 @@ namespace sat { it2++; continue; } - if (!c.frozen()) + if (!c.frozen()) { m_solver.detach_clause(c); + } + + // save clause to be deleted for drat + if (m_solver.m_config.m_drat) { + if (!m_to_delete) m_to_delete = alloc(tmp_clause); + m_to_delete->set(sz, c.begin(), c.is_learned()); + } + // apply substitution for (i = 0; i < sz; i++) { literal lit = c[i]; @@ -124,60 +144,69 @@ namespace sat { CTRACE("sat", l != norm(roots, l), tout << l << " " << norm(roots, l) << "\n"; tout.flush();); SASSERT(l == norm(roots, l)); } }); + // remove duplicates, and check if it is a tautology - literal l_prev = null_literal; unsigned j = 0; + literal l_prev = null_literal; for (i = 0; i < sz; i++) { literal l = c[i]; - if (l == l_prev) - continue; - if (l == ~l_prev) + if (l == ~l_prev) { break; + } + if (l == l_prev) { + continue; + } + SASSERT(l != ~l_prev); l_prev = l; lbool val = m_solver.value(l); - if (val == l_true) - break; // clause was satisfied - if (val == l_false) + if (val == l_true) { + break; + } + if (val == l_false) { continue; // skip + } c[j] = l; j++; } + TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";); + if (i < sz) { - // clause is a tautology or was simplified to true - m_solver.del_clause(c); + drat_delete_clause(); + m_solver.del_clause(c, false); continue; } - if (j == 0) { - // empty clause + + switch (j) { + case 0: m_solver.set_conflict(justification()); for (; it != end; ++it) { *it2 = *it; it2++; } cs.set_end(it2); - return; - } - TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";); - - SASSERT(j >= 1); - switch (j) { + return; case 1: m_solver.assign(c[0], justification()); - m_solver.del_clause(c); + m_solver.del_clause(c, false); + drat_delete_clause(); break; case 2: m_solver.mk_bin_clause(c[0], c[1], c.is_learned()); - m_solver.del_clause(c); + m_solver.del_clause(c, false); + drat_delete_clause(); break; default: SASSERT(*it == &c); if (j < sz) { - if (m_solver.m_config.m_drat) m_solver.m_drat.del(c); c.shrink(j); - if (m_solver.m_config.m_drat) m_solver.m_drat.add(c, true); } - else + else { c.update_approx(); + } + if (m_solver.m_config.m_drat) { + m_solver.m_drat.add(c, true); + drat_delete_clause(); + } DEBUG_CODE(for (literal l : c) VERIFY(l == norm(roots, l));); diff --git a/src/sat/sat_elim_eqs.h b/src/sat/sat_elim_eqs.h index 143fcbb3f..ac132b213 100644 --- a/src/sat/sat_elim_eqs.h +++ b/src/sat/sat_elim_eqs.h @@ -23,6 +23,7 @@ Revision History: namespace sat { class solver; + class tmp_clause; class elim_eqs { struct bin { @@ -32,6 +33,8 @@ namespace sat { }; svector m_new_bin; solver & m_solver; + tmp_clause* m_to_delete; + void drat_delete_clause(); void save_elim(literal_vector const & roots, bool_var_vector const & to_elim); void cleanup_clauses(literal_vector const & roots, clause_vector & cs); void cleanup_bin_watches(literal_vector const & roots); @@ -39,6 +42,7 @@ namespace sat { bool check_clause(clause const& c, literal_vector const& roots) const; public: elim_eqs(solver & s); + ~elim_eqs(); void operator()(literal_vector const & roots, bool_var_vector const & to_elim); }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index fc5fce252..6731adc92 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -298,14 +298,14 @@ namespace sat { mk_clause(3, ls, learned); } - void solver::del_clause(clause& c) { + void solver::del_clause(clause& c, bool enable_drat) { if (!c.is_learned()) { m_stats.m_non_learned_generation++; } if (c.frozen()) { --m_num_frozen; } - if (m_config.m_drat && !m_drat.is_cleaned(c)) { + if (enable_drat && m_config.m_drat && !m_drat.is_cleaned(c)) { m_drat.del(c); } dealloc_clause(&c); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 8402fc898..3937c67e8 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -232,7 +232,7 @@ namespace sat { void defrag_clauses(); bool should_defrag(); bool memory_pressure(); - void del_clause(clause & c); + void del_clause(clause & c, bool enable_drat = true); clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned); clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.c_ptr()); } clause * mk_clause_core(unsigned num_lits, literal * lits) { return mk_clause_core(num_lits, lits, false); }