diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/options | 3 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 7 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 3 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 643 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 95 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 114 | ||||
-rw-r--r-- | src/parser/tptp/tptp_input.cpp | 4 |
8 files changed, 669 insertions, 202 deletions
diff --git a/src/parser/options b/src/parser/options index e16f963f4..f277b231d 100644 --- a/src/parser/options +++ b/src/parser/options @@ -14,9 +14,6 @@ option memoryMap --mmap bool option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking disable ALL semantic checks, including type checks -option szsCompliant --szs-compliant bool :default false - temporary support for szs ontolotogy, print if conjecture is found - # this is just to support security in the online version # (--no-include-file disables filesystem access in TPTP and SMT2 parsers) undocumented-option canIncludeFile /--no-include-file bool :default true diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 684a495b6..cb8c0d4f6 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -90,11 +90,7 @@ Parser* ParserBuilder::build() parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); break; case language::input::LANG_TPTP: - { - Tptp * tparser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly); - tparser->d_szsCompliant = d_szsCompliant; - parser = tparser; - } + parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly); break; default: parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly); @@ -152,7 +148,6 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) { } ParserBuilder& ParserBuilder::withOptions(const Options& options) { - d_szsCompliant = options[options::szsCompliant]; return withInputLanguage(options[options::inputLanguage]) .withMmap(options[options::memoryMap]) diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 9779bf37b..b6e15b2ff 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -80,9 +80,6 @@ class CVC4_PUBLIC ParserBuilder { /** Are we parsing only? */ bool d_parseOnly; - /** hack for szs compliance */ - bool d_szsCompliant; - /** Initialize this parser builder */ void init(ExprManager* exprManager, const std::string& filename); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 16b5bc4ea..c048feea7 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -786,7 +786,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) && args.size() > 2 ) { /* "chainable", but CVC4 internally only supports 2 args */ - expr = MK_EXPR(CVC4::kind::CHAIN, MK_CONST(kind), args); + expr = MK_EXPR(MK_CONST(Chain(kind)), args); } else if( PARSER_STATE->strictModeEnabled() && kind == CVC4::kind::ABS && args.size() == 1 && !args[0].getType().isInteger() ) { /* first, check that ABS is even defined in this logic */ diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 9e814b358..beeca818e 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -27,7 +27,7 @@ options { // Only lookahead of <= k requested (disable for LL* parsing) // Note that CVC4's BoundedTokenBuffer requires a fixed k ! // If you change this k, change it also in tptp_input.cpp ! - k = 1; + k = 2; }/* options */ @header { @@ -102,6 +102,8 @@ using namespace CVC4::parser; #include "util/output.h" #include "util/rational.h" #include <vector> +#include <iterator> +#include <algorithm> using namespace CVC4; using namespace CVC4::parser; @@ -114,12 +116,12 @@ using namespace CVC4::parser; #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR #define MK_EXPR EXPR_MANAGER->mkExpr +#undef MK_EXPR_ASSOCIATIVE +#define MK_EXPR_ASSOCIATIVE EXPR_MANAGER->mkAssociative #undef MK_CONST #define MK_CONST EXPR_MANAGER->mkConst #define UNSUPPORTED PARSER_STATE->unimplementedFeature - - }/* parser::postinclude */ /** @@ -139,46 +141,81 @@ parseCommand returns [CVC4::Command* cmd = NULL] @declarations { Expr expr; Tptp::FormulaRole fr; - std::string name; - std::string incl_args; + 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->cnf=true; PARSER_STATE->pushScope(); } + { PARSER_STATE->cnf = true; PARSER_STATE->fof = false; PARSER_STATE->pushScope(); } cnfFormula[expr] { PARSER_STATE->popScope(); std::vector<Expr> bvl = PARSER_STATE->getFreeVar(); - if(!bvl.empty()){ + if(!bvl.empty()) { expr = MK_EXPR(kind::FORALL,MK_EXPR(kind::BOUND_VAR_LIST,bvl),expr); }; } (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK { - cmd = PARSER_STATE->makeCommand(fr,expr); + cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ true); } | FOF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK - { PARSER_STATE->cnf=false; } + { PARSER_STATE->cnf = false; PARSER_STATE->fof = true; } fofFormula[expr] (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK { - cmd = PARSER_STATE->makeCommand(fr,expr); + cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false); } + | TFF_TOK LPAREN_TOK nameN[name] COMMA_TOK + ( TYPE_TOK COMMA_TOK tffTypedAtom[cmd] + | formulaRole[fr] COMMA_TOK + { PARSER_STATE->cnf = false; PARSER_STATE->fof = false; } + tffFormula[expr] (COMMA_TOK anything*)? + { + cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false); + } + ) RPAREN_TOK DOT_TOK | INCLUDE_TOK LPAREN_TOK unquotedFileName[name] - ( COMMA_TOK LBRACK_TOK nameN[incl_args] ( COMMA_TOK nameN[incl_args] )* RBRACK_TOK )? + ( COMMA_TOK LBRACK_TOK nameN[inclSymbol] + ( COMMA_TOK nameN[inclSymbol] )* RBRACK_TOK )? RPAREN_TOK DOT_TOK - { - PARSER_STATE->includeFile(name); - // The command of the included file will be produce at the new parseCommand call + { /* TODO - implement symbol filtering for file inclusion. + * the following removes duplicates and "all", just need to pass it + * through to includeFile() and implement it there. + std::sort(inclArgs.begin(), inclArgs.end()); + std::vector<std::string>::iterator it = + std::unique(inclArgs.begin(), inclArgs.end()); + inclArgs.resize(std::distance(inclArgs.begin(), it)); + it = std::lower_bound(inclArgs.begin(), inclArgs.end(), std::string("all")); + if(it != inclArgs.end() && *it == "all") { + inclArgs.erase(it); + } + */ + PARSER_STATE->includeFile(name /* , inclArgs */ ); + // The command of the included file will be produced at the new parseCommand call cmd = new EmptyCommand("include::" + name); } | EOF { - PARSER_STATE->preemptCommand(new CheckSatCommand(MK_CONST(bool(true)))); + std::string filename = PARSER_STATE->getInput()->getInputStreamName(); + size_t i = filename.find_last_of('/'); + if(i != std::string::npos) { + filename = filename.substr(i + 1); + } + if(filename.substr(filename.length() - 2) == ".p") { + filename = filename.substr(0, filename.length() - 2); + } + CommandSequence* seq = new CommandSequence(); + seq->addCommand(new SetInfoCommand("name", filename)); + if(PARSER_STATE->hasConjecture()) { + seq->addCommand(new QueryCommand(MK_CONST(bool(false)))); + } else { + seq->addCommand(new CheckSatCommand()); + } + PARSER_STATE->preemptCommand(seq); cmd = NULL; } ; /* Parse a formula Role */ -formulaRole[CVC4::parser::Tptp::FormulaRole & role] +formulaRole[CVC4::parser::Tptp::FormulaRole& role] : LOWER_WORD { std::string r = AntlrInput::tokenText($LOWER_WORD); @@ -204,33 +241,30 @@ formulaRole[CVC4::parser::Tptp::FormulaRole & role] /* CNF */ /* It can parse a little more than the cnf grammar: false and true can appear. - Normally only false can appear and only at top level -*/ + * Normally only false can appear and only at top level. */ cnfFormula[CVC4::Expr& expr] - : - LPAREN_TOK disjunction[expr] RPAREN_TOK -| disjunction[expr] + : LPAREN_TOK cnfDisjunction[expr] RPAREN_TOK + | cnfDisjunction[expr] //| FALSE_TOK { expr = MK_CONST(bool(false)); } ; -disjunction[CVC4::Expr& expr] +cnfDisjunction[CVC4::Expr& expr] @declarations { std::vector<Expr> args; } - : - literal[expr] {args.push_back(expr); } ( OR_TOK literal[expr] {args.push_back(expr); } )* - { - if(args.size() > 1){ - expr = MK_EXPR(kind::OR,args); + : cnfLiteral[expr] { args.push_back(expr); } + ( OR_TOK cnfLiteral[expr] { args.push_back(expr); } )* + { if(args.size() > 1) { + expr = MK_EXPR_ASSOCIATIVE(kind::OR, args); } // else its already in the expr } ; -literal[CVC4::Expr& expr] +cnfLiteral[CVC4::Expr& expr] : atomicFormula[expr] - | NOT_TOK atomicFormula[expr] { expr = MK_EXPR(kind::NOT,expr); } -// | folInfixUnary[expr] + | NOT_TOK atomicFormula[expr] { expr = MK_EXPR(kind::NOT, expr); } +//| folInfixUnary[expr] ; atomicFormula[CVC4::Expr& expr] @@ -241,28 +275,32 @@ atomicFormula[CVC4::Expr& expr] bool equal; } : atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)? - ( ( equalOp[equal] //equality/disequality between terms - { - PARSER_STATE->makeApplication(expr,name,args,true); - } - term[expr2] - { - expr = MK_EXPR(kind::EQUAL, expr, expr2); - if(!equal) expr = MK_EXPR(kind::NOT,expr); - } - ) - | //predicate - { - PARSER_STATE->makeApplication(expr,name,args,false); + ( equalOp[equal] term[expr2] + { // equality/disequality between terms + PARSER_STATE->makeApplication(expr, name, args, true); + expr = MK_EXPR(kind::EQUAL, expr, expr2); + if(!equal) expr = MK_EXPR(kind::NOT, expr); } - ) - | simpleTerm[expr] equalOp[equal] term[expr2] - { + | { // predicate + 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); + } + | (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); + if(!equal) expr = MK_EXPR(kind::NOT, expr); } + | definedPred[expr] LPAREN_TOK arguments[args] RPAREN_TOK + { 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 $$. @@ -270,35 +308,170 @@ definedProp[CVC4::Expr& expr] : TRUE_TOK { expr = MK_CONST(bool(true)); } | FALSE_TOK { expr = MK_CONST(bool(false)); } ; + +definedPred[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' // all "real" are actually "rat" in CVC4 + { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + n = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); + expr = MK_EXPR(CVC4::kind::LAMBDA, n, MK_CONST(bool(true))); + } + | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); } + | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); } + ; + +definedFun[CVC4::Expr& expr] +@declarations { + bool remainder = false; +} + : '$uminus' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::UMINUS); } + | '$sum' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::PLUS); } + | '$difference' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::MINUS); } + | '$product' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::MULT); } + | '$quotient' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DIVISION_TOTAL); } + | ( '$quotient_e' { remainder = false; } + | '$remainder_e' { remainder = true; } + ) + { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType()); + Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d); + expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d); + expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, d, MK_CONST(Rational(0))), + MK_EXPR(CVC4::kind::TO_INTEGER, expr), + MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr)))); + if(remainder) { + expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)); + } + expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + } + | ( '$quotient_t' { remainder = false; } + | '$remainder_t' { remainder = true; } + ) + { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType()); + Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d); + expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d); + expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, expr, MK_CONST(Rational(0))), + MK_EXPR(CVC4::kind::TO_INTEGER, expr), + MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr)))); + if(remainder) { + expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)); + } + expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + } + | ( '$quotient_f' { remainder = false; } + | '$remainder_f' { remainder = true; } + ) + { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType()); + Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d); + expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d); + expr = MK_EXPR(CVC4::kind::TO_INTEGER, expr); + if(remainder) { + expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)); + } + expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + } + | '$floor' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_INTEGER); } + | '$ceiling' + { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); + expr = MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, n))); + expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + } + | '$truncate' + { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); + expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, n, MK_CONST(Rational(0))), + MK_EXPR(CVC4::kind::TO_INTEGER, n), + MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, n)))); + expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + } + | '$round' + { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); + Expr decPart = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::TO_INTEGER, n)); + expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::LT, decPart, MK_CONST(Rational(1, 2))), + // if decPart < 0.5, round down + MK_EXPR(CVC4::kind::TO_INTEGER, n), + MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GT, decPart, MK_CONST(Rational(1, 2))), + // if decPart > 0.5, round up + MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::PLUS, n, MK_CONST(Rational(1)))), + // if decPart == 0.5, round to nearest even integer: + // result is: to_int(n/2 + .5) * 2 + MK_EXPR(CVC4::kind::MULT, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::PLUS, MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, MK_CONST(Rational(2))), MK_CONST(Rational(1, 2)))), MK_CONST(Rational(2))))); + expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + } + | '$to_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_INTEGER); } + | '$to_rat' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_REAL); } + | '$to_real' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_REAL); } + ; + //%----Pure CNF should not use $true or $false in problems, and use $false only //%----at the roots of a refutation. -equalOp[bool & equal] - : EQUAL_TOK {equal = true;} - | DISEQUAL_TOK {equal = false;} +equalOp[bool& equal] + : EQUAL_TOK { equal = true; } + | DISEQUAL_TOK { equal = false; } ; term[CVC4::Expr& expr] - : functionTerm[expr] + : functionTerm[expr] + | conditionalTerm[expr] | simpleTerm[expr] -// | conditionalTerm -// | let_term + | letTerm[expr] + ; + +letTerm[CVC4::Expr& expr] +@declarations { + CVC4::Expr lhs, rhs; +} + : '$let_ft' LPAREN_TOK { PARSER_STATE->pushScope(); } + tffLetFormulaDefn[lhs, rhs] COMMA_TOK + term[expr] + { PARSER_STATE->popScope(); + expr = expr.substitute(lhs, rhs); + } + RPAREN_TOK + | '$let_tt' LPAREN_TOK { PARSER_STATE->pushScope(); } + tffLetTermDefn[lhs, rhs] COMMA_TOK + term[expr] + { PARSER_STATE->popScope(); + expr = expr.substitute(lhs, rhs); + } + RPAREN_TOK ; /* Not an application */ simpleTerm[CVC4::Expr& expr] : variable[expr] | NUMBER { expr = PARSER_STATE->d_tmp_expr; } - | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted( - AntlrInput::tokenText($DISTINCT_OBJECT)); } -; + | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(AntlrInput::tokenText($DISTINCT_OBJECT)); } + ; functionTerm[CVC4::Expr& expr] - : plainTerm[expr] // | <defined_term> | <system_term> +@declarations { + std::vector<CVC4::Expr> args; +} + : plainTerm[expr] + | definedFun[expr] LPAREN_TOK arguments[args] RPAREN_TOK + { expr = EXPR_MANAGER->mkExpr(expr, args); } +// | <system_term> + ; + +conditionalTerm[CVC4::Expr& expr] +@declarations { + CVC4::Expr expr2, expr3; +} + : '$ite_t' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK term[expr2] COMMA_TOK term[expr3] RPAREN_TOK + { expr = EXPR_MANAGER->mkExpr(CVC4::kind::ITE, expr, expr2, expr3); } ; plainTerm[CVC4::Expr& expr] -@declarations{ +@declarations { std::string name; std::vector<Expr> args; } @@ -308,19 +481,19 @@ plainTerm[CVC4::Expr& expr] } ; -arguments[std::vector<CVC4::Expr> & args] -@declarations{ +arguments[std::vector<CVC4::Expr>& args] +@declarations { Expr expr; } : term[expr] { args.push_back(expr); } ( COMMA_TOK term[expr] { args.push_back(expr); } )* ; -variable[CVC4::Expr & expr] +variable[CVC4::Expr& expr] : UPPER_WORD { std::string name = AntlrInput::tokenText($UPPER_WORD); - if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)){ + if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)) { expr = PARSER_STATE->getVariable(name); } else { expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted); @@ -331,18 +504,18 @@ variable[CVC4::Expr & expr] /*******/ /* FOF */ -fofFormula[CVC4::Expr & expr] : fofLogicFormula[expr] ; +fofFormula[CVC4::Expr& expr] : fofLogicFormula[expr] ; -fofLogicFormula[CVC4::Expr & expr] -@declarations{ +fofLogicFormula[CVC4::Expr& expr] +@declarations { tptp::NonAssoc na; std::vector< Expr > args; Expr expr2; } : fofUnitaryFormula[expr] - ( //Non Assoc <=> <~> ~& ~| + ( // Non-associative: <=> <~> ~& ~| ( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2] - { switch(na){ + { switch(na) { case tptp::NA_IFF: expr = MK_EXPR(kind::IFF,expr,expr2); break; @@ -364,21 +537,21 @@ fofLogicFormula[CVC4::Expr & expr] } } ) - | //And & + | // N-ary and & ( { args.push_back(expr); } ( AND_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+ - { expr = MK_EXPR(kind::AND,args); } + { expr = MK_EXPR_ASSOCIATIVE(kind::AND, args); } ) - | //Or | + | // N-ary or | ( { args.push_back(expr); } ( OR_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+ - { expr = MK_EXPR(kind::OR,args); } + { expr = MK_EXPR_ASSOCIATIVE(kind::OR, args); } ) - )? + )? ; -fofUnitaryFormula[CVC4::Expr & expr] -@declarations{ +fofUnitaryFormula[CVC4::Expr& expr] +@declarations { Kind kind; std::vector< Expr > bv; } @@ -389,20 +562,20 @@ fofUnitaryFormula[CVC4::Expr & expr] folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();} ( bindvariable[expr] { bv.push_back(expr); } ( COMMA_TOK bindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK - COLON_TOK fofUnitaryFormula[expr] - { PARSER_STATE->popScope(); - expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr); - } ; + COLON_TOK fofUnitaryFormula[expr] + { PARSER_STATE->popScope(); + expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr); + } + ; -bindvariable[CVC4::Expr & expr] +bindvariable[CVC4::Expr& expr] : UPPER_WORD - { - std::string name = AntlrInput::tokenText($UPPER_WORD); + { std::string name = AntlrInput::tokenText($UPPER_WORD); expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted); } - ; + ; -fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc & na] +fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc& na] : IFF_TOK { na = tptp::NA_IFF; } | REVIFF_TOK { na = tptp::NA_REVIFF; } | REVOR_TOK { na = tptp::NA_REVOR; } @@ -411,11 +584,229 @@ fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc & na] | REVIMPLIES_TOK { na = tptp::NA_REVIMPLIES; } ; -folQuantifier[CVC4::Kind & kind] +folQuantifier[CVC4::Kind& kind] : BANG_TOK { kind = kind::FORALL; } | MARK_TOK { kind = kind::EXISTS; } ; +/*******/ +/* TFF */ +tffFormula[CVC4::Expr& expr] : tffLogicFormula[expr]; + +tffTypedAtom[CVC4::Command*& cmd] +@declarations { + CVC4::Expr expr; + CVC4::Type type; + std::string name; +} + : LPAREN_TOK tffTypedAtom[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); + } + } + | parseType[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 expr; + if(type.isFunction()) { + expr = PARSER_STATE->mkTffFunction(name, type); + } else { + expr = PARSER_STATE->mkTffVar(name, type); + } + cmd = new DeclareFunctionCommand(name, expr, type); + } + } + ) + ; + +tffLogicFormula[CVC4::Expr& expr] +@declarations { + tptp::NonAssoc na; + std::vector< Expr > args; + Expr expr2; +} + : tffUnitaryFormula[expr] + ( // Non Assoc <=> <~> ~& ~| + ( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2] + { switch(na) { + case tptp::NA_IFF: + expr = MK_EXPR(kind::IFF,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; + } + } + ) + | // And & + ( { args.push_back(expr); } + ( AND_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+ + { expr = MK_EXPR(kind::AND,args); } + ) + | // Or | + ( { args.push_back(expr); } + ( OR_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+ + { expr = MK_EXPR(kind::OR,args); } + ) + )? + ; + +tffUnitaryFormula[CVC4::Expr& expr] +@declarations { + Kind kind; + std::vector< Expr > bv; + Expr lhs, rhs; +} + : atomicFormula[expr] + | LPAREN_TOK tffLogicFormula[expr] RPAREN_TOK + | NOT_TOK tffUnitaryFormula[expr] { expr = MK_EXPR(kind::NOT,expr); } + | // Quantified + folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();} + ( tffbindvariable[expr] { bv.push_back(expr); } + ( COMMA_TOK tffbindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK + COLON_TOK tffUnitaryFormula[expr] + { PARSER_STATE->popScope(); + expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr); + } + | '$ite_f' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK tffLogicFormula[lhs] COMMA_TOK tffLogicFormula[rhs] RPAREN_TOK + { expr = EXPR_MANAGER->mkExpr(CVC4::kind::ITE, expr, lhs, rhs); } + | '$let_tf' LPAREN_TOK { PARSER_STATE->pushScope(); } + tffLetTermDefn[lhs, rhs] COMMA_TOK + tffFormula[expr] + { PARSER_STATE->popScope(); + expr = expr.substitute(lhs, rhs); + } + RPAREN_TOK + | '$let_ff' LPAREN_TOK { PARSER_STATE->pushScope(); } + tffLetFormulaDefn[lhs, rhs] COMMA_TOK + tffFormula[expr] + { PARSER_STATE->popScope(); + expr = expr.substitute(lhs, rhs); + } + RPAREN_TOK + ; + +tffLetTermDefn[CVC4::Expr& lhs, CVC4::Expr& rhs] +@declarations { + std::vector<CVC4::Expr> bvlist; +} + : (BANG_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)* + tffLetTermBinding[bvlist, lhs, rhs] + ; + +tffLetTermBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs] + : term[lhs] EQUAL_TOK term[rhs] + { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); + rhs = MK_EXPR(CVC4::kind::LAMBDA, MK_EXPR(CVC4::kind::BOUND_VAR_LIST, lhs.getChildren()), rhs); + lhs = lhs.getOperator(); + } + | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK + ; + +tffLetFormulaDefn[CVC4::Expr& lhs, CVC4::Expr& rhs] +@declarations { + std::vector<CVC4::Expr> bvlist; +} + : (BANG_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)* + tffLetFormulaBinding[bvlist, lhs, rhs] + ; + +tffLetFormulaBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs] + : atomicFormula[lhs] IFF_TOK tffUnitaryFormula[rhs] + { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true); + rhs = MK_EXPR(CVC4::kind::LAMBDA, MK_EXPR(CVC4::kind::BOUND_VAR_LIST, lhs.getChildren()), rhs); + lhs = lhs.getOperator(); + } + | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK + ; + +tffbindvariable[CVC4::Expr& expr] +@declarations { + CVC4::Type type = PARSER_STATE->d_unsorted; +} + : UPPER_WORD + ( COLON_TOK parseType[type] )? + { std::string name = AntlrInput::tokenText($UPPER_WORD); + expr = PARSER_STATE->mkBoundVar(name, type); + } + ; + +// bvlist is accumulative; it can already contain elements +// on the way in, which are left undisturbed +tffVariableList[std::vector<CVC4::Expr>& bvlist] +@declarations { + CVC4::Expr e; +} + : tffbindvariable[e] { bvlist.push_back(e); } + ( COMMA_TOK tffbindvariable[e] { bvlist.push_back(e); } )* + ; + +parseType[CVC4::Type& type] +@declarations { + std::vector<CVC4::Type> v; +} + : simpleType[type] + | ( simpleType[type] { v.push_back(type); } + | LPAREN_TOK simpleType[type] { v.push_back(type); } + ( TIMES_TOK simpleType[type] { v.push_back(type); } )+ + RPAREN_TOK + ) + GREATER_TOK simpleType[type] + { v.push_back(type); + type = EXPR_MANAGER->mkFunctionType(v); + } + ; + +// non-function types +simpleType[CVC4::Type& type] + : DEFINED_SYMBOL + { std::string s = AntlrInput::tokenText($DEFINED_SYMBOL); + if(s == "\$i") type = PARSER_STATE->d_unsorted; + else if(s == "\$o") type = EXPR_MANAGER->booleanType(); + else if(s == "\$int") type = EXPR_MANAGER->integerType(); + else if(s == "\$rat") type = EXPR_MANAGER->realType(); + else if(s == "\$real") type = EXPR_MANAGER->realType(); + else if(s == "\$tType") PARSER_STATE->parseError("Type of types `\$tType' cannot be used here"); + else PARSER_STATE->parseError("unknown defined type `" + s + "'"); + } + | LOWER_WORD + { type = PARSER_STATE->getSort(AntlrInput::tokenText($LOWER_WORD)); } + ; + /***********************************************/ /* Anything well parenthesis */ @@ -447,6 +838,7 @@ anything | FOF_TOK | THF_TOK | TFF_TOK + | TYPE_TOK | INCLUDE_TOK | DISTINCT_OBJECT | UPPER_WORD @@ -467,6 +859,8 @@ LBRACK_TOK : '['; RBRACK_TOK : ']'; COLON_TOK : ':'; +GREATER_TOK : '>'; + //operator OR_TOK : '|'; NOT_TOK : '~'; @@ -494,6 +888,7 @@ CNF_TOK : 'cnf'; FOF_TOK : 'fof'; THF_TOK : 'thf'; TFF_TOK : 'tff'; +TYPE_TOK : 'type'; INCLUDE_TOK : 'include'; //Other defined symbols, must be defined after all the other @@ -533,30 +928,30 @@ UPPER_WORD : UPPER_ALPHA ALPHA_NUMERIC*; LOWER_WORD : LOWER_ALPHA ALPHA_NUMERIC*; /* filename */ -unquotedFileName[std::string & name] /* Beware fileName identifier is used by the backend ... */ +unquotedFileName[std::string& name] /* Beware fileName identifier is used by the backend ... */ : (s=LOWER_WORD_SINGLE_QUOTED | s=SINGLE_QUOTED) { name = AntlrInput::tokenText($s); name = name.substr(1, name.size() - 2 ); }; /* axiom name */ -nameN[std::string & name] +nameN[std::string& name] : atomicWord[name] | NUMBER { name = AntlrInput::tokenText($NUMBER); } ; /* atomic word everything (fof, cnf, thf, tff, include must not be keyword at this position ) */ -atomicWord[std::string & name] +atomicWord[std::string& name] : FOF_TOK { name = "fof"; } | CNF_TOK { name = "cnf"; } | THF_TOK { name = "thf"; } | TFF_TOK { name = "tff"; } + | TYPE_TOK { name = "type"; } | INCLUDE_TOK { name = "include"; } | LOWER_WORD { name = AntlrInput::tokenText($LOWER_WORD); } - | LOWER_WORD_SINGLE_QUOTED //the lower word single quoted are considered without quote - { - /* strip off the quotes */ - name = AntlrInput::tokenTextSubstr($LOWER_WORD_SINGLE_QUOTED,1, + | LOWER_WORD_SINGLE_QUOTED // the lower word single quoted are considered without quote + { /* strip off the quotes */ + name = AntlrInput::tokenTextSubstr($LOWER_WORD_SINGLE_QUOTED, 1 , ($LOWER_WORD_SINGLE_QUOTED->stop - $LOWER_WORD_SINGLE_QUOTED->start) - 1); } | SINGLE_QUOTED {name = AntlrInput::tokenText($SINGLE_QUOTED); }; //for the others the quote remains @@ -565,35 +960,34 @@ atomicWord[std::string & name] /* Rational */ fragment DOT : '.'; -fragment EXPONENT : 'E'|'e'; +fragment EXPONENT : 'E' | 'e'; fragment SLASH : '/'; fragment DECIMAL : NUMERIC+; -/* Currently we put all in the rationnal type */ -fragment SIGN[bool & pos] : PLUS_TOK | MINUS_TOK { pos = false; } ; - +/* Currently we put all in the rational type */ +fragment SIGN[bool& pos] + : PLUS_TOK { pos = true; } + | MINUS_TOK { pos = false; } + ; NUMBER -@declarations{ +@declarations { bool pos = true; bool posE = true; } - : - ( SIGN[pos]? num=DECIMAL - { - Integer i (AntlrInput::tokenText($num)); - Rational r = ( pos ? i : -i ); - PARSER_STATE->d_tmp_expr = MK_CONST(r); - } - | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)? - { - std::string snum = AntlrInput::tokenText($num); + : ( SIGN[pos]? num=DECIMAL + { Integer i(AntlrInput::tokenText($num)); + Rational r = pos ? i : -i; + PARSER_STATE->d_tmp_expr = MK_CONST(r); + } + | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)? + { std::string snum = AntlrInput::tokenText($num); std::string sden = AntlrInput::tokenText($den); /* compute the numerator */ - Integer inum( snum + sden ); + Integer inum(snum + sden); // The sign - inum = pos ? inum : - inum; + inum = pos ? inum : -inum; // The exponent size_t exp = ($e == NULL ? 0 : AntlrInput::tokenToUnsigned($e)); // Decimal part @@ -601,26 +995,25 @@ NUMBER /* multiply it by 10 raised to the exponent reduced by the * number of decimal place in den (dec) */ Rational r; - if( !posE ) r = Rational(inum, Integer(10).pow(exp + dec)); - else if( exp == dec ) r = Rational(inum); - else if( exp > dec ) r = Rational(inum * Integer(10).pow(exp - dec)); + if(!posE) r = Rational(inum, Integer(10).pow(exp + dec)); + else if(exp == dec) r = Rational(inum); + else if(exp > dec) r = Rational(inum * Integer(10).pow(exp - dec)); else r = Rational(inum, Integer(10).pow(dec - exp)); - PARSER_STATE->d_tmp_expr = MK_CONST( r ); + PARSER_STATE->d_tmp_expr = MK_CONST(r); + } + | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL + { Integer inum(AntlrInput::tokenText($num)); + Integer iden(AntlrInput::tokenText($den)); + PARSER_STATE->d_tmp_expr = MK_CONST(Rational(pos ? inum : -inum, iden)); + } + ) + { if(PARSER_STATE->cnf || PARSER_STATE->fof) { + // We're in an unsorted context, so put a conversion around it + PARSER_STATE->d_tmp_expr = PARSER_STATE->convertRatToUnsorted( PARSER_STATE->d_tmp_expr ); } - | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL - { - Integer inum(AntlrInput::tokenText($num)); - Integer iden(AntlrInput::tokenText($den)); - PARSER_STATE->d_tmp_expr = MK_CONST( - Rational(pos ? inum : -inum, iden)); - } - ) { - //Put a convertion around it - PARSER_STATE->d_tmp_expr = PARSER_STATE->convertRatToUnsorted( PARSER_STATE->d_tmp_expr ); } ; - /** * Matches the comments and ignores them */ @@ -629,5 +1022,3 @@ COMMENT | '/*' ( options {greedy=false;} : . )* '*/' { SKIP(); } //comment block ; - - diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 93c2168b1..3e6aa82b7 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -33,26 +33,26 @@ Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn /* Try to find TPTP dir */ // From tptp4x FileUtilities //----Try the TPTP directory, and TPTP variations - char* home = getenv("TPTP"); - if (home == NULL) { - home = getenv("TPTP_HOME"); + char* home = getenv("TPTP"); + if(home == NULL) { + home = getenv("TPTP_HOME"); // //----If no TPTP_HOME, try the tptp user (aaargh) -// if (home == NULL && (PasswdEntry = getpwnam("tptp")) != NULL) { -// home = PasswdEntry->pw_dir; +// if(home == NULL && (PasswdEntry = getpwnam("tptp")) != NULL) { +// home = PasswdEntry->pw_dir; // } //----Now look in the TPTP directory from there - if (home != NULL) { - d_tptpDir = home; - d_tptpDir.append("/TPTP/"); - } - } else { + if(home != NULL) { d_tptpDir = home; - //add trailing "/" - if( d_tptpDir[d_tptpDir.size() - 1] != '/'){ - d_tptpDir.append("/"); - } + d_tptpDir.append("/TPTP/"); } - d_hasConjecture = false; + } else { + d_tptpDir = home; + //add trailing "/" + if(d_tptpDir[d_tptpDir.size() - 1] != '/') { + d_tptpDir.append("/"); + } + } + d_hasConjecture = false; } void Tptp::addTheory(Theory theory) { @@ -92,7 +92,7 @@ void Tptp::addTheory(Theory theory) { /* The include are managed in the lexer but called in the parser */ // Inspired by http://www.antlr3.org/api/C/interop.html -bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){ +bool newInputStream(std::string fileName, pANTLR3_LEXER lexer) { Debug("parser") << "Including " << fileName << std::endl; // Create a new input stream and take advantage of built in stream stacking // in C target runtime. @@ -103,7 +103,7 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){ #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */ in = antlr3FileStreamNew((pANTLR3_UINT8) fileName.c_str(), ANTLR3_ENC_8BIT); #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */ - if( in == NULL ) { + if(in == NULL) { Debug("parser") << "Can't open " << fileName << std::endl; return false; } @@ -126,8 +126,15 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){ return true; } +/* overridden popCharStream for the lexer - necessary if we had symbol + * filtering in file inclusion. +void Tptp::myPopCharStream(pANTLR3_LEXER lexer) { + ((Tptp*)lexer->super)->d_oldPopCharStream(lexer); + ((Tptp*)lexer->super)->popScope(); +} +*/ -void Tptp::includeFile(std::string fileName){ +void Tptp::includeFile(std::string fileName) { // security for online version if(!canIncludeFile()) { parseError("include-file feature was disabled for this run."); @@ -136,36 +143,78 @@ void Tptp::includeFile(std::string fileName){ // Get the lexer AntlrInput * ai = static_cast<AntlrInput *>(getInput()); pANTLR3_LEXER lexer = ai->getAntlr3Lexer(); + + // set up popCharStream - would be necessary for handling symbol + // filtering in inclusions + /* + if(d_oldPopCharStream == NULL) { + d_oldPopCharStream = lexer->popCharStream; + lexer->popCharStream = myPopCharStream; + } + */ + + // push the inclusion scope; will be popped by our special popCharStream + // would be necessary for handling symbol filtering in inclusions + //pushScope(); + // get the name of the current stream "Does it work inside an include?" const std::string inputName = ai->getInputStreamName(); // Test in the directory of the actual parsed file std::string currentDirFileName; - if( inputName != "<stdin>"){ + if(inputName != "<stdin>") { // TODO: Use dirname ot Boost::filesystem? size_t pos = inputName.rfind('/'); - if( pos != std::string::npos){ + if(pos != std::string::npos) { currentDirFileName = std::string(inputName, 0, pos + 1); } currentDirFileName.append(fileName); - if( newInputStream(currentDirFileName,lexer) ){ + if(newInputStream(currentDirFileName,lexer)) { return; } } else { currentDirFileName = "<unknown current directory for stdin>"; } - if( d_tptpDir.empty() ){ + if(d_tptpDir.empty()) { parseError("Couldn't open included file: " + fileName + " at " + currentDirFileName + " and the TPTP directory is not specified (environment variable TPTP)"); }; std::string tptpDirFileName = d_tptpDir + fileName; - if( !newInputStream(tptpDirFileName,lexer) ){ + if(! newInputStream(tptpDirFileName,lexer)) { parseError("Couldn't open included file: " + fileName + " at " + currentDirFileName + " or " + tptpDirFileName); } } +void Tptp::checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula) { + if(lhs.getKind() != CVC4::kind::APPLY_UF) { + parseError("malformed let: LHS must be a flat function application"); + } + std::vector<CVC4::Expr> v = lhs.getChildren(); + if(formula && !lhs.getType().isBoolean()) { + parseError("malformed let: LHS must be formula"); + } + for(size_t i = 0; i < v.size(); ++i) { + if(v[i].hasOperator()) { + parseError("malformed let: LHS must be flat, illegal child: " + v[i].toString()); + } + } + std::sort(v.begin(), v.end()); + std::sort(bvlist.begin(), bvlist.end()); + // ensure all let-bound variables appear on the LHS, and appear only once + for(size_t i = 0; i < bvlist.size(); ++i) { + std::vector<CVC4::Expr>::const_iterator found = std::lower_bound(v.begin(), v.end(), bvlist[i]); + if(found == v.end() || *found != bvlist[i]) { + parseError("malformed let: LHS must make use of all quantified variables, missing `" + bvlist[i].toString() + "'"); + } + std::vector<CVC4::Expr>::const_iterator found2 = found + 1; + if(found2 != v.end() && *found2 == *found) { + parseError("malformed let: LHS cannot use same bound variable twice: " + (*found).toString()); + } + } +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index cea246282..79092e98f 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -25,6 +25,7 @@ #include <ext/hash_set> #include <cassert> #include "parser/options.h" +#include "parser/antlr_input.h" namespace CVC4 { @@ -46,51 +47,57 @@ class Tptp : public Parser { std::hash_set<Expr, ExprHashFunction> d_r_converted; std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects; - //TPTP directory where to find includes + // TPTP directory where to find includes; // empty if none could be determined std::string d_tptpDir; - //hack to make output SZS ontology-compliant + // hack to make output SZS ontology-compliant bool d_hasConjecture; - // hack for szs compliance - bool d_szsCompliant; + + static void myPopCharStream(pANTLR3_LEXER lexer); + void (*d_oldPopCharStream)(pANTLR3_LEXER); public: - bool cnf; //in a cnf formula - void addFreeVar(Expr var){assert(cnf); d_freeVar.push_back(var); }; - std::vector< Expr > getFreeVar(){ + bool cnf; // in a cnf formula + bool fof; // in an fof formula + + void addFreeVar(Expr var) { + assert(cnf); + d_freeVar.push_back(var); + } + std::vector< Expr > getFreeVar() { assert(cnf); std::vector< Expr > r; r.swap(d_freeVar); return r; } - inline Expr convertRatToUnsorted(Expr expr){ + inline Expr convertRatToUnsorted(Expr expr) { ExprManager * em = getExprManager(); // Create the conversion function If they doesn't exists - if(d_rtu_op.isNull()){ + if(d_rtu_op.isNull()) { Type t; - //Conversion from rational to unsorted + // Conversion from rational to unsorted t = em->mkFunctionType(em->realType(), d_unsorted); d_rtu_op = em->mkVar("$$rtu",t); preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t)); - //Conversion from unsorted to rational + // Conversion from unsorted to rational t = em->mkFunctionType(d_unsorted, em->realType()); d_utr_op = em->mkVar("$$utr",t); - preemptCommand(new DeclareFunctionCommand("$$utur", d_utr_op, t)); + preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t)); } // Add the inverse in order to show that over the elements that // appear in the problem there is a bijection between unsorted and // rational Expr ret = em->mkExpr(kind::APPLY_UF,d_rtu_op,expr); - if ( d_r_converted.find(expr) == d_r_converted.end() ){ + if(d_r_converted.find(expr) == d_r_converted.end()) { d_r_converted.insert(expr); - Expr eq = em->mkExpr(kind::EQUAL,expr, - em->mkExpr(kind::APPLY_UF,d_utr_op,ret)); + Expr eq = em->mkExpr(kind::EQUAL, expr, + em->mkExpr(kind::APPLY_UF, d_utr_op, ret)); preemptCommand(new AssertCommand(eq)); - }; + } return ret; } @@ -104,12 +111,13 @@ public: public: - //TPTP (CNF and FOF) is unsorted so we define this common type + // CNF and FOF are unsorted so we define this common type. + // This is also the Type of $i in TFF. Type d_unsorted; enum Theory { THEORY_CORE, - }; + };/* enum Theory */ enum FormulaRole { FR_AXIOM, @@ -126,8 +134,9 @@ public: FR_FI_FUNCTORS, FR_FI_PREDICATES, FR_TYPE, - }; + };/* enum FormulaRole */ + bool hasConjecture() const { return d_hasConjecture; } protected: Tptp(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); @@ -140,10 +149,30 @@ public: */ void addTheory(Theory theory); - inline void makeApplication(Expr & expr, std::string & name, - std::vector<Expr> & args, bool term); + inline void makeApplication(Expr& expr, std::string& name, + std::vector<Expr>& args, bool term); + + inline Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf); + + inline Expr mkTffVar(std::string& name, const Type& type) { + std::string orig = name; + std::stringstream ss; + ss << name << "_0"; + name = ss.str(); + Expr var = mkVar(name, type); + defineFunction(orig, var); + return var; + } - inline Command* makeCommand(FormulaRole fr, Expr & expr); + inline Expr mkTffFunction(std::string& name, const FunctionType& type) { + std::string orig = name; + std::stringstream ss; + ss << name << "_" << type.getArity(); + name = ss.str(); + Expr fun = mkFunction(name, type); + defineFunction(orig, fun); + return fun; + } /** Ugly hack because I don't know how to return an expression from a token */ @@ -153,48 +182,57 @@ public: is reused */ void includeFile(std::string fileName); + /** Check a TPTP let binding for well-formedness. */ + void checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula); + private: void addArithmeticOperators(); };/* class Tptp */ -inline void Tptp::makeApplication(Expr & expr, std::string & name, - std::vector<Expr> & args, bool term){ +inline void Tptp::makeApplication(Expr& expr, std::string& name, + std::vector<Expr>& args, bool term) { // We distinguish the symbols according to their arities std::stringstream ss; ss << name << "_" << args.size(); name = ss.str(); - if(args.empty()){ // Its a constant - if(isDeclared(name)){ //already appeared + 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,true); //levelZero + expr = mkVar(name, t, true); // levelZero preemptCommand(new DeclareFunctionCommand(name, expr, t)); } } else { // Its an application - if(isDeclared(name)){ //already appeared + 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,true); //levelZero + expr = mkVar(name, t, true); // 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); } -}; +} -inline Command* Tptp::makeCommand(FormulaRole fr, Expr & expr){ - //hack for SZS ontology compliance - if(d_szsCompliant && (fr==FR_NEGATED_CONJECTURE || fr==FR_CONJECTURE)){ - if( !d_hasConjecture ){ - d_hasConjecture = true; - std::cout << "conjecture-"; - } +inline Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) { + // For SZS ontology compliance. + // if we're in cnf() though, conjectures don't result in "Theorem" or + // "CounterSatisfiable". + if(!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) { + d_hasConjecture = true; } - switch(fr){ + switch(fr) { case FR_AXIOM: case FR_HYPOTHESIS: case FR_DEFINITION: diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index 34a620187..bfaeb07c9 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -28,9 +28,9 @@ namespace CVC4 { namespace parser { -/* Use lookahead=1 */ +/* Use lookahead=2 */ TptpInput::TptpInput(AntlrInputStream& inputStream) : - AntlrInput(inputStream, 1) { + AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); assert( input != NULL ); |