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

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 8a6d5d4a30b804ac7927405d2b68969a33e1c2d3..f80961cf8e4b4b3fa425ff70ea7e9d1b79040ad6 100644 (file)
--- 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 87db183e29f338e7bbc77365c9d618365122c5ff..bd133b0afa397e02bf40714cb54171da8ac64884 100644 (file)
--- 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 09991c571dc010864281b35e044650919ead27a6..9c96bbf15af1012742417801480986f1786b661d 100644 (file)
--- 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 84743fc1d6a92ec480453a96c60374f39ba5014b..33dfa19bcb7a9627d164d72c2ec418f688ff60b9 100644 (file)
--- 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;