From 3344979103bcec622276fca7c2a21cc0945f6c56 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 15 Jun 2017 10:31:58 -0500 Subject: [PATCH] Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cbqi for datatypes with uninterpreted sort subfields. Simplify fmc model construction. --- src/theory/datatypes/theory_datatypes.cpp | 61 ++++++++++++++----- src/theory/datatypes/theory_datatypes.h | 7 ++- src/theory/quantifiers/first_order_model.cpp | 3 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 44 ++++++++++--- src/theory/quantifiers/inst_strategy_cbqi.h | 1 + 5 files changed, 88 insertions(+), 28 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 4ca631184..1a466ff8a 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1222,6 +1222,42 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ 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; imkNode( 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; @@ -1268,8 +1304,16 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { } 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; @@ -1654,19 +1698,6 @@ void TheoryDatatypes::collectTerms( Node n ) { } } -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() ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 6a26352ad..98d8d53b1 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -192,7 +192,8 @@ private: /** 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]; @@ -284,6 +285,8 @@ private: 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, @@ -302,8 +305,6 @@ private: 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 */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 084912f5a..612646b42 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -734,8 +734,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { 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 ) ); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 88f8e2484..58bebef35 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -496,21 +496,49 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit } return false; } -int InstStrategyCbqi::hasNonCbqiVariable( Node q ){ - int hmin = 1; - for( unsigned i=0; i& 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; igetQuantEPR(); 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 visited; + int handled = isCbqiSort( tn, visited ); if( handled==-1 ){ return -1; }else if( handled& 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 */ -- 2.30.2