From: Andrew Reynolds Date: Thu, 6 Aug 2020 18:41:24 +0000 (-0500) Subject: Updates not related to creation for eliminating Expr-level datatype (#4838) X-Git-Tag: cvc5-1.0.0~3033 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=816d5e7624c9d088c469f7e23d11394f5b385b84;p=cvc5.git Updates not related to creation for eliminating Expr-level datatype (#4838) This updates remaining uses of the Expr-level Datatype that are not related to their creation / memory management in ExprManager. This required updating a unit test from Expr -> Node. --- diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 9ec3ac5fd..f8712e20e 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -304,6 +304,7 @@ void Datatype::setRecord() { PrettyCheckArgument( !isResolved(), this, "cannot set record to a finalized Datatype"); d_isRecord = true; + d_internal->setRecord(); } Cardinality Datatype::getCardinality(Type t) const diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 85e07866b..c64814ed6 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -66,7 +66,7 @@ void DTypeConstructor::addArgSelf(std::string selectorName) { Trace("datatypes") << "DTypeConstructor::addArgSelf" << std::endl; std::shared_ptr a = - std::make_shared(selectorName, Node::null()); + std::make_shared(selectorName + '\0', Node::null()); addArg(a); } diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 68d3904d3..1da60eb05 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -26,6 +26,7 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/context.h" +#include "expr/dtype.h" #include "expr/expr.h" #include "expr/expr_manager_scope.h" #include "expr/type.h" @@ -212,11 +213,10 @@ Expr OverloadedTypeTrie::getOverloadedFunctionForTypes( Trace("parser-overloading") << "Parametric overloaded datatype selector " << name << " " << tna << std::endl; - DatatypeType tnd = static_cast(argTypes[i]); - const Datatype& dt = tnd.getDatatype(); + const DType& dt = TypeNode::fromType(argTypes[i]).getDType(); // tng is the "generalized" version of the instantiated parametric // type tna - Type tng = dt.getDatatypeType(); + Type tng = dt.getTypeNode().toType(); itc = tat->d_children.find(tng); if (itc != tat->d_children.end()) { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 7696d9d7a..8232ef339 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -331,8 +331,7 @@ bool Type::isTuple() const { /** Is this a record type? */ bool Type::isRecord() const { NodeManagerScope nms(d_nodeManager); - return d_typeNode->getKind() == kind::DATATYPE_TYPE - && DatatypeType(*this).getDatatype().isRecord(); + return d_typeNode->isRecord(); } /** Is this a symbolic expression type? */ @@ -586,7 +585,8 @@ std::vector ConstructorType::getArgTypes() const { return args; } -const Datatype& DatatypeType::getDatatype() const { +const Datatype& DatatypeType::getDatatype() const +{ NodeManagerScope nms(d_nodeManager); Assert(isDatatype()); if (d_typeNode->getKind() == kind::DATATYPE_TYPE) @@ -602,10 +602,6 @@ bool DatatypeType::isParametric() const { return d_typeNode->isParametricDatatype(); } -Expr DatatypeType::getConstructor(std::string name) const { - return getDatatype().getConstructor(name); -} - bool DatatypeType::isInstantiated() const { return d_typeNode->isInstantiatedDatatype(); } @@ -662,14 +658,6 @@ std::vector DatatypeType::getTupleTypes() const { return vect; } -/** Get the description of the record type */ -const Record& DatatypeType::getRecord() const { - NodeManagerScope nms(d_nodeManager); - Assert(isRecord()); - const Datatype& dt = getDatatype(); - return *(dt.getRecord()); -} - DatatypeType SelectorType::getDomain() const { return DatatypeType(makeType((*d_typeNode)[0])); } diff --git a/src/expr/type.h b/src/expr/type.h index 61cb7eabf..0067ba7e7 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -621,13 +621,6 @@ class CVC4_PUBLIC DatatypeType : public Type { /** Is this datatype parametric? */ bool isParametric() const; - - /** - * Get the constructor operator associated to the given constructor - * name in this datatype. - */ - Expr getConstructor(std::string name) const; - /** * Has this datatype been fully instantiated ? * @@ -654,9 +647,6 @@ class CVC4_PUBLIC DatatypeType : public Type { /** Get the constituent types of a tuple type */ std::vector getTupleTypes() const; - /** Get the description of the record type */ - const Record& getRecord() const; - };/* class DatatypeType */ /** Class encapsulating the constructor type. */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index c97a24d6d..7e38fac3d 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -396,12 +396,16 @@ std::vector TypeNode::getParamTypes() const { return params; } - -/** Is this a tuple type? */ -bool TypeNode::isTuple() const { +bool TypeNode::isTuple() const +{ return (getKind() == kind::DATATYPE_TYPE && getDType().isTuple()); } +bool TypeNode::isRecord() const +{ + return (getKind() == kind::DATATYPE_TYPE && getDType().isRecord()); +} + size_t TypeNode::getTupleLength() const { Assert(isTuple()); const DType& dt = getDType(); diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 0d0c17edf..b836e5069 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -599,6 +599,9 @@ public: /** Is this a tuple type? */ bool isTuple() const; + /** Is this a record type? */ + bool isRecord() const; + /** Get the length of a tuple type */ size_t getTupleLength() const; diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 7d1f66d65..53abf2e3d 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -18,6 +18,7 @@ #include "preprocessing/passes/unconstrained_simplifier.h" +#include "expr/dtype.h" #include "smt/smt_statistics_registry.h" #include "theory/logic_info.h" #include "theory/rewriter.h" @@ -262,8 +263,8 @@ void UnconstrainedSimplifier::processUnconstrained() if (parent[0].getType().isDatatype()) { TypeNode tn = parent[0].getType(); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if (dt.isRecursiveSingleton(tn.toType())) + const DType& dt = tn.getDType(); + if (dt.isRecursiveSingleton(tn)) { // domain size may be 1 break; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 9ec522141..243592456 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -214,23 +214,26 @@ void CvcPrinter::toStream( const Datatype& dt = NodeManager::currentNM()->toExprManager()->getDatatypeForIndex( n.getConst().getIndex()); + if( dt.isTuple() ){ out << '['; for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { if (i > 0) { out << ", "; } - Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType(); + Type t = dt[0][i].getRangeType(); out << t; } out << ']'; - }else if( dt.isRecord() ){ + } + else if (dt.isRecord()) + { out << "[# "; for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { if (i > 0) { out << ", "; } - Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType(); + Type t = dt[0][i].getRangeType(); out << dt[0][i].getSelector() << ":" << t; } out << " #]"; @@ -414,18 +417,17 @@ void CvcPrinter::toStream( } else if (t.toType().isRecord()) { - const Record& rec = static_cast(t.toType()).getRecord(); + const DType& dt = t.getDType(); + const DTypeConstructor& recCons = dt[0]; out << "(# "; - TNode::iterator i = n.begin(); - bool first = true; - const Record::FieldVector& fields = rec.getFields(); - for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) { - if(!first) { + for (size_t i = 0, nargs = recCons.getNumArgs(); i < nargs; i++) + { + if (i != 0) + { out << ", "; } - out << (*j).first << " := "; - toStream(out, *i, depth, types, false); - first = false; + out << recCons[i].getName() << " := "; + toStream(out, n[i], depth, types, false); } out << " #)"; return; @@ -450,18 +452,17 @@ void CvcPrinter::toStream( { toStream(op, opn, depth, types, false); } - else if (t.isTuple() - || DatatypeType(t.toType()).isRecord()) + else if (t.isTuple() || t.isRecord()) { toStream(out, n[0], depth, types, true); out << '.'; - const Datatype& dt = ((DatatypeType)t.toType()).getDatatype(); + const DType& dt = t.getDType(); if (t.isTuple()) { int sindex; if (n.getKind() == kind::APPLY_SELECTOR) { - sindex = Datatype::indexOf(opn.toExpr()); + sindex = DType::indexOf(opn.toExpr()); } else { @@ -483,9 +484,9 @@ void CvcPrinter::toStream( case kind::APPLY_TESTER: { Assert(!n.getType().isTuple() && !n.getType().toType().isRecord()); op << "is_"; - unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); - const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); - toStream(op, Node::fromExpr(dt[cindex].getConstructor()), depth, types, false); + unsigned cindex = DType::indexOf(n.getOperator()); + const DType& dt = DType::datatypeOf(n.getOperator()); + toStream(op, dt[cindex].getConstructor(), depth, types, false); } break; case kind::CONSTRUCTOR_TYPE: @@ -1515,7 +1516,7 @@ static void toStream(std::ostream& out, { const vector& datatypes = c->getDatatypes(); Assert(!datatypes.empty() && datatypes[0].isDatatype()); - const Datatype& dt0 = DatatypeType(datatypes[0]).getDatatype(); + const DType& dt0 = TypeNode::fromType(datatypes[0]).getDType(); //do not print tuple/datatype internal declarations if (datatypes.size() != 1 || (!dt0.isTuple() && !dt0.isRecord())) { @@ -1526,7 +1527,7 @@ static void toStream(std::ostream& out, if(! firstDatatype) { out << ',' << endl; } - const Datatype& dt = DatatypeType(t).getDatatype(); + const DType& dt = TypeNode::fromType(t).getDType(); out << " " << dt.getName(); if(dt.isParametric()) { out << '['; @@ -1539,31 +1540,28 @@ static void toStream(std::ostream& out, out << ']'; } out << " = "; - bool firstConstructor = true; - for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) { - if(! firstConstructor) { + for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) + { + const DTypeConstructor& cons = dt[j]; + if (j != 0) + { out << " | "; } - firstConstructor = false; - const DatatypeConstructor& cons = *j; out << cons.getName(); if (cons.getNumArgs() > 0) { out << '('; - bool firstSelector = true; - for (DatatypeConstructor::const_iterator k = cons.begin(); - k != cons.end(); - ++k) + for (size_t k = 0, nargs = cons.getNumArgs(); k < nargs; k++) { - if(! firstSelector) { + if (k != 0) + { out << ", "; } - firstSelector = false; - const DatatypeConstructorArg& selector = *k; - Type tr = SelectorType(selector.getType()).getRangeType(); + const DTypeSelector& selector = cons[k]; + TypeNode tr = selector.getRangeType(); if (tr.isDatatype()) { - const Datatype& sdt = DatatypeType(tr).getDatatype(); + const DType& sdt = tr.getDType(); out << selector.getName() << ": " << sdt.getName(); } else diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 7560b2ce4..b92490ae2 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -793,7 +793,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::APPLY_CONSTRUCTOR: { typeChildren = true; - const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); + const DType& dt = DType::datatypeOf(n.getOperator()); if (dt.isTuple()) { stillNeedToPrintParams = false; @@ -898,16 +898,24 @@ void Smt2Printer::toStream(std::ostream& out, if(toDepth != 0) { if (n.getKind() == kind::APPLY_TESTER) { - unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); - const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); + unsigned cindex = DType::indexOf(n.getOperator().toExpr()); + const DType& dt = DType::datatypeOf(n.getOperator().toExpr()); if (isVariant_2_6(d_variant)) { out << "(_ is "; - toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); + toStream(out, + dt[cindex].getConstructor(), + toDepth < 0 ? toDepth : toDepth - 1, + types, + TypeNode::null()); out << ")"; }else{ out << "is-"; - toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); + toStream(out, + dt[cindex].getConstructor(), + toDepth < 0 ? toDepth : toDepth - 1, + types, + TypeNode::null()); } }else{ toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); @@ -963,14 +971,14 @@ void Smt2Printer::toStream(std::ostream& out, TypeNode opt = n.getOperator().getType(); if (n.getKind() == kind::APPLY_CONSTRUCTOR) { - Type tn = n.getType().toType(); + TypeNode tn = n.getType(); // may be parametric, in which case the constructor type must be // specialized - const Datatype& dt = static_cast(tn).getDatatype(); + const DType& dt = tn.getDType(); if (dt.isParametric()) { - unsigned ci = Datatype::indexOf(n.getOperator().toExpr()); - opt = TypeNode::fromType(dt[ci].getSpecializedConstructorType(tn)); + unsigned ci = DType::indexOf(n.getOperator().toExpr()); + opt = dt[ci].getSpecializedConstructorType(tn); } } Assert(opt.getNumChildren() == n.getNumChildren() + 1); @@ -1845,16 +1853,20 @@ static void toStream(std::ostream& out, const GetOptionCommand* c) out << "(get-option :" << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const Datatype & d) { - for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end(); - ctor != ctor_end; ++ctor){ - if( ctor!=d.begin() ) out << " "; - out << "(" << CVC4::quoteSymbol(ctor->getName()); - - for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end(); - arg != arg_end; ++arg){ - out << " (" << arg->getSelector() << " " - << static_cast(arg->getType()).getRangeType() << ")"; +static void toStream(std::ostream& out, const DType& dt) +{ + for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + const DTypeConstructor& cons = dt[i]; + if (i != 0) + { + out << " "; + } + out << "(" << CVC4::quoteSymbol(cons.getName()); + for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++) + { + const DTypeSelector& arg = cons[j]; + out << " (" << arg.getSelector() << " " << arg.getRangeType() << ")"; } out << ")"; } @@ -1867,8 +1879,7 @@ static void toStream(std::ostream& out, const std::vector& datatypes = c->getDatatypes(); Assert(!datatypes.empty()); Assert(datatypes[0].isDatatype()); - DatatypeType dt0 = DatatypeType(datatypes[0]); - const Datatype& d0 = dt0.getDatatype(); + const DType& d0 = TypeNode::fromType(datatypes[0]).getDType(); if (d0.isTuple()) { // not necessary to print tuples @@ -1887,7 +1898,7 @@ static void toStream(std::ostream& out, for (const Type& t : datatypes) { Assert(t.isDatatype()); - const Datatype& d = DatatypeType(t).getDatatype(); + const DType& d = TypeNode::fromType(t).getDType(); out << "(" << CVC4::quoteSymbol(d.getName()); out << " " << d.getNumParameters() << ")"; } @@ -1895,7 +1906,7 @@ static void toStream(std::ostream& out, for (const Type& t : datatypes) { Assert(t.isDatatype()); - const Datatype& d = DatatypeType(t).getDatatype(); + const DType& d = TypeNode::fromType(t).getDType(); if (d.isParametric()) { out << "(par ("; @@ -1927,7 +1938,7 @@ static void toStream(std::ostream& out, for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++) { Assert(datatypes[j].isDatatype()); - const Datatype& dj = DatatypeType(datatypes[j]).getDatatype(); + const DType& dj = TypeNode::fromType(datatypes[j]).getDType(); if (dj.getNumParameters() != nparam) { success = false; @@ -1967,7 +1978,7 @@ static void toStream(std::ostream& out, for (const Type& t : datatypes) { Assert(t.isDatatype()); - const Datatype& dt = DatatypeType(t).getDatatype(); + const DType& dt = TypeNode::fromType(t).getDType(); out << "(" << CVC4::quoteSymbol(dt.getName()) << " "; toStream(out, dt); out << ")"; @@ -2011,13 +2022,13 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v) static void toStreamSygusGrammar(std::ostream& out, const Type& t) { if (!t.isNull() && t.isDatatype() - && static_cast(t).getDatatype().isSygus()) + && TypeNode::fromType(t).getDType().isSygus()) { std::stringstream types_predecl, types_list; - std::set grammarTypes; - std::list typesToPrint; - grammarTypes.insert(t); - typesToPrint.push_back(t); + std::set grammarTypes; + std::list typesToPrint; + grammarTypes.insert(TypeNode::fromType(t)); + typesToPrint.push_back(TypeNode::fromType(t)); NodeManager* nm = NodeManager::currentNM(); // for each datatype in grammar // name @@ -2025,28 +2036,28 @@ static void toStreamSygusGrammar(std::ostream& out, const Type& t) // constructors in order do { - Type curr = typesToPrint.front(); + TypeNode curr = typesToPrint.front(); typesToPrint.pop_front(); - Assert(curr.isDatatype() - && static_cast(curr).getDatatype().isSygus()); - const Datatype& dt = static_cast(curr).getDatatype(); + Assert(curr.isDatatype() && curr.getDType().isSygus()); + const DType& dt = curr.getDType(); types_list << '(' << dt.getName() << ' ' << dt.getSygusType() << " ("; types_predecl << '(' << dt.getName() << ' ' << dt.getSygusType() << ") "; if (dt.getSygusAllowConst()) { types_list << "(Constant " << dt.getSygusType() << ") "; } - for (const DatatypeConstructor& cons : dt) + for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) { + const DTypeConstructor& cons = dt[i]; // make a sygus term std::vector cchildren; - cchildren.push_back(Node::fromExpr(cons.getConstructor())); - for (const DatatypeConstructorArg& i : cons) + cchildren.push_back(cons.getConstructor()); + for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++) { - Type argType = i.getRangeType(); + TypeNode argType = cons[j].getRangeType(); std::stringstream ss; ss << argType; - Node bv = nm->mkBoundVar(ss.str(), TypeNode::fromType(argType)); + Node bv = nm->mkBoundVar(ss.str(), argType); cchildren.push_back(bv); // if fresh type, store it for later processing if (grammarTypes.insert(argType).second) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 585c2819d..c2d1a971e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1335,10 +1335,9 @@ void SmtEngine::declareSynthFun(const std::string& id, setUserAttribute("sygus-synth-fun-var-list", func, attr_val_bvl, ""); } // whether sygus type encodes syntax restrictions - if (sygusType.isDatatype() - && static_cast(sygusType).getDatatype().isSygus()) + TypeNode stn = TypeNode::fromType(sygusType); + if (sygusType.isDatatype() && stn.getDType().isSygus()) { - TypeNode stn = TypeNode::fromType(sygusType); Node sym = d_nodeManager->mkBoundVar("sfproxy", stn); std::vector attr_value; attr_value.push_back(sym.toExpr()); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9b8badc5e..17a43bc04 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -18,7 +18,6 @@ #include #include "base/check.h" -#include "expr/datatype.h" #include "expr/dtype.h" #include "expr/kind.h" #include "options/datatypes_options.h" @@ -654,10 +653,11 @@ TrustNode TheoryDatatypes::expandDefinition(Node n) } else { - Assert(tn.toType().isRecord()); - const Record& record = DatatypeType(tn.toType()).getRecord(); - size = record.getNumFields(); - updateIndex = record.getIndex( + Assert(tn.isRecord()); + const DTypeConstructor& recCons = dt[0]; + size = recCons.getNumArgs(); + // get the index for the name + updateIndex = recCons.getSelectorIndexForName( n.getOperator().getConst().getField()); } Debug("tuprec") << "expr is " << n << std::endl; diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index ac27acfb5..6d92668be 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::Datatype + ** \brief Black box testing of CVC4::DType ** - ** Black box testing of CVC4::Datatype. + ** Black box testing of CVC4::DType. **/ #include @@ -19,7 +19,7 @@ #include #include "api/cvc4cpp.h" -#include "expr/datatype.h" +#include "expr/dtype.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" @@ -33,8 +33,8 @@ class DatatypeBlack : public CxxTest::TestSuite { void setUp() override { d_slv = new api::Solver(); - d_em = d_slv->getExprManager(); - d_scope = new ExprManagerScope(*d_em); + d_nm = d_slv->getNodeManager(); + d_scope = new NodeManagerScope(d_nm); Debug.on("datatypes"); Debug.on("groundterms"); } @@ -46,12 +46,16 @@ class DatatypeBlack : public CxxTest::TestSuite { } void testEnumeration() { - Datatype colors(d_em, "colors"); + DType colors("colors"); - DatatypeConstructor yellow("yellow"); - DatatypeConstructor blue("blue"); - DatatypeConstructor green("green"); - DatatypeConstructor red("red"); + std::shared_ptr yellow = + std::make_shared("yellow"); + std::shared_ptr blue = + std::make_shared("blue"); + std::shared_ptr green = + std::make_shared("green"); + std::shared_ptr red = + std::make_shared("red"); colors.addConstructor(yellow); colors.addConstructor(blue); @@ -59,159 +63,171 @@ class DatatypeBlack : public CxxTest::TestSuite { colors.addConstructor(red); Debug("datatypes") << colors << std::endl; - DatatypeType colorsType = d_em->mkDatatypeType(colors); + TypeNode colorsType = d_nm->mkDatatypeType(colors); Debug("datatypes") << colorsType << std::endl; - Expr ctor = colorsType.getDatatype()[1].getConstructor(); - Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor); + Node ctor = colorsType.getDType()[1].getConstructor(); + Node apply = d_nm->mkNode(kind::APPLY_CONSTRUCTOR, ctor); Debug("datatypes") << apply << std::endl; - const Datatype& colorsDT = colorsType.getDatatype(); - TS_ASSERT(colorsDT.getConstructor("blue") == ctor); - TS_ASSERT(colorsDT["blue"].getConstructor() == ctor); - TS_ASSERT_THROWS(colorsDT["blue"].getSelector("foo"), - IllegalArgumentException&); - TS_ASSERT_THROWS(colorsDT["blue"]["foo"], IllegalArgumentException&); - - TS_ASSERT(! colorsType.getDatatype().isParametric()); - TS_ASSERT(colorsType.getDatatype().isFinite()); - TS_ASSERT(colorsType.getDatatype().getCardinality().compare(4) == Cardinality::EQUAL); + TS_ASSERT(!colorsType.getDType().isParametric()); + TS_ASSERT(colorsType.getDType().isFinite()); + TS_ASSERT(colorsType.getDType().getCardinality().compare(4) + == Cardinality::EQUAL); TS_ASSERT(ctor.getType().getCardinality().compare(1) == Cardinality::EQUAL); - TS_ASSERT(colorsType.getDatatype().isWellFounded()); - Debug("groundterms") << "ground term of " << colorsType.getDatatype().getName() << endl + TS_ASSERT(colorsType.getDType().isWellFounded()); + Debug("groundterms") << "ground term of " << colorsType.getDType().getName() + << endl << " is " << colorsType.mkGroundTerm() << endl; TS_ASSERT(colorsType.mkGroundTerm().getType() == colorsType); } void testNat() { - Datatype nat(d_em, "nat"); + DType nat("nat"); - DatatypeConstructor succ("succ"); - succ.addArg("pred", DatatypeSelfType()); + std::shared_ptr succ = + std::make_shared("succ"); + succ->addArgSelf("pred"); nat.addConstructor(succ); - DatatypeConstructor zero("zero"); + std::shared_ptr zero = + std::make_shared("zero"); nat.addConstructor(zero); Debug("datatypes") << nat << std::endl; - DatatypeType natType = d_em->mkDatatypeType(nat); + TypeNode natType = d_nm->mkDatatypeType(nat); Debug("datatypes") << natType << std::endl; - Expr ctor = natType.getDatatype()[1].getConstructor(); - Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor); + Node ctor = natType.getDType()[1].getConstructor(); + Node apply = d_nm->mkNode(kind::APPLY_CONSTRUCTOR, ctor); Debug("datatypes") << apply << std::endl; - TS_ASSERT(! natType.getDatatype().isParametric()); - TS_ASSERT(! natType.getDatatype().isFinite()); - TS_ASSERT(natType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); - TS_ASSERT(natType.getDatatype().isWellFounded()); - Debug("groundterms") << "ground term of " << natType.getDatatype().getName() << endl + TS_ASSERT(!natType.getDType().isParametric()); + TS_ASSERT(!natType.getDType().isFinite()); + TS_ASSERT(natType.getDType().getCardinality().compare(Cardinality::INTEGERS) + == Cardinality::EQUAL); + TS_ASSERT(natType.getDType().isWellFounded()); + Debug("groundterms") << "ground term of " << natType.getDType().getName() + << endl << " is " << natType.mkGroundTerm() << endl; TS_ASSERT(natType.mkGroundTerm().getType() == natType); } void testTree() { - Datatype tree(d_em, "tree"); - Type integerType = d_em->integerType(); + DType tree("tree"); + TypeNode integerType = d_nm->integerType(); - DatatypeConstructor node("node"); - node.addArg("left", DatatypeSelfType()); - node.addArg("right", DatatypeSelfType()); + std::shared_ptr node = + std::make_shared("node"); + node->addArgSelf("left"); + node->addArgSelf("right"); tree.addConstructor(node); - DatatypeConstructor leaf("leaf"); - leaf.addArg("leaf", integerType); + std::shared_ptr leaf = + std::make_shared("leaf"); + leaf->addArg("leaf", integerType); tree.addConstructor(leaf); Debug("datatypes") << tree << std::endl; - DatatypeType treeType = d_em->mkDatatypeType(tree); + TypeNode treeType = d_nm->mkDatatypeType(tree); Debug("datatypes") << treeType << std::endl; - Expr ctor = treeType.getDatatype()[1].getConstructor(); - TS_ASSERT(treeType.getConstructor("leaf") == ctor); - TS_ASSERT(treeType.getConstructor("leaf") == ctor); - TS_ASSERT_THROWS(treeType.getConstructor("leff"), - IllegalArgumentException&); - - TS_ASSERT(! treeType.getDatatype().isParametric()); - TS_ASSERT(! treeType.getDatatype().isFinite()); - TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); - TS_ASSERT(treeType.getDatatype().isWellFounded()); - Debug("groundterms") << "ground term of " << treeType.getDatatype().getName() << endl + TS_ASSERT(!treeType.getDType().isParametric()); + TS_ASSERT(!treeType.getDType().isFinite()); + TS_ASSERT( + treeType.getDType().getCardinality().compare(Cardinality::INTEGERS) + == Cardinality::EQUAL); + TS_ASSERT(treeType.getDType().isWellFounded()); + Debug("groundterms") << "ground term of " << treeType.getDType().getName() + << endl << " is " << treeType.mkGroundTerm() << endl; TS_ASSERT(treeType.mkGroundTerm().getType() == treeType); } void testListInt() { - Datatype list(d_em, "list"); - Type integerType = d_em->integerType(); + DType list("list"); + TypeNode integerType = d_nm->integerType(); - DatatypeConstructor cons("cons"); - cons.addArg("car", integerType); - cons.addArg("cdr", DatatypeSelfType()); + std::shared_ptr cons = + std::make_shared("cons"); + cons->addArg("car", integerType); + cons->addArgSelf("cdr"); list.addConstructor(cons); - DatatypeConstructor nil("nil"); + std::shared_ptr nil = + std::make_shared("nil"); list.addConstructor(nil); Debug("datatypes") << list << std::endl; - DatatypeType listType = d_em->mkDatatypeType(list); + TypeNode listType = d_nm->mkDatatypeType(list); Debug("datatypes") << listType << std::endl; - TS_ASSERT(! listType.getDatatype().isParametric()); - TS_ASSERT(! listType.getDatatype().isFinite()); - TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); - TS_ASSERT(listType.getDatatype().isWellFounded()); - Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl + TS_ASSERT(!listType.getDType().isParametric()); + TS_ASSERT(!listType.getDType().isFinite()); + TS_ASSERT( + listType.getDType().getCardinality().compare(Cardinality::INTEGERS) + == Cardinality::EQUAL); + TS_ASSERT(listType.getDType().isWellFounded()); + Debug("groundterms") << "ground term of " << listType.getDType().getName() + << endl << " is " << listType.mkGroundTerm() << endl; TS_ASSERT(listType.mkGroundTerm().getType() == listType); } void testListReal() { - Datatype list(d_em, "list"); - Type realType = d_em->realType(); + DType list("list"); + TypeNode realType = d_nm->realType(); - DatatypeConstructor cons("cons"); - cons.addArg("car", realType); - cons.addArg("cdr", DatatypeSelfType()); + std::shared_ptr cons = + std::make_shared("cons"); + cons->addArg("car", realType); + cons->addArgSelf("cdr"); list.addConstructor(cons); - DatatypeConstructor nil("nil"); + std::shared_ptr nil = + std::make_shared("nil"); list.addConstructor(nil); Debug("datatypes") << list << std::endl; - DatatypeType listType = d_em->mkDatatypeType(list); + TypeNode listType = d_nm->mkDatatypeType(list); Debug("datatypes") << listType << std::endl; - TS_ASSERT(! listType.getDatatype().isParametric()); - TS_ASSERT(! listType.getDatatype().isFinite()); - TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL); - TS_ASSERT(listType.getDatatype().isWellFounded()); - Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl + TS_ASSERT(!listType.getDType().isParametric()); + TS_ASSERT(!listType.getDType().isFinite()); + TS_ASSERT(listType.getDType().getCardinality().compare(Cardinality::REALS) + == Cardinality::EQUAL); + TS_ASSERT(listType.getDType().isWellFounded()); + Debug("groundterms") << "ground term of " << listType.getDType().getName() + << endl << " is " << listType.mkGroundTerm() << endl; TS_ASSERT(listType.mkGroundTerm().getType() == listType); } void testListBoolean() { - Datatype list(d_em, "list"); - Type booleanType = d_em->booleanType(); + DType list("list"); + TypeNode booleanType = d_nm->booleanType(); - DatatypeConstructor cons("cons"); - cons.addArg("car", booleanType); - cons.addArg("cdr", DatatypeSelfType()); + std::shared_ptr cons = + std::make_shared("cons"); + cons->addArg("car", booleanType); + cons->addArgSelf("cdr"); list.addConstructor(cons); - DatatypeConstructor nil("nil"); + std::shared_ptr nil = + std::make_shared("nil"); list.addConstructor(nil); Debug("datatypes") << list << std::endl; - DatatypeType listType = d_em->mkDatatypeType(list); + TypeNode listType = d_nm->mkDatatypeType(list); Debug("datatypes") << listType << std::endl; - TS_ASSERT(! listType.getDatatype().isFinite()); - TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); - TS_ASSERT(listType.getDatatype().isWellFounded()); - Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl + TS_ASSERT(!listType.getDType().isFinite()); + TS_ASSERT( + listType.getDType().getCardinality().compare(Cardinality::INTEGERS) + == Cardinality::EQUAL); + TS_ASSERT(listType.getDType().isWellFounded()); + Debug("groundterms") << "ground term of " << listType.getDType().getName() + << endl << " is " << listType.mkGroundTerm() << endl; TS_ASSERT(listType.mkGroundTerm().getType() == listType); } @@ -225,156 +241,192 @@ class DatatypeBlack : public CxxTest::TestSuite { * list = cons(car: tree, cdr: list) | nil * END; */ - Datatype tree(d_em, "tree"); - DatatypeConstructor node("node"); - node.addArg("left", DatatypeSelfType()); - node.addArg("right", DatatypeSelfType()); + std::set unresolvedTypes; + TypeNode unresList = + d_nm->mkSort("list", ExprManager::SORT_FLAG_PLACEHOLDER); + unresolvedTypes.insert(unresList); + TypeNode unresTree = + d_nm->mkSort("tree", ExprManager::SORT_FLAG_PLACEHOLDER); + unresolvedTypes.insert(unresTree); + + DType tree("tree"); + std::shared_ptr node = + std::make_shared("node"); + node->addArgSelf("left"); + node->addArgSelf("right"); tree.addConstructor(node); - DatatypeConstructor leaf("leaf"); - leaf.addArg("leaf", DatatypeUnresolvedType("list")); + std::shared_ptr leaf = + std::make_shared("leaf"); + leaf->addArg("leaf", unresList); tree.addConstructor(leaf); Debug("datatypes") << tree << std::endl; - Datatype list(d_em, "list"); - DatatypeConstructor cons("cons"); - cons.addArg("car", DatatypeUnresolvedType("tree")); - cons.addArg("cdr", DatatypeSelfType()); + DType list("list"); + std::shared_ptr cons = + std::make_shared("cons"); + cons->addArg("car", unresTree); + cons->addArgSelf("cdr"); list.addConstructor(cons); - DatatypeConstructor nil("nil"); + std::shared_ptr nil = + std::make_shared("nil"); list.addConstructor(nil); Debug("datatypes") << list << std::endl; TS_ASSERT(! tree.isResolved()); - TS_ASSERT(! node.isResolved()); - TS_ASSERT(! leaf.isResolved()); TS_ASSERT(! list.isResolved()); - TS_ASSERT(! cons.isResolved()); - TS_ASSERT(! nil.isResolved()); - vector dts; + vector dts; dts.push_back(tree); dts.push_back(list); - vector dtts = d_em->mkMutualDatatypeTypes(dts); + vector dtts = d_nm->mkMutualDatatypeTypes(dts, unresolvedTypes); - TS_ASSERT(dtts[0].getDatatype().isResolved()); - TS_ASSERT(dtts[1].getDatatype().isResolved()); + TS_ASSERT(dtts[0].getDType().isResolved()); + TS_ASSERT(dtts[1].getDType().isResolved()); - TS_ASSERT(! dtts[0].getDatatype().isFinite()); - TS_ASSERT(dtts[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); - TS_ASSERT(dtts[0].getDatatype().isWellFounded()); - Debug("groundterms") << "ground term of " << dtts[0].getDatatype().getName() << endl + TS_ASSERT(!dtts[0].getDType().isFinite()); + TS_ASSERT(dtts[0].getDType().getCardinality().compare(Cardinality::INTEGERS) + == Cardinality::EQUAL); + TS_ASSERT(dtts[0].getDType().isWellFounded()); + Debug("groundterms") << "ground term of " << dtts[0].getDType().getName() + << endl << " is " << dtts[0].mkGroundTerm() << endl; TS_ASSERT(dtts[0].mkGroundTerm().getType() == dtts[0]); - TS_ASSERT(! dtts[1].getDatatype().isFinite()); - TS_ASSERT(dtts[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); - TS_ASSERT(dtts[1].getDatatype().isWellFounded()); - Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl + TS_ASSERT(!dtts[1].getDType().isFinite()); + TS_ASSERT(dtts[1].getDType().getCardinality().compare(Cardinality::INTEGERS) + == Cardinality::EQUAL); + TS_ASSERT(dtts[1].getDType().isWellFounded()); + Debug("groundterms") << "ground term of " << dtts[1].getDType().getName() + << endl << " is " << dtts[1].mkGroundTerm() << endl; TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]); } void testMutualListTrees2() { - Datatype tree(d_em, "tree"); - DatatypeConstructor node("node"); - node.addArg("left", DatatypeSelfType()); - node.addArg("right", DatatypeSelfType()); + std::set unresolvedTypes; + TypeNode unresList = + d_nm->mkSort("list", ExprManager::SORT_FLAG_PLACEHOLDER); + unresolvedTypes.insert(unresList); + TypeNode unresTree = + d_nm->mkSort("tree", ExprManager::SORT_FLAG_PLACEHOLDER); + unresolvedTypes.insert(unresTree); + + DType tree("tree"); + std::shared_ptr node = + std::make_shared("node"); + node->addArgSelf("left"); + node->addArgSelf("right"); tree.addConstructor(node); - DatatypeConstructor leaf("leaf"); - leaf.addArg("leaf", DatatypeUnresolvedType("list")); + std::shared_ptr leaf = + std::make_shared("leaf"); + leaf->addArg("leaf", unresList); tree.addConstructor(leaf); - Datatype list(d_em, "list"); - DatatypeConstructor cons("cons"); - cons.addArg("car", DatatypeUnresolvedType("tree")); - cons.addArg("cdr", DatatypeSelfType()); + DType list("list"); + std::shared_ptr cons = + std::make_shared("cons"); + cons->addArg("car", unresTree); + cons->addArgSelf("cdr"); list.addConstructor(cons); - DatatypeConstructor nil("nil"); + std::shared_ptr nil = + std::make_shared("nil"); list.addConstructor(nil); // add another constructor to list datatype resulting in an // "otherNil-list" - DatatypeConstructor otherNil("otherNil"); + std::shared_ptr otherNil = + std::make_shared("otherNil"); list.addConstructor(otherNil); - vector dts; + vector dts; dts.push_back(tree); dts.push_back(list); // remake the types - vector dtts2 = d_em->mkMutualDatatypeTypes(dts); - - TS_ASSERT(! dtts2[0].getDatatype().isFinite()); - TS_ASSERT(dtts2[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); - TS_ASSERT(dtts2[0].getDatatype().isWellFounded()); - Debug("groundterms") << "ground term of " << dtts2[0].getDatatype().getName() << endl + vector dtts2 = d_nm->mkMutualDatatypeTypes(dts, unresolvedTypes); + + TS_ASSERT(!dtts2[0].getDType().isFinite()); + TS_ASSERT( + dtts2[0].getDType().getCardinality().compare(Cardinality::INTEGERS) + == Cardinality::EQUAL); + TS_ASSERT(dtts2[0].getDType().isWellFounded()); + Debug("groundterms") << "ground term of " << dtts2[0].getDType().getName() + << endl << " is " << dtts2[0].mkGroundTerm() << endl; TS_ASSERT(dtts2[0].mkGroundTerm().getType() == dtts2[0]); - TS_ASSERT(! dtts2[1].getDatatype().isParametric()); - TS_ASSERT(! dtts2[1].getDatatype().isFinite()); - TS_ASSERT(dtts2[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); - TS_ASSERT(dtts2[1].getDatatype().isWellFounded()); - Debug("groundterms") << "ground term of " << dtts2[1].getDatatype().getName() << endl + TS_ASSERT(!dtts2[1].getDType().isParametric()); + TS_ASSERT(!dtts2[1].getDType().isFinite()); + TS_ASSERT( + dtts2[1].getDType().getCardinality().compare(Cardinality::INTEGERS) + == Cardinality::EQUAL); + TS_ASSERT(dtts2[1].getDType().isWellFounded()); + Debug("groundterms") << "ground term of " << dtts2[1].getDType().getName() + << endl << " is " << dtts2[1].mkGroundTerm() << endl; TS_ASSERT(dtts2[1].mkGroundTerm().getType() == dtts2[1]); } void testNotSoWellFounded() { - Datatype tree(d_em, "tree"); + DType tree("tree"); - DatatypeConstructor node("node"); - node.addArg("left", DatatypeSelfType()); - node.addArg("right", DatatypeSelfType()); + std::shared_ptr node = + std::make_shared("node"); + node->addArgSelf("left"); + node->addArgSelf("right"); tree.addConstructor(node); Debug("datatypes") << tree << std::endl; - DatatypeType treeType = d_em->mkDatatypeType(tree); + TypeNode treeType = d_nm->mkDatatypeType(tree); Debug("datatypes") << treeType << std::endl; - TS_ASSERT(! treeType.getDatatype().isParametric()); - TS_ASSERT(! treeType.getDatatype().isFinite()); - TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); - TS_ASSERT(! treeType.getDatatype().isWellFounded()); - TS_ASSERT_THROWS_ANYTHING( treeType.mkGroundTerm() ); - TS_ASSERT_THROWS_ANYTHING( treeType.getDatatype().mkGroundTerm( treeType ) ); + TS_ASSERT(!treeType.getDType().isParametric()); + TS_ASSERT(!treeType.getDType().isFinite()); + TS_ASSERT( + treeType.getDType().getCardinality().compare(Cardinality::INTEGERS) + == Cardinality::EQUAL); + TS_ASSERT(!treeType.getDType().isWellFounded()); + TS_ASSERT(treeType.mkGroundTerm().isNull()); + TS_ASSERT(treeType.getDType().mkGroundTerm(treeType).isNull()); } - void testParametricDatatype() { - vector v; - Type t1, t2; - v.push_back(t1 = d_em->mkSort("T1")); - v.push_back(t2 = d_em->mkSort("T2")); - Datatype pair(d_em, "pair", v); - - DatatypeConstructor mkpair("mk-pair"); - mkpair.addArg("first", t1); - mkpair.addArg("second", t2); + void testParametricDType() + { + vector v; + TypeNode t1, t2; + v.push_back(t1 = d_nm->mkSort("T1")); + v.push_back(t2 = d_nm->mkSort("T2")); + DType pair("pair", v); + + std::shared_ptr mkpair = + std::make_shared("mk-pair"); + mkpair->addArg("first", t1); + mkpair->addArg("second", t2); pair.addConstructor(mkpair); - DatatypeType pairType = d_em->mkDatatypeType(pair); + TypeNode pairType = d_nm->mkDatatypeType(pair); - TS_ASSERT(pairType.getDatatype().isParametric()); + TS_ASSERT(pairType.getDType().isParametric()); v.clear(); - v.push_back(d_em->integerType()); - v.push_back(d_em->integerType()); - DatatypeType pairIntInt = pairType.getDatatype().getDatatypeType(v); + v.push_back(d_nm->integerType()); + v.push_back(d_nm->integerType()); + TypeNode pairIntInt = pairType.getDType().getTypeNode(v); v.clear(); - v.push_back(d_em->realType()); - v.push_back(d_em->realType()); - DatatypeType pairRealReal = pairType.getDatatype().getDatatypeType(v); + v.push_back(d_nm->realType()); + v.push_back(d_nm->realType()); + TypeNode pairRealReal = pairType.getDType().getTypeNode(v); v.clear(); - v.push_back(d_em->realType()); - v.push_back(d_em->integerType()); - DatatypeType pairRealInt = pairType.getDatatype().getDatatypeType(v); + v.push_back(d_nm->realType()); + v.push_back(d_nm->integerType()); + TypeNode pairRealInt = pairType.getDType().getTypeNode(v); v.clear(); - v.push_back(d_em->integerType()); - v.push_back(d_em->realType()); - DatatypeType pairIntReal = pairType.getDatatype().getDatatypeType(v); + v.push_back(d_nm->integerType()); + v.push_back(d_nm->realType()); + TypeNode pairIntReal = pairType.getDType().getTypeNode(v); TS_ASSERT_DIFFERS(pairIntInt, pairRealReal); TS_ASSERT_DIFFERS(pairIntReal, pairRealReal); @@ -417,26 +469,34 @@ class DatatypeBlack : public CxxTest::TestSuite { TS_ASSERT(!pairRealInt.isSubtypeOf(pairIntInt)); TS_ASSERT(pairIntInt.isSubtypeOf(pairIntInt)); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealReal)).toType(), pairRealReal); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealReal)).isNull()); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealReal)).isNull()); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealReal)).isNull()); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealInt)).isNull()); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealInt)).isNull()); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealInt)).toType(), pairRealInt); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealInt)).isNull()); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntReal)).isNull()); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntReal)).toType(), pairIntReal); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntReal)).isNull()); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntReal)).isNull()); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntInt)).isNull()); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntInt)).isNull()); - TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntInt)).isNull()); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt); + TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairRealReal, pairRealReal), + pairRealReal); + TS_ASSERT( + TypeNode::leastCommonTypeNode(pairIntReal, pairRealReal).isNull()); + TS_ASSERT( + TypeNode::leastCommonTypeNode(pairRealInt, pairRealReal).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairRealReal).isNull()); + TS_ASSERT( + TypeNode::leastCommonTypeNode(pairRealReal, pairRealInt).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntReal, pairRealInt).isNull()); + TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairRealInt, pairRealInt), + pairRealInt); + TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairRealInt).isNull()); + TS_ASSERT( + TypeNode::leastCommonTypeNode(pairRealReal, pairIntReal).isNull()); + TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairIntReal, pairIntReal), + pairIntReal); + TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealInt, pairIntReal).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairIntReal).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealReal, pairIntInt).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntReal, pairIntInt).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealInt, pairIntInt).isNull()); + TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairIntInt, pairIntInt), + pairIntInt); } private: api::Solver* d_slv; - ExprManager* d_em; - ExprManagerScope* d_scope; -};/* class DatatypeBlack */ + NodeManager* d_nm; + NodeManagerScope* d_scope; +}; /* class DTypeBlack */