mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

#5532

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-03 12:20:23 -07:00
parent c4158ebc33
commit 87f5b9282f
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/euf_solver.cpp
View file

@ -591,6 +591,7 @@ namespace euf {
else
lit = si.internalize(e, true);
VERIFY(lit.var() == v);
attach_lit(lit, e);
}
@ -654,10 +655,10 @@ namespace euf {
break;
}
case OP_TRUE:
add_root(lit);
add_aux(lit);
break;
case OP_FALSE:
add_root(~lit);
add_aux(~lit);
break;
case OP_ITE: {
auto lit1 = si.internalize(to_app(e)->get_arg(0), true);

1
src/sat/smt/euf_solver.h
View file

@ -369,6 +369,7 @@ namespace euf {
void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); }
void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); }
void add_aux(unsigned n, sat::literal const* lits);
void add_aux(sat::literal a) { sat::literal lits[1] = { a }; add_aux(1, lits); }
void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); }
void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); }
void track_relevancy(sat::bool_var v);