Missing

ajreynol · Feb 22, 2025 · acbb4c5 · acbb4c5
1 parent 6c280c9
commit acbb4c5
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 0 deletions.
diff --git a/proofs/eo/cpc/Cpc.eo b/proofs/eo/cpc/Cpc.eo
@@ -118,6 +118,7 @@
       (($run_evaluate (not b))             (eo::not ($run_evaluate b)))
       (($run_evaluate (ite b x y))         (eo::ite ($run_evaluate b) ($run_evaluate x) ($run_evaluate y)))
       (($run_evaluate (or x ys))           (eo::or ($run_evaluate x) ($run_evaluate ys)))
+      (($run_evaluate (=> x y))            (eo::or (eo::not ($run_evaluate x)) ($run_evaluate y)))
       (($run_evaluate (and x ys))          (eo::and ($run_evaluate x) ($run_evaluate ys)))
       (($run_evaluate (xor x y))           (eo::xor ($run_evaluate x) ($run_evaluate y)))
 

diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp
@@ -416,6 +416,7 @@ bool AlfPrinter::canEvaluate(Node n)
         case Kind::NOT:
         case Kind::AND:
         case Kind::OR:
+        case Kind::IMPLIES:
         case Kind::XOR:
         case Kind::CONST_BOOLEAN:
         case Kind::CONST_INTEGER:

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
@@ -455,6 +455,12 @@ EvalResult Evaluator::evalInternal(
           results[currNode] = EvalResult(res);
           break;
         }
+        case Kind::IMPLIES:
+        {
+          bool res = !results[currNode[0]].d_bool || results[currNode[1]].d_bool;
+          results[currNode] = EvalResult(res);
+          break;
+        }
         case Kind::XOR:
         {
           bool res = results[currNode[0]].d_bool;