summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_util.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
-rw-r--r--src/theory/quantifiers/term_util.cpp209
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 ) );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback