mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

update defaults to make it easier to test polysat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-13 19:46:45 +02:00
parent 2d8b7b5ac6
commit 7036dd826f
3 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_params.pyg
View file

@ -59,7 +59,7 @@ def_module_params('sat',
('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'),
('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'),
('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'),
('euf', BOOL, False, 'enable euf solver (this feature is preliminary and not ready for general consumption)'),
('euf', BOOL, True, 'enable euf solver (this feature is preliminary and not ready for general consumption)'),
('ddfw_search', BOOL, False, 'use ddfw local search instead of CDCL'),
('ddfw.init_clause_weight', UINT, 8, 'initial clause weight for DDFW local search'),
('ddfw.use_reward_pct', UINT, 15, 'percentage to pick highest reward variable when it has reward 0'),

2
src/smt/params/smt_params_helper.pyg
View file

@ -49,7 +49,7 @@ def_module_params(module_name='smt',
('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'),
('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'),
('bv.polysat', BOOL, False, 'use polysat bit-vector solver'),
('bv.polysat', BOOL, True, 'use polysat bit-vector solver'),
('bv.eq_axioms', BOOL, True, 'enable redundant equality axioms for bit-vectors'),
('bv.size_reduce', BOOL, False, 'turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),

2
src/tactic/tactic_params.pyg
View file

@ -9,7 +9,7 @@ def_module_params('tactic',
('blast_term_ite.max_inflation', UINT, UINT_MAX, "multiplicative factor of initial term size."),
('blast_term_ite.max_steps', UINT, UINT_MAX, "maximal number of steps allowed for tactic."),
('propagate_values.max_rounds', UINT, 4, "maximal number of rounds to propagate values."),
('default_tactic', SYMBOL, '', "overwrite default tactic in strategic solver"),
('default_tactic', SYMBOL, 'smt', "overwrite default tactic in strategic solver"),
# ('aig.per_assertion', BOOL, True, "process one assertion at a time"),
# ('add_bounds.lower, INT, -2, "lower bound to be added to unbounded variables."),