mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

#5422

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-21 06:25:11 -07:00
parent 0ba518b0c0
commit 8a4b292f3e
1 changed files with 8 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -69,7 +69,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
atom2bool_var & m_map; atom2bool_var & m_map;
dep2asm_map & m_dep2asm; dep2asm_map & m_dep2asm;
obj_map<expr, sat::bool_var>* m_expr2var_replay { nullptr }; obj_map<expr, sat::bool_var>* m_expr2var_replay { nullptr };
sat::literal m_true;
bool m_ite_extra; bool m_ite_extra;
unsigned long long m_max_memory; unsigned long long m_max_memory;
expr_ref_vector m_trail; expr_ref_vector m_trail;
@ -92,7 +91,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_unhandled_funs(m), m_unhandled_funs(m),
m_default_external(default_external) { m_default_external(default_external) {
updt_params(p); updt_params(p);
m_true = sat::null_literal;
} }
~imp() override { ~imp() override {
@ -198,16 +196,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
ensure_euf()->drat_bool_def(v, n); ensure_euf()->drat_bool_def(v, n);
} }
sat::literal mk_true() {
if (m_true == sat::null_literal) {
// create fake variable to represent true;
m_true = sat::literal(add_var(false, m.mk_true()), false);
mk_clause(m_true); // v is true
add_dual_root(1, &m_true);
}
return m_true;
}
sat::bool_var to_bool_var(expr* e) override { sat::bool_var to_bool_var(expr* e) override {
sat::literal l; sat::literal l;
sat::bool_var v = m_map.to_bool_var(e); sat::bool_var v = m_map.to_bool_var(e);
@ -301,10 +289,16 @@ struct goal2sat::imp : public sat::sat_internalizer {
sat::bool_var v = m_map.to_bool_var(t); sat::bool_var v = m_map.to_bool_var(t);
if (v == sat::null_bool_var) { if (v == sat::null_bool_var) {
if (m.is_true(t)) { if (m.is_true(t)) {
l = sign ? ~mk_true() : mk_true(); sat::literal tt = sat::literal(add_var(false, m.mk_true()), false);
mk_clause(tt);
add_dual_root(1, &tt);
l = sign ? ~tt : tt;
} }
else if (m.is_false(t)) { else if (m.is_false(t)) {
l = sign ? mk_true() : ~mk_true(); sat::literal tt = sat::literal(add_var(false, m.mk_false()), true);
mk_clause(tt);
add_dual_root(1, &tt);
l = sign ? tt : ~tt;
} }
else { else {
if (m_euf) { if (m_euf) {
@ -932,7 +926,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
} }
void user_pop(unsigned n) { void user_pop(unsigned n) {
m_true = sat::null_literal;
} }
}; };