From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 6 Mar 2013 19:17:43 +0000 (-0500)
Subject: Best heuristics for handling decision requests from arrays
X-Git-Tag: cvc5-1.0.0~7397
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9817df56827b4ee0ee67a33361f8619c5d1df6ed;p=cvc5.git

Best heuristics for handling decision requests from arrays
---

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index aabd3a62d..dcf4813fc 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1324,7 +1324,9 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
   // Prefer equality between indexes so as not to introduce new read terms
   if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
-    d_decisionRequests.push(i.eqNode(j));
+    Node i_eq_j = d_valuation.ensureLiteral(i.eqNode(j));
+    getOutputChannel().requirePhase(i_eq_j, true);
+    d_decisionRequests.push(i_eq_j);
   }
 
   // TODO: maybe add triggers here
@@ -1392,7 +1394,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
 Node TheoryArrays::getNextDecisionRequest() {
   if(! d_decisionRequests.empty()) {
-    Node n = d_valuation.ensureLiteral(d_decisionRequests.front());
+    Node n = d_decisionRequests.front();
     d_decisionRequests.pop();
     return n;
   } else {