Eliminate APPLY kind (#2976)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 4cd9f49237cf1be97be1f6efe01d50a3794e25a8..ab34e62b480e068f15686800e3ac5b1ca2281420 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -52,8 +52,6 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     /* Builtin ------------------------------------------------------------- */
     {UNINTERPRETED_CONSTANT, CVC4::Kind::UNINTERPRETED_CONSTANT},
     {ABSTRACT_VALUE, CVC4::Kind::ABSTRACT_VALUE},
-    {FUNCTION, CVC4::Kind::FUNCTION},
-    {APPLY, CVC4::Kind::APPLY},
     {EQUAL, CVC4::Kind::EQUAL},
     {DISTINCT, CVC4::Kind::DISTINCT},
     {CONSTANT, CVC4::Kind::VARIABLE},
@@ -300,8 +298,6 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         /* Builtin --------------------------------------------------------- */
         {CVC4::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT},
         {CVC4::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE},
-        {CVC4::Kind::FUNCTION, FUNCTION},
-        {CVC4::Kind::APPLY, APPLY},
         {CVC4::Kind::EQUAL, EQUAL},
         {CVC4::Kind::DISTINCT, DISTINCT},
         {CVC4::Kind::VARIABLE, CONSTANT},

diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index d4f6880f9a4d26fcec1d6ad482832422e7611911..7d9ec28c6e2b253cee5aa00c47c10f99d2a20596 100644 (file)
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -78,31 +78,6 @@ enum CVC4_PUBLIC Kind : int32_t
   /* Built-in operator */
   BUILTIN,
 #endif
-  /**
-   * Defined function.
-   * Parameters: 3 (4)
-   *   See defineFun().
-   * Create with:
-   *   defineFun(const std::string& symbol,
-   *             const std::vector<Term>& bound_vars,
-   *             Sort sort,
-   *             Term term)
-   *   defineFun(Term fun,
-   *             const std::vector<Term>& bound_vars,
-   *             Term term)
-   */
-  FUNCTION,
-  /**
-   * Application of a defined function.
-   * Parameters: n > 1
-   *   -[1]..[n]: Function argument instantiation Terms
-   * Create with:
-   *   mkTerm(Kind kind, Term child)
-   *   mkTerm(Kind kind, Term child1, Term child2)
-   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
-   *   mkTerm(Kind kind, const std::vector<Term>& children)
-   */
-  APPLY,
   /**
    * Equality.
    * Parameters: 2

diff --git a/src/expr/node.h b/src/expr/node.h
index 935cde30868156d95941bffa4e8d6a0a0b676136..768d7b948e025ca55a1d3964e163412bb2fda623 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -489,7 +489,7 @@ public:
 
   /**
    * Returns a node representing the operator of this expression.
-   * If this is an APPLY, then the operator will be a functional term.
+   * If this is an APPLY_UF, then the operator will be a functional term.
    * Otherwise, it will be a node with kind BUILTIN.
    */
   NodeTemplate<true> getOperator() const;
@@ -1273,7 +1273,7 @@ NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
 
 /**
  * Returns a node representing the operator of this expression.
- * If this is an APPLY, then the operator will be a functional term.
+ * If this is an APPLY_UF, then the operator will be a functional term.
  * Otherwise, it will be a node with kind BUILTIN.
  */
 template <bool ref_count>

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index bc88166d35fa96bc913745b3027bf48b73f5ac28..28489154acfa74fbb936f48bb70d0af7d9fb201b 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -128,23 +128,18 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) {
   }
   // now, post-process the expression
   assert( !expr.isNull() );
-  if(isDefinedFunction(expr)) {
-    // defined functions/constants are wrapped in an APPLY so that they are
-    // expanded into their definition, e.g. during SmtEnginePrivate::expandDefinitions
-    expr = getExprManager()->mkExpr(CVC4::kind::APPLY, expr);
-  }else{
-    Type te = expr.getType();
-    if(te.isConstructor() && ConstructorType(te).getArity() == 0) {
-      // nullary constructors have APPLY_CONSTRUCTOR kind with no children
-      expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr);
-    }
+  Type te = expr.getType();
+  if (te.isConstructor() && ConstructorType(te).getArity() == 0)
+  {
+    // nullary constructors have APPLY_CONSTRUCTOR kind with no children
+    expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr);
   }
   return expr;
 }
 
 Kind Parser::getKindForFunction(Expr fun) {
   if(isDefinedFunction(fun)) {
-    return APPLY;
+    return APPLY_UF;
   }
   Type t = fun.getType();
   if(t.isConstructor()) {

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 75df38637c05981aa0085492b3f3518b88fff743..9ba7f4b2eb560297d0990efdca0cc33508df14ca 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2091,7 +2091,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
              // however, we need to apply partial version since we don't have the internal selector available
              aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR, dtc[i].getSelector(), expr ) );
            }
-           patexprs.push_back( MK_EXPR( CVC4::kind::APPLY, aargs ) );
+           patexprs.push_back( MK_EXPR( CVC4::kind::APPLY_UF, aargs ) );
            patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
          }
          RPAREN_TOK 

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 47da10f42e2ecc0130a69debbaecf935e2af2e5b..71ba81124565cd9ce6a6f8ae320a8a32a94a3f59 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -859,7 +859,9 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
           children.push_back( it->second );
         }
       }
-      Kind sk = sop.getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(sop);
+      Kind sk = sop.getKind() != kind::BUILTIN
+                    ? kind::APPLY_UF
+                    : getExprManager()->operatorToKind(sop);
       Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
       Expr e = getExprManager()->mkExpr( sk, children );
       Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
@@ -1072,7 +1074,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
         }
         children.insert(children.end(), largs.begin(), largs.end());
         Kind sk = ops[i].getKind() != kind::BUILTIN
-                      ? kind::APPLY
+                      ? kind::APPLY_UF
                       : getExprManager()->operatorToKind(ops[i]);
         Expr body = getExprManager()->mkExpr(sk, children);
         // replace by lambda
@@ -1131,14 +1133,13 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
             std::vector<Expr> largs;
             Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
             largs.insert(largs.begin(), ops[i]);
-            Expr body = getExprManager()->mkExpr(kind::APPLY, largs);
+            Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs);
             ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
             Debug("parser-sygus") << "  ...replace op : " << ops[i]
                                   << std::endl;
           }
           else
           {
-            ops[i] = getExprManager()->mkExpr(kind::APPLY, ops[i]);
             Debug("parser-sygus") << "  ...replace op : " << ops[i]
                                   << std::endl;
           }

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index c95ff57811b3f0febe1f0371c5a9d1f9b60f4170..630d8bdd71b74215f77b11dc779108cf35808c3d 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -280,9 +280,6 @@ void CvcPrinter::toStream(
       out << ")";
       return;
       break;
-    case kind::APPLY:
-      toStream(op, n.getOperator(), depth, types, true);
-      break;
     case kind::CHAIN:
     case kind::DISTINCT: // chain and distinct not supported directly in CVC4, blast them away with the rewriter
       toStream(out, theory::Rewriter::rewrite(n), depth, types, true);

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7ea7765d892b089368b98d54c574500da674f163..5311f1bec93c09a433824540fc6c126f01bd29ac 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -475,7 +475,6 @@ void Smt2Printer::toStream(std::ostream& out,
   }
   switch(Kind k = n.getKind()) {
     // builtin theory
-  case kind::APPLY: break;
   case kind::EQUAL:
   case kind::DISTINCT:
     out << smtKindString(k, d_variant) << " ";
@@ -965,7 +964,6 @@ static string smtKindString(Kind k, Variant v)
 {
   switch(k) {
     // builtin theory
-  case kind::APPLY: break;
   case kind::EQUAL: return "=";
   case kind::DISTINCT: return "distinct";
   case kind::CHAIN: break;

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index ecd3c6f16d2339cea56ff35bf449fb437efd68e3..b1936d8cc95bba5bd37b73e57065c8902bc0c0ea 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1358,8 +1358,7 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine)
   this->DefineFunctionCommand::invoke(smtEngine);
   if (!d_func.isNull() && d_func.getType().isBoolean())
   {
-    smtEngine->addToAssignment(
-        d_func.getExprManager()->mkExpr(kind::APPLY, d_func));
+    smtEngine->addToAssignment(d_func);
   }
   d_commandStatus = CommandSuccess::instance();
 }
@@ -1751,14 +1750,7 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine)
     for (const auto& p : assignments)
     {
       vector<SExpr> v;
-      if (p.first.getKind() == kind::APPLY)
-      {
-        v.emplace_back(SExpr::Keyword(p.first.getOperator().toString()));
-      }
-      else
-      {
-        v.emplace_back(SExpr::Keyword(p.first.toString()));
-      }
+      v.emplace_back(SExpr::Keyword(p.first.toString()));
       v.emplace_back(SExpr::Keyword(p.second.toString()));
       sexprs.emplace_back(v);
     }

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d035f88c1b365e766638872431a61973dfeac176..66198946fa03c7316f11b8c2bd000abea6170a38 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2734,13 +2734,20 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
       if(n.isVar()) {
         SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
         if(i != d_smt.d_definedFunctions->end()) {
+          Node f = (*i).second.getFormula();
+          // must expand its definition
+          Node fe = expandDefinitions(f, cache, expandOnly);
           // replacement must be closed
           if((*i).second.getFormals().size() > 0) {
-            result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula()));
+            result.push(d_smt.d_nodeManager->mkNode(
+                kind::LAMBDA,
+                d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST,
+                                            (*i).second.getFormals()),
+                fe));
             continue;
           }
           // don't bother putting in the cache
-          result.push((*i).second.getFormula());
+          result.push(fe);
           continue;
         }
         // don't bother putting in the cache
@@ -2758,11 +2765,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
 
       // otherwise expand it
       bool doExpand = false;
-      if (k == kind::APPLY)
-      {
-        doExpand = true;
-      }
-      else if (k == kind::APPLY_UF)
+      if (k == kind::APPLY_UF)
       {
         // Always do beta-reduction here. The reason is that there may be
         // operators such as INTS_MODULUS in the body of the lambda that would
@@ -2775,10 +2778,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
         {
           doExpand = true;
         }
-        else if (options::macrosQuant() || options::sygusInference())
+        else
         {
-          // The above options assign substitutions to APPLY_UF, thus we check
-          // here and expand if this operator corresponds to a defined function.
+          // We always check if this operator corresponds to a defined function.
           doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr());
         }
       }
@@ -3969,8 +3971,7 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv,
     {
       children.insert(children.end(), vars.begin(), vars.end());
     }
-    terms[i] =
-        d_nodeManager->mkNode(i == 0 ? kind::APPLY_UF : kind::APPLY, children);
+    terms[i] = d_nodeManager->mkNode(kind::APPLY_UF, children);
     // make application of Inv on primed variables
     if (i == 0)
     {
@@ -4218,15 +4219,15 @@ bool SmtEngine::addToAssignment(const Expr& ex) {
       "expected Boolean-typed variable or function application "
       "in addToAssignment()" );
   Node n = e.getNode();
-  // must be an APPLY of a zero-ary defined function, or a variable
+  // must be a defined constant, or a variable
   PrettyCheckArgument(
-      ( ( n.getKind() == kind::APPLY &&
-          ( d_definedFunctions->find(n.getOperator()) !=
-            d_definedFunctions->end() ) &&
-          n.getNumChildren() == 0 ) ||
-        n.isVar() ), e,
+      (((d_definedFunctions->find(n) != d_definedFunctions->end())
+        && n.getNumChildren() == 0)
+       || n.isVar()),
+      e,
       "expected variable or defined-function application "
-      "in addToAssignment(),\ngot %s", e.toString().c_str() );
+      "in addToAssignment(),\ngot %s",
+      e.toString().c_str());
   if(!options::produceAssignments()) {
     return false;
   }
@@ -4295,8 +4296,7 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment()
       // ensure it's a constant
       Assert(resultNode.isConst());
 
-      Assert(as.getKind() == kind::APPLY || as.isVar());
-      Assert(as.getKind() != kind::APPLY || as.getNumChildren() == 0);
+      Assert(as.isVar());
       res.emplace_back(as.toExpr(), resultNode.toExpr());
     }
   }

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 3313a684f7bf263104df3910eefd39e83b5dc17d..15891dfadb73bbd00fbfaef372888a8a18358509 100644 (file)
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -289,9 +289,6 @@ constant BUILTIN \
     "expr/kind.h" \
     "the kind of expressions representing built-in operators"
 
-variable FUNCTION "a defined function"
-parameterized APPLY FUNCTION 0: "application of a defined function"
-
 operator EQUAL 2 "equality (two parameters only, sorts must match)"
 operator DISTINCT 2: "disequality (N-ary, sorts must match)"
 variable VARIABLE "a variable (not permitted in bindings)"
@@ -332,7 +329,6 @@ well-founded SEXPR_TYPE \
     "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 
-typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 2c726d12fe059e759984b0e012ddfd089360aa02..db427d21ea2e7839aa4afe296554f4f28b820009 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -31,44 +31,6 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-class ApplyTypeRule {
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TNode f = n.getOperator();
-    TypeNode fType = f.getType(check);
-    if( !fType.isFunction() && n.getNumChildren() > 0 ) {
-      throw TypeCheckingExceptionPrivate(n, "operator does not have function type");
-    }
-    if( check ) {
-      if(fType.isFunction()) {
-        if(n.getNumChildren() != fType.getNumChildren() - 1) {
-          throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
-        }
-        TNode::iterator argument_it = n.begin();
-        TNode::iterator argument_it_end = n.end();
-        TypeNode::iterator argument_type_it = fType.begin();
-        for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) {
-          if(!(*argument_it).getType().isComparableTo(*argument_type_it)) {
-            std::stringstream ss;
-            ss << "argument types do not match the function type:\n"
-               << "argument:  " << *argument_it << "\n"
-               << "has type:  " << (*argument_it).getType() << "\n"
-               << "not equal: " << *argument_type_it;
-            throw TypeCheckingExceptionPrivate(n, ss.str());
-          }
-        }
-      } else {
-        if( n.getNumChildren() > 0 ) {
-          throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
-        }
-      }
-    }
-    return fType.isFunction() ? fType.getRangeType() : fType;
-  }
-};/* class ApplyTypeRule */
-
-
 class EqualityTypeRule {
  public:
   inline static TypeNode computeType(NodeManager* nodeManager,

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 5d3a92cdcb0ad7739b9d7ec20b6fa9b28530c41e..be87b7e8d858a212c54de53d97a914eb83356322 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -191,8 +191,6 @@ Kind DatatypesRewriter::getOperatorKindForSygusBuiltin(Node op)
   Assert(op.getKind() != BUILTIN);
   if (op.getKind() == LAMBDA)
   {
-    // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF
-    // does beta-reduction but does not for APPLY
     return APPLY_UF;
   }
   TypeNode tn = op.getType();
@@ -247,7 +245,16 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt,
   Kind ok = NodeManager::operatorToKind(op);
   if (ok != UNDEFINED_KIND)
   {
-    ret = NodeManager::currentNM()->mkNode(ok, schildren);
+    if (ok == APPLY_UF && schildren.size() == 1)
+    {
+      // This case is triggered for defined constant symbols. In this case,
+      // we return the operator itself instead of an APPLY_UF node.
+      ret = schildren[0];
+    }
+    else
+    {
+      ret = NodeManager::currentNM()->mkNode(ok, schildren);
+    }
     Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
     return ret;
   }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 25c0e92aa8605b84000a1c5c6f3cca88590a50ab..c9514dd76b7ecdd0195f74e620e6d187e2c9a3d0 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -414,6 +414,7 @@ set(regress_0_tests
   regress0/decision/wchains010ue.delta02.smt
   regress0/declare-fun-is-match.smt2
   regress0/declare-funs.smt2
+  regress0/define-fun-model.smt2
   regress0/distinct.smt
   regress0/expect/scrub.01.smt
   regress0/expect/scrub.02.smt

diff --git a/test/regress/regress0/define-fun-model.smt2 b/test/regress/regress0/define-fun-model.smt2
new file mode 100644 (file)
index 0000000..c6ca206
--- /dev/null
+++ b/test/regress/regress0/define-fun-model.smt2
@@ -0,0 +1,16 @@
+; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/'
+; EXPECT: sat
+; EXPECT: (((f 4) 7))
+; EXPECT: ((g (lambda ((BOUND_VARIABLE Int)) 7)))
+; EXPECT: ((f (lambda ((BOUND_VARIABLE Int)) 7)))
+(set-logic UFLIA)
+(set-option :produce-models true)
+(define-fun f ((x Int)) Int 7)
+(declare-fun g (Int) Int)
+
+(assert (= (g 5) (f 5)))
+
+(check-sat)
+(get-value ((f 4)))
+(get-value (g))
+(get-value (f))