From b11ec3bfbf2378a8f29f8ae3097e154cfbd4011c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Jan 2019 15:17:42 -0800 Subject: [PATCH] merge sat_tactic from csp Signed-off-by: Nikolaj Bjorner --- src/sat/tactic/sat_tactic.cpp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index e6369a918..bd100d620 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include "tactic/tactical.h" #include "sat/tactic/goal2sat.h" #include "sat/sat_solver.h" +#include "sat/sat_params.hpp" class sat_tactic : public tactic { @@ -36,6 +37,7 @@ class sat_tactic : public tactic { m_solver(p, m.limit()), m_params(p) { SASSERT(!m.proofs_enabled()); + updt_params(p); } void operator()(goal_ref const & g, @@ -130,13 +132,20 @@ class sat_tactic : public tactic { lit2asm.insert(kv.m_value.index(), kv.m_key); } } + + void updt_params(params_ref const& p) { + m_solver.updt_params(p); + } + }; + struct scoped_set_imp { sat_tactic * m_owner; scoped_set_imp(sat_tactic * o, imp * i):m_owner(o) { - m_owner->m_imp = i; + m_owner->m_imp = i; + m_owner->updt_params(m_owner->m_params); } ~scoped_set_imp() { @@ -152,6 +161,8 @@ public: sat_tactic(ast_manager & m, params_ref const & p): m_imp(nullptr), m_params(p) { + sat_params p1(p); + m_params.set_bool("xor_solver", p1.xor_solver()); } tactic * translate(ast_manager & m) override { @@ -164,6 +175,9 @@ public: void updt_params(params_ref const & p) override { m_params = p; + sat_params p1(p); + m_params.set_bool("xor_solver", p1.xor_solver()); + if (m_imp) m_imp->updt_params(p); } void collect_param_descrs(param_descrs & r) override {