diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-06 13:41:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-06 13:41:24 -0500 |
commit | 816d5e7624c9d088c469f7e23d11394f5b385b84 (patch) | |
tree | bbb39e63a6b00c45be028d9be51b5a22cc640ddb /src | |
parent | 956ffda5632b388a887003a5e030696091339bd2 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/datatype.cpp | 1 | ||||
-rw-r--r-- | src/expr/dtype_cons.cpp | 2 | ||||
-rw-r--r-- | src/expr/symbol_table.cpp | 6 | ||||
-rw-r--r-- | src/expr/type.cpp | 18 | ||||
-rw-r--r-- | src/expr/type.h | 10 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 10 | ||||
-rw-r--r-- | src/expr/type_node.h | 3 | ||||
-rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 5 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 68 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 89 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 10 |
12 files changed, 111 insertions, 116 deletions
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<DTypeSelector> a = - std::make_shared<DTypeSelector>(selectorName, Node::null()); + std::make_shared<DTypeSelector>(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<DatatypeType>(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<Type> 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<Type> 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<Type> 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> 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<DatatypeIndexConstant>().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<DatatypeType>(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<Type>& 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<DatatypeType>(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<SelectorType>(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<Type>& 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<DatatypeType>(t).getDatatype().isSygus()) + && TypeNode::fromType(t).getDType().isSygus()) { std::stringstream types_predecl, types_list; - std::set<Type> grammarTypes; - std::list<Type> typesToPrint; - grammarTypes.insert(t); - typesToPrint.push_back(t); + std::set<TypeNode> grammarTypes; + std::list<TypeNode> 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<DatatypeType>(curr).getDatatype().isSygus()); - const Datatype& dt = static_cast<DatatypeType>(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<Node> 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<DatatypeType>(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<Expr> 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 <map> #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<RecordUpdate>().getField()); } Debug("tuprec") << "expr is " << n << std::endl; |