Fixes for free variables in assertions (#1762)

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 250c21202a3de7e32eb99908cb933ce191f1cab3..fc10d2b4bb078aa29e6a179bd1634607c658b7e2 100644 (file)
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -215,8 +215,11 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
     // The representation is now the skolem
     return skolem;
   }
-  
-  if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+
+  if (node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS
+      || node.getKind() == kind::LAMBDA
+      || node.getKind() == kind::CHOICE)
+  {
     // Remember if we're inside a quantifier
     inQuant = true;
   }else if( !inTerm && hasNestedTermChildren( node ) ){
@@ -275,7 +278,10 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
     return cached.isNull() ? Node(node) : cached;
   }
 
-  if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+  if (node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS
+      || node.getKind() == kind::LAMBDA
+      || node.getKind() == kind::CHOICE)
+  {
     // Remember if we're inside a quantifier
     inQuant = true;
   }else if( !inTerm && hasNestedTermChildren( node ) ){

diff --git a/src/theory/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp
index 5b995f05236f69b11efdac1fe5b97317df98b124..cea992f5476cf558390ec14b5b3aab8a266c989a 100644 (file)
--- a/src/theory/quantifiers/sygus_inference.cpp
+++ b/src/theory/quantifiers/sygus_inference.cpp
@@ -192,7 +192,7 @@ bool SygusInference::simplify(std::vector<Node>& assertions)
 
   // sygus attribute to mark the conjecture as a sygus conjecture
   Trace("sygus-infer") << "Make outer sygus conjecture..." << std::endl;
-  Node sygusVar = nm->mkBoundVar("sygus", nm->booleanType());
+  Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
   SygusAttribute ca;
   sygusVar.setAttribute(ca, true);
   Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar);

diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 4f87f6aae014d249ef03859b802fd5852f8212d5..4bb28fe79a0244c6223d18feae6bc575ed820787 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -58,10 +58,6 @@ class TheoryQuantifiers : public Theory {
                         Node n,
                         std::vector<Node> node_values,
                         std::string str_value) override;
-  bool ppDontRewriteSubterm(TNode atom) override
-  {
-    return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS;
-  }
 
  private:
   void assertUniversal( Node n );

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 1e1a2e8e60641b6017cebf0b94626761348fe986..eae5578cfc24b39750c277553c53ea7d8fc38b0a 100644 (file)
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -35,15 +35,17 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
 
   Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 
-  if( ( parent.getKind() == kind::FORALL ||
-        parent.getKind() == kind::EXISTS ||
-        parent.getKind() == kind::REWRITE_RULE ||
-        parent.getKind() == kind::SEP_STAR ||
-        parent.getKind() == kind::SEP_WAND ||
-        ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() )
-        // parent.getKind() == kind::CARDINALITY_CONSTRAINT
-      ) &&
-      current != parent ) {
+  if ((parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS
+       || parent.getKind() == kind::LAMBDA
+       || parent.getKind() == kind::CHOICE
+       || parent.getKind() == kind::REWRITE_RULE
+       || parent.getKind() == kind::SEP_STAR
+       || parent.getKind() == kind::SEP_WAND
+       || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
+       // parent.getKind() == kind::CARDINALITY_CONSTRAINT
+       )
+      && current != parent)
+  {
     Debug("register::internal") << "quantifier:true" << std::endl;
     return true;
   }
@@ -179,15 +181,17 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 
   Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 
-  if( ( parent.getKind() == kind::FORALL ||
-        parent.getKind() == kind::EXISTS ||
-        parent.getKind() == kind::REWRITE_RULE ||
-        parent.getKind() == kind::SEP_STAR ||
-        parent.getKind() == kind::SEP_WAND ||
-        ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() )
-        // parent.getKind() == kind::CARDINALITY_CONSTRAINT
-      ) &&
-      current != parent ) {
+  if ((parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS
+       || parent.getKind() == kind::LAMBDA
+       || parent.getKind() == kind::CHOICE
+       || parent.getKind() == kind::REWRITE_RULE
+       || parent.getKind() == kind::SEP_STAR
+       || parent.getKind() == kind::SEP_WAND
+       || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
+       // parent.getKind() == kind::CARDINALITY_CONSTRAINT
+       )
+      && current != parent)
+  {
     Debug("register::internal") << "quantifier:true" << std::endl;
     return true;
   }

diff --git a/src/theory/theory.h b/src/theory/theory.h
index f38cda90a65c3b72f2e1d045dadcbad6f45338ff..2f7ce699945e9c1420e85ec72942b92908c04c53 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -552,11 +552,6 @@ public:
    */
   virtual Node ppRewrite(TNode atom) { return atom; }
 
-  /**
-   * Don't preprocess subterm of this term
-   */
-  virtual bool ppDontRewriteSubterm(TNode atom) { return false; }
-
   /**
    * Notify preprocessed assertions. Called on new assertions after
    * preprocessing before they are asserted to theory engine.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index de71a8b5e9974826c07796c96e2cf6c51fd6ccca..38885db853af68bd01c45b3a186147c762d8d8f8 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -394,6 +394,8 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       }
 
       // the atom should not have free variables
+      Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
+                      << std::endl;
       Assert(!preprocessed.hasFreeVar());
       // Pre-register the terms in the atom
       Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
@@ -1056,9 +1058,15 @@ Node TheoryEngine::ppTheoryRewrite(TNode term) {
   Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
 
   Node newTerm;
-  if (theoryOf(term)->ppDontRewriteSubterm(term)) {
+  // do not rewrite inside quantifiers
+  if (term.getKind() == kind::FORALL || term.getKind() == kind::EXISTS
+      || term.getKind() == kind::CHOICE
+      || term.getKind() == kind::LAMBDA)
+  {
     newTerm = Rewriter::rewrite(term);
-  } else {
+  }
+  else
+  {
     NodeBuilder<> newNode(term.getKind());
     if (term.getMetaKind() == kind::metakind::PARAMETERIZED) {
       newNode << term.getOperator();