allow for internalize implies

Author: NikolajBjorner

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);

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));

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<relevancy_propagator_imp&>(rp).propagate_relevant_or(m_parent);
     }
 
+    void implies_relevancy_eh::operator()(relevancy_propagator& rp) {
+        if (rp.is_relevant(m_parent))
+            static_cast<relevancy_propagator_imp&>(rp).propagate_relevant_implies(m_parent);
+    }
+
     void ite_relevancy_eh::operator()(relevancy_propagator & rp) {
         if (rp.is_relevant(m_parent)) {
             static_cast<relevancy_propagator_imp&>(rp).propagate_relevant_ite(m_parent);

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);