From b71bbbbc607b5ca0c2bec8b8cf6c7af596d21997 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Apr 2014 04:28:44 -0500 Subject: [PATCH] Add initial support for co-datatypes. --- src/compat/cvc3_compat.cpp | 2 +- src/parser/cvc/Cvc.g | 2 +- src/parser/smt2/Smt2.g | 38 ++- src/smt/boolean_terms.cpp | 4 +- src/theory/builtin/kinds | 2 + .../builtin/theory_builtin_type_rules.h | 18 ++ src/theory/datatypes/theory_datatypes.cpp | 284 +++++++++++++++--- src/theory/datatypes/theory_datatypes.h | 8 + src/util/datatype.h | 18 +- 9 files changed, 310 insertions(+), 66 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 27d1249a1..427282490 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1189,7 +1189,7 @@ void ValidityChecker::dataType(const std::vector& names, // Set up the datatype specifications. for(unsigned i = 0; i < names.size(); ++i) { - CVC4::Datatype dt(names[i]); + CVC4::Datatype dt(names[i], false); CVC4::CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size"); CVC4::CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size"); for(unsigned j = 0; j < constructors[i].size(); ++j) { diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 792c3cf9d..f9055f5db 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2018,7 +2018,7 @@ datatypeDef[std::vector& datatypes] params.push_back( t ); } )* RBRACKET )? - { datatypes.push_back(Datatype(id, params)); + { datatypes.push_back(Datatype(id, params, false)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 659fc97d9..2118a240d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -464,17 +464,8 @@ extendedCommand[CVC4::Command*& cmd] } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ - : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { /* open a scope to keep the UnresolvedTypes contained */ - PARSER_STATE->pushScope(true); } - LPAREN_TOK /* parametric sorts */ - ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { - sorts.push_back( PARSER_STATE->mkSort(name) ); } - )* - RPAREN_TOK - LPAREN_TOK ( LPAREN_TOK datatypeDef[dts, sorts] RPAREN_TOK )+ RPAREN_TOK - { PARSER_STATE->popScope(); - cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] + | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | /* get model */ GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd = new GetModelCommand(); } @@ -603,6 +594,26 @@ extendedCommand[CVC4::Command*& cmd] { cmd = new SimplifyCommand(e); } ; + +datatypesDefCommand[bool isCo, CVC4::Command*& cmd] +@declarations { + std::vector dts; + std::string name; + std::vector sorts; +} + : { PARSER_STATE->checkThatLogicIsSet(); + /* open a scope to keep the UnresolvedTypes contained */ + PARSER_STATE->pushScope(true); } + LPAREN_TOK /* parametric sorts */ + ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { + sorts.push_back( PARSER_STATE->mkSort(name) ); } + )* + RPAREN_TOK + LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK + { PARSER_STATE->popScope(); + cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + ; + rewriterulesCommand[CVC4::Command*& cmd] @declarations { std::vector > sortedVarNames; @@ -1530,7 +1541,7 @@ nonemptyNumeralList[std::vector& numerals] /** * Parses a datatype definition */ -datatypeDef[std::vector& datatypes, std::vector< CVC4::Type >& params] +datatypeDef[bool isCo, std::vector& datatypes, std::vector< CVC4::Type >& params] @init { std::string id; } @@ -1548,7 +1559,7 @@ datatypeDef[std::vector& datatypes, std::vector< CVC4::Type >& p params.push_back( t ); } )* ']' )?*/ //AJR: this isn't necessary if we use z3's style - { datatypes.push_back(Datatype(id,params)); + { datatypes.push_back(Datatype(id,params,isCo)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); @@ -1623,6 +1634,7 @@ AS_TOK : 'as'; // extended commands DECLARE_DATATYPES_TOK : 'declare-datatypes'; +DECLARE_CODATATYPES_TOK : 'declare-codatatypes'; GET_MODEL_TOK : 'get-model'; ECHO_TOK : 'echo'; REWRITE_RULE_TOK : 'assert-rewrite'; diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index e46a76ed7..c779af4ff 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -228,9 +228,9 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw( } vector newDtVector; if(dt.isParametric()) { - newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters())); + newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters(), false)); } else { - newDtVector.push_back(Datatype(dt.getName() + "'")); + newDtVector.push_back(Datatype(dt.getName() + "'", false)); } Datatype& newDt = newDtVector.front(); Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl; diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index b3383e6c4..d140d1990 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -302,6 +302,7 @@ variable SKOLEM "skolem var" operator SEXPR 0: "a symbolic expression" operator LAMBDA 2 "lambda" +operator MU 2 "mu" parameterized CHAIN CHAIN_OP 2: "chained operator" constant CHAIN_OP \ @@ -334,6 +335,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule +typerule MU ::CVC4::theory::builtin::MuTypeRule typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index c7143bdeb..f35286f05 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -164,6 +164,24 @@ public: } };/* class LambdaTypeRule */ +class MuTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + if( n[0].getType(check) != nodeManager->boundVarListType() ) { + std::stringstream ss; + ss << "expected a bound var list for MU expression, got `" + << n[0].getType().toString() << "'"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + std::vector argTypes; + for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) { + argTypes.push_back((*i).getType()); + } + TypeNode rangeType = n[1].getType(check); + return nodeManager->mkFunctionType(argTypes, rangeType); + } +};/* class MuTypeRule */ + class ChainTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 0b0f5807c..fc37c5417 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -123,13 +123,19 @@ void TheoryDatatypes::check(Effort e) { if( e == EFFORT_FULL ) { //check for cycles - checkCycles(); - if( d_conflict ){ - return; - } + bool addedFact; + do { + checkCycles(); + addedFact = !d_pending.empty() || !d_pending_merge.empty(); + flushPendingFacts(); + if( d_conflict ){ + return; + } + }while( addedFact ); + //check for splits Debug("datatypes-split") << "Check for splits " << e << endl; - bool addedFact = false; + addedFact = false; do { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ @@ -146,7 +152,7 @@ void TheoryDatatypes::check(Effort e) { Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n ); d_pending.push_back( t ); d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true ); - Trace("datatypes-infer") << "DtInfer : " << t << ", trivial" << std::endl; + Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; d_infer.push_back( t ); }else{ std::vector< bool > pcons; @@ -493,21 +499,37 @@ bool TheoryDatatypes::propagate(TNode literal){ return ok; } +void TheoryDatatypes::addAssumptions( std::vector& assumptions, std::vector& tassumptions ) { + for( unsigned i=0; i& assumptions ) { + if( a!=b ){ + std::vector tassumptions; + d_equalityEngine.explainEquality(a, b, polarity, tassumptions); + addAssumptions( assumptions, tassumptions ); + } +} + +void TheoryDatatypes::explainPredicate( TNode p, bool polarity, std::vector& assumptions ) { + std::vector tassumptions; + d_equalityEngine.explainPredicate(p, polarity, tassumptions); + addAssumptions( assumptions, tassumptions ); +} + /** explain */ void TheoryDatatypes::explain(TNode literal, std::vector& assumptions){ Debug("datatypes-explain") << "Explain " << literal << std::endl; bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - std::vector tassumptions; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions); + explainEquality( atom[0], atom[1], polarity, assumptions ); } else { - d_equalityEngine.explainPredicate(atom, polarity, tassumptions); - } - for( unsigned i=0; i assumptions; explain( t, assumptions ); - explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions ); + explainEquality( eqc->d_constructor.get(), tt[0], true, assumptions ); d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); @@ -808,7 +830,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; d_pending.push_back( t_concl ); d_pending_exp[ t_concl ] = t_concl_exp; - Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl; + Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl; d_infer.push_back( t_concl ); d_infer_exp.push_back( t_concl_exp ); return; @@ -822,7 +844,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ std::vector< TNode > assumptions; explain( j, assumptions ); explain( t, assumptions ); - explain( jt[0].eqNode( tt[0] ), assumptions ); + explainEquality( jt[0], tt[0], true, assumptions ); d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); @@ -866,7 +888,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ Node n = *i; std::vector< TNode > assumptions; explain( *i, assumptions ); - explain( c.eqNode( (*i)[0][0] ), assumptions ); + explainEquality( c, (*i)[0][0], true, assumptions ); d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); @@ -901,7 +923,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { d_pending.push_back( eq ); d_pending_exp[ eq ] = eq_exp; - Trace("datatypes-infer") << "DtInfer : " << eq << " by " << eq_exp << " (collapse selector)" << std::endl; + Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl; d_infer.push_back( eq ); d_infer_exp.push_back( eq_exp ); } @@ -1141,7 +1163,7 @@ void TheoryDatatypes::processNewTerm( Node n ){ Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n ); d_pending.push_back( eq ); d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); - Trace("datatypes-infer") << "DtInfer : " << eq << ", trivial" << std::endl; + Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl; d_infer.push_back( eq ); } } @@ -1219,7 +1241,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl; d_pending.push_back( eq ); d_pending_exp[ eq ] = exp; - Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl; + Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl; //eqc->d_inst.set( eq ); d_infer.push_back( eq ); d_infer_exp.push_back( exp ); @@ -1233,33 +1255,201 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ void TheoryDatatypes::checkCycles() { Debug("datatypes-cycle-check") << "Check cycles" << std::endl; + std::vector< Node > cod_eqc; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); if( DatatypesRewriter::isTermDatatype( eqc ) ) { - map< Node, bool > visited; - std::vector< TNode > expl; - Node cn = searchForCycle( eqc, eqc, visited, expl ); - //if we discovered a different cycle while searching this one - if( !cn.isNull() && cn!=eqc ){ - visited.clear(); - expl.clear(); - Node prev = cn; - cn = searchForCycle( cn, cn, visited, expl ); - Assert( prev==cn ); - } + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); + if( !dt.isCodatatype() ){ + //do cycle checks + map< Node, bool > visited; + std::vector< TNode > expl; + Node cn = searchForCycle( eqc, eqc, visited, expl ); + //if we discovered a different cycle while searching this one + if( !cn.isNull() && cn!=eqc ){ + visited.clear(); + expl.clear(); + Node prev = cn; + cn = searchForCycle( cn, cn, visited, expl ); + Assert( prev==cn ); + } - if( !cn.isNull() ) { - Assert( expl.size()>0 ); - d_conflictNode = mkAnd( expl ); - Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_conflict = true; - return; + if( !cn.isNull() ) { + Assert( expl.size()>0 ); + d_conflictNode = mkAnd( expl ); + Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; + } + }else{ + //indexing + cod_eqc.push_back( eqc ); } } ++eqcs_i; } + //process codatatypes + if( cod_eqc.size()>1 ){ + std::vector< std::vector< Node > > part_out; + std::vector< TNode > exp; + std::map< Node, Node > cn; + std::map< Node, std::map< Node, int > > dni; + for( unsigned i=0; i part; + part.push_back( part_out[i][0] ); + for( unsigned j=1; j > tpart_out; + exp.clear(); + cn.clear(); + cn[part_out[i][0]] = part_out[i][0]; + cn[part_out[i][j]] = part_out[i][j]; + dni.clear(); + separateBisimilar( part, tpart_out, exp, cn, dni, 0, true ); + Assert( tpart_out.size()==1 && tpart_out[0].size()==2 ); + part.pop_back(); + //merge based on explanation + Trace("dt-cod") << " exp is : "; + for( unsigned k=0; k& part, std::vector< std::vector< Node > >& part_out, + std::vector< TNode >& exp, + std::map< Node, Node >& cn, + std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ){ + if( !mkExp ){ + Trace("dt-cod-debug") << "Separate bisimilar : " << std::endl; + for( unsigned i=0; isecond << std::endl; } + new_part_rec[ it_rec->second ].push_back( part[j] ); + }else{ + if( DatatypesRewriter::isTermDatatype( c ) ){ + bool foundCons = false; + EqcInfo* eqc = getOrMakeEqcInfo( c, false ); + if( eqc ){ + Node ncons = eqc->d_constructor.get(); + if( !ncons.isNull() ) { + foundCons = true; + Node cc = ncons.getOperator(); + cn_cons[part[j]] = ncons; + if( mkExp ){ + explainEquality( c, ncons, true, exp ); + } + new_part[cc].push_back( part[j] ); + if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is datatype " << ncons << "." << std::endl; } + } + } + if( !foundCons ){ + new_part_c[c].push_back( part[j] ); + if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is unspecified datatype." << std::endl; } + } + }else{ + //add equivalences + if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is term " << c << "." << std::endl; } + new_part_c[c].push_back( part[j] ); + } + } + } + //direct add for constants + for( std::map< Node, std::vector< Node > >::iterator it = new_part_c.begin(); it != new_part_c.end(); ++it ){ + if( it->second.size()>1 ){ + std::vector< Node > vec; + vec.insert( vec.begin(), it->second.begin(), it->second.end() ); + part_out.push_back( vec ); + } + } + //direct add for recursive + for( std::map< int, std::vector< Node > >::iterator it = new_part_rec.begin(); it != new_part_rec.end(); ++it ){ + if( it->second.size()>1 ){ + std::vector< Node > vec; + vec.insert( vec.begin(), it->second.begin(), it->second.end() ); + part_out.push_back( vec ); + }else{ + //add back : could match a datatype? + } + } + //recurse for the datatypes + for( std::map< Node, std::vector< Node > >::iterator it = new_part.begin(); it != new_part.end(); ++it ){ + if( it->second.size()>1 ){ + //set dni to check for loops + std::map< Node, Node > dni_rem; + for( unsigned i=0; isecond.size(); i++ ){ + Node n = it->second[i]; + dni[n][cn[n]] = dniLvl; + dni_rem[n] = cn[n]; + } + + //we will split based on the arguments of the datatype + std::vector< std::vector< Node > > split_new_part; + split_new_part.push_back( it->second ); + + unsigned nChildren = cn_cons[it->second[0]].getNumChildren(); + //for each child of constructor + unsigned cindex = 0; + while( cindexfirst << "..." << std::endl; } + std::vector< std::vector< Node > > next_split_new_part; + for( unsigned j=0; j > c_part_out; + separateBisimilar( split_new_part[j], c_part_out, exp, cn, dni, dniLvl+1, mkExp ); + next_split_new_part.insert( next_split_new_part.end(), c_part_out.begin(), c_part_out.end() ); + } + split_new_part.clear(); + split_new_part.insert( split_new_part.end(), next_split_new_part.begin(), next_split_new_part.end() ); + cindex++; + } + part_out.insert( part_out.end(), split_new_part.begin(), split_new_part.end() ); + + for( std::map< Node, Node >::iterator it2 = dni_rem.begin(); it2 != dni_rem.end(); ++it2 ){ + dni[it2->first].erase( it2->second ); + } + } + } } //postcondition: if cycle detected, explanation is why n is a subterm of on @@ -1272,8 +1462,7 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on, if( !firstTime ){ nn = getRepresentative( n ); if( nn==on ){ - Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, nn ); - explain( lit, explanation ); + explainEquality( n, nn, true, explanation ); return on; } }else{ @@ -1293,8 +1482,7 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on, //} //add explanation for why the constructor is connected if( n != ncons ) { - Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, ncons ); - explain( lit, explanation ); + explainEquality( n, ncons, true, explanation ); } return on; }else if( !cn.isNull() ){ @@ -1306,7 +1494,13 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on, visited.erase( nn ); return Node::null(); }else{ - return nn; + if( DatatypesRewriter::isTermDatatype( nn ) ) { + const Datatype& dt = ((DatatypeType)(nn.getType()).toType()).getDatatype(); + if( !dt.isCodatatype() ){ + return nn; + } + } + return Node::null(); } } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 2a93878d0..eb8d792cf 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -195,6 +195,9 @@ public: /** propagate */ bool propagate(TNode literal); /** explain */ + void addAssumptions( std::vector& assumptions, std::vector& tassumptions ); + void explainEquality( TNode a, TNode b, bool polarity, std::vector& assumptions ); + void explainPredicate( TNode p, bool polarity, std::vector& assumptions ); void explain( TNode literal, std::vector& assumptions ); Node explain( TNode literal ); /** Conflict when merging two constants */ @@ -236,6 +239,11 @@ private: Node searchForCycle( Node n, Node on, std::map< Node, bool >& visited, std::vector< TNode >& explanation, bool firstTime = true ); + /** for checking whether two codatatype terms must be equal */ + void separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out, + std::vector< TNode >& exp, + std::map< Node, Node >& cn, + std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ); /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ diff --git a/src/util/datatype.h b/src/util/datatype.h index 02e0b6be8..a8f3b404a 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -448,6 +448,7 @@ public: private: std::string d_name; std::vector d_params; + bool d_isCo; std::vector d_constructors; bool d_resolved; Type d_self; @@ -494,13 +495,13 @@ private: public: /** Create a new Datatype of the given name. */ - inline explicit Datatype(std::string name); + inline explicit Datatype(std::string name, bool isCo = false); /** * Create a new Datatype of the given name, with the given * parameterization. */ - inline Datatype(std::string name, const std::vector& params); + inline Datatype(std::string name, const std::vector& params, bool isCo = false); /** * Add a constructor to this Datatype. Constructor names need not @@ -526,6 +527,9 @@ public: /** Get parameters */ inline std::vector getParameters() const; + /** is this a co-datatype? */ + inline bool isCodatatype() const; + /** * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be @@ -662,18 +666,20 @@ inline std::string DatatypeUnresolvedType::getName() const throw() { return d_name; } -inline Datatype::Datatype(std::string name) : +inline Datatype::Datatype(std::string name, bool isCo) : d_name(name), d_params(), + d_isCo(isCo), d_constructors(), d_resolved(false), d_self(), d_card(CardinalityUnknown()) { } -inline Datatype::Datatype(std::string name, const std::vector& params) : +inline Datatype::Datatype(std::string name, const std::vector& params, bool isCo) : d_name(name), d_params(params), + d_isCo(isCo), d_constructors(), d_resolved(false), d_self(), @@ -707,6 +713,10 @@ inline std::vector Datatype::getParameters() const { return d_params; } +inline bool Datatype::isCodatatype() const { + return d_isCo; +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } -- 2.30.2