summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/options3
-rw-r--r--src/parser/parser_builder.cpp7
-rw-r--r--src/parser/parser_builder.h3
-rw-r--r--src/parser/smt2/Smt2.g2
-rw-r--r--src/parser/tptp/Tptp.g643
-rw-r--r--src/parser/tptp/tptp.cpp95
-rw-r--r--src/parser/tptp/tptp.h114
-rw-r--r--src/parser/tptp/tptp_input.cpp4
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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback