summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cvc4cpp.cpp5
-rw-r--r--src/api/cvc4cpp.h5
-rw-r--r--src/expr/datatype.cpp25
-rw-r--r--src/expr/datatype.h21
-rw-r--r--src/parser/cvc/Cvc.g7
-rw-r--r--src/parser/cvc/cvc.cpp8
-rw-r--r--src/parser/cvc/cvc.h3
-rw-r--r--src/parser/parser.cpp18
-rw-r--r--src/parser/parser.h16
-rw-r--r--src/parser/smt2/Smt2.g6
-rw-r--r--src/parser/smt2/smt2.cpp14
-rw-r--r--src/parser/smt2/smt2.h6
-rw-r--r--test/regress/regress0/datatypes/data-nested-codata.smt212
-rw-r--r--test/regress/regress0/datatypes/is_test.smt22
-rw-r--r--test/regress/regress0/quantifiers/simp-len.smt22
-rw-r--r--test/regress/regress0/smtlib/global-decls.smt24
-rw-r--r--test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt22
-rw-r--r--test/regress/regress2/bug674.smt24
-rw-r--r--test/unit/api/datatype_api_black.h3
-rw-r--r--test/unit/util/datatype_black.h48
20 files changed, 105 insertions, 106 deletions
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
@@ -1412,11 +1412,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.
*/
size_t getNumSelectors() const;
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<cargs.size(); j++ ){
Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl;
@@ -515,21 +513,10 @@ const std::vector<DatatypeConstructor>* 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<DTypeConstructor>(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<DTypeConstructor>(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() {}
/**
@@ -310,11 +300,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.
*/
size_t getNumArgs() const;
@@ -456,8 +441,6 @@ class CVC4_PUBLIC DatatypeConstructor {
private:
/** The internal representation */
std::shared_ptr<DTypeConstructor> 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<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,
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<DatatypeType> 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
@@ -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
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<uint64_t>& 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<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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback