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.

2 files changed, 5 insertions, 41 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index dd5f12b28..3925e1434 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -273,10 +273,8 @@ void Datatype::addSygusConstructor(Expr op,
   std::stringstream ss;
   ss << getName() << "_" << getNumConstructors() << "_" << cname;
   std::string name = ss.str();
-  std::string testerId("is-");
-  testerId.append(name);
   unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1);
-  DatatypeConstructor c(name, testerId, cweight);
+  DatatypeConstructor c(name, cweight);
   c.setSygus(op, spc);
   for( unsigned j=0; j<cargs.size(); j++ ){
     Debug("parser-sygus-debug") << "  arg " << j << " : " << cargs[j] << std::endl;
@@ -515,21 +513,10 @@ const std::vector<DatatypeConstructor>* Datatype::getConstructors() const
   return &d_constructors;
 }
 
-DatatypeConstructor::DatatypeConstructor(std::string name)
-    : d_internal(nullptr),
-      d_testerName("is_" + name)  // default tester name is "is_FOO"
-{
-  PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
-  d_internal = std::make_shared<DTypeConstructor>(name, 1);
-}
-
-DatatypeConstructor::DatatypeConstructor(std::string name,
-                                         std::string tester,
-                                         unsigned weight)
-    : d_internal(nullptr), d_testerName(tester)
+DatatypeConstructor::DatatypeConstructor(std::string name, unsigned weight)
+    : d_internal(nullptr)
 {
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
-  PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
   d_internal = std::make_shared<DTypeConstructor>(name, weight);
 }
 
@@ -594,12 +581,6 @@ std::string DatatypeConstructor::getName() const
   return d_internal->getName();
 }
 
-std::string DatatypeConstructor::getTesterName() const
-{
-  // not stored internally, since tester names only pertain to parsing
-  return d_testerName;
-}
-
 Expr DatatypeConstructor::getConstructor() const {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_constructor;
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index f9edb998f..0f99499ce 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -213,24 +213,14 @@ class CVC4_PUBLIC DatatypeConstructor {
 
   /**
    * Create a new Datatype constructor with the given name for the
-   * constructor and the same name (prefixed with "is_") for the
-   * tester.  The actual constructor and tester (meaning, the Exprs
+   * constructor.  The actual constructor and tester (meaning, the Exprs
    * representing operators for these entities) aren't created until
    * resolution time.
-   */
-  explicit DatatypeConstructor(std::string name);
-
-  /**
-   * Create a new Datatype constructor with the given name for the
-   * constructor and the given name for the tester.  The actual
-   * constructor and tester aren't created until resolution time.
    * weight is the value that this constructor carries when computing size.
    * For example, if A, B, C have weights 0, 1, and 3 respectively, then
    * C( B( A() ), B( A() ) ) has size 5.
    */
-  DatatypeConstructor(std::string name,
-                      std::string tester,
-                      unsigned weight = 1);
+  explicit DatatypeConstructor(std::string name, unsigned weight = 1);
 
   ~DatatypeConstructor() {}
   /**
@@ -310,11 +300,6 @@ class CVC4_PUBLIC DatatypeConstructor {
   unsigned getWeight() const;
 
   /**
-   * Get the tester name for this Datatype constructor.
-   */
-  std::string getTesterName() const;
-
-  /**
    * Get the number of arguments (so far) of this Datatype constructor.
    */
   size_t getNumArgs() const;
@@ -456,8 +441,6 @@ class CVC4_PUBLIC DatatypeConstructor {
  private:
   /** The internal representation */
   std::shared_ptr<DTypeConstructor> d_internal;
-  /** the name of the tester */
-  std::string d_testerName;
   /** The constructor */
   Expr d_constructor;
   /** the arguments of this constructor */