From 63545c1e7b668220796c02c22da93fd67a3ef83b Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Mon, 23 Oct 2017 12:51:19 -0700 Subject: [PATCH 1/6] Fixes --- src/sat/sat_simplifier.cpp | 12 +++++------- src/sat/sat_simplifier_params.pyg | 2 +- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 3ccd183c2..a5f66dfd9 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -974,9 +974,9 @@ namespace sat { void operator()() { if (s.bce_enabled()) block_clauses(); - if (s.m_cce) + if (s.cce_enabled()) cce(); - if (s.m_bca) + if (s.bca_enabled()) bca(); } @@ -1176,7 +1176,7 @@ namespace sat { is_tautology = add_cla(blocked); } while (m_covered_clause.size() > sz && !is_tautology); - if (s.m_acce && !is_tautology) { + if (s.acce_enabled() && !is_tautology) { sz = m_covered_clause.size(); add_ala(); } @@ -1338,11 +1338,9 @@ namespace sat { } if (!found) { IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";); - watched w(l2, false); - w.set_blocked(); + watched w(l2, true); s.get_wlist(~l).push_back(w); - w = watched(l, false); - w.set_blocked(); + w = watched(l, true); s.get_wlist(~l2).push_back(w); ++s.m_num_bca; } diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg index 6528e6699..07088a60b 100644 --- a/src/sat/sat_simplifier_params.pyg +++ b/src/sat/sat_simplifier_params.pyg @@ -20,6 +20,6 @@ def_module_params(module_name='sat', ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'), ('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'), ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'), - ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'), + ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'), ('subsumption', BOOL, True, 'eliminate subsumed clauses'), ('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)'))) From 80041d7131cb61843cebe4045c2314a7e7eef55f Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Tue, 24 Oct 2017 13:51:27 -0700 Subject: [PATCH 2/6] Fixed infinite loop bugs in blocked clause retention. Added option to disable incremental sat solver --- src/sat/sat_params.pyg | 1 + src/sat/sat_simplifier.cpp | 6 +++--- src/sat/sat_solver/inc_sat_solver.cpp | 10 ++++++++-- 3 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index d803617f5..ada6f910b 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -32,6 +32,7 @@ def_module_params('sat', ('cardinality.solver', BOOL, False, 'use cardinality solver'), ('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'), ('xor.solver', BOOL, False, 'use xor solver'), + ('disable_incremental', BOOL, False, 'disable incremental solving. Allows stronger simplification, but solver cannot be re-used.'), ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('local_search', BOOL, False, 'use local search instead of CDCL'), diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index a5f66dfd9..9042587b7 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1044,6 +1044,7 @@ namespace sat { clause_use_list::iterator it = occs.mk_iterator(); while (!it.at_end()) { clause & c = it.curr(); + it.next(); if (c.is_blocked()) continue; m_counter -= c.size(); SASSERT(c.contains(l)); @@ -1053,7 +1054,6 @@ namespace sat { s.m_num_blocked_clauses++; } s.unmark_all(c); - it.next(); } for (clause* c : m_to_remove) s.block_clause(*c); @@ -1086,6 +1086,7 @@ namespace sat { while (!it.at_end()) { bool tautology = false; clause & c = it.curr(); + it.next(); if (c.is_blocked()) continue; for (literal lit : c) { if (s.is_marked(~lit) && lit != ~l) { @@ -1110,7 +1111,6 @@ namespace sat { if (j == 0) return false; } } - it.next(); } return first; } @@ -1360,6 +1360,7 @@ namespace sat { clause_use_list::iterator it = neg_occs.mk_iterator(); while (!it.at_end()) { clause & c = it.curr(); + it.next(); if (c.is_blocked()) continue; m_counter -= c.size(); unsigned sz = c.size(); @@ -1370,7 +1371,6 @@ namespace sat { } if (i == sz) return false; - it.next(); } if (s.s.m_ext) { diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 53383a7c2..099dc701b 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -29,6 +29,7 @@ Notes: #include "tactic/bv/bit_blaster_tactic.h" #include "tactic/core/simplify_tactic.h" #include "sat/tactic/goal2sat.h" +#include "sat/tactic/sat_tactic.h" #include "ast/ast_pp.h" #include "model/model_smt2_pp.h" #include "tactic/filter_model_converter.h" @@ -848,8 +849,13 @@ private: }; -solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p) { - return alloc(inc_sat_solver, m, p); +solver* mk_inc_sat_solver(ast_manager& m, params_ref const& _p) { + sat_params p(_p); + if (p.disable_incremental()) { + tactic_ref t = mk_sat_tactic(m, _p); + return mk_tactic2solver(m, t.get(), _p); + } + return alloc(inc_sat_solver, m, _p); } From 8915d0a21f60a46ad82092e5a9689cf15ab88460 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Tue, 24 Oct 2017 14:08:44 -0700 Subject: [PATCH 3/6] Tidy --- src/sat/sat_simplifier.cpp | 83 ++++++++++++++++++++------------------ 1 file changed, 43 insertions(+), 40 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 9042587b7..11ad8a85c 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1044,16 +1044,17 @@ namespace sat { clause_use_list::iterator it = occs.mk_iterator(); while (!it.at_end()) { clause & c = it.curr(); - it.next(); - if (c.is_blocked()) continue; - m_counter -= c.size(); - SASSERT(c.contains(l)); - s.mark_all_but(c, l); - if (all_tautology(l)) { - block_clause(c, l, new_entry); - s.m_num_blocked_clauses++; + if (!c.is_blocked()) { + m_counter -= c.size(); + SASSERT(c.contains(l)); + s.mark_all_but(c, l); + if (all_tautology(l)) { + block_clause(c, l, new_entry); + s.m_num_blocked_clauses++; + } + s.unmark_all(c); } - s.unmark_all(c); + it.next(); } for (clause* c : m_to_remove) s.block_clause(*c); @@ -1086,31 +1087,32 @@ namespace sat { while (!it.at_end()) { bool tautology = false; clause & c = it.curr(); - it.next(); - if (c.is_blocked()) continue; - for (literal lit : c) { - if (s.is_marked(~lit) && lit != ~l) { - tautology = true; - break; - } - } - if (!tautology) { - if (first) { - for (literal lit : c) { - if (lit != ~l && !s.is_marked(lit)) inter.push_back(lit); + if (!c.is_blocked()) { + for (literal lit : c) { + if (s.is_marked(~lit) && lit != ~l) { + tautology = true; + break; } - first = false; - if (inter.empty()) return false; } - else { - unsigned j = 0; - for (literal lit : inter) - if (c.contains(lit)) - inter[j++] = lit; - inter.shrink(j); - if (j == 0) return false; + if (!tautology) { + if (first) { + for (literal lit : c) { + if (lit != ~l && !s.is_marked(lit)) inter.push_back(lit); + } + first = false; + if (inter.empty()) return false; + } + else { + unsigned j = 0; + for (literal lit : inter) + if (c.contains(lit)) + inter[j++] = lit; + inter.shrink(j); + if (j == 0) return false; + } } } + it.next(); } return first; } @@ -1360,17 +1362,18 @@ namespace sat { clause_use_list::iterator it = neg_occs.mk_iterator(); while (!it.at_end()) { clause & c = it.curr(); - it.next(); - if (c.is_blocked()) continue; - m_counter -= c.size(); - unsigned sz = c.size(); - unsigned i; - for (i = 0; i < sz; i++) { - if (s.is_marked(~c[i])) - break; + if (!c.is_blocked()) { + m_counter -= c.size(); + unsigned sz = c.size(); + unsigned i; + for (i = 0; i < sz; i++) { + if (s.is_marked(~c[i])) + break; + } + if (i == sz) + return false; } - if (i == sz) - return false; + it.next(); } if (s.s.m_ext) { From 4d9492176e8905a0ed06b5d82d29130623f7b6be Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Tue, 24 Oct 2017 15:19:45 -0700 Subject: [PATCH 4/6] Removed incremental disabling --- src/sat/sat_params.pyg | 1 - src/sat/sat_solver/inc_sat_solver.cpp | 5 ----- 2 files changed, 6 deletions(-) diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index ada6f910b..d803617f5 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -32,7 +32,6 @@ def_module_params('sat', ('cardinality.solver', BOOL, False, 'use cardinality solver'), ('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'), ('xor.solver', BOOL, False, 'use xor solver'), - ('disable_incremental', BOOL, False, 'disable incremental solving. Allows stronger simplification, but solver cannot be re-used.'), ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('local_search', BOOL, False, 'use local search instead of CDCL'), diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 099dc701b..15c1cb240 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -850,11 +850,6 @@ private: solver* mk_inc_sat_solver(ast_manager& m, params_ref const& _p) { - sat_params p(_p); - if (p.disable_incremental()) { - tactic_ref t = mk_sat_tactic(m, _p); - return mk_tactic2solver(m, t.get(), _p); - } return alloc(inc_sat_solver, m, _p); } From 3a05313c6795b831f27f88c6a925af0773e7a258 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Fri, 27 Oct 2017 12:36:09 -0700 Subject: [PATCH 5/6] Python API context fix --- src/api/python/z3/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 4379e3fe1..ab6249ff6 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6315,11 +6315,11 @@ class Solver(Z3PPObject): def from_file(self, filename): """Parse assertions from a file""" - self.add([f for f in parse_smt2_file(filename)]) + self.add([f for f in parse_smt2_file(filename, ctx=self.ctx)]) def from_string(self, s): """Parse assertions from a string""" - self.add([f for f in parse_smt2_string(s)]) + self.add([f for f in parse_smt2_string(s, ctx=self.ctx)]) def assertions(self): """Return an AST vector containing all added constraints. From f1bad9160979ed010a585f784b57d6abc8857ae3 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Fri, 27 Oct 2017 12:39:36 -0700 Subject: [PATCH 6/6] Clean-up --- src/sat/sat_solver/inc_sat_solver.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index dcfec489d..742f9e103 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -29,7 +29,6 @@ Notes: #include "tactic/bv/bit_blaster_tactic.h" #include "tactic/core/simplify_tactic.h" #include "sat/tactic/goal2sat.h" -#include "sat/tactic/sat_tactic.h" #include "ast/ast_pp.h" #include "model/model_smt2_pp.h" #include "tactic/filter_model_converter.h"