diff --git a/src/math/polynomial/algebraic_params.pyg b/src/math/polynomial/algebraic_params.pyg index 773548494..0e53a40b8 100644 --- a/src/math/polynomial/algebraic_params.pyg +++ b/src/math/polynomial/algebraic_params.pyg @@ -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'), ('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_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'))) diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 893b4bfd6..15f5e5d05 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,7 +3,7 @@ def_module_params('opt', export=True, 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'"), - ('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_models', BOOL, False, 'display intermediary models to stdout'), ('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'), ('rc2.totalizer', BOOL, True, 'use totalizer for rc2 encoding'), ('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_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'), diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 6ec362449..f2e08aaf5 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -99,14 +99,13 @@ def_module_params(module_name='smt', ('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.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.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'), ('array.weak', BOOL, False, 'weak array theory'), ('array.extensional', BOOL, True, 'extensional array theory'), ('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.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.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), diff --git a/src/solver/parallel_params.pyg b/src/solver/parallel_params.pyg index 628d4242a..60a77d49a 100644 --- a/src/solver/parallel_params.pyg +++ b/src/solver/parallel_params.pyg @@ -10,7 +10,7 @@ def_module_params('parallel', ('conquer.delay', UINT, 10, 'delay of cubes until applying 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.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.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), ))