mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix #4400

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-19 15:55:45 -07:00
parent 7756e2c6d5
commit 1ce63363ba
2 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.h
View file

@ -848,7 +848,7 @@ namespace smt {
void mk_or_cnstr(app * n);
void mk_iff_cnstr(app * n);
void mk_iff_cnstr(app * n, bool sign);
void mk_ite_cnstr(app * n);

11
src/smt/smt_internalizer.cpp
View file

@ -648,7 +648,7 @@ namespace smt {
break;
case OP_EQ:
if (m.is_iff(n))
mk_iff_cnstr(to_app(n));
mk_iff_cnstr(to_app(n), false);
break;
case OP_ITE:
mk_ite_cnstr(to_app(n));
@ -657,9 +657,11 @@ namespace smt {
case OP_TRUE:
case OP_FALSE:
break;
case OP_XOR:
mk_iff_cnstr(to_app(n), true);
break;
case OP_DISTINCT:
case OP_IMPLIES:
case OP_XOR:
throw default_exception("formula has not been simplified");
case OP_OEQ:
UNREACHABLE();
@ -1624,10 +1626,13 @@ namespace smt {
mk_gate_clause(buffer.size(), buffer.c_ptr());
}
void context::mk_iff_cnstr(app * n) {
void context::mk_iff_cnstr(app * n, bool sign) {
if (n->get_num_args() != 2)
throw default_exception("formula has not been simplified");
literal l = get_literal(n);
literal l1 = get_literal(n->get_arg(0));
literal l2 = get_literal(n->get_arg(1));
if (sign) l.neg();
TRACE("mk_iff_cnstr", tout << "l: " << l << ", l1: " << l1 << ", l2: " << l2 << "\n";);
mk_gate_clause(~l, l1, ~l2);
mk_gate_clause(~l, ~l1 , l2);