diff options
Diffstat (limited to 'src/parser/tptp/Tptp.g')
| -rw-r--r-- | src/parser/tptp/Tptp.g | 527 |
1 files changed, 488 insertions, 39 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 758198e0d..599b3bbe1 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -148,7 +148,6 @@ parseCommand returns [CVC4::Command* cmd = NULL] Tptp::FormulaRole fr; std::string name, inclSymbol; } -// : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; } : CNF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK { PARSER_STATE->setCnf(true); PARSER_STATE->setFof(false); @@ -203,6 +202,26 @@ parseCommand returns [CVC4::Command* cmd = NULL] cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); } ) RPAREN_TOK DOT_TOK + | THF_TOK LPAREN_TOK nameN[name] COMMA_TOK + // Supported THF formulas: either a logic formula or a typing atom (i.e. we + // ignore subtyping and logic sequents). Also, only TH0 + ( TYPE_TOK COMMA_TOK thfAtomTyping[cmd] + | formulaRole[fr] COMMA_TOK + { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(false); } + thfLogicFormula[expr] (COMMA_TOK anything*)? + { + Expr aexpr = PARSER_STATE->getAssertionExpr(fr,expr); + if (!aexpr.isNull()) + { + // set the expression name (e.g. used with unsat core printing) + Command* csen = new SetExpressionNameCommand(aexpr, name); + csen->setMuted(true); + PARSER_STATE->preemptCommand(csen); + } + // make the command to assert the formula + cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); + } + ) RPAREN_TOK DOT_TOK | INCLUDE_TOK LPAREN_TOK unquotedFileName[name] ( COMMA_TOK LBRACK_TOK nameN[inclSymbol] ( COMMA_TOK nameN[inclSymbol] )* RBRACK_TOK )? @@ -226,13 +245,13 @@ parseCommand returns [CVC4::Command* cmd = NULL] | EOF { CommandSequence* seq = new CommandSequence(); - // assert that all distinct constants are distinct + // assert that all distinct constants are distinct Expr aexpr = PARSER_STATE->getAssertionDistinctConstants(); if( !aexpr.isNull() ) { seq->addCommand(new AssertCommand(aexpr, false)); } - + std::string filename = PARSER_STATE->getInput()->getInputStreamName(); size_t i = filename.find_last_of('/'); if(i != std::string::npos) { @@ -284,7 +303,6 @@ formulaRole[CVC4::parser::Tptp::FormulaRole& role] cnfFormula[CVC4::Expr& expr] : LPAREN_TOK cnfDisjunction[expr] RPAREN_TOK | cnfDisjunction[expr] -//| FALSE_TOK { expr = MK_CONST(bool(false)); } ; cnfDisjunction[CVC4::Expr& expr] @@ -302,7 +320,6 @@ cnfDisjunction[CVC4::Expr& expr] cnfLiteral[CVC4::Expr& expr] : atomicFormula[expr] | NOT_TOK atomicFormula[expr] { expr = MK_EXPR(kind::NOT, expr); } -//| folInfixUnary[expr] ; atomicFormula[CVC4::Expr& expr] @@ -323,22 +340,77 @@ atomicFormula[CVC4::Expr& expr] PARSER_STATE->makeApplication(expr, name, args, false); } ) - | definedFun[expr] LPAREN_TOK arguments[args] RPAREN_TOK - equalOp[equal] term[expr2] - { expr = EXPR_MANAGER->mkExpr(expr, args); - expr = MK_EXPR(kind::EQUAL, expr, expr2); - if(!equal) expr = MK_EXPR(kind::NOT, expr); - } + | definedFun[expr] + ( + LPAREN_TOK arguments[args] RPAREN_TOK + equalOp[equal] term[expr2] + { + expr = EXPR_MANAGER->mkExpr(expr, args); + expr = MK_EXPR(kind::EQUAL, expr, expr2); + if (!equal) + { + expr = MK_EXPR(kind::NOT, expr); + } + } + )? | (simpleTerm[expr] | letTerm[expr] | conditionalTerm[expr]) - equalOp[equal] term[expr2] - { // equality/disequality between terms - expr = MK_EXPR(kind::EQUAL, expr, expr2); - if(!equal) expr = MK_EXPR(kind::NOT, expr); + ( + equalOp[equal] term[expr2] + { // equality/disequality between terms + expr = MK_EXPR(kind::EQUAL, expr, expr2); + if (!equal) + { + expr = MK_EXPR(kind::NOT, expr); + } + } + )? + | definedPred[expr] (LPAREN_TOK arguments[args] RPAREN_TOK)? + { + if (!args.empty()) + { + expr = EXPR_MANAGER->mkExpr(expr, args); + } } - | definedPred[expr] LPAREN_TOK arguments[args] RPAREN_TOK - { expr = EXPR_MANAGER->mkExpr(expr, args); } | definedProp[expr] ; + +thfAtomicFormula[CVC4::Expr& expr] +@declarations { + Expr expr2; + std::string name; + std::vector<CVC4::Expr> args; + bool equal; +} + : atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)? + { + PARSER_STATE->makeApplication(expr, name, args, true); + } + | definedFun[expr] + ( + LPAREN_TOK arguments[args] RPAREN_TOK + equalOp[equal] term[expr2] + { + expr = EXPR_MANAGER->mkExpr(expr, args); + expr = MK_EXPR(kind::EQUAL, expr, expr2); + if (!equal) + { + expr = MK_EXPR(kind::NOT, expr); + } + } + )? + | thfSimpleTerm[expr] + | letTerm[expr] + | conditionalTerm[expr] + | thfDefinedPred[expr] (LPAREN_TOK arguments[args] RPAREN_TOK)? + { + if (!args.empty()) + { + expr = EXPR_MANAGER->mkExpr(expr, args); + } + } + | definedProp[expr] + ; + //%----Using <plain_term> removes a reduce/reduce ambiguity in lex/yacc. //%----Note: "defined" means a word starting with one $ and "system" means $$. @@ -373,6 +445,45 @@ definedPred[CVC4::Expr& expr] } | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); } | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); } + | AND_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::AND); } + | IMPLIES_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IMPLIES); } + | OR_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::OR); } + ; + +thfDefinedPred[CVC4::Expr& expr] + : '$less' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LT); } + | '$lesseq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LEQ); } + | '$greater' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GT); } + | '$greatereq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GEQ); } + | '$is_rat' + // a real n is a rational if there exists q,r integers such that + // to_real(q) = n*to_real(r), + // where r is non-zero. + { + Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType()); + Expr qr = MK_EXPR(CVC4::kind::TO_REAL, q); + Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType()); + Expr rr = MK_EXPR(CVC4::kind::TO_REAL, r); + Expr body = MK_EXPR( + CVC4::kind::AND, + MK_EXPR(CVC4::kind::NOT, + MK_EXPR(CVC4::kind::EQUAL, r, MK_CONST(Rational(0)))), + MK_EXPR(CVC4::kind::EQUAL, qr, MK_EXPR(CVC4::kind::MULT, n, rr))); + Expr bvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, q, r); + body = MK_EXPR(CVC4::kind::EXISTS, bvl, body); + Expr lbvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); + expr = MK_EXPR(CVC4::kind::LAMBDA, lbvl, body); + } + | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); } + | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); } + | LPAREN_TOK + ( + AND_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::AND); } + | OR_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::OR); } + | IMPLIES_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IMPLIES); } + ) + RPAREN_TOK ; definedFun[CVC4::Expr& expr] @@ -504,6 +615,16 @@ simpleTerm[CVC4::Expr& expr] | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(AntlrInput::tokenText($DISTINCT_OBJECT)); } ; +/* Not an application */ +thfSimpleTerm[CVC4::Expr& expr] + : NUMBER { expr = PARSER_STATE->d_tmp_expr; } + | DISTINCT_OBJECT + { + expr = PARSER_STATE->convertStrToUnsorted( + AntlrInput::tokenText($DISTINCT_OBJECT)); + } + ; + functionTerm[CVC4::Expr& expr] @declarations { std::vector<CVC4::Expr> args; @@ -637,8 +758,283 @@ fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc& na] ; folQuantifier[CVC4::Kind& kind] - : BANG_TOK { kind = kind::FORALL; } - | MARK_TOK { kind = kind::EXISTS; } + : FORALL_TOK { kind = kind::FORALL; } + | EXISTS_TOK { kind = kind::EXISTS; } + ; + +/*******/ +/* THF */ + +thfQuantifier[CVC4::Kind& kind] + : FORALL_TOK { kind = kind::FORALL; } + | EXISTS_TOK { kind = kind::EXISTS; } + | LAMBDA_TOK { kind = kind::LAMBDA; } + | CHOICE_TOK { kind = kind::CHOICE; } + | DEF_DESC_TOK + { + UNSUPPORTED("Description quantifier"); + } + | (TH1_UN_A | TH1_UN_E) + { + UNSUPPORTED("TH1 operator"); + } + ; + +thfAtomTyping[CVC4::Command*& cmd] +// for now only supports mapping types (i.e. no applied types) +@declarations { + CVC4::Expr expr; + CVC4::Type type; + std::string name; +} + : LPAREN_TOK thfAtomTyping[cmd] RPAREN_TOK + | nameN[name] COLON_TOK + ( '$tType' + { + if (PARSER_STATE->isDeclared(name, SYM_SORT)) + { + // duplicate declaration is fine, they're compatible + cmd = new EmptyCommand("compatible redeclaration of sort " + name); + } + else if (PARSER_STATE->isDeclared(name, SYM_VARIABLE)) + { + // error: cannot be both sort and constant + PARSER_STATE->parseError( + "Symbol `" + name + + "' previously declared as a constant; cannot also be a sort"); + } + else + { + // as yet, it's undeclared + Type type = PARSER_STATE->mkSort(name); + cmd = new DeclareTypeCommand(name, 0, type); + } + } + | parseThfType[type] + { + if (PARSER_STATE->isDeclared(name, SYM_SORT)) + { + // error: cannot be both sort and constant + PARSER_STATE->parseError("Symbol `" + name + + "' previously declared as a sort"); + cmd = new EmptyCommand("compatible redeclaration of sort " + name); + } + else if (PARSER_STATE->isDeclared(name, SYM_VARIABLE)) + { + if (type == PARSER_STATE->getVariable(name).getType()) + { + // duplicate declaration is fine, they're compatible + cmd = new EmptyCommand("compatible redeclaration of constant " + + name); + } + else + { + // error: sorts incompatible + PARSER_STATE->parseError( + "Symbol `" + name + + "' declared previously with a different sort"); + } + } + else + { + // as yet, it's undeclared + CVC4::Expr freshExpr; + if (type.isFunction()) + { + freshExpr = PARSER_STATE->mkFunction(name, type); + } + else + { + freshExpr = PARSER_STATE->mkVar(name, type); + } + cmd = new DeclareFunctionCommand(name, freshExpr, type); + } + } + ) + ; + +thfLogicFormula[CVC4::Expr& expr] +@declarations { + tptp::NonAssoc na; + std::vector< Expr > args; + Expr expr2; + bool equal; +} + //prefix unary formula case + // ~ + : thfUnitaryFormula[expr] + ( // Equality: = + equalOp[equal] + thfUnitaryFormula[expr2] + { + if (expr.getKind() == kind::BUILTIN && expr2.getKind() != kind::BUILTIN) + { + // make expr with a lambda of the same type as expr + PARSER_STATE->mkLambdaWrapper(expr, expr2.getType()); + } + else if (expr2.getKind() == kind::BUILTIN + && expr.getKind() != kind::BUILTIN) + { + // make expr2 with a lambda of the same type as expr + PARSER_STATE->mkLambdaWrapper(expr2, expr.getType()); + } + else if (expr.getKind() == kind::BUILTIN + && expr2.getKind() == kind::BUILTIN) + { + // TODO create whatever lambda + } + expr = MK_EXPR(kind::EQUAL, expr, expr2); + if (!equal) + { + expr = MK_EXPR(kind::NOT, expr); + } + } + | // Non-associative: <=> <~> ~& ~| + fofBinaryNonAssoc[na] thfUnitaryFormula[expr2] + { + switch(na) { + case tptp::NA_IFF: + expr = MK_EXPR(kind::EQUAL,expr,expr2); + break; + case tptp::NA_REVIFF: + expr = MK_EXPR(kind::XOR,expr,expr2); + break; + case tptp::NA_IMPLIES: + expr = MK_EXPR(kind::IMPLIES,expr,expr2); + break; + case tptp::NA_REVIMPLIES: + expr = MK_EXPR(kind::IMPLIES,expr2,expr); + break; + case tptp::NA_REVOR: + expr = MK_EXPR(kind::NOT,MK_EXPR(kind::OR,expr,expr2)); + break; + case tptp::NA_REVAND: + expr = MK_EXPR(kind::NOT,MK_EXPR(kind::AND,expr,expr2)); + break; + } + } + | // N-ary and & + ( { args.push_back(expr); } + ( AND_TOK thfUnitaryFormula[expr] { args.push_back(expr); } )+ + { + expr = MK_EXPR_ASSOCIATIVE(kind::AND, args); + } + ) + | // N-ary or | + ( { args.push_back(expr); } + ( OR_TOK thfUnitaryFormula[expr] { args.push_back(expr); } )+ + { + expr = MK_EXPR_ASSOCIATIVE(kind::OR, args); + } + ) + | // N-ary @ | + // + // @ (denoting apply) is left-associative and lambda is right-associative. + // ^ [X] : ^ [Y] : f @ g (where f is a <thf_apply_formula> and g is a + // <thf_unitary_formula>) should be parsed as: (^ [X] : (^ [Y] : f)) @ g. + // That is, g is not in the scope of either lambda. + { args.push_back(expr); } + ( APP_TOK + ( + thfUnitaryFormula[expr] { args.push_back(expr); } + | LBRACK_TOK + { UNSUPPORTED("Tuple terms"); } + thfTupleForm[args] + RBRACK_TOK + ) + )+ + { + expr = args[0]; + // also add case for total applications + if (expr.getKind() == kind::BUILTIN) + { + args.erase(args.begin()); + expr = EXPR_MANAGER->mkExpr(expr, args); + } + else + { + // check if any argument is a bultin node, e.g. "~", and create a + // lambda wrapper then, e.g. (\lambda x. ~ x) + for (unsigned i = 1; i < args.size(); ++i) + { + // create a lambda wrapper, e.g. (\lambda x. ~ x) + if (args[i].getKind() != kind::BUILTIN) + { + continue; + } + PARSER_STATE->mkLambdaWrapper( + args[i], + (static_cast<FunctionType>(args[0].getType())) + .getArgTypes()[i - 1]); + } + for (unsigned i = 1; i < args.size(); ++i) + { + expr = MK_EXPR(kind::HO_APPLY, expr, args[i]); + } + } + } + )? + ; + +thfTupleForm[std::vector<CVC4::Expr>& args] +@declarations { + Expr expr; +} + : thfUnitaryFormula[expr] + { args.push_back(expr); } + ( COMMA_TOK thfUnitaryFormula[expr] { args.push_back(expr); } )+ +; + +thfUnitaryFormula[CVC4::Expr& expr] +@declarations { + Kind kind; + std::vector< Expr > bv; + Expr expr2; + bool equal; +} + : variable[expr] + | thfAtomicFormula[expr] + | LPAREN_TOK + thfLogicFormula[expr] + RPAREN_TOK + | NOT_TOK + { expr = EXPR_MANAGER->operatorOf(CVC4::kind::NOT); } + (thfUnitaryFormula[expr2] { expr = MK_EXPR(expr,expr2); })? + | // Quantified + thfQuantifier[kind] + LBRACK_TOK {PARSER_STATE->pushScope();} + thfBindVariable[expr] + { + bv.push_back(expr); + } + ( COMMA_TOK thfBindVariable[expr] + { + bv.push_back(expr); + } + )* + RBRACK_TOK COLON_TOK + thfUnitaryFormula[expr] + { + PARSER_STATE->popScope(); + // handle lambda case, in which return type must be flattened and the + // auxiliary variables introduced in the proccess must be added no the + // variable list + // + // see documentation of mkFlatFunctionType for how it's done + // + // flatten body via flattening its type + std::vector<Type> sorts; + std::vector<Expr> flattenVars; + PARSER_STATE->mkFlatFunctionType(sorts, expr.getType(), flattenVars); + if (!flattenVars.empty()) + { + // apply body of lambda to flatten vars + expr = PARSER_STATE->mkHoApply(expr, flattenVars); + // add variables to BOUND_VAR_LIST + bv.insert(bv.end(), flattenVars.begin(), flattenVars.end()); + } + expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr); + } ; /*******/ @@ -776,7 +1172,7 @@ tffLetTermDefn[CVC4::Expr& lhs, CVC4::Expr& rhs] @declarations { std::vector<CVC4::Expr> bvlist; } - : (BANG_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)* + : (FORALL_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)* tffLetTermBinding[bvlist, lhs, rhs] ; @@ -793,7 +1189,7 @@ tffLetFormulaDefn[CVC4::Expr& lhs, CVC4::Expr& rhs] @declarations { std::vector<CVC4::Expr> bvlist; } - : (BANG_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)* + : (FORALL_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)* tffLetFormulaBinding[bvlist, lhs, rhs] ; @@ -806,6 +1202,20 @@ tffLetFormulaBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Exp | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK ; +thfBindVariable[CVC4::Expr& expr] +@declarations { + std::string name; + CVC4::Type type = PARSER_STATE->d_unsorted; +} + : UPPER_WORD + { name = AntlrInput::tokenText($UPPER_WORD); } + ( COLON_TOK parseThfType[type] )? + { + expr = PARSER_STATE->mkBoundVar(name, type); + } + ; + + tffbindvariable[CVC4::Expr& expr] @declarations { CVC4::Type type = PARSER_STATE->d_unsorted; @@ -827,8 +1237,39 @@ tffVariableList[std::vector<CVC4::Expr>& bvlist] ( COMMA_TOK tffbindvariable[e] { bvlist.push_back(e); } )* ; -parseType[CVC4::Type& type] +parseThfType[CVC4::Type& type] +// assumes only mapping types (arrows), no tuple type @declarations { + std::vector<CVC4::Type> sorts; +} + : thfType[type] { sorts.push_back(type); } + ( + (ARROW_TOK | TIMES_TOK) thfType[type] { sorts.push_back(type); } + )* + { + if (sorts.size() < 1) + { + type = sorts[0]; + } + else + { + Type range = sorts.back(); + sorts.pop_back(); + type = PARSER_STATE->mkFlatFunctionType(sorts, range); + } + } + ; + +thfType[CVC4::Type& type] +// assumes only mapping types (arrows), no tuple type + : simpleType[type] + | LPAREN_TOK parseThfType[type] RPAREN_TOK + | LBRACK_TOK { UNSUPPORTED("Tuple types"); } parseThfType[type] RBRACK_TOK + ; + +parseType[CVC4::Type & type] +@declarations +{ std::vector<CVC4::Type> v; } : simpleType[type] @@ -837,7 +1278,7 @@ parseType[CVC4::Type& type] ( TIMES_TOK simpleType[type] { v.push_back(type); } )+ RPAREN_TOK ) - GREATER_TOK simpleType[type] + ARROW_TOK simpleType[type] { v.push_back(type); type = EXPR_MANAGER->mkFunctionType(v); } @@ -873,8 +1314,8 @@ anything | COLON_TOK | OR_TOK | NOT_TOK - | BANG_TOK - | MARK_TOK + | FORALL_TOK + | EXISTS_TOK | AND_TOK | IFF_TOK | IMPLIES_TOK @@ -914,23 +1355,32 @@ LBRACK_TOK : '['; RBRACK_TOK : ']'; COLON_TOK : ':'; -GREATER_TOK : '>'; +// typing +ARROW_TOK : '>'; +SUBTYPE_TOK : '>>'; //operator -OR_TOK : '|'; -NOT_TOK : '~'; -BANG_TOK : '!'; -MARK_TOK : '?'; -AND_TOK : '&'; -IFF_TOK : '<=>'; +OR_TOK : '|'; +NOT_TOK : '~'; +FORALL_TOK : '!'; +EXISTS_TOK : '?'; +LAMBDA_TOK : '^'; +CHOICE_TOK : '@+'; +DEF_DESC_TOK : '@-'; +AND_TOK : '&'; +IFF_TOK : '<=>'; IMPLIES_TOK : '=>'; REVIMPLIES_TOK : '<='; -REVIFF_TOK : '<~>'; -REVOR_TOK : '~|'; -REVAND_TOK : '~&'; -TIMES_TOK : '*'; -PLUS_TOK : '+'; -MINUS_TOK : '-'; +REVIFF_TOK : '<~>'; +REVOR_TOK : '~|'; +REVAND_TOK : '~&'; +TIMES_TOK : '*'; +PLUS_TOK : '+'; +MINUS_TOK : '-'; +APP_TOK : '@'; + +TH1_UN_A : '!!'; +TH1_UN_E : '??'; //predicate TRUE_TOK : '$true'; @@ -1076,4 +1526,3 @@ COMMENT : '%' (~('\n' | '\r'))* { SKIP(); } //comment line | '/*' ( options {greedy=false;} : . )* '*/' { SKIP(); } //comment block ; - |