mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

update documentation for renamed parameter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-06 21:25:38 -07:00
parent 3ae0ea8246
commit e4ae80b3f2
2 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/qe/qe_arith_plugin.cpp
View file

@ -1301,6 +1301,7 @@ namespace qe {
ptr_vector<expr> todo; ptr_vector<expr> todo;
todo.push_back(a); todo.push_back(a);
rational k1, k2; rational k1, k2;
expr* e1 = nullptr, *e2 = nullptr;
expr_ref rest(m); expr_ref rest(m);
while (!todo.empty()) { while (!todo.empty()) {
expr* e = todo.back(); expr* e = todo.back();
@ -1319,9 +1320,9 @@ namespace qe {
return false; return false;
} }
a = to_app(e); a = to_app(e);
if (m_util.m_arith.is_mod(e) && if (m_util.m_arith.is_mod(e, e1, e2) &&
m_util.m_arith.is_numeral(to_app(e)->get_arg(1), k1) && m_util.m_arith.is_numeral(e2, k1) &&
m_util.get_coeff(contains_x, to_app(e)->get_arg(0), k2, rest)) { m_util.get_coeff(contains_x, e1, k2, rest)) {
app_ref z(m), z_bv(m); app_ref z(m), z_bv(m);
m_util.mk_bounded_var(k1, z_bv, z); m_util.mk_bounded_var(k1, z_bv, z);
m_nested_div_terms.push_back(rest); m_nested_div_terms.push_back(rest);
@ -1331,9 +1332,8 @@ namespace qe {
m_nested_div_z.push_back(z); m_nested_div_z.push_back(z);
continue; continue;
} }
unsigned num_args = a->get_num_args(); for (expr* arg : *a) {
for (unsigned i = 0; i < num_args; ++i) { todo.push_back(arg);
todo.push_back(a->get_arg(i));
} }
} }
return true; return true;

2
src/sat/sat_params.pyg
View file

@ -43,7 +43,7 @@ def_module_params('sat',
('cardinality.solver', BOOL, True, 'use cardinality solver'), ('cardinality.solver', BOOL, True, 'use cardinality solver'),
('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use native solver)'), ('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use native solver)'),
('xor.solver', BOOL, False, 'use xor solver'), ('xor.solver', BOOL, False, 'use xor solver'),
('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered, unate, circuit'), ('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'),
('local_search', BOOL, False, 'use local search instead of CDCL'), ('local_search', BOOL, False, 'use local search instead of CDCL'),
('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'), ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),