diff options
Diffstat (limited to 'src/parser/tptp/tptp.cpp')
-rw-r--r-- | src/parser/tptp/tptp.cpp | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index c4efe5e09..694369429 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -121,7 +121,7 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer, std::vector< pANT // Same thing as the predefined PUSHSTREAM(in); lexer->pushCharStream(lexer,in); // restart it - //lexer->rec->state->tokenStartCharIndex = -10; + //lexer->rec->state->tokenStartCharIndex = -10; //lexer->emit(lexer); // Note that the input stream is not closed when it EOFs, I don't bother @@ -301,6 +301,27 @@ void Tptp::makeApplication(Expr& expr, std::string& name, } } +void Tptp::mkLambdaWrapper(Expr& expr, Type argType) +{ + std::vector<Expr> lvars; + std::vector<Type> domainTypes = + (static_cast<FunctionType>(argType)).getArgTypes(); + for (unsigned i = 0, size = domainTypes.size(); i < size; ++i) + { + // the introduced variable is internal (not parsable) + std::stringstream ss; + ss << "_lvar_" << i; + Expr v = getExprManager()->mkBoundVar(ss.str(), domainTypes[i]); + lvars.push_back(v); + } + // apply body of lambda to variables + Expr wrapper = getExprManager()->mkExpr( + kind::LAMBDA, + getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars), + getExprManager()->mkExpr(expr, lvars)); + + expr = wrapper; +} Expr Tptp::getAssertionExpr(FormulaRole fr, Expr expr) { switch (fr) { |