Updates to E-matching to avoid entailed instantiations earlier. Minor updates to datatypes lemmas, other minor changes.

1 files changed, 17 insertions, 0 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 1f1efa2a8..eb92b0f70 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -377,3 +377,20 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool&
     newPol = pol;
   }
 }
+
+void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
+  if( n.getKind()==AND || n.getKind()==OR ){
+    newHasPol = hasPol && pol==( n.getKind()==AND );
+    newPol = pol;
+  }else if( n.getKind()==IMPLIES ){
+    newHasPol = hasPol && !pol;
+    newPol = child==0 ? !pol : pol;
+  }else if( n.getKind()==NOT ){
+    newHasPol = hasPol;
+    newPol = !pol;
+  }else{
+    newHasPol = false;
+    newPol = pol;
+  }
+}
+