diff options
Diffstat (limited to 'src/parser/tptp/tptp.cpp')
| -rw-r--r-- | src/parser/tptp/tptp.cpp | 20 |
1 files changed, 17 insertions, 3 deletions
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 |