summaryrefslogtreecommitdiff
path: root/src/parser/tptp/tptp.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/tptp/tptp.cpp')
-rw-r--r--src/parser/tptp/tptp.cpp192
1 files changed, 160 insertions, 32 deletions
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 694369429..71a3e4bee 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -22,6 +22,7 @@
#include "api/cvc4cpp.h"
#include "expr/type.h"
+#include "options/options.h"
#include "parser/parser.h"
// ANTLR defines these, which is really bad!
@@ -214,6 +215,165 @@ void Tptp::checkLetBinding(const std::vector<Expr>& bvlist, Expr lhs, Expr rhs,
}
}
+Expr Tptp::parseOpToExpr(ParseOp& p)
+{
+ Expr expr;
+ if (!p.d_expr.isNull())
+ {
+ return p.d_expr;
+ }
+ // if it has a kind, it's a builtin one
+ if (p.d_kind != kind::NULL_EXPR)
+ {
+ return getExprManager()->operatorOf(p.d_kind);
+ }
+ if (isDeclared(p.d_name))
+ { // already appeared
+ expr = getVariable(p.d_name);
+ }
+ else
+ {
+ Type t =
+ p.d_type == getExprManager()->booleanType() ? p.d_type : d_unsorted;
+ expr = mkVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
+ preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t));
+ }
+ return expr;
+}
+
+Expr Tptp::applyParseOp(ParseOp& p, std::vector<Expr>& args)
+{
+ assert(!args.empty());
+ bool isBuiltinOperator = false;
+ // the builtin kind of the overall return expression
+ Kind kind = kind::NULL_EXPR;
+ // First phase: process the operator
+ ExprManager* em = getExprManager();
+ // If operator already defined, just build application
+ if (!p.d_expr.isNull())
+ {
+ return em->mkExpr(p.d_expr, args);
+ }
+ // Otherwise piece operator together
+ if (p.d_kind == kind::NULL_EXPR)
+ {
+ // A non-built-in function application, get the expression
+ Expr v;
+ if (isDeclared(p.d_name))
+ { // already appeared
+ v = getVariable(p.d_name);
+ }
+ else
+ {
+ std::vector<Type> sorts(args.size(), d_unsorted);
+ Type t = p.d_type == em->booleanType() ? p.d_type : d_unsorted;
+ t = getExprManager()->mkFunctionType(sorts, t);
+ v = mkVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
+ preemptCommand(new DeclareFunctionCommand(p.d_name, v, t));
+ }
+ // args might be rationals, in which case we need to create
+ // distinct constants of the "unsorted" sort to represent them
+ for (size_t i = 0; i < args.size(); ++i)
+ {
+ if (args[i].getType().isReal()
+ && FunctionType(v.getType()).getArgTypes()[i] == d_unsorted)
+ {
+ args[i] = convertRatToUnsorted(args[i]);
+ }
+ }
+ assert(!v.isNull());
+ checkFunctionLike(v);
+ kind = getKindForFunction(v);
+ args.insert(args.begin(), v);
+ }
+ else
+ {
+ kind = p.d_kind;
+ isBuiltinOperator = true;
+ }
+ assert(kind != kind::NULL_EXPR);
+ // Second phase: apply the arguments to the parse op
+ if (isBuiltinOperator)
+ {
+ if (!em->getOptions().getUfHo()
+ && (kind == kind::EQUAL || kind == kind::DISTINCT))
+ {
+ // need --uf-ho if these operators are applied over function args
+ for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+ {
+ if ((*i).getType().isFunction())
+ {
+ parseError(
+ "Cannot apply equalty to functions unless --uf-ho is set.");
+ }
+ }
+ }
+ 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->mkExpr(em->mkConst(Chain(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)
+ {
+ // Unary AND/OR can be replaced with the argument.
+ return args[0];
+ }
+ if (kind == kind::MINUS && args.size() == 1)
+ {
+ return em->mkExpr(kind::UMINUS, args[0]);
+ }
+ checkOperator(kind, args.size());
+ return em->mkExpr(kind, args);
+ }
+
+ // check if partially applied function, in this case we use HO_APPLY
+ if (args.size() >= 2)
+ {
+ Type argt = args[0].getType();
+ if (argt.isFunction())
+ {
+ unsigned arity = static_cast<FunctionType>(argt).getArity();
+ if (args.size() - 1 < arity)
+ {
+ if (!em->getOptions().getUfHo())
+ {
+ parseError("Cannot partially apply functions unless --uf-ho is set.");
+ }
+ Debug("parser") << "Partial application of " << args[0];
+ 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 em->mkExpr(kind, args);
+}
+
void Tptp::forceLogic(const std::string& logic)
{
Parser::forceLogic(logic);
@@ -269,38 +429,6 @@ Expr Tptp::convertStrToUnsorted(std::string str) {
return e;
}
-void Tptp::makeApplication(Expr& expr, std::string& name,
- std::vector<Expr>& args, bool term) {
- if (args.empty()) { // Its a constant
- if (isDeclared(name)) { // already appeared
- expr = getVariable(name);
- } else {
- Type t = term ? d_unsorted : getExprManager()->booleanType();
- expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
- preemptCommand(new DeclareFunctionCommand(name, expr, t));
- }
- } else { // Its an application
- if (isDeclared(name)) { // already appeared
- expr = getVariable(name);
- } else {
- std::vector<Type> sorts(args.size(), d_unsorted);
- Type t = term ? d_unsorted : getExprManager()->booleanType();
- t = getExprManager()->mkFunctionType(sorts, t);
- expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
- preemptCommand(new DeclareFunctionCommand(name, expr, t));
- }
- // args might be rationals, in which case we need to create
- // distinct constants of the "unsorted" sort to represent them
- for (size_t i = 0; i < args.size(); ++i) {
- if (args[i].getType().isReal() &&
- FunctionType(expr.getType()).getArgTypes()[i] == d_unsorted) {
- args[i] = convertRatToUnsorted(args[i]);
- }
- }
- expr = getExprManager()->mkExpr(kind::APPLY_UF, expr, args);
- }
-}
-
void Tptp::mkLambdaWrapper(Expr& expr, Type argType)
{
std::vector<Expr> lvars;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback