mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Removed incremental disabling

Browse source
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-10-24 15:19:45 -07:00
parent 69c253e8e6
commit 4d9492176e
2 changed files with 0 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_params.pyg
View file

@ -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'),

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

@ -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);
}