mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt

Browse source
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-11-21 13:23:40 -08:00
parent 37c39f4073 c6cb739b44
commit d2f52ca359
2 changed files with 14 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/sat/sat_probing.cpp
View file

@ -19,6 +19,7 @@ Revision History:
--*/ --*/
#include "sat/sat_probing.h" #include "sat/sat_probing.h"
#include "sat/sat_solver.h" #include "sat/sat_solver.h"
#include "sat/sat_simplifier_params.hpp"
namespace sat { namespace sat {
probing::probing(solver & _s, params_ref const & p): probing::probing(solver & _s, params_ref const & p):
@ -238,12 +239,13 @@ namespace sat {
return r; return r;
} }
void probing::updt_params(params_ref const & p) { void probing::updt_params(params_ref const & _p) {
m_probing = p.get_bool("probing", true); sat_simplifier_params p(_p);
m_probing_limit = p.get_uint("probing_limit", 5000000); m_probing = p.probing();
m_probing_cache = p.get_bool("probing_cache", true); m_probing_limit = p.probing_limit();
m_probing_binary = p.get_bool("probing_binary", true); m_probing_cache = p.probing_cache();
m_probing_cache_limit = megabytes_to_bytes(p.get_uint("probing_chache_limit", 1024)); m_probing_binary = p.probing_binary();
m_probing_cache_limit = p.probing_cache_limit();
} }
void probing::collect_param_descrs(param_descrs & d) { void probing::collect_param_descrs(param_descrs & d) {

7
src/sat/sat_simplifier_params.pyg
View file

@ -23,6 +23,11 @@ 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'), ('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', 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', 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'),
('probing', BOOL, True, 'apply failed literal detection during simplification'),
('probing_limit', UINT, 5000000, 'limit to the number of probe calls'),
('probing_cache', BOOL, True, 'add binary literals as lemmas'),
('probing_cache_limit', UINT, 1024, 'cache binaries unless overall memory usage exceeds cache limit'),
('probing_binary', BOOL, True, 'probe binary clauses'),
('subsumption', BOOL, True, 'eliminate subsumed clauses'), ('subsumption', BOOL, True, 'eliminate subsumed clauses'),
('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)'))) ('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))