diff options
author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-05-30 15:48:53 +0200 |
---|---|---|
committer | ajreynol <reynolds@larapc05.epfl.ch> | 2014-05-30 15:48:53 +0200 |
commit | 73f533efbd887bae36a63a21bc531d412866e5a6 (patch) | |
tree | 9dbc23ccf018f47c1fa8e6ba56b3978402c3fc06 | |
parent | d74d59d27b255a6f245da1530a6b75168fade48b (diff) |
Improve --dt-stc-ind for multi-variable datatype properties.
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 59 |
1 files changed, 33 insertions, 26 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 36859ddaa..5636e0c5f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -495,33 +495,40 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes if( !ind_vars.empty() ){ Trace("stc-ind") << "Ind strengthen : (not " << f << ")" << std::endl; Trace("stc-ind") << "Skolemized is : " << ret << std::endl; - for( unsigned v=0; v<ind_vars.size(); v++ ){ - Node k = sk[ind_var_indicies[v]]; - TypeNode tn = k.getType(); - if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ - //can strengthen this, by asserting that subs[0] is the smallest term such that the existential holds. - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - std::vector< Node > disj; - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - std::vector< Node > conj; - conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() ); - std::vector< Node > selfSel; - getSelfSel( dt[i], k, tn, selfSel ); - for( unsigned j=0; j<selfSel.size(); j++ ){ - conj.push_back( ret.substitute( ind_vars[v], selfSel[j] ).negate() ); - } - disj.push_back( conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( OR, conj ) ); - } - Assert( !disj.empty() ); - Node n_str_ind = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( AND, disj ); - Trace("stc-ind") << "Strengthening is : " << n_str_ind << std::endl; - - Node nret = ret.substitute( ind_vars[v], k ); - ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind ); - }else{ - Assert( false ); + Node nret; + Node n_str_ind; + TypeNode tn = ind_vars[0].getType(); + if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + Node k = sk[ind_var_indicies[0]]; + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + std::vector< Node > disj; + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + std::vector< Node > selfSel; + getSelfSel( dt[i], k, tn, selfSel ); + std::vector< Node > conj; + conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() ); + for( unsigned j=0; j<selfSel.size(); j++ ){ + conj.push_back( ret.substitute( ind_vars[0], selfSel[j] ).negate() ); + } + disj.push_back( conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( OR, conj ) ); } - } + Assert( !disj.empty() ); + n_str_ind = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( AND, disj ); + Trace("stc-ind") << "Strengthening is : " << n_str_ind << std::endl; + nret = ret.substitute( ind_vars[0], k ); + }else{ + Trace("stc-ind") << "Unknown induction for term : " << ind_vars[0] << ", type = " << tn << std::endl; + Assert( false ); + } + + std::vector< Node > rem_ind_vars; + rem_ind_vars.insert( rem_ind_vars.end(), ind_vars.begin()+1, ind_vars.end() ); + if( !rem_ind_vars.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, rem_ind_vars ); + nret = NodeManager::currentNM()->mkNode( FORALL, bvl, nret ); + n_str_ind = NodeManager::currentNM()->mkNode( FORALL, bvl, n_str_ind.negate() ).negate(); + } + ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind ); } Trace("quantifiers-sk") << "mkSkolem body for " << f << " returns : " << ret << std::endl; return ret; |