diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-09-30 13:56:51 -0400 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2013-09-30 13:56:51 -0400 |
commit | 7d2265eb2b5dc96ddff04211959e208b1cb8a7f0 (patch) | |
tree | 26fb270349580c90efe163ca7767bccce6607902 /src/parser/tptp/tptp.h | |
parent | db6df44574927f9b75db664e1e490f757725d13a (diff) | |
parent | 0c2eafec69b694a507ac914bf285fe0574be085f (diff) |
merged golden
Diffstat (limited to 'src/parser/tptp/tptp.h')
-rw-r--r-- | src/parser/tptp/tptp.h | 93 |
1 files changed, 60 insertions, 33 deletions
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 6b7adbbf7..e180d1524 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -24,6 +24,8 @@ #include "util/hash.h" #include <ext/hash_set> #include <cassert> +#include "parser/options.h" +#include "parser/antlr_input.h" namespace CVC4 { @@ -45,46 +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 + bool d_hasConjecture; + + 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; } @@ -98,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, @@ -120,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); @@ -134,10 +149,10 @@ 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); + inline Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf); /** Ugly hack because I don't know how to return an expression from a token */ @@ -147,41 +162,53 @@ 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){ - // 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 +inline void Tptp::makeApplication(Expr& expr, std::string& name, + std::vector<Expr>& args, bool term) { + if(args.empty()) { // Its a constant + if(isDeclared(name)) { // already appeared expr = getVariable(name); } else { Type t = term ? d_unsorted : getExprManager()->booleanType(); - expr = mkVar(name,t,true); //levelZero + expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // 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, ExprManager::VAR_FLAG_GLOBAL); // levelZero preemptCommand(new DeclareFunctionCommand(name, expr, t)); } + // args might be rationals, in which case we need to create + // distinct constants of the "unsorted" sort to represent them + for(size_t i = 0; i < args.size(); ++i) { + if(args[i].getType().isReal() && FunctionType(expr.getType()).getArgTypes()[i] == d_unsorted) { + args[i] = convertRatToUnsorted(args[i]); + } + } expr = getExprManager()->mkExpr(kind::APPLY_UF, expr, args); } -}; +} -inline Command* Tptp::makeCommand(FormulaRole fr, Expr & expr){ - switch(fr){ +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) { case FR_AXIOM: case FR_HYPOTHESIS: case FR_DEFINITION: |