diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 3dbadc1cb..4d8508def 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -904,6 +904,8 @@ namespace smt { void add_or_rel_watches(app * n); + void add_implies_rel_watches(app* n); + void add_ite_rel_watches(app * n); void mk_not_cnstr(app * n); @@ -912,6 +914,8 @@ namespace smt { void mk_or_cnstr(app * n); + void mk_implies_cnstr(app* n); + void mk_iff_cnstr(app * n, bool sign); void mk_ite_cnstr(app * n); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index c15505ab0..9aa6d68f4 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -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)); diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index f7ba3dcce..48fa3657d 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -62,6 +62,13 @@ namespace smt { void operator()(relevancy_propagator & rp) override; }; + class implies_relevancy_eh : public relevancy_eh { + app* m_parent; + public: + implies_relevancy_eh(app* p) :m_parent(p) {} + void operator()(relevancy_propagator& rp) override; + }; + class ite_relevancy_eh : public relevancy_eh { app * m_parent; public: @@ -108,6 +115,11 @@ namespace smt { return mk_relevancy_eh(or_relevancy_eh(n)); } + relevancy_eh* relevancy_propagator::mk_implies_relevancy_eh(app* n) { + SASSERT(get_manager().is_implies(n)); + return mk_relevancy_eh(implies_relevancy_eh(n)); + } + relevancy_eh * relevancy_propagator::mk_and_relevancy_eh(app * n) { SASSERT(get_manager().is_and(n)); return mk_relevancy_eh(and_relevancy_eh(n)); @@ -357,8 +369,38 @@ namespace smt { --j; mark_as_relevant(n->get_arg(j)); } - } + } + void propagate_relevant_implies(app* n) { + SASSERT(get_manager().is_implies(n)); + lbool val = m_context.find_assignment(n); + // If val is l_undef, then the expression + // is a root, and no boolean variable was created for it. + if (val == l_undef) + val = l_true; + switch (val) { + case l_false: + propagate_relevant_app(n); + break; + case l_undef: + break; + case l_true: { + expr* true_arg = nullptr; + auto arg0 = n->get_arg(0); + auto arg1 = n->get_arg(1); + if (m_context.find_assignment(arg0) == l_false) { + if (!is_relevant_core(arg0)) + mark_as_relevant(arg0); + return; + } + if (m_context.find_assignment(arg1) == l_true) { + if (!is_relevant_core(arg1)) + mark_as_relevant(arg1); + return; + } + } + } + } /** \brief Propagate relevancy for an or-application. */ @@ -470,6 +512,9 @@ namespace smt { case OP_AND: propagate_relevant_and(to_app(n)); break; + case OP_IMPLIES: + propagate_relevant_implies(to_app(n)); + break; case OP_ITE: propagate_relevant_ite(to_app(n)); break; @@ -505,6 +550,8 @@ namespace smt { propagate_relevant_or(to_app(n)); else if (m.is_and(n)) propagate_relevant_and(to_app(n)); + else if (m.is_implies(n)) + propagate_relevant_implies(to_app(n)); } relevancy_ehs * ehs = get_watches(n, val); while (ehs != nullptr) { @@ -644,6 +691,11 @@ namespace smt { static_cast(rp).propagate_relevant_or(m_parent); } + void implies_relevancy_eh::operator()(relevancy_propagator& rp) { + if (rp.is_relevant(m_parent)) + static_cast(rp).propagate_relevant_implies(m_parent); + } + void ite_relevancy_eh::operator()(relevancy_propagator & rp) { if (rp.is_relevant(m_parent)) { static_cast(rp).propagate_relevant_ite(m_parent); diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h index 8dea2842f..4827fffcb 100644 --- a/src/smt/smt_relevancy.h +++ b/src/smt/smt_relevancy.h @@ -188,6 +188,7 @@ namespace smt { void add_dependency(expr * src, expr * target); relevancy_eh * mk_or_relevancy_eh(app * n); + relevancy_eh* mk_implies_relevancy_eh(app* n); relevancy_eh * mk_and_relevancy_eh(app * n); relevancy_eh * mk_ite_relevancy_eh(app * n); relevancy_eh * mk_term_ite_relevancy_eh(app * c, app * t, app * e);