diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-02 14:25:07 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-02 14:25:07 -0600 |
commit | c3c8d013d2a879eaa1d205e57af32a7f8bb8c0b7 (patch) | |
tree | f4a8372d8cd693df5f33e8d49cea53dbb418349e /src/theory | |
parent | 623e701247ed08e3f59d57b18ebe42f4d4db221e (diff) |
Bug fixes and refactoring of parametric datatypes, add some regressions.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 11 | ||||
-rw-r--r-- | src/theory/datatypes/datatypes_sygus.cpp | 14 | ||||
-rw-r--r-- | src/theory/datatypes/kinds | 4 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 42 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.cpp | 6 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv_sol.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 26 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 2 | ||||
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 2 |
14 files changed, 62 insertions, 73 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index dd2803d30..e58289568 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -134,7 +134,7 @@ public: //if( !tn.isSort() ){ // useTe = false; //} - if( isTypeDatatype( tn ) ){ + if( tn.isDatatype() ){ const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype(); useTe = !dta.isCodatatype(); } @@ -376,15 +376,6 @@ public: } return true; } - - /** is this term a datatype */ - static bool isTermDatatype( TNode n ){ - TypeNode tn = n.getType(); - return tn.isDatatype() || tn.isParametricDatatype(); - } - static bool isTypeDatatype( TypeNode tn ){ - return tn.isDatatype() || tn.isParametricDatatype(); - } private: static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending, std::vector< Node >& terms, std::map< Node, bool >& cdts ){ diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 0ecc6e547..fe07e44da 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -57,7 +57,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > if( sIndex==1 && pdt[csIndex].getNumArgs()==2 ){ arg1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] ); tn1 = arg1.getType(); - if( !DatatypesRewriter::isTypeDatatype( tn1 ) ){ + if( !tn1.isDatatype() ){ arg1 = Node::null(); } } @@ -193,7 +193,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > void SygusSplit::registerSygusType( TypeNode tn ) { if( d_register.find( tn )==d_register.end() ){ - if( !DatatypesRewriter::isTypeDatatype( tn ) ){ + if( !tn.isDatatype() ){ d_register[tn] = TypeNode::null(); }else{ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); @@ -319,7 +319,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& if( parentKind!=UNDEFINED_KIND && pdt[csIndex].getNumArgs()==2 ){ int osIndex = sIndex==0 ? 1 : 0; TypeNode tnno = d_tds->getArgType( pdt[csIndex], osIndex ); - if( DatatypesRewriter::isTypeDatatype( tnno ) ){ + if( tnno.isDatatype() ){ const Datatype& dto = ((DatatypeType)(tnno).toType()).getDatatype(); registerSygusTypeConstructorArg( tnno, dto, tnnp, pdt, csIndex, osIndex ); //compute relationships when doing 0-arg @@ -700,7 +700,7 @@ int SygusSplit::getFirstArgOccurrence( const DatatypeConstructor& c, const Datat bool SygusSplit::isArgDatatype( const DatatypeConstructor& c, int i, const Datatype& dt ) { TypeNode tni = d_tds->getArgType( c, i ); - if( datatypes::DatatypesRewriter::isTypeDatatype( tni ) ){ + if( tni.isDatatype() ){ const Datatype& adt = ((DatatypeType)(tni).toType()).getDatatype(); if( adt==dt ){ return true; @@ -784,7 +784,7 @@ void SygusSymBreak::addTester( int tindex, Node n, Node exp ) { if( it==d_prog_search.end() ){ //check if sygus type TypeNode tn = a.getType(); - Assert( DatatypesRewriter::isTypeDatatype( tn ) ); + Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); if( dt.isSygus() ){ ps = new ProgSearch( this, a, d_context ); @@ -837,7 +837,7 @@ void SygusSymBreak::ProgSearch::addTester( int tindex, Node n, Node exp ) { bool SygusSymBreak::ProgSearch::assignTester( int tindex, Node n, int depth ) { Trace("sygus-sym-break-debug") << "SymBreak : Assign tester : " << tindex << " " << n << ", depth = " << depth << " of " << d_anchor << std::endl; TypeNode tn = n.getType(); - Assert( DatatypesRewriter::isTypeDatatype( tn ) ); + Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); std::vector< Node > tst_waiting; for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){ @@ -941,7 +941,7 @@ Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog int tindex = DatatypesRewriter::isTester( tst );//Datatype::indexOf( tst.getOperator().toExpr() ); Assert( tindex!=-1 ); TypeNode tn = prog.getType(); - Assert( DatatypesRewriter::isTypeDatatype( tn ) ); + Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); std::map< int, Node > pre; if( curr_depth<depth ){ diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 42399d61f..efee5e876 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -44,7 +44,7 @@ constant DATATYPE_TYPE \ "expr/datatype.h" \ "a datatype type index" cardinality DATATYPE_TYPE \ - "%TYPE%.getDatatype().getCardinality()" \ + "%TYPE%.getDatatype().getCardinality(%TYPE%.toType())" \ "expr/datatype.h" well-founded DATATYPE_TYPE \ "%TYPE%.getDatatype().isWellFounded()" \ @@ -57,7 +57,7 @@ enumerator DATATYPE_TYPE \ operator PARAMETRIC_DATATYPE 1: "parametric datatype" cardinality PARAMETRIC_DATATYPE \ - "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \ + "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality(%TYPE%.toType())" \ "expr/datatype.h" well-founded PARAMETRIC_DATATYPE \ "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 59b9f1d96..3d114f9f1 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -185,16 +185,17 @@ void TheoryDatatypes::check(Effort e) { while( !eqcs_i.isFinished() ){ Node n = (*eqcs_i); TypeNode tn = n.getType(); - if( DatatypesRewriter::isTypeDatatype( tn ) ){ + if( tn.isDatatype() ){ Trace("datatypes-debug") << "Process equivalence class " << n << std::endl; EqcInfo* eqc = getOrMakeEqcInfo( n ); //if there are more than 1 possible constructors for eqc if( !hasLabel( eqc, n ) ){ Trace("datatypes-debug") << "No constructor..." << std::endl; - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isInterpretedFinite() << " " << dt.isRecursiveSingleton() << std::endl; + Type tt = tn.toType(); + const Datatype& dt = ((DatatypeType)tt).getDatatype(); + Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite( tt ) << " " << dt.isInterpretedFinite( tt ) << " " << dt.isRecursiveSingleton( tt ) << std::endl; bool continueProc = true; - if( dt.isRecursiveSingleton() ){ + if( dt.isRecursiveSingleton( tt ) ){ Trace("datatypes-debug") << "Check recursive singleton..." << std::endl; //handle recursive singleton case std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn ); @@ -209,8 +210,8 @@ void TheoryDatatypes::check(Effort e) { // do not infer the equality if at least one sort was processed. //otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one, // infer the equality. - for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes(); i++ ){ - TypeNode tn = TypeNode::fromType( dt.getRecursiveSingletonArgType( i ) ); + for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes( tt ); i++ ){ + TypeNode tn = TypeNode::fromType( dt.getRecursiveSingletonArgType( tt, i ) ); if( getQuantifiersEngine() ){ // under the assumption that the cardinality of this type is one Node a = getSingletonLemma( tn, true ); @@ -253,7 +254,7 @@ void TheoryDatatypes::check(Effort e) { if( consIndex==-1 ){ consIndex = j; } - if( !dt[ j ].isInterpretedFinite() ) { + if( !dt[ j ].isInterpretedFinite( tt ) ) { if( !eqc || !eqc->d_selectors ){ needSplit = false; } @@ -773,7 +774,7 @@ void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){ /** called when two equivalance classes have merged */ void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){ - if( DatatypesRewriter::isTermDatatype( t1 ) ){ + if( t1.getType().isDatatype() ){ Trace("datatypes-debug") << "NotifyPostMerge : " << t1 << " " << t2 << std::endl; d_pending_merge.push_back( t1.eqNode( t2 ) ); } @@ -1441,7 +1442,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ while( !eqccs_i.isFinished() ){ Node eqc = (*eqccs_i); //for all equivalence classes that are datatypes - if( DatatypesRewriter::isTermDatatype( eqc ) ){ + if( eqc.getType().isDatatype() ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); if( ei && !ei->d_constructor.get().isNull() ){ Node c = ei->d_constructor.get(); @@ -1467,7 +1468,8 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Node eqc = nodes[index]; Node neqc; bool addCons = false; - const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); + Type tt = eqc.getType().toType(); + const Datatype& dt = ((DatatypeType)tt).getDatatype(); if( !d_equalityEngine.hasTerm( eqc ) ){ Assert( false ); /* @@ -1533,12 +1535,12 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ if( neqc.isNull() ){ for( unsigned i=0; i<pcons.size(); i++ ){ //must try the infinite ones first - bool cfinite = dt[ i ].isInterpretedFinite(); + bool cfinite = dt[ i ].isInterpretedFinite( tt ); if( pcons[i] && (r==1)==cfinite ){ neqc = DatatypesRewriter::getInstCons( eqc, dt, i ); //for( unsigned j=0; j<neqc.getNumChildren(); j++ ){ - // //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){ - // if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){ + // //if( sels[i].find( j )==sels[i].end() && neqc[j].getType().isDatatype() ){ + // if( !d_equalityEngine.hasTerm( neqc[j] ) && neqc[j].getType().isDatatype() ){ // nodes.push_back( neqc[j] ); // } //} @@ -1586,7 +1588,7 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c if( itv!=vmap.end() ){ int debruijn = depth - 1 - itv->second; return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn)); - }else if( DatatypesRewriter::isTermDatatype( n ) ){ + }else if( n.getType().isDatatype() ){ Node nc = eqc_cons[n]; if( !nc.isNull() ){ vmap[n] = depth; @@ -1789,7 +1791,7 @@ void TheoryDatatypes::checkCycles() { while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); TypeNode tn = eqc.getType(); - if( DatatypesRewriter::isTypeDatatype( tn ) ) { + if( tn.isDatatype() ) { if( !tn.isCodatatype() ){ if( options::dtCyclic() ){ //do cycle checks @@ -1895,7 +1897,7 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector< if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is looping at index " << it_rec->second << std::endl; } new_part_rec[ it_rec->second ].push_back( part[j] ); }else{ - if( DatatypesRewriter::isTermDatatype( c ) ){ + if( c.getType().isDatatype() ){ Node ncons = getEqcConstructor( c ); if( ncons.getKind()==APPLY_CONSTRUCTOR ) { Node cc = ncons.getOperator(); @@ -2021,7 +2023,7 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, return Node::null(); }else{ TypeNode tn = nn.getType(); - if( DatatypesRewriter::isTypeDatatype( tn ) ) { + if( tn.isDatatype() ) { if( !tn.isCodatatype() ){ return nn; } @@ -2045,7 +2047,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ addLemma = true; }else if( n.getKind()==EQUAL ){ TypeNode tn = n[0].getType(); - if( !DatatypesRewriter::isTypeDatatype( tn ) ){ + if( !tn.isDatatype() ){ addLemma = true; }else{ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); @@ -2109,7 +2111,7 @@ void TheoryDatatypes::printModelDebug( const char* c ){ while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); if( !eqc.getType().isBoolean() ){ - if( DatatypesRewriter::isTermDatatype( eqc ) ){ + if( eqc.getType().isDatatype() ){ Trace( c ) << "DATATYPE : "; } Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl; @@ -2123,7 +2125,7 @@ void TheoryDatatypes::printModelDebug( const char* c ){ ++eqc_i; } Trace( c ) << "}" << std::endl; - if( DatatypesRewriter::isTermDatatype( eqc ) ){ + if( eqc.getType().isDatatype() ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); if( ei ){ Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl; diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index c0539743f..60d319da3 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -170,9 +170,9 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl; Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl; Debug("dt-enum") << "datatype is " << d_type << std::endl; - Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton(); - Debug("dt-enum") << " " << d_datatype.isFinite() << std::endl; - Debug("dt-enum") << " " << d_datatype.isInterpretedFinite() << std::endl; + Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton( d_type.toType() ); + Debug("dt-enum") << " " << d_datatype.isFinite( d_type.toType() ) << std::endl; + Debug("dt-enum") << " " << d_datatype.isInterpretedFinite( d_type.toType() ) << std::endl; if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){ //start with uninterpreted constant diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 8473b5d69..83c938299 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -61,7 +61,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> { bool d_child_enum; bool hasCyclesDt( const Datatype& dt ) { - return dt.isRecursiveSingleton() || !dt.isFinite(); + return dt.isRecursiveSingleton( d_type.toType() ) || !dt.isFinite( d_type.toType() ); } bool hasCycles( TypeNode tn ){ if( tn.isDatatype() ){ @@ -159,7 +159,7 @@ public: } if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){ //try next size limit as long as new terms were generated at last size, or other cases - if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite() ){ + if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite( d_type.toType() ) ){ d_size_limit++; d_ctor = d_zeroCtor; for( unsigned i=0; i<d_sel_sum.size(); i++ ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index ecf4bb74d..f4b63f929 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -17,7 +17,6 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" @@ -277,7 +276,7 @@ void CegInstantiation::preRegisterQuantifier( Node q ) { Node pat = q[2][0][0]; if( pat.getKind()==APPLY_UF ){ TypeNode tn = pat[0].getType(); - if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + if( tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); if( dt.isSygus() ){ //do unfolding if it induces Boolean structure, @@ -696,7 +695,7 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) if( n.getKind()==APPLY_UF ){ TypeNode tn = n[0].getType(); Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl; - if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + if( tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); if( dt.isSygus() ){ Trace("cegqi-eager") << "Unfold eager : " << n << std::endl; @@ -769,7 +768,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { std::string f(ss.str()); f.erase(f.begin()); TypeNode tn = prog.getType(); - Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ); + Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Assert( dt.isSygus() ); //get the solution diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index e0bbbf8ac..44ac135a7 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -16,7 +16,6 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/ce_guided_single_inv_ei.h" #include "theory/quantifiers/first_order_model.h" @@ -147,7 +146,7 @@ void CegConjectureSingleInv::initialize( Node q ) { d_has_ites = false; } } - Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Assert( dt.isSygus() ); if( !dt.getSygusAllowAll() ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 240c2ed12..5cc46d163 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -16,7 +16,6 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/ce_guided_single_inv.h" #include "theory/quantifiers/first_order_model.h" @@ -655,7 +654,7 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int if( Trace.isOn("csi-rcons") ){ for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){ TypeNode tn = it->first; - Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName() << " : " << std::endl; for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ @@ -732,7 +731,7 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in int id = allocate( t, stn ); d_rcons_to_status[stn][t] = -1; TypeNode tn = t.getType(); - Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) ); + Assert( stn.isDatatype() ); const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); Assert( dt.isSygus() ); Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 5f73fe6d0..c88430dbf 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -43,16 +43,16 @@ void QuantDSplit::preRegisterQuantifier( Node q ) { TypeNode tn = q[0][i].getType(); if( tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isRecursiveSingleton() ){ + if( dt.isRecursiveSingleton( tn.toType() ) ){ Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl; }else{ int score = -1; if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ - score = dt.isInterpretedFinite() ? 1 : 0; + score = dt.isInterpretedFinite( tn.toType() ) ? 1 : 0; }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ - score = dt.isInterpretedFinite() ? 1 : -1; + score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1; } - Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite() << " " << dt.isFinite() << ")" << std::endl; + Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl; if( score>max_score ){ max_index = i; max_score = score; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index de8875ae3..fcd8d1829 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2c6bfb7d3..0bdfa2d24 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -17,7 +17,6 @@ #include "expr/datatype.h" #include "options/base_options.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fun_def_engine.h" @@ -1088,7 +1087,7 @@ void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, Type } } /* TODO: more than weak structural induction - else if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) && std::find( visited.begin(), visited.end(), tn )==visited.end() ){ + else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn )==visited.end() ){ visited.push_back( tn ); const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype(); std::vector< Node > disj; @@ -1160,7 +1159,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes Node nret = ret.substitute( ind_vars[0], k ); //note : everything is under a negation //the following constructs ~( R( x, k ) => ~P( x ) ) - if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + if( options::dtStcInduction() && tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); std::vector< Node > disj; for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ @@ -1273,7 +1272,7 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) { ret = false; }else if( tn.isSet() ){ ret = isClosedEnumerableType( tn.getSetElementType() ); - }else if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + }else if( tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ @@ -1978,8 +1977,9 @@ void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ } bool TermDb::isInductionTerm( Node n ) { - if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTermDatatype( n ) ){ - const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); + TypeNode tn = n.getType(); + if( options::dtStcInduction() && tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); return !dt.isCodatatype(); } if( options::intWfInduction() && n.getType().isInteger() ){ @@ -2295,7 +2295,7 @@ TNode TermDbSygus::getVar( TypeNode tn, int i ) { while( i>=(int)d_fv[tn].size() ){ std::stringstream ss; TypeNode vtn = tn; - if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ){ + if( tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); ss << "fv_" << dt.getName() << "_" << i; if( !dt.getSygusType().isNull() ){ @@ -2373,7 +2373,7 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect } bool TermDbSygus::getMatch( Node t, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc, int index_start ) { - Assert( datatypes::DatatypesRewriter::isTypeDatatype( st ) ); + Assert( st.isDatatype() ); const Datatype& dt = ((DatatypeType)(st).toType()).getDatatype(); Assert( dt.isSygus() ); std::map< Kind, std::vector< Node > > kgens; @@ -2530,7 +2530,7 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) { Node sc; d_builtin_const_to_sygus[tn][c] = sc; Assert( c.isConst() ); - Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ); + Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in " << dt.getName() << std::endl; Assert( dt.isSygus() ); @@ -2839,7 +2839,7 @@ struct sortConstants { void TermDbSygus::registerSygusType( TypeNode tn ){ if( d_register.find( tn )==d_register.end() ){ - if( !datatypes::DatatypesRewriter::isTypeDatatype( tn ) ){ + if( !tn.isDatatype() ){ d_register[tn] = TypeNode::null(); }else{ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); @@ -3234,7 +3234,7 @@ void TermDbSygus::registerEvalTerm( Node n ) { if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){ Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl; TypeNode tn = n[0].getType(); - if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + if( tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); if( dt.isSygus() ){ Node f = n.getOperator(); @@ -3242,7 +3242,7 @@ void TermDbSygus::registerEvalTerm( Node n ) { if( n[0].getKind()!=APPLY_CONSTRUCTOR ){ d_evals[n[0]].push_back( n ); TypeNode tn = n[0].getType(); - Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Node var_list = Node::fromExpr( dt.getSygusVarList() ); Assert( dt.isSygus() ); @@ -3281,7 +3281,7 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems unsigned start = d_node_mv_args_proc[n][vn]; Node antec = n.eqNode( vn ).negate(); TypeNode tn = n.getType(); - Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Assert( dt.isSygus() ); Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 71d82d5e4..8579ad55f 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -819,7 +819,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) bool isCorecursive = false; if( t.isDatatype() ){ const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype(); - isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() ); + isCorecursive = dt.isCodatatype() && ( !dt.isFinite( t.toType() ) || dt.isRecursiveSingleton( t.toType() ) ); } #ifdef CVC4_ASSERTIONS bool isUSortFiniteRestricted = false; diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index d13cc1f03..8284f6ff4 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -202,7 +202,7 @@ void UnconstrainedSimplifier::processUnconstrained() if( parent[0].getType().isDatatype() ){ TypeNode tn = parent[0].getType(); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isRecursiveSingleton() ){ + if( dt.isRecursiveSingleton( tn.toType() ) ){ //domain size may be 1 break; } |