eqc->d_constructor.set( c );
}
+Node TheoryDatatypes::removeUninterpretedConstants( Node n, std::map< Node, Node >& visited ){
+ std::map< Node, Node >::iterator it = visited.find( n );
+ if( it==visited.end() ){
+ Node ret = n;
+ if( n.getKind()==UNINTERPRETED_CONSTANT ){
+ std::map< Node, Node >::iterator itu = d_uc_to_fresh_var.find( n );
+ if( itu==d_uc_to_fresh_var.end() ){
+ Node k = NodeManager::currentNM()->mkSkolem( "w", n.getType(), "Skolem for wrongly applied selector." );
+ d_uc_to_fresh_var[n] = k;
+ ret = k;
+ }else{
+ ret = itu->second;
+ }
+ }else if( n.getNumChildren()>0 ){
+ std::vector< Node > children;
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ bool childChanged = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nc = removeUninterpretedConstants( n[i], visited );
+ childChanged = childChanged || nc!=n[i];
+ children.push_back( nc );
+ }
+ if( childChanged ){
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ }
+ visited[n] = ret;
+ return ret;
+ }else{
+ return it->second;
+ }
+}
+
+
void TheoryDatatypes::collapseSelector( Node s, Node c ) {
Assert( c.getKind()==APPLY_CONSTRUCTOR );
Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
}
if( !r.isNull() ){
Node rr = Rewriter::rewrite( r );
- if( use_s!=rr ){
- Node eq = use_s.eqNode( rr );
+ Node rrs = rr;
+ if( wrong ){
+ // we have inference S_i( C_j( t ) ) = t' for i != j, where t' is result of mkGroundTerm.
+ // we must eliminate uninterpreted constants for datatypes that have uninterpreted sort subfields,
+ // since uninterpreted constants should not appear in lemmas
+ std::map< Node, Node > visited;
+ rrs = removeUninterpretedConstants( rr, visited );
+ }
+ if( use_s!=rrs ){
+ Node eq = use_s.eqNode( rrs );
Node eq_exp;
if( options::dtRefIntro() ){
eq_exp = d_true;
}
}
-void TheoryDatatypes::processNewTerm( Node n ){
- Trace("dt-terms") << "Created term : " << n << std::endl;
- //see if it is rewritten to be something different
- Node rn = Rewriter::rewrite( n );
- if( rn!=n && !areEqual( rn, n ) ){
- Node eq = rn.eqNode( n );
- d_pending.push_back( eq );
- d_pending_exp[ eq ] = d_true;
- Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl;
- d_infer.push_back( eq );
- }
-}
-
Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index ){
std::map< int, Node >::iterator it = d_inst_map[n].find( index );
if( it!=d_inst_map[n].end() ){
/** sygus utilities */
SygusSplit * d_sygus_split;
SygusSymBreak * d_sygus_sym_break;
-
+ /** uninterpreted constant to variable map */
+ std::map< Node, Node > d_uc_to_fresh_var;
private:
/** singleton lemmas (for degenerate co-datatype case) */
std::map< TypeNode, Node > d_singleton_lemma[2];
void merge( Node t1, Node t2 );
/** collapse selector, s is of the form sel( n ) where n = c */
void collapseSelector( Node s, Node c );
+ /** remove uninterpreted constants */
+ Node removeUninterpretedConstants( Node n, std::map< Node, Node >& visited );
/** for checking if cycles exist */
void checkCycles();
Node searchForCycle( TNode n, TNode on,
void collectTerms( Node n );
/** get instantiate cons */
Node getInstantiateCons( Node n, const Datatype& dt, int index );
- /** process new term that was created internally */
- void processNewTerm( Node n );
/** check instantiate */
void instantiate( EqcInfo* eqc, Node n );
/** must communicate fact */
if( !isStar(cond[j][1]) ){
children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) );
}
- }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground eqc of this type
- d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){
+ }else if( !isStar(cond[j]) ){
Node c = getRepresentative( cond[j] );
c = getRepresentative( c );
children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
}
return false;
}
-int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
- int hmin = 1;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- TypeNode tn = q[0][i].getType();
- int handled = -1;
+
+// -1 : not cbqi sort, 0 : cbqi sort, 1 : cbqi sort regardless of quantifier body
+int InstStrategyCbqi::isCbqiSort( TypeNode tn, std::map< TypeNode, int >& visited ) {
+ std::map< TypeNode, int >::iterator itv = visited.find( tn );
+ if( itv==visited.end() ){
+ visited[tn] = 0;
+ int ret = -1;
if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){
- handled = 0;
+ ret = 0;
}else if( tn.isDatatype() ){
- handled = 0;
+ ret = 1;
+ const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+ TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() );
+ int cret = isCbqiSort( crange, visited );
+ if( cret==-1 ){
+ visited[tn] = -1;
+ return -1;
+ }else if( cret<ret ){
+ ret = cret;
+ }
+ }
+ }
}else if( tn.isSort() ){
QuantEPR * qepr = d_quantEngine->getQuantEPR();
if( qepr!=NULL ){
- handled = qepr->isEPR( tn ) ? 1 : -1;
+ ret = qepr->isEPR( tn ) ? 1 : -1;
}
}
+ visited[tn] = ret;
+ return ret;
+ }else{
+ return itv->second;
+ }
+}
+
+int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
+ int hmin = 1;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ TypeNode tn = q[0][i].getType();
+ std::map< TypeNode, int > visited;
+ int handled = isCbqiSort( tn, visited );
if( handled==-1 ){
return -1;
}else if( handled<hmin ){
/** helper functions */
int hasNonCbqiVariable( Node q );
bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
+ int isCbqiSort( TypeNode tn, std::map< TypeNode, int >& visited );
/** get next decision request with dependency checking */
Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc );
/** process functions */
projects / cvc5.git / commitdiff