mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

merge sat_tactic from csp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-14 15:17:42 -08:00
parent ee07008fb9
commit b11ec3bfbf
1 changed files with 15 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/sat/tactic/sat_tactic.cpp
View file

@ -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 {