From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 9 Nov 2017 17:36:37 +0000 (-0600)
Subject: Higher-order prep (#1338)
X-Git-Tag: cvc5-1.0.0~5492
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ada7b0ac4b3832d8fbf5e31080cb85df330049f;p=cvc5.git

Higher-order prep (#1338)

* Minor preparation for final higher-order merge.

* Format
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index f292c0a2e..3caeeaaaa 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -116,43 +116,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     return;
   }
 
-  if( !force_nt.isNull() && n.getKind()!=kind::CONST_RATIONAL ){
-    if( n.getType()!=force_nt ){
-      if( force_nt.isReal() ){
-        out << "(" << smtKindString( force_nt.isInteger() ? kind::TO_INTEGER : kind::TO_REAL) << " ";
-        toStream(out, n, toDepth, types, TypeNode::null());
-        out << ")";
-      }else{            
-        Node nn = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                                   NodeManager::currentNM()->mkConst(AscriptionType(force_nt.toType())), n );
-        toStream(out, nn, toDepth, types, TypeNode::null());                                 
-      }
-      return;  
-    }
-  }
-
-  // variable
-  if(n.isVar()) {
-    string s;
-    if(n.getAttribute(expr::VarNameAttr(), s)) {
-      out << maybeQuoteSymbol(s);
-    } else {
-      if(n.getKind() == kind::VARIABLE) {
-        out << "var_";
-      } else {
-        out << n.getKind() << '_';
-      }
-      out << n.getId();
-    }
-    if(types) {
-      // print the whole type, but not *its* type
-      out << ":";
-      n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
-    }
-
-    return;
-  }
-
   // constant
   if(n.getMetaKind() == kind::metakind::CONSTANT) {
     switch(n.getKind()) {
@@ -325,6 +288,61 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     return;
   }
 
+  if (!force_nt.isNull())
+  {
+    if (n.getType() != force_nt)
+    {
+      if (force_nt.isReal())
+      {
+        out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER
+                                                         : kind::TO_REAL)
+            << " ";
+        toStream(out, n, toDepth, types, TypeNode::null());
+        out << ")";
+      }
+      else
+      {
+        Node nn = NodeManager::currentNM()->mkNode(
+            kind::APPLY_TYPE_ASCRIPTION,
+            NodeManager::currentNM()->mkConst(
+                AscriptionType(force_nt.toType())),
+            n);
+        toStream(out, nn, toDepth, types, TypeNode::null());
+      }
+      return;
+    }
+  }
+
+  // variable
+  if (n.isVar())
+  {
+    string s;
+    if (n.getAttribute(expr::VarNameAttr(), s))
+    {
+      out << maybeQuoteSymbol(s);
+    }
+    else
+    {
+      if (n.getKind() == kind::VARIABLE)
+      {
+        out << "var_";
+      }
+      else
+      {
+        out << n.getKind() << '_';
+      }
+      out << n.getId();
+    }
+    if (types)
+    {
+      // print the whole type, but not *its* type
+      out << ":";
+      n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
+    }
+
+    return;
+  }
+
   bool stillNeedToPrintParams = true;
   bool forceBinary = false; // force N-ary to binary when outputing children
   bool parametricTypeChildren = false;   // parametric operators that are (op t1 ... tn) where t1...tn must have same type
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1634345e0..a1a15b25a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2424,8 +2424,10 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
           fm = def.getFormula();
         }
 
-        Node instance = fm.substitute(formals.begin(), formals.end(),
-                                      n.begin(), n.end());
+        Node instance = fm.substitute(formals.begin(),
+                                      formals.end(),
+                                      n.begin(),
+                                      n.begin() + formals.size());
         Debug("expand") << "made : " << instance << endl;
 
         Node expanded = expandDefinitions(instance, cache, expandOnly);
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0ffed5243..45c418996 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -105,6 +105,10 @@ void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node
         activeMap[ n ] = true;
       }
     }else{
+      if (n.hasOperator())
+      {
+        computeArgs(args, activeMap, n.getOperator(), visited);
+      }
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
         computeArgs( args, activeMap, n[i], visited );
       }