Do not introduce uinterpreted constants in TPTP parser (#1743)

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 1bed634969a2a0d586cb08b5e00ef2fdd2f9e660..0695349743f909360d70490316652cc32fc7f53a 100644 (file)
--- 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 70430bcaecdafb090fbf76626a613eee4b9ca832..09c3b3a2a1e2ec798dbd1c6e3227ad5cca206042 100644 (file)
--- 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 4e03bc57624de529a09835fb8d77849acb0afb69..e12a3020a56263ec8d4ffccc861a4253aeb15e74 100644 (file)
--- 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