summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/datatypes/datatypes_rewriter.h11
-rw-r--r--src/theory/datatypes/datatypes_sygus.cpp14
-rw-r--r--src/theory/datatypes/kinds4
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp42
-rw-r--r--src/theory/datatypes/type_enumerator.cpp6
-rw-r--r--src/theory/datatypes/type_enumerator.h4
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp7
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.cpp3
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv_sol.cpp5
-rw-r--r--src/theory/quantifiers/quant_split.cpp8
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp1
-rw-r--r--src/theory/quantifiers/term_database.cpp26
-rw-r--r--src/theory/theory_model.cpp2
-rw-r--r--src/theory/unconstrained_simplifier.cpp2
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback