diff options
| -rw-r--r-- | src/parser/tptp/Tptp.g | 9 | ||||
| -rw-r--r-- | src/parser/tptp/tptp.cpp | 20 | ||||
| -rw-r--r-- | src/parser/tptp/tptp.h | 15 |
3 files changed, 39 insertions, 5 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 1bed63496..069534974 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -233,6 +233,14 @@ parseCommand returns [CVC4::Command* cmd = NULL] } | EOF { + CommandSequence* seq = new CommandSequence(); + // assert that all distinct constants are distinct + Expr aexpr = PARSER_STATE->getAssertionDistinctConstants(); + if( !aexpr.isNull() ) + { + seq->addCommand(new AssertCommand(aexpr, false)); + } + std::string filename = PARSER_STATE->getInput()->getInputStreamName(); size_t i = filename.find_last_of('/'); if(i != std::string::npos) { @@ -241,7 +249,6 @@ parseCommand returns [CVC4::Command* cmd = NULL] if(filename.substr(filename.length() - 2) == ".p") { filename = filename.substr(0, filename.length() - 2); } - CommandSequence* seq = new CommandSequence(); seq->addCommand(new SetInfoCommand("name", SExpr(filename))); if(PARSER_STATE->hasConjecture()) { seq->addCommand(new QueryCommand(MK_CONST(bool(false)))); diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 70430bcae..09c3b3a2a 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -257,9 +257,9 @@ Expr Tptp::convertRatToUnsorted(Expr expr) { 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)); + if (e.isNull()) + { + e = getExprManager()->mkVar(str, d_unsorted); } return e; } @@ -325,6 +325,20 @@ Expr Tptp::getAssertionExpr(FormulaRole fr, Expr expr) { return d_nullExpr; } +Expr Tptp::getAssertionDistinctConstants() +{ + std::vector<Expr> constants; + for (std::pair<const std::string, Expr>& cs : d_distinct_objects) + { + constants.push_back(cs.second); + } + if (constants.size() > 1) + { + return getExprManager()->mkExpr(kind::DISTINCT, constants); + } + return d_nullExpr; +} + Command* Tptp::makeAssertCommand(FormulaRole fr, Expr expr, bool cnf, bool inUnsatCore) { // For SZS ontology compliance. // if we're in cnf() though, conjectures don't result in "Theorem" or diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 4e03bc576..e12a3020a 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -46,6 +46,11 @@ class Tptp : public Parser { std::vector< Expr > getFreeVar(); Expr convertRatToUnsorted(Expr expr); + /** + * Returns a free constant corresponding to the string str. We ensure that + * these constants are one-to-one with str. We assert that all these free + * constants are pairwise distinct before issuing satisfiability queries. + */ Expr convertStrToUnsorted(std::string str); // CNF and FOF are unsorted so we define this common type. @@ -97,7 +102,15 @@ class Tptp : public Parser { * For example, if the role is "conjecture", then the return value is the negation of expr. */ Expr getAssertionExpr(FormulaRole fr, Expr expr); - + + /** get assertion for distinct constants + * + * This returns a node of the form distinct( k1, ..., kn ) where k1, ..., kn + * are the distinct constants introduced by this parser (see + * convertStrToUnsorted) if n>1, or null otherwise. + */ + Expr getAssertionDistinctConstants(); + /** returns the appropriate AssertCommand, given a role, expression expr to assert, * and information about the assertion. * The assertion expr is literally what should be asserted (it is already been processed |