mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

parameters

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-28 18:21:04 -07:00
parent e4f57a13ba
commit fcdf220559
2 changed files with 21 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/sat/sat_params.pyg
View file

@ -62,7 +62,6 @@ def_module_params('sat',
('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'), ('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'),
('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'), ('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, False, 'enable euf solver (this feature is preliminary and not ready for general consumption)'),
('enable_xor', BOOL, False, 'enable xor solver plugin in combination with pure SAT solving'),
('ddfw_search', BOOL, False, 'use ddfw local search instead of CDCL'), ('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.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'), ('ddfw.use_reward_pct', UINT, 15, 'percentage to pick highest reward variable when it has reward 0'),
@ -112,7 +111,7 @@ def_module_params('sat',
('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'),
('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
('lookahead.delta_fraction', DOUBLE, 1.0, 'number between 0 and 1, the smaller the more literals are selected for double lookahead'), ('lookahead.delta_fraction', DOUBLE, 1.0, 'number between 0 and 1, the smaller the more literals are selected for double lookahead'),
('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')) ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'),
# reward function used to determine which literal to cube on. # reward function used to determine which literal to cube on.
# - ternary: reward function useful for random 3-SAT instances. Used by Heule and Knuth in March. # - ternary: reward function useful for random 3-SAT instances. Used by Heule and Knuth in March.
# - heule_schur: reward function based on "Schur Number 5", Heule, AAAI 2018 # - heule_schur: reward function based on "Schur Number 5", Heule, AAAI 2018
@ -126,5 +125,23 @@ def_module_params('sat',
# - march_cu: default reward function used in a version of March # - march_cu: default reward function used in a version of March
# Each reward function also comes with its own variant of "mix_diff", which # Each reward function also comes with its own variant of "mix_diff", which
# is the function for combining reward metrics for the positive and negative variant of a literal. # is the function for combining reward metrics for the positive and negative variant of a literal.
) # Xor parameters
('xor.enable', BOOL, False, 'enable xor solver plugin in combination with pure SAT solving'))
# Pull in other xor parameters as they are determined to be relevant
# ('xor.max_to_find', UINT, 'tbd'),
# ('xor.max_to_find_slow', UINT, 'tbd'),
# ('xor.max_xor_matrix, UINT64, 'tbd'),
# ('xor.allow_elim_vars', BOOL, 'tbd'),
# ('xor.var_per_cut', UINT, 'tbd'),
# ('xor.force_preserve_xors', BOOL, 'tbd'),
# ('xor.gauss.max_matrix_columns', UINT, 'tbd'),
# ('xor.gauss.max_matrix_rows', UINT, 'The maximum matrix size -- no. of rows'),
# ('xor.gauss.min_matrix_rows', UINT, 'The minimum matrix size -- no. of rows'),
# ('xor.gauss.max_num_matrices', UINT, 'Maximum number of matrices'),
# ('xor.gauss.autodisable', BOOL, False, 'tbd'),
# ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0, 'tbd'),
# ('xor.gauss.do_matrix_find', BOOL, True, 'tbd'),
# ('xor.gauss.min_xor_clauses', UINT, 2, 'tbd'),
# ('xor.gauss.max_xor_clauses, UINT, 500000, 'tbd')
)

2
src/sat/tactic/goal2sat.cpp
View file

@ -102,7 +102,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_ite_extra = p.get_bool("ite_extra", true); m_ite_extra = p.get_bool("ite_extra", true);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_euf = sp.euf(); m_euf = sp.euf();
m_xor = sp.enable_xor(); m_xor = sp.xor_enable();
} }
void throw_op_not_handled(std::string const& s) { void throw_op_not_handled(std::string const& s) {