From e76b70bfa6053b8de7868e595cbe6317ae0ef11c Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 26 Sep 2017 11:26:40 -0700 Subject: [PATCH] Fixing Cid 1172009 (#1141) --- src/parser/tptp/Tptp.g | 14 +-- src/parser/tptp/tptp.cpp | 113 +++++++++++++++++++++++ src/parser/tptp/tptp.h | 194 ++++++++++----------------------------- 3 files changed, 167 insertions(+), 154 deletions(-) diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index fbd3d8cfb..8163eb239 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -158,7 +158,9 @@ parseCommand returns [CVC4::Command* cmd = NULL] } // : 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->fof = false; PARSER_STATE->pushScope(); } + { PARSER_STATE->setCnf(true); + PARSER_STATE->setFof(false); + PARSER_STATE->pushScope(); } cnfFormula[expr] { PARSER_STATE->popScope(); std::vector bvl = PARSER_STATE->getFreeVar(); @@ -171,7 +173,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] 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->fof = true; } + { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(true); } fofFormula[expr] (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK { cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false); @@ -179,7 +181,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] | 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; } + { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(false); } tffFormula[expr] (COMMA_TOK anything*)? { cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false); @@ -506,11 +508,11 @@ 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); - if(PARSER_STATE->cnf) PARSER_STATE->addFreeVar(expr); + if(PARSER_STATE->cnf()) PARSER_STATE->addFreeVar(expr); } } ; @@ -1023,7 +1025,7 @@ NUMBER PARSER_STATE->d_tmp_expr = MK_CONST(Rational(pos ? inum : -inum, iden)); } ) - { if(PARSER_STATE->cnf || PARSER_STATE->fof) { + { 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 ); } diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 719f2f38e..a01de9df4 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -231,5 +231,118 @@ void Tptp::checkLetBinding(std::vector& bvlist, Expr lhs, Expr rhs, bool f } } +void Tptp::addFreeVar(Expr var) { + assert(cnf()); + d_freeVar.push_back(var); +} + +std::vector Tptp::getFreeVar() { + assert(cnf()); + std::vector r; + r.swap(d_freeVar); + return r; +} + +Expr Tptp::convertRatToUnsorted(Expr expr) { + ExprManager* em = getExprManager(); + + // Create the conversion function If they doesn't exists + if (d_rtu_op.isNull()) { + Type t; + // 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 + t = em->mkFunctionType(d_unsorted, em->realType()); + d_utr_op = em->mkVar("$$utr", 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()) { + d_r_converted.insert(expr); + Expr eq = em->mkExpr(kind::EQUAL, expr, + em->mkExpr(kind::APPLY_UF, d_utr_op, ret)); + preemptCommand(new AssertCommand(eq)); + } + return ret; +} + +Expr Tptp::convertStrToUnsorted(std::string str) { + Expr& e = d_distinct_objects[str]; + if (e.isNull()) { + e = getExprManager()->mkConst( + UninterpretedConstant(d_unsorted, d_distinct_objects.size() - 1)); + } + return e; +} + +void Tptp::makeApplication(Expr& expr, std::string& name, + std::vector& 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, ExprManager::VAR_FLAG_GLOBAL); // levelZero + preemptCommand(new DeclareFunctionCommand(name, expr, t)); + } + } else { // Its an application + if (isDeclared(name)) { // already appeared + expr = getVariable(name); + } else { + std::vector sorts(args.size(), d_unsorted); + Type t = term ? d_unsorted : getExprManager()->booleanType(); + t = getExprManager()->mkFunctionType(sorts, t); + 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); + } +} + +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: + case FR_ASSUMPTION: + case FR_LEMMA: + case FR_THEOREM: + case FR_NEGATED_CONJECTURE: + case FR_PLAIN: + // it's a usual assert + return new AssertCommand(expr); + case FR_CONJECTURE: + // something to prove + return new AssertCommand(getExprManager()->mkExpr(kind::NOT, expr)); + case FR_UNKNOWN: + case FR_FI_DOMAIN: + case FR_FI_FUNCTORS: + case FR_FI_PREDICATES: + case FR_TYPE: + return new EmptyCommand("Untreated role"); + } + assert(false); // unreachable + return nullptr; +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 3afd29415..e6d7bbb47 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -30,90 +30,23 @@ #include "util/hash.h" namespace CVC4 { - -class SExpr; - namespace parser { class Tptp : public Parser { + private: friend class ParserBuilder; + public: + bool cnf() const { return d_cnf; } + void setCnf(bool cnf) { d_cnf = cnf; } - // In CNF variable are implicitly binded - // d_freevar collect them - std::vector< Expr > d_freeVar; - Expr d_rtu_op; - Expr d_stu_op; - Expr d_utr_op; - Expr d_uts_op; - // The set of expression that already have a bridge - std::unordered_set d_r_converted; - std::unordered_map d_distinct_objects; - - std::vector< pANTLR3_INPUT_STREAM > d_in_created; - - // 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; + bool fof() const { return d_fof; } + void setFof(bool fof) { d_fof = fof; } - static void myPopCharStream(pANTLR3_LEXER lexer); - void (*d_oldPopCharStream)(pANTLR3_LEXER); + void addFreeVar(Expr var); + std::vector< Expr > getFreeVar(); -public: - - 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) { - ExprManager * em = getExprManager(); - - // Create the conversion function If they doesn't exists - if(d_rtu_op.isNull()) { - Type t; - // 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 - t = em->mkFunctionType(d_unsorted, em->realType()); - d_utr_op = em->mkVar("$$utr",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()) { - d_r_converted.insert(expr); - Expr eq = em->mkExpr(kind::EQUAL, expr, - em->mkExpr(kind::APPLY_UF, d_utr_op, ret)); - preemptCommand(new AssertCommand(eq)); - } - return ret; - } - - inline Expr convertStrToUnsorted(std::string str) { - Expr& e = d_distinct_objects[str]; - if(e.isNull()) { - e = getExprManager()->mkConst(UninterpretedConstant(d_unsorted, d_distinct_objects.size() - 1)); - } - return e; - } - -public: + Expr convertRatToUnsorted(Expr expr); + Expr convertStrToUnsorted(std::string str); // CNF and FOF are unsorted so we define this common type. // This is also the Type of $i in TFF. @@ -142,10 +75,11 @@ public: bool hasConjecture() const { return d_hasConjecture; } -protected: - Tptp(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); + protected: + Tptp(ExprManager* exprManager, Input* input, bool strictMode = false, + bool parseOnly = false); -public: + public: ~Tptp(); /** * Add theory symbols to the parser state. @@ -154,10 +88,10 @@ public: */ void addTheory(Theory theory); - inline void makeApplication(Expr& expr, std::string& name, - std::vector& args, bool term); + void makeApplication(Expr& expr, std::string& name, std::vector& args, + bool term); - inline Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf); + Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf); /** Ugly hack because I don't know how to return an expression from a token */ @@ -168,75 +102,39 @@ public: void includeFile(std::string fileName); /** Check a TPTP let binding for well-formedness. */ - void checkLetBinding(std::vector& bvlist, Expr lhs, Expr rhs, bool formula); - -private: + void checkLetBinding(std::vector& bvlist, Expr lhs, Expr rhs, + bool formula); + private: void addArithmeticOperators(); + + // In CNF variable are implicitly binded + // d_freevar collect them + std::vector< Expr > d_freeVar; + Expr d_rtu_op; + Expr d_stu_op; + Expr d_utr_op; + Expr d_uts_op; + // The set of expression that already have a bridge + std::unordered_set d_r_converted; + std::unordered_map d_distinct_objects; + + std::vector< pANTLR3_INPUT_STREAM > d_in_created; + + // 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; + + bool d_cnf; // in a cnf formula + bool d_fof; // in an fof formula + + static void myPopCharStream(pANTLR3_LEXER lexer); + void (*d_oldPopCharStream)(pANTLR3_LEXER); };/* class Tptp */ -inline void Tptp::makeApplication(Expr& expr, std::string& name, - std::vector& 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, ExprManager::VAR_FLAG_GLOBAL); // levelZero - preemptCommand(new DeclareFunctionCommand(name, expr, t)); - } - } else { // Its an application - if(isDeclared(name)) { // already appeared - expr = getVariable(name); - } else { - std::vector sorts(args.size(), d_unsorted); - Type t = term ? d_unsorted : getExprManager()->booleanType(); - t = getExprManager()->mkFunctionType(sorts, t); - 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, 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: - case FR_ASSUMPTION: - case FR_LEMMA: - case FR_THEOREM: - case FR_NEGATED_CONJECTURE: - case FR_PLAIN: - // it's a usual assert - return new AssertCommand(expr); - case FR_CONJECTURE: - // something to prove - return new AssertCommand(getExprManager()->mkExpr(kind::NOT,expr)); - case FR_UNKNOWN: - case FR_FI_DOMAIN: - case FR_FI_FUNCTORS: - case FR_FI_PREDICATES: - case FR_TYPE: - return new EmptyCommand("Untreated role"); - } - assert(false);// unreachable - return NULL; -} namespace tptp { /** -- 2.30.2