mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

spell check from https://github.com/microsoft/z3guide/pull/165

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-12 09:57:41 -08:00
parent 27171591d1
commit 3381fd2b52
4 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/polynomial/algebraic_params.pyg
View file

@ -5,6 +5,6 @@ def_module_params('algebraic',
('min_mag', UINT, 16, 'Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16'), ('min_mag', UINT, 16, 'Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16'),
('factor', BOOL, True, 'use polynomial factorization to simplify polynomials representing algebraic numbers'), ('factor', BOOL, True, 'use polynomial factorization to simplify polynomials representing algebraic numbers'),
('factor_max_prime', UINT, 31, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step'), ('factor_max_prime', UINT, 31, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step'),
('factor_num_primes', UINT, 1, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)\'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching'), ('factor_num_primes', UINT, 1, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)\'s. This parameter specify the maximum number of finite factorizations to be considered, before lifting and searching'),
('factor_search_size', UINT, 5000, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space'))) ('factor_search_size', UINT, 5000, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space')))

4
src/opt/opt_params.pyg
View file

@ -3,7 +3,7 @@ def_module_params('opt',
export=True, export=True,
params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'symba'"), params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'symba'"),
('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'rc2'"), ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'rc2'"),
('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box'"), ('priority', SYMBOL, 'lex', "select how to prioritize objectives: 'lex' (lexicographic), 'pareto', 'box'"),
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('dump_models', BOOL, False, 'display intermediary models to stdout'), ('dump_models', BOOL, False, 'display intermediary models to stdout'),
('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"), ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"),
@ -22,7 +22,7 @@ def_module_params('opt',
('maxlex.enable', BOOL, True, 'enable maxlex heuristic for lexicographic MaxSAT problems'), ('maxlex.enable', BOOL, True, 'enable maxlex heuristic for lexicographic MaxSAT problems'),
('rc2.totalizer', BOOL, True, 'use totalizer for rc2 encoding'), ('rc2.totalizer', BOOL, True, 'use totalizer for rc2 encoding'),
('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'), ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'), ('maxres.add_upper_bound_block', BOOL, False, 'restrict upper bound with constraint'),
('maxres.max_num_cores', UINT, 200, 'maximal number of cores per round'), ('maxres.max_num_cores', UINT, 200, 'maximal number of cores per round'),
('maxres.max_core_size', UINT, 3, 'break batch of generated cores if size reaches this number'), ('maxres.max_core_size', UINT, 3, 'break batch of generated cores if size reaches this number'),
('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'), ('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'),

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

@ -99,14 +99,13 @@ def_module_params(module_name='smt',
('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'), ('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'),
('arith.bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'), ('arith.bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'),
('arith.print_ext_var_names', BOOL, False, 'print external variable names'), ('arith.print_ext_var_names', BOOL, False, 'print external variable names'),
('arith.validate', BOOL, False, 'validate lemmas generated by arithmetic solver'),
('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'), ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'), ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
('array.weak', BOOL, False, 'weak array theory'), ('array.weak', BOOL, False, 'weak array theory'),
('array.extensional', BOOL, True, 'extensional array theory'), ('array.extensional', BOOL, True, 'extensional array theory'),
('clause_proof', BOOL, False, 'record a clausal proof'), ('clause_proof', BOOL, False, 'record a clausal proof'),
('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'), ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'), ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transitivity of equalities'),
('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'), ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'),
('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),

2
src/solver/parallel_params.pyg
View file

@ -10,7 +10,7 @@ def_module_params('parallel',
('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'), ('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'),
('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'), ('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'),
('simplify.exp', DOUBLE, 1, 'restart and inprocess max is multiplied by simplify.exp ^ depth'), ('simplify.exp', DOUBLE, 1, 'restart and inprocess max is multiplied by simplify.exp ^ depth'),
('simplify.max_conflicts', UINT, UINT_MAX, 'maximal number of conflicts during simplifcation phase'), ('simplify.max_conflicts', UINT, UINT_MAX, 'maximal number of conflicts during simplification phase'),
('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'), ('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'),
('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), ('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'),
)) ))