Refactor operator applications in the parser (#3831)

This PR refactors how a term is constructed based on information regarding an operator (ParseOp) and its arguments. It also makes a few miscellaneous fixes. This includes:

Indexed ops are carried in ParseOp via api::Op not Expr,
getKindForFunction is limited to "APPLY" kinds from the new API,
The TPTP/SMT2 parsers rely on mkTermInternal for handling associativity.
TPTP should use DIVISION not DIVISION_TOTAL.
This is in preparation for parser migration. These are the essential behavioral changes required for using the new API for the majority of the parser.

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 33ca7bcf2d88f7b04a3178eae14f9a117a92e266..94904f6d95b86df4f4bfe7ceb6573d50cc0f19d3 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1780,8 +1780,9 @@ postfixTerm[CVC4::Expr& f]
     | LPAREN { args.push_back(f); }
       formula[f] { args.push_back(f); }
       ( COMMA formula[f] { args.push_back(f); } )* RPAREN
-      // TODO: check arity
-      { Kind k = PARSER_STATE->getKindForFunction(args.front());
+      { 
+        PARSER_STATE->checkFunctionLike(args.front());
+        Kind k = PARSER_STATE->getKindForFunction(args.front());
         Debug("parser") << "expr is " << args.front() << std::endl;
         Debug("parser") << "kind is " << k << std::endl;
         f = MK_EXPR(k, args);

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index d2577433e4efa60dd5256bb9983d65b8e32921c9..5beec65657cc3d8d1f179504def0069bb590e4a0 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -138,11 +138,6 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) {
 }
 
 Kind Parser::getKindForFunction(Expr fun) {
-  Kind k = getExprManager()->operatorToKind(fun);
-  if (k != UNDEFINED_KIND)
-  {
-    return k;
-  }
   Type t = fun.getType();
   if (t.isFunction())
   {

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index caa3e471f48c943026b45299c3b27f472240be29..a47d58944a98762e2e8ac2f8d0035ec90a0842db 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1973,8 +1973,7 @@ identifier[CVC4::ParseOp& p]
       }
     | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
       {
-        p.d_expr = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals)
-                   .getExpr();
+        p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals);
       }
     )
     RPAREN_TOK

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 48c1c96c7138d0e0aec049c8ccafdb1938cb1c93..ef13d379e9ec80166f820b961fa93ea1b607ed1f 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1634,13 +1634,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
   // First phase: process the operator
   if (Debug.isOn("parser"))
   {
-    Debug("parser") << "Apply parse op to:" << std::endl;
-    Debug("parser") << "args has size " << args.size() << std::endl;
+    Debug("parser") << "applyParseOp: " << p << " to:" << std::endl;
     for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
     {
       Debug("parser") << "++ " << *i << std::endl;
     }
   }
+  api::Op op;
   if (p.d_kind != kind::NULL_EXPR)
   {
     // It is a special case, e.g. tupSel or array constant specification.
@@ -1659,6 +1659,11 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
       kind = fkind;
     }
   }
+  else if (!p.d_op.isNull())
+  {
+    // it was given an operator
+    op = p.d_op;
+  }
   else
   {
     isBuiltinOperator = isOperatorEnabled(p.d_name);
@@ -1808,37 +1813,8 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
         }
       }
     }
-    if (args.size() > 2)
-    {
-      if (kind == kind::INTS_DIVISION || kind == kind::XOR
-          || kind == kind::MINUS || kind == kind::DIVISION
-          || (kind == kind::BITVECTOR_XNOR && v2_6()))
-      {
-        // Builtin operators that are not tokenized, are left associative,
-        // but not internally variadic must set this.
-        return em->mkLeftAssociative(kind, args);
-      }
-      else if (kind == kind::IMPLIES)
-      {
-        /* right-associative, but CVC4 internally only supports 2 args */
-        return em->mkRightAssociative(kind, args);
-      }
-      else if (kind == kind::EQUAL || kind == kind::LT || kind == kind::GT
-               || kind == kind::LEQ || kind == kind::GEQ)
-      {
-        /* "chainable", but CVC4 internally only supports 2 args */
-        return em->mkChain(kind, args);
-      }
-    }
-
-    if (kind::isAssociative(kind) && args.size() > em->maxArity(kind))
-    {
-      /* Special treatment for associative operators with lots of children
-       */
-      return em->mkAssociative(kind, args);
-    }
-    else if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR)
-             && args.size() == 1)
+    if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR)
+        && args.size() == 1)
     {
       // Unary AND/OR can be replaced with the argument.
       return args[0];
@@ -1847,11 +1823,11 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
     {
       return em->mkExpr(kind::UMINUS, args[0]);
     }
-    else
-    {
-      checkOperator(kind, args.size());
-      return em->mkExpr(kind, args);
-    }
+    api::Term ret =
+        d_solver->mkTerm(intToExtKind(kind), api::exprVectorToTerms(args));
+    Debug("parser") << "applyParseOp: return default builtin " << ret
+                    << std::endl;
+    return ret.getExpr();
   }
 
   if (args.size() >= 2)
@@ -1875,6 +1851,12 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
       }
     }
   }
+  if (!op.isNull())
+  {
+    api::Term ret = d_solver->mkTerm(op, api::exprVectorToTerms(args));
+    Debug("parser") << "applyParseOp: return op : " << ret << std::endl;
+    return ret.getExpr();
+  }
   if (kind == kind::NULL_EXPR)
   {
     std::vector<Expr> eargs(args.begin() + 1, args.end());

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index c4b4ddbc05b4e4b5d41509ccf57c36aab05a35cf..873fde25c3c9e7a48921676292921e65ec1d024a 100644 (file)
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -595,7 +595,7 @@ definedFun[CVC4::ParseOp& p]
     }
   | '$quotient'
     {
-      p.d_kind = kind::DIVISION_TOTAL;
+      p.d_kind = kind::DIVISION;
     }
   | ( '$quotient_e' { remainder = false; }
     | '$remainder_e' { remainder = true; }

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 006f20a61dc4db546e9dbae590339526d78c7067..d18e4a77842c6873119ed9abe9afcad760bedb09 100644 (file)
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -241,6 +241,14 @@ Expr Tptp::parseOpToExpr(ParseOp& p)
 
 Expr Tptp::applyParseOp(ParseOp& p, std::vector<Expr>& args)
 {
+  if (Debug.isOn("parser"))
+  {
+    Debug("parser") << "applyParseOp: " << p << " to:" << std::endl;
+    for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+    {
+      Debug("parser") << "++ " << *i << std::endl;
+    }
+  }
   assert(!args.empty());
   ExprManager* em = getExprManager();
   // If operator already defined, just build application
@@ -308,35 +316,6 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector<Expr>& args)
         }
       }
     }
-
-    if (args.size() > 2)
-    {
-      if (kind == kind::INTS_DIVISION || kind == kind::XOR
-          || kind == kind::MINUS || kind == kind::DIVISION)
-      {
-        // Builtin operators that are not tokenized, are left associative,
-        // but not internally variadic must set this.
-        return em->mkLeftAssociative(kind, args);
-      }
-      if (kind == kind::IMPLIES)
-      {
-        /* right-associative, but CVC4 internally only supports 2 args */
-        return em->mkRightAssociative(kind, args);
-      }
-      if (kind == kind::EQUAL || kind == kind::LT || kind == kind::GT
-          || kind == kind::LEQ || kind == kind::GEQ)
-      {
-        /* "chainable", but CVC4 internally only supports 2 args */
-        return em->mkChain(kind, args);
-      }
-    }
-
-    if (kind::isAssociative(kind) && args.size() > em->maxArity(kind))
-    {
-      /* Special treatment for associative operators with lots of children
-       */
-      return em->mkAssociative(kind, args);
-    }
     if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR)
         && args.size() == 1)
     {
@@ -347,8 +326,8 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector<Expr>& args)
     {
       return em->mkExpr(kind::UMINUS, args[0]);
     }
-    checkOperator(kind, args.size());
-    return em->mkExpr(kind, args);
+    return d_solver->mkTerm(intToExtKind(kind), api::exprVectorToTerms(args))
+        .getExpr();
   }
 
   // check if partially applied function, in this case we use HO_APPLY
@@ -368,7 +347,8 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector<Expr>& args)
         Debug("parser") << " : #argTypes = " << arity;
         Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
         // must curry the partial application
-        return em->mkLeftAssociative(kind::HO_APPLY, args);
+        return d_solver->mkTerm(api::HO_APPLY, api::exprVectorToTerms(args))
+            .getExpr();
       }
     }
   }