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, 37 insertions, 40 deletions

diff --git a/test/regress/regress0/datatypes/data-nested-codata.smt2 b/test/regress/regress0/datatypes/data-nested-codata.smt2
index 159ae4ae9..6a5716123 100644
--- a/test/regress/regress0/datatypes/data-nested-codata.smt2
+++ b/test/regress/regress0/datatypes/data-nested-codata.smt2
@@ -8,14 +8,14 @@
 
 
 (declare-fun x () Stream)
-(assert (not (is-nil (shead x))))
-(assert (not (is-nil (tail (shead x)))))
+(assert (not ((_ is nil) (shead x))))
+(assert (not ((_ is nil) (tail (shead x)))))
 (declare-fun y () Stream)
-(assert (not (is-nil (shead y))))
-(assert (not (is-nil (tail (shead y)))))
+(assert (not ((_ is nil) (shead y))))
+(assert (not ((_ is nil) (tail (shead y)))))
 (declare-fun z () Stream)
-(assert (not (is-nil (shead z))))
-(assert (not (is-nil (tail (shead z)))))
+(assert (not ((_ is nil) (shead z))))
+(assert (not ((_ is nil) (tail (shead z)))))
 (assert (distinct x y z))
 
 (check-sat)
diff --git a/test/regress/regress0/datatypes/is_test.smt2 b/test/regress/regress0/datatypes/is_test.smt2
index f13a4f21f..c54a84859 100644
--- a/test/regress/regress0/datatypes/is_test.smt2
+++ b/test/regress/regress0/datatypes/is_test.smt2
@@ -2,5 +2,5 @@
 (set-info :status unsat)
 (declare-datatypes ((Unit 0)) (((u))))
 (declare-fun x () Unit)
-(assert (not (is-u x)))
+(assert (not ((_ is u) x)))
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/simp-len.smt2 b/test/regress/regress0/quantifiers/simp-len.smt2
index 0a736d7b3..06ae23f8d 100644
--- a/test/regress/regress0/quantifiers/simp-len.smt2
+++ b/test/regress/regress0/quantifiers/simp-len.smt2
@@ -3,7 +3,7 @@
 
 (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
 
-(define-fun-rec len ((x Lst)) Int (ite (is-cons x) (+ 1 (len (tail x))) 0))
+(define-fun-rec len ((x Lst)) Int (ite ((_ is cons) x) (+ 1 (len (tail x))) 0))
 
 (assert (= (len (cons 0 nil)) 0))
 (check-sat)
diff --git a/test/regress/regress0/smtlib/global-decls.smt2 b/test/regress/regress0/smtlib/global-decls.smt2
index a8b6c17b2..4b1c8a0ae 100644
--- a/test/regress/regress0/smtlib/global-decls.smt2
+++ b/test/regress/regress0/smtlib/global-decls.smt2
@@ -16,8 +16,8 @@
 (define-fun y () (Struct1 Bool) (mk-struct1 true))
 (declare-const z Unit)
 (assert (= u u))
-(assert (is-mk-struct1 y))
-(assert (is-u z))
+(assert ((_ is mk-struct1) y))
+(assert ((_ is u) z))
 
 (declare-fun size (Tree) Int)
 (assert (= (size nil) 0))
diff --git a/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2 b/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2
index 229a5e17a..01a274e8a 100644
--- a/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2
+++ b/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --incremental --fmf-fun
 (set-logic ALL_SUPPORTED)
 (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
-(define-fun-rec sum ((l Lst)) Int (ite (is-nil l) 0 (+ (head l) (sum (tail l)))))
+(define-fun-rec sum ((l Lst)) Int (ite ((_ is nil) l) 0 (+ (head l) (sum (tail l)))))
 
 (declare-fun input () Int)
 (declare-fun p () Bool)
diff --git a/test/regress/regress2/bug674.smt2 b/test/regress/regress2/bug674.smt2
index fccde862a..31eaa5aba 100644
--- a/test/regress/regress2/bug674.smt2
+++ b/test/regress/regress2/bug674.smt2
@@ -1,8 +1,8 @@
 ; COMMAND-LINE: --quant-ind --incremental --rewrite-divk
 (set-logic ALL_SUPPORTED)
 (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
-(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite (is-nil l1) l2 (cons (head l1) (app (tail l1) l2))))
-(define-fun-rec rev ((l Lst)) Lst (ite (is-nil l) nil (app (rev (tail l)) (cons (head l) nil))))
+(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite ((_ is nil) l1) l2 (cons (head l1) (app (tail l1) l2))))
+(define-fun-rec rev ((l Lst)) Lst (ite ((_ is nil) l) nil (app (rev (tail l)) (cons (head l) nil))))
 ; EXPECT: unsat
 (push 1)
 (assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0)))))))
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h
index 2d7a9c12b..dcccd2628 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.h
@@ -83,9 +83,6 @@ void DatatypeBlack::testDatatypeStructs()
   DatatypeConstructor dcons = dt[0];
   Term consTerm = dcons.getConstructorTerm();
   TS_ASSERT(dcons.getNumSelectors() == 2);
-  // get tester name: notice this is only to support the Z3-style datatypes
-  // prior to SMT-LIB 2.6 where testers where changed to indexed symbols.
-  TS_ASSERT_THROWS_NOTHING(dcons.getTesterName());
 
   // create datatype sort to test
   DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index e81caf36f..5b98f4d13 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -49,10 +49,10 @@ class DatatypeBlack : public CxxTest::TestSuite {
   void testEnumeration() {
     Datatype colors(d_em, "colors");
 
-    DatatypeConstructor yellow("yellow", "is_yellow");
-    DatatypeConstructor blue("blue", "is_blue");
-    DatatypeConstructor green("green", "is_green");
-    DatatypeConstructor red("red", "is_red");
+    DatatypeConstructor yellow("yellow");
+    DatatypeConstructor blue("blue");
+    DatatypeConstructor green("green");
+    DatatypeConstructor red("red");
 
     colors.addConstructor(yellow);
     colors.addConstructor(blue);
@@ -87,11 +87,11 @@ class DatatypeBlack : public CxxTest::TestSuite {
   void testNat() {
     Datatype nat(d_em, "nat");
 
-    DatatypeConstructor succ("succ", "is_succ");
+    DatatypeConstructor succ("succ");
     succ.addArg("pred", DatatypeSelfType());
     nat.addConstructor(succ);
 
-    DatatypeConstructor zero("zero", "is_zero");
+    DatatypeConstructor zero("zero");
     nat.addConstructor(zero);
 
     Debug("datatypes") << nat << std::endl;
@@ -115,12 +115,12 @@ class DatatypeBlack : public CxxTest::TestSuite {
     Datatype tree(d_em, "tree");
     Type integerType = d_em->integerType();
 
-    DatatypeConstructor node("node", "is_node");
+    DatatypeConstructor node("node");
     node.addArg("left", DatatypeSelfType());
     node.addArg("right", DatatypeSelfType());
     tree.addConstructor(node);
 
-    DatatypeConstructor leaf("leaf", "is_leaf");
+    DatatypeConstructor leaf("leaf");
     leaf.addArg("leaf", integerType);
     tree.addConstructor(leaf);
 
@@ -147,12 +147,12 @@ class DatatypeBlack : public CxxTest::TestSuite {
     Datatype list(d_em, "list");
     Type integerType = d_em->integerType();
 
-    DatatypeConstructor cons("cons", "is_cons");
+    DatatypeConstructor cons("cons");
     cons.addArg("car", integerType);
     cons.addArg("cdr", DatatypeSelfType());
     list.addConstructor(cons);
 
-    DatatypeConstructor nil("nil", "is_nil");
+    DatatypeConstructor nil("nil");
     list.addConstructor(nil);
 
     Debug("datatypes") << list << std::endl;
@@ -172,12 +172,12 @@ class DatatypeBlack : public CxxTest::TestSuite {
     Datatype list(d_em, "list");
     Type realType = d_em->realType();
 
-    DatatypeConstructor cons("cons", "is_cons");
+    DatatypeConstructor cons("cons");
     cons.addArg("car", realType);
     cons.addArg("cdr", DatatypeSelfType());
     list.addConstructor(cons);
 
-    DatatypeConstructor nil("nil", "is_nil");
+    DatatypeConstructor nil("nil");
     list.addConstructor(nil);
 
     Debug("datatypes") << list << std::endl;
@@ -197,12 +197,12 @@ class DatatypeBlack : public CxxTest::TestSuite {
     Datatype list(d_em, "list");
     Type booleanType = d_em->booleanType();
 
-    DatatypeConstructor cons("cons", "is_cons");
+    DatatypeConstructor cons("cons");
     cons.addArg("car", booleanType);
     cons.addArg("cdr", DatatypeSelfType());
     list.addConstructor(cons);
 
-    DatatypeConstructor nil("nil", "is_nil");
+    DatatypeConstructor nil("nil");
     list.addConstructor(nil);
 
     Debug("datatypes") << list << std::endl;
@@ -227,24 +227,24 @@ class DatatypeBlack : public CxxTest::TestSuite {
      *   END;
      */
     Datatype tree(d_em, "tree");
-    DatatypeConstructor node("node", "is_node");
+    DatatypeConstructor node("node");
     node.addArg("left", DatatypeSelfType());
     node.addArg("right", DatatypeSelfType());
     tree.addConstructor(node);
 
-    DatatypeConstructor leaf("leaf", "is_leaf");
+    DatatypeConstructor leaf("leaf");
     leaf.addArg("leaf", DatatypeUnresolvedType("list"));
     tree.addConstructor(leaf);
 
     Debug("datatypes") << tree << std::endl;
 
     Datatype list(d_em, "list");
-    DatatypeConstructor cons("cons", "is_cons");
+    DatatypeConstructor cons("cons");
     cons.addArg("car", DatatypeUnresolvedType("tree"));
     cons.addArg("cdr", DatatypeSelfType());
     list.addConstructor(cons);
 
-    DatatypeConstructor nil("nil", "is_nil");
+    DatatypeConstructor nil("nil");
     list.addConstructor(nil);
 
     Debug("datatypes") << list << std::endl;
@@ -281,27 +281,27 @@ class DatatypeBlack : public CxxTest::TestSuite {
   void testMutualListTrees2()
   {
     Datatype tree(d_em, "tree");
-    DatatypeConstructor node("node", "is_node");
+    DatatypeConstructor node("node");
     node.addArg("left", DatatypeSelfType());
     node.addArg("right", DatatypeSelfType());
     tree.addConstructor(node);
 
-    DatatypeConstructor leaf("leaf", "is_leaf");
+    DatatypeConstructor leaf("leaf");
     leaf.addArg("leaf", DatatypeUnresolvedType("list"));
     tree.addConstructor(leaf);
 
     Datatype list(d_em, "list");
-    DatatypeConstructor cons("cons", "is_cons");
+    DatatypeConstructor cons("cons");
     cons.addArg("car", DatatypeUnresolvedType("tree"));
     cons.addArg("cdr", DatatypeSelfType());
     list.addConstructor(cons);
 
-    DatatypeConstructor nil("nil", "is_nil");
+    DatatypeConstructor nil("nil");
     list.addConstructor(nil);
 
     // add another constructor to list datatype resulting in an
     // "otherNil-list"
-    DatatypeConstructor otherNil("otherNil", "is_otherNil");
+    DatatypeConstructor otherNil("otherNil");
     list.addConstructor(otherNil);
 
     vector<Datatype> dts;
@@ -329,7 +329,7 @@ class DatatypeBlack : public CxxTest::TestSuite {
   void testNotSoWellFounded() {
     Datatype tree(d_em, "tree");
 
-    DatatypeConstructor node("node", "is_node");
+    DatatypeConstructor node("node");
     node.addArg("left", DatatypeSelfType());
     node.addArg("right", DatatypeSelfType());
     tree.addConstructor(node);