diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-15 10:31:58 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-15 10:31:58 -0500 |
commit | 3344979103bcec622276fca7c2a21cc0945f6c56 (patch) | |
tree | 8cdcd2cec0db34d70a2bbdb0443bbe3d250995cf /src/theory | |
parent | 8bb55a22b7c0f20305274f8609b9e8404e4bb41c (diff) |
Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cbqi for datatypes with uninterpreted sort subfields. Simplify fmc model construction.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 61 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 44 | ||||
-rw-r--r-- | 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; 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; @@ -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<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 ){ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 2cd5f6e1c..6c2dc9275 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -58,6 +58,7 @@ protected: /** 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 */ |