mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Fixed infinite loop bugs in blocked clause retention. Added option to

Browse source 
disable incremental sat solver
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-10-24 13:51:27 -07:00
parent 63545c1e7b
commit 80041d7131
3 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_params.pyg
View file

@ -32,6 +32,7 @@ def_module_params('sat',
('cardinality.solver', BOOL, False, 'use cardinality solver'), ('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)'), ('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'), ('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'), ('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_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('local_search', BOOL, False, 'use local search instead of CDCL'), ('local_search', BOOL, False, 'use local search instead of CDCL'),

6
src/sat/sat_simplifier.cpp
View file

@ -1044,6 +1044,7 @@ namespace sat {
clause_use_list::iterator it = occs.mk_iterator(); clause_use_list::iterator it = occs.mk_iterator();
while (!it.at_end()) { while (!it.at_end()) {
clause & c = it.curr(); clause & c = it.curr();
it.next();
if (c.is_blocked()) continue; if (c.is_blocked()) continue;
m_counter -= c.size(); m_counter -= c.size();
SASSERT(c.contains(l)); SASSERT(c.contains(l));
@ -1053,7 +1054,6 @@ namespace sat {
s.m_num_blocked_clauses++; s.m_num_blocked_clauses++;
} }
s.unmark_all(c); s.unmark_all(c);
it.next();
} }
for (clause* c : m_to_remove) for (clause* c : m_to_remove)
s.block_clause(*c); s.block_clause(*c);
@ -1086,6 +1086,7 @@ namespace sat {
while (!it.at_end()) { while (!it.at_end()) {
bool tautology = false; bool tautology = false;
clause & c = it.curr(); clause & c = it.curr();
it.next();
if (c.is_blocked()) continue; if (c.is_blocked()) continue;
for (literal lit : c) { for (literal lit : c) {
if (s.is_marked(~lit) && lit != ~l) { if (s.is_marked(~lit) && lit != ~l) {
@ -1110,7 +1111,6 @@ namespace sat {
if (j == 0) return false; if (j == 0) return false;
} }
} }
it.next();
} }
return first; return first;
} }
@ -1360,6 +1360,7 @@ namespace sat {
clause_use_list::iterator it = neg_occs.mk_iterator(); clause_use_list::iterator it = neg_occs.mk_iterator();
while (!it.at_end()) { while (!it.at_end()) {
clause & c = it.curr(); clause & c = it.curr();
it.next();
if (c.is_blocked()) continue; if (c.is_blocked()) continue;
m_counter -= c.size(); m_counter -= c.size();
unsigned sz = c.size(); unsigned sz = c.size();
@ -1370,7 +1371,6 @@ namespace sat {
} }
if (i == sz) if (i == sz)
return false; return false;
it.next();
} }
if (s.s.m_ext) { if (s.s.m_ext) {

10
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -29,6 +29,7 @@ Notes:
#include "tactic/bv/bit_blaster_tactic.h" #include "tactic/bv/bit_blaster_tactic.h"
#include "tactic/core/simplify_tactic.h" #include "tactic/core/simplify_tactic.h"
#include "sat/tactic/goal2sat.h" #include "sat/tactic/goal2sat.h"
#include "sat/tactic/sat_tactic.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "model/model_smt2_pp.h" #include "model/model_smt2_pp.h"
#include "tactic/filter_model_converter.h" #include "tactic/filter_model_converter.h"
@ -848,8 +849,13 @@ private:
}; };
solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p) { solver* mk_inc_sat_solver(ast_manager& m, params_ref const& _p) {
return alloc(inc_sat_solver, m, 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);
} }