From b3f716fc402e2508a2ae1183fcfebebd2c95d6a3 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 15 May 2017 11:44:15 -0500
Subject: [PATCH] Fix bug 806. Minor fixes to remove term formula pass.

---
 src/expr/datatype.cpp                           |  2 +-
 src/smt/term_formula_removal.cpp                | 16 +++++++++++-----
 src/smt/term_formula_removal.h                  |  2 ++
 src/theory/quantifiers/ce_guided_single_inv.cpp |  1 +
 4 files changed, 15 insertions(+), 6 deletions(-)

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;
-- 
2.30.2