mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-01 21:49:29 +00:00
Code Activity

allow for internalize implies

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-07-31 20:48:15 -07:00
parent f77123c13c
commit 2d876d5af1
4 changed files with 87 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/smt/smt_internalizer.cpp
View file

@ -696,6 +696,10 @@ namespace smt {
mk_or_cnstr(to_app(n));
add_or_rel_watches(to_app(n));
break;
case OP_IMPLIES:
mk_implies_cnstr(to_app(n));
add_implies_rel_watches(to_app(n));
break;
case OP_EQ:
if (m.is_iff(n))
mk_iff_cnstr(to_app(n), false);
@ -711,8 +715,7 @@ namespace smt {
mk_iff_cnstr(to_app(n), true);
break;
case OP_DISTINCT:
case OP_IMPLIES:
throw default_exception("formula has not been simplified");
throw default_exception(std::string("formula has not been simplified") + " : " + mk_pp(n, m));
case OP_OEQ:
UNREACHABLE();
default:
@ -1687,6 +1690,14 @@ namespace smt {
}
}
void context::add_implies_rel_watches(app* n) {
if (relevancy()) {
relevancy_eh* eh = m_relevancy_propagator->mk_implies_relevancy_eh(n);
add_rel_watch(~get_literal(n->get_arg(0)), eh);
add_rel_watch(get_literal(n->get_arg(1)), eh);
}
}
void context::add_ite_rel_watches(app * n) {
if (relevancy()) {
relevancy_eh * eh = m_relevancy_propagator->mk_ite_relevancy_eh(n);
@ -1733,9 +1744,24 @@ namespace smt {
mk_gate_clause(buffer.size(), buffer.data());
}
void context::mk_implies_cnstr(app* n) {
literal l = get_literal(n);
literal_buffer buffer;
buffer.push_back(~l);
auto arg1 = n->get_arg(0);
literal l_arg1 = get_literal(arg1);
mk_gate_clause(l, l_arg1);
buffer.push_back(~l_arg1);
auto arg2 = n->get_arg(1);
literal l_arg2 = get_literal(arg2);
mk_gate_clause(l, ~l_arg2);
buffer.push_back(l_arg2);
mk_gate_clause(buffer.size(), buffer.data());
}
void context::mk_iff_cnstr(app * n, bool sign) {
if (n->get_num_args() != 2)
throw default_exception("formula has not been simplified");
throw default_exception(std::string("formula has not been simplified") + " : " + mk_pp(n, m));
literal l = get_literal(n);
literal l1 = get_literal(n->get_arg(0));
literal l2 = get_literal(n->get_arg(1));