From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Jan 2022 19:18:07 +0000 (-0600)
Subject: Fix bug in evaluator for division by zero (#7942)
X-Git-Tag: cvc5-1.0.0~550
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=579984e9e184ef8a31181b43152d8f24f0401de8;p=cvc5.git

Fix bug in evaluator for division by zero (#7942)

Fixes #7917.
---

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 3552d0a31..6b4176c13 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -469,7 +469,12 @@ EvalResult Evaluator::evalInternal(
             }
             res = res / results[currNode[i]].d_rat;
           }
-          if (!divbyzero)
+          if (divbyzero)
+          {
+            processUnhandled(
+                currNode, currNodeVal, evalAsNode, results, needsReconstruct);
+          }
+          else
           {
             results[currNode] = EvalResult(res);
           }
@@ -894,10 +899,8 @@ EvalResult Evaluator::evalInternal(
         {
           Trace("evaluator") << "Kind " << currNodeVal.getKind()
                              << " not supported" << std::endl;
-          results[currNode] = EvalResult();
-          evalAsNode[currNode] =
-              needsReconstruct ? reconstruct(currNode, results, evalAsNode)
-                               : currNodeVal;
+          processUnhandled(
+              currNode, currNodeVal, evalAsNode, results, needsReconstruct);
         }
       }
     }
@@ -970,5 +973,15 @@ Node Evaluator::reconstruct(TNode n,
   return nn;
 }
 
+void Evaluator::processUnhandled(TNode n,
+                                 TNode nv,
+                                 std::unordered_map<TNode, Node>& evalAsNode,
+                                 std::unordered_map<TNode, EvalResult>& results,
+                                 bool needsReconstruct) const
+{
+  results[n] = EvalResult();
+  evalAsNode[n] = needsReconstruct ? reconstruct(n, results, evalAsNode) : Node(nv);
+}
+
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index bd10129e2..a85071277 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -159,6 +159,17 @@ class Evaluator
   Node reconstruct(TNode n,
                    std::unordered_map<TNode, EvalResult>& eresults,
                    std::unordered_map<TNode, Node>& evalAsNode) const;
+  /**
+   * Process unhandled, called when n cannot be evaluated. This updates
+   * evalAsNode and results with the proper entries for this case. The term
+   * nv is the (Node) value of n if it exists, otherwise if needsReconstruct
+   * is true, the value of n is reconstructed based on evalAsNode and results.
+   */
+  void processUnhandled(TNode n,
+                        TNode nv,
+                        std::unordered_map<TNode, Node>& evalAsNode,
+                        std::unordered_map<TNode, EvalResult>& results,
+                        bool needsReconstruct) const;
   /** The (optional) rewriter to be used */
   Rewriter* d_rr;
   /** The cardinality of the alphabet of strings */