}
// : 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<Expr> bvl = PARSER_STATE->getFreeVar();
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);
| 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);
: 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);
}
}
;
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 );
}
}
}
+void Tptp::addFreeVar(Expr var) {
+ assert(cnf());
+ d_freeVar.push_back(var);
+}
+
+std::vector<Expr> Tptp::getFreeVar() {
+ assert(cnf());
+ std::vector<Expr> 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<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, 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<Type> 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 */
#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<Expr, ExprHashFunction> d_r_converted;
- std::unordered_map<std::string, Expr> 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.
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.
*/
void addTheory(Theory theory);
- inline void makeApplication(Expr& expr, std::string& name,
- std::vector<Expr>& args, bool term);
+ void makeApplication(Expr& expr, std::string& name, std::vector<Expr>& 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 */
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 checkLetBinding(std::vector<Expr>& 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<Expr, ExprHashFunction> d_r_converted;
+ std::unordered_map<std::string, Expr> 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<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, 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<Type> 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 {
/**
projects / cvc5.git / commitdiff