Remove tester name from APIs (#3929)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 6 Mar 2020 20:27:10 +0000 (14:27 -0600)
committerGitHub <noreply@github.com>
Fri, 6 Mar 2020 20:27:10 +0000 (14:27 -0600)
commit89337334236176bff2d561c42b9b55ab9d91bd62
treea7ca068313b3625865bedc425a9607b814e5868e
parentb9347f7d0ca130f85df103e5271536a165a04a64
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.
20 files changed:
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/expr/datatype.cpp
src/expr/datatype.h
src/parser/cvc/Cvc.g
src/parser/cvc/cvc.cpp
src/parser/cvc/cvc.h
src/parser/parser.cpp
src/parser/parser.h
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
test/regress/regress0/datatypes/data-nested-codata.smt2
test/regress/regress0/datatypes/is_test.smt2
test/regress/regress0/quantifiers/simp-len.smt2
test/regress/regress0/smtlib/global-decls.smt2
test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2
test/regress/regress2/bug674.smt2
test/unit/api/datatype_api_black.h
test/unit/util/datatype_black.h