From e4ae80b3f23ad35b6fffb71ded2319764b4cd60c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Jul 2018 21:25:38 -0700 Subject: [PATCH] update documentation for renamed parameter Signed-off-by: Nikolaj Bjorner --- src/qe/qe_arith_plugin.cpp | 14 +++++++------- src/sat/sat_params.pyg | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 21e50182f..f8c519285 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -1301,6 +1301,7 @@ namespace qe { ptr_vector todo; todo.push_back(a); rational k1, k2; + expr* e1 = nullptr, *e2 = nullptr; expr_ref rest(m); while (!todo.empty()) { expr* e = todo.back(); @@ -1319,9 +1320,9 @@ namespace qe { return false; } a = to_app(e); - if (m_util.m_arith.is_mod(e) && - m_util.m_arith.is_numeral(to_app(e)->get_arg(1), k1) && - m_util.get_coeff(contains_x, to_app(e)->get_arg(0), k2, rest)) { + if (m_util.m_arith.is_mod(e, e1, e2) && + m_util.m_arith.is_numeral(e2, k1) && + m_util.get_coeff(contains_x, e1, k2, rest)) { app_ref z(m), z_bv(m); m_util.mk_bounded_var(k1, z_bv, z); m_nested_div_terms.push_back(rest); @@ -1331,10 +1332,9 @@ namespace qe { m_nested_div_z.push_back(z); continue; } - unsigned num_args = a->get_num_args(); - for (unsigned i = 0; i < num_args; ++i) { - todo.push_back(a->get_arg(i)); - } + for (expr* arg : *a) { + todo.push_back(arg); + } } return true; } diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 714bf0e24..89776c479 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -43,7 +43,7 @@ def_module_params('sat', ('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)'), ('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_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'),