Remove tester name from APIs (#3929)

This removes the field "tester name" from the Expr-level and Term-level APIs. This field is an artifact of parsing and thus should be handled in the parsers.

This refactor uncovered an issue in our regressions, namely our smt version >= 2.6 was not strictly complaint, since the symbol is-cons was being automatically defined for testers of constructors cons. This disables this behavior when strict mode is enabled. It updates the regressions with this issue.

This is work towards parser migration.

8 files changed, 63 insertions, 15 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index ffdef5ba2..e3d0e0696 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2354,11 +2354,8 @@ constructorDef[CVC4::Datatype& type]
   std::unique_ptr<CVC4::DatatypeConstructor> ctor;
 }
   : identifier[id,CHECK_UNDECLARED,SYM_SORT]
-    { // make the tester
-      std::string testerId("is_");
-      testerId.append(id);
-      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
-      ctor.reset(new CVC4::DatatypeConstructor(id, testerId));
+    {
+      ctor.reset(new CVC4::DatatypeConstructor(id));
     }
     ( LPAREN
       selector[&ctor]
diff --git a/src/parser/cvc/cvc.cpp b/src/parser/cvc/cvc.cpp
index 9b7e1f403..f312fe13c 100644
--- a/src/parser/cvc/cvc.cpp
+++ b/src/parser/cvc/cvc.cpp
@@ -25,5 +25,13 @@ void Cvc::forceLogic(const std::string& logic)
   preemptCommand(new SetBenchmarkLogicCommand(logic));
 }
 
+bool Cvc::getTesterName(api::Term cons, std::string& name)
+{
+  std::stringstream ss;
+  ss << "is_" << cons;
+  name = ss.str();
+  return true;
+}
+
 }  // namespace parser
 }  // namespace CVC4
diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h
index feb962a09..58d387ca8 100644
--- a/src/parser/cvc/cvc.h
+++ b/src/parser/cvc/cvc.h
@@ -34,6 +34,9 @@ class Cvc : public Parser
  public:
   void forceLogic(const std::string& logic) override;
 
+  /** Updates name to the tester name of cons, e.g. "is_cons" */
+  bool getTesterName(api::Term cons, std::string& name) override;
+
  protected:
   Cvc(api::Solver* solver,
       Input* input,
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 55a52e8d6..f4ea6d56c 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -143,6 +143,8 @@ api::Term Parser::getExpressionForNameAndType(const std::string& name,
   return expr;
 }
 
+bool Parser::getTesterName(api::Term cons, std::string& name) { return false; }
+
 api::Kind Parser::getKindForFunction(api::Term fun)
 {
   api::Sort t = fun.getSort();
@@ -447,13 +449,17 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
         }else{
           throw ParserException(constructorName + " already declared in this datatype");
         }
-        api::Term tester = ctor.getTesterTerm();
-        Debug("parser-idt") << "+ define " << tester << std::endl;
-        string testerName = ctor.getTesterName();
-        if(!doOverload) {
-          checkDeclaration(testerName, CHECK_UNDECLARED);
+        std::string testerName;
+        if (getTesterName(constructor, testerName))
+        {
+          api::Term tester = ctor.getTesterTerm();
+          Debug("parser-idt") << "+ define " << testerName << std::endl;
+          if (!doOverload)
+          {
+            checkDeclaration(testerName, CHECK_UNDECLARED);
+          }
+          defineVar(testerName, tester, d_globalDeclarations, doOverload);
         }
-        defineVar(testerName, tester, d_globalDeclarations, doOverload);
         for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++)
         {
           const api::DatatypeSelector& sel = ctor[k];
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 373da6c47..3237c2893 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -368,6 +368,22 @@ public:
                                                 api::Sort t);
 
   /**
+   * If this method returns true, then name is updated with the tester name
+   * for constructor cons.
+   *
+   * In detail, notice that (user-defined) datatypes associate a unary predicate
+   * for each constructor, called its "tester". This symbol is automatically
+   * defined when a datatype is defined. The tester name for a constructor
+   * (e.g. "cons") depends on the language:
+   * - In smt versions < 2.6, the (non-standard) syntax is "is-cons",
+   * - In smt versions >= 2.6, the indexed symbol "(_ is cons)" is used. Thus,
+   * no tester symbol is necessary, since "is" is a builtin symbol. We still use
+   * the above syntax if strict mode is disabled.
+   * - In cvc, the syntax for testers is "is_cons".
+   */
+  virtual bool getTesterName(api::Term cons, std::string& name);
+
+  /**
    * Returns the kind that should be used for applications of expression fun.
    * This is a generalization of ExprManager::operatorToKind that also
    * handles variables whose types are "function-like", i.e. where
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 14396c771..d1544f03c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2548,10 +2548,8 @@ constructorDef[CVC4::Datatype& type]
   CVC4::DatatypeConstructor* ctor = NULL;
 }
   : symbol[id,CHECK_NONE,SYM_VARIABLE]
-    { // make the tester
-      std::string testerId("is-");
-      testerId.append(id);
-      ctor = new CVC4::DatatypeConstructor(id, testerId);
+    {
+      ctor = new CVC4::DatatypeConstructor(id);
     }
     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
     { // make the constructor
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 73be8910f..2df73d9e4 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -505,6 +505,20 @@ api::Term Smt2::getExpressionForNameAndType(const std::string& name,
   return Parser::getExpressionForNameAndType(name, t);
 }
 
+bool Smt2::getTesterName(api::Term cons, std::string& name)
+{
+  if (v2_6() && strictModeEnabled())
+  {
+    // 2.6 or above uses indexed tester symbols, if we are in strict mode,
+    // we do not automatically define is-cons for constructor cons.
+    return false;
+  }
+  std::stringstream ss;
+  ss << "is-" << cons;
+  name = ss.str();
+  return true;
+}
+
 api::Term Smt2::mkIndexedConstant(const std::string& name,
                                   const std::vector<uint64_t>& numerals)
 {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index afa60bf2f..bf4b231b1 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -150,6 +150,12 @@ class Smt2 : public Parser
   api::Term getExpressionForNameAndType(const std::string& name,
                                         api::Sort t) override;
 
+  /**
+   * If we are in a version < 2.6, this updates name to the tester name of cons,
+   * e.g. "is-cons".
+   */
+  bool getTesterName(api::Term cons, std::string& name) override;
+
   /** Make function defined by a define-fun(s)-rec command.
    *
    * fname : the name of the function.