mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

fix offset bug in explain

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-12 10:04:43 -08:00
parent 70d2057557
commit abc0cf3775
5 changed files with 8 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/euf/euf_bv_plugin.cpp
View file

@ -521,7 +521,7 @@ namespace euf {
just.push_back({ n, sib, j });
for (unsigned j = sib->num_args(); j-- > 0; ) {
auto arg = sib->get_arg(j);
m_jtodo.push_back({ arg, offset + delta, j2 });
m_jtodo.push_back({ arg, offs + delta, j2 });
delta += width(arg);
}
}
@ -531,10 +531,11 @@ namespace euf {
SASSERT(g.find(e)->get_root() == n->get_root());
unsigned j2 = just.size();
just.push_back({ g.find(e), n, j});
m_jtodo.push_back({ p, offset + lo, j2});
m_jtodo.push_back({ p, offs + lo, j2});
}
}
}
UNREACHABLE();
}

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'),
('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')))

4
src/opt/opt_params.pyg
View file

@ -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'),

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

@ -105,7 +105,7 @@ def_module_params(module_name='smt',
('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'),

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.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'),
))