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.

3 files changed, 13 insertions, 5 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,