mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

testing inc-sat solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-07-30 17:49:51 -07:00
parent bfc0af7820
commit 365f05b41a
4 changed files with 26 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/sat/tactic/goal2sat.cpp
View file

@ -59,13 +59,15 @@ struct goal2sat::imp {
unsigned long long m_max_memory;
volatile bool m_cancel;
expr_ref_vector m_trail;
bool m_default_external;
imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm):
imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
m(_m),
m_solver(s),
m_map(map),
m_dep2asm(dep2asm),
m_trail(m) {
m_trail(m),
m_default_external(default_external) {
updt_params(p);
m_cancel = false;
m_true = sat::null_bool_var;
@ -121,7 +123,7 @@ struct goal2sat::imp {
l = sat::literal(mk_true(), !sign);
}
else {
bool ext = !is_uninterp_const(t) || m_interface_vars.contains(t);
bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
sat::bool_var v = m_solver.mk_var(ext);
m_map.insert(t, v);
l = sat::literal(v, sign);
@ -486,8 +488,8 @@ struct goal2sat::scoped_set_imp {
}
};
void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm) {
imp proc(g.m(), p, t, m, dep2asm);
void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) {
imp proc(g.m(), p, t, m, dep2asm, default_external);
scoped_set_imp set(this, &proc);
proc(g);
}