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.

1 files changed, 16 insertions, 0 deletions

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