From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 15 May 2017 16:44:15 +0000 (-0500)
Subject: Fix bug 806. Minor fixes to remove term formula pass.
X-Git-Tag: cvc5-1.0.0~5801
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3f716fc402e2508a2ae1183fcfebebd2c95d6a3;p=cvc5.git

Fix bug 806. Minor fixes to remove term formula pass.
---

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 8a6d5d4a3..f80961cf8 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -601,7 +601,7 @@ bool Datatype::getSygusAllowConst() const {
 }
 
 bool Datatype::getSygusAllowAll() const {
-  return d_sygus_allow_const;
+  return d_sygus_allow_all;
 }
 
 Expr Datatype::getSygusEvaluationFunc() const {
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 87db183e2..bd133b0af 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -153,10 +153,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
   if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
     // Remember if we're inside a quantifier
     inQuant = true;
-  }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && 
-            node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && 
-            node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL && 
-            node.getKind()!=kind::BITVECTOR_EAGER_ATOM ){
+  }else if( !inTerm && hasNestedTermChildren( node ) ){
     // Remember if we're inside a term
     Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl;
     inTerm = true;
@@ -208,7 +205,7 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
   if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
     // Remember if we're inside a quantifier
     inQuant = true;
-  }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){
+  }else if( !inTerm && hasNestedTermChildren( node ) ){
     // Remember if we're inside a term
     inTerm = true;
   }  
@@ -233,4 +230,13 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
   }
 }
 
+// returns true if the children of node should be considered nested terms 
+bool RemoveTermFormulas::hasNestedTermChildren( TNode node ) {
+  return theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && 
+         node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && 
+         node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL && 
+         node.getKind()!=kind::BITVECTOR_EAGER_ATOM;
+         // dont' worry about FORALL or EXISTS (handled separately)
+}
+
 }/* CVC4 namespace */
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 09991c571..9c96bbf15 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -40,6 +40,8 @@ class RemoveTermFormulas {
   ITECache d_iteCache;
 
   static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); }
+  
+  static bool hasNestedTermChildren( TNode node );
 public:
 
   RemoveTermFormulas(context::UserContext* u);
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 84743fc1d..33dfa19bc 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -817,6 +817,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
 Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus ) {
   d_solution = s;
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+  Trace("csi-sol") << "Reconstruct to syntax " << s << ", allow all = " << dt.getSygusAllowAll() << " " << stn << ", reconstruct = " << rconsSygus << std::endl;
 
   //reconstruct the solution into sygus if necessary
   reconstructed = 0;