diff options
Diffstat (limited to 'src/parser/tptp')
-rw-r--r-- | src/parser/tptp/Tptp.g | 2 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 44 |
2 files changed, 13 insertions, 33 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index c4b4ddbc0..873fde25c 100644 --- 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 006f20a61..d18e4a778 100644 --- 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(); } } } |