diff options
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
-rw-r--r-- | src/theory/quantifiers/term_util.cpp | 209 |
1 files changed, 0 insertions, 209 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 6ffc50c97..c9c738eb3 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -304,215 +304,6 @@ void TermUtil::computeInstConstContainsForQuant(Node q, } } -void TermUtil::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) { - if( inc_delta ){ - Node delta = getVtsDelta( isFree, create ); - if( !delta.isNull() ){ - t.push_back( delta ); - } - } - for( unsigned r=0; r<2; r++ ){ - Node inf = getVtsInfinityIndex( r, isFree, create ); - if( !inf.isNull() ){ - t.push_back( inf ); - } - } -} - -Node TermUtil::getVtsDelta( bool isFree, bool create ) { - if( create ){ - if( d_vts_delta_free.isNull() ){ - d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" ); - Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, d_zero ); - d_quantEngine->getOutputChannel().lemma( delta_lem ); - } - if( d_vts_delta.isNull() ){ - d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" ); - //mark as a virtual term - VirtualTermSkolemAttribute vtsa; - d_vts_delta.setAttribute(vtsa,true); - } - } - return isFree ? d_vts_delta_free : d_vts_delta; -} - -Node TermUtil::getVtsInfinity( TypeNode tn, bool isFree, bool create ) { - if( create ){ - if( d_vts_inf_free[tn].isNull() ){ - d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf_free", tn, "free infinity for virtual term substitution" ); - } - if( d_vts_inf[tn].isNull() ){ - d_vts_inf[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "infinity for virtual term substitution" ); - //mark as a virtual term - VirtualTermSkolemAttribute vtsa; - d_vts_inf[tn].setAttribute(vtsa,true); - } - } - return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn]; -} - -Node TermUtil::getVtsInfinityIndex( int i, bool isFree, bool create ) { - if( i==0 ){ - return getVtsInfinity( NodeManager::currentNM()->realType(), isFree, create ); - }else if( i==1 ){ - return getVtsInfinity( NodeManager::currentNM()->integerType(), isFree, create ); - }else{ - Assert( false ); - return Node::null(); - } -} - -Node TermUtil::substituteVtsFreeTerms( Node n ) { - std::vector< Node > vars; - getVtsTerms( vars, false, false ); - std::vector< Node > vars_free; - getVtsTerms( vars_free, true, false ); - Assert( vars.size()==vars_free.size() ); - if( !vars.empty() ){ - return n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() ); - }else{ - return n; - } -} - -Node TermUtil::rewriteVtsSymbols( Node n ) { - if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){ - Trace("quant-vts-debug") << "VTS : process " << n << std::endl; - Node rew_vts_inf; - bool rew_delta = false; - //rewriting infinity always takes precedence over rewriting delta - for( unsigned r=0; r<2; r++ ){ - Node inf = getVtsInfinityIndex( r, false, false ); - if (!inf.isNull() && expr::hasSubterm(n, inf)) - { - if( rew_vts_inf.isNull() ){ - rew_vts_inf = inf; - }else{ - //for mixed int/real with multiple infinities - Trace("quant-vts-debug") << "Multiple infinities...equate " << inf << " = " << rew_vts_inf << std::endl; - std::vector< Node > subs_lhs; - subs_lhs.push_back( inf ); - std::vector< Node > subs_rhs; - subs_lhs.push_back( rew_vts_inf ); - n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - n = Rewriter::rewrite( n ); - // may have cancelled - if (!expr::hasSubterm(n, rew_vts_inf)) - { - rew_vts_inf = Node::null(); - } - } - } - } - if (rew_vts_inf.isNull()) - { - if (!d_vts_delta.isNull() && expr::hasSubterm(n, d_vts_delta)) - { - rew_delta = true; - } - } - if( !rew_vts_inf.isNull() || rew_delta ){ - std::map< Node, Node > msum; - if (ArithMSum::getMonomialSumLit(n, msum)) - { - if( Trace.isOn("quant-vts-debug") ){ - Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; - ArithMSum::debugPrintMonomialSum(msum, "quant-vts-debug"); - } - Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta; - Assert( !vts_sym.isNull() ); - Node iso_n; - Node nlit; - int res = ArithMSum::isolate(vts_sym, msum, iso_n, n.getKind(), true); - if( res!=0 ){ - Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; - Node slv = iso_n[res==1 ? 1 : 0]; - //ensure the vts terms have been eliminated - if( containsVtsTerm( slv ) ){ - Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but bad solved form " << slv << "." << std::endl; - nlit = substituteVtsFreeTerms( n ); - Trace("quant-vts-debug") << "...return " << nlit << std::endl; - //Assert( false ); - //safe case: just convert to free symbols - return nlit; - }else{ - if( !rew_vts_inf.isNull() ){ - nlit = ( n.getKind()==GEQ && res==1 ) ? d_true : d_false; - }else{ - Assert( iso_n[res==1 ? 0 : 1]==d_vts_delta ); - if( n.getKind()==EQUAL ){ - nlit = d_false; - }else if( res==1 ){ - nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv ); - }else{ - nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero ); - } - } - } - Trace("quant-vts-debug") << "Return " << nlit << std::endl; - return nlit; - }else{ - Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but could not isolate." << std::endl; - //safe case: just convert to free symbols - nlit = substituteVtsFreeTerms( n ); - Trace("quant-vts-debug") << "...return " << nlit << std::endl; - //Assert( false ); - return nlit; - } - } - } - return n; - }else if( n.getKind()==FORALL ){ - //cannot traverse beneath quantifiers - return substituteVtsFreeTerms( n ); - }else{ - bool childChanged = false; - std::vector< Node > children; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node nn = rewriteVtsSymbols( n[i] ); - children.push_back( nn ); - childChanged = childChanged || nn!=n[i]; - } - if( childChanged ){ - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.insert( children.begin(), n.getOperator() ); - } - Node ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); - Trace("quant-vts-debug") << "...make node " << ret << std::endl; - return ret; - }else{ - return n; - } - } -} - -bool TermUtil::containsVtsTerm( Node n, bool isFree ) { - std::vector< Node > t; - getVtsTerms( t, isFree, false ); - return expr::hasSubterm(n, t); -} - -bool TermUtil::containsVtsTerm( std::vector< Node >& n, bool isFree ) { - std::vector< Node > t; - getVtsTerms( t, isFree, false ); - if( !t.empty() ){ - for (const Node& nc : n) - { - if (expr::hasSubterm(nc, t)) - { - return true; - } - } - } - return false; -} - -bool TermUtil::containsVtsInfinity( Node n, bool isFree ) { - std::vector< Node > t; - getVtsTerms( t, isFree, false, false ); - return expr::hasSubterm(n, t); -} - Node TermUtil::ensureType( Node n, TypeNode tn ) { TypeNode ntn = n.getType(); Assert( ntn.isComparableTo( tn ) ); |