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

expose probing configuration parameters

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-20 12:09:37 -08:00
parent dc0b2a8acf
commit 92cd92e690
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)')))