mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
6a5695463f
commit
b4e7730034
|
@ -244,7 +244,7 @@ namespace sat {
|
|||
throw sat_param_exception("invalid PB lemma format: 'cardinality' or 'pb' expected");
|
||||
|
||||
m_card_solver = p.cardinality_solver();
|
||||
m_xor_solver = false && p.xor_solver(); // hide this option until thoroughly tested
|
||||
m_xor_solver = false; // prevent users from playing with this option
|
||||
|
||||
sat_simplifier_params sp(_p);
|
||||
m_elim_vars = sp.elim_vars();
|
||||
|
|
|
@ -53,7 +53,6 @@ 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), binary_merge, segmented, solver (use native solver)'),
|
||||
('pb.min_arity', UINT, 9, 'minimal arity to compile pb/cardinality constraints to CNF'),
|
||||
('xor.solver', BOOL, False, 'use xor solver'),
|
||||
('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'),
|
||||
('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'),
|
||||
('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'),
|
||||
|
|
|
@ -325,7 +325,6 @@ public:
|
|||
sat_params p1(p);
|
||||
m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
|
||||
m_params.set_sym("pb.solver", p1.pb_solver());
|
||||
m_params.set_bool("xor_solver", p1.xor_solver());
|
||||
m_solver.updt_params(m_params);
|
||||
m_solver.set_incremental(is_incremental() && !override_incremental());
|
||||
|
||||
|
|
|
@ -156,15 +156,12 @@ class sat_tactic : public tactic {
|
|||
imp * m_imp;
|
||||
params_ref m_params;
|
||||
statistics m_stats;
|
||||
symbol m_xor_solver;
|
||||
|
||||
public:
|
||||
sat_tactic(ast_manager & m, params_ref const & p):
|
||||
m_imp(nullptr),
|
||||
m_params(p),
|
||||
m_xor_solver("xor_solver") {
|
||||
m_params(p) {
|
||||
sat_params p1(p);
|
||||
m_params.set_bool(m_xor_solver, p1.xor_solver());
|
||||
}
|
||||
|
||||
tactic * translate(ast_manager & m) override {
|
||||
|
@ -177,8 +174,6 @@ public:
|
|||
|
||||
void updt_params(params_ref const & p) override {
|
||||
m_params = p;
|
||||
sat_params p1(p);
|
||||
m_params.set_bool(m_xor_solver, p1.xor_solver());
|
||||
if (m_imp) m_imp->updt_params(p);
|
||||
}
|
||||
|
||||
|
|
|
@ -228,9 +228,6 @@ unsigned read_dimacs(char const * file_name) {
|
|||
sat_params sp(p);
|
||||
reslimit limit;
|
||||
sat::solver solver(p, limit);
|
||||
if (sp.xor_solver()) {
|
||||
solver.set_extension(alloc(sat::ba_solver));
|
||||
}
|
||||
g_solver = &solver;
|
||||
|
||||
if (file_name) {
|
||||
|
|
Loading…
Reference in a new issue