From: Andrew Reynolds Date: Fri, 6 Mar 2020 20:27:10 +0000 (-0600) Subject: Remove tester name from APIs (#3929) X-Git-Tag: cvc5-1.0.0~3554 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=89337334236176bff2d561c42b9b55ab9d91bd62;p=cvc5.git 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. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 63ebdbea6..3b28e2f5c 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1959,11 +1959,6 @@ Term DatatypeConstructor::getTesterTerm() const return tst; } -std::string DatatypeConstructor::getTesterName() const -{ - return d_ctor->getTesterName(); -} - size_t DatatypeConstructor::getNumSelectors() const { return d_ctor->getNumArgs(); diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 3317348fe..db29359c5 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1411,11 +1411,6 @@ class CVC4_PUBLIC DatatypeConstructor */ Term getTesterTerm() const; - /** - * @return the tester name for this Datatype constructor. - */ - std::string getTesterName() const; - /** * @return the number of selectors (so far) of this Datatype constructor. */ 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* 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(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(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() {} /** @@ -309,11 +299,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. */ @@ -456,8 +441,6 @@ class CVC4_PUBLIC DatatypeConstructor { private: /** The internal representation */ std::shared_ptr d_internal; - /** the name of the tester */ - std::string d_testerName; /** The constructor */ Expr d_constructor; /** the arguments of this constructor */ 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 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, diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 55a52e8d6..f4ea6d56c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -143,6 +143,8 @@ api::Term Parser::getExpressionForNameAndType(const std::string& name, return expr; } +bool Parser::getTesterName(api::Term cons, std::string& name) { return false; } + api::Kind Parser::getKindForFunction(api::Term fun) { api::Sort t = fun.getSort(); @@ -447,13 +449,17 @@ std::vector Parser::mkMutualDatatypeTypes( }else{ throw ParserException(constructorName + " already declared in this datatype"); } - api::Term tester = ctor.getTesterTerm(); - Debug("parser-idt") << "+ define " << tester << std::endl; - string testerName = ctor.getTesterName(); - if(!doOverload) { - checkDeclaration(testerName, CHECK_UNDECLARED); + std::string testerName; + if (getTesterName(constructor, testerName)) + { + api::Term tester = ctor.getTesterTerm(); + Debug("parser-idt") << "+ define " << testerName << std::endl; + if (!doOverload) + { + checkDeclaration(testerName, CHECK_UNDECLARED); + } + defineVar(testerName, tester, d_globalDeclarations, doOverload); } - defineVar(testerName, tester, d_globalDeclarations, doOverload); for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++) { const api::DatatypeSelector& sel = ctor[k]; 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 @@ -367,6 +367,22 @@ public: virtual api::Term getExpressionForNameAndType(const std::string& name, 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 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 14396c771..d1544f03c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2548,10 +2548,8 @@ constructorDef[CVC4::Datatype& type] CVC4::DatatypeConstructor* ctor = NULL; } : symbol[id,CHECK_NONE,SYM_VARIABLE] - { // make the tester - std::string testerId("is-"); - testerId.append(id); - ctor = new CVC4::DatatypeConstructor(id, testerId); + { + ctor = new CVC4::DatatypeConstructor(id); } ( LPAREN_TOK selector[*ctor] RPAREN_TOK )* { // make the constructor diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 73be8910f..2df73d9e4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -505,6 +505,20 @@ api::Term Smt2::getExpressionForNameAndType(const std::string& name, return Parser::getExpressionForNameAndType(name, t); } +bool Smt2::getTesterName(api::Term cons, std::string& name) +{ + if (v2_6() && strictModeEnabled()) + { + // 2.6 or above uses indexed tester symbols, if we are in strict mode, + // we do not automatically define is-cons for constructor cons. + return false; + } + std::stringstream ss; + ss << "is-" << cons; + name = ss.str(); + return true; +} + api::Term Smt2::mkIndexedConstant(const std::string& name, const std::vector& numerals) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index afa60bf2f..bf4b231b1 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -150,6 +150,12 @@ class Smt2 : public Parser api::Term getExpressionForNameAndType(const std::string& name, api::Sort t) override; + /** + * If we are in a version < 2.6, this updates name to the tester name of cons, + * e.g. "is-cons". + */ + bool getTesterName(api::Term cons, std::string& name) override; + /** Make function defined by a define-fun(s)-rec command. * * fname : the name of the function. 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 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);