diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-01 12:25:11 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-01 12:25:11 +0200 |
commit | 8f4e966ae0c0f42e595e1c603cb7c3f779b713ef (patch) | |
tree | f3a46b20e752a2fb34e310ca477d4fb90bd7138e /src/theory/quantifiers | |
parent | 91f40dee752910fca5d749656c0b6ee1bc1281aa (diff) |
Support for default grammar for datatypes in sygus. Support vts for infinity.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 94 |
1 files changed, 58 insertions, 36 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 132c55cd9..380ee19fd 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1338,51 +1338,73 @@ Node TermDb::getVtsInfinity( bool isFree, bool create ) { } Node TermDb::rewriteVtsSymbols( Node n ) { - Assert( !d_vts_delta_free.isNull() ); - Assert( !d_vts_delta.isNull() ); - if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) && containsTerm( n, d_vts_delta ) ){ + if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){ Trace("quant-vts-debug") << "VTS : process " << n << std::endl; - if( n.getKind()==EQUAL ){ - return d_false; - }else{ - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( n, msum ) ){ - if( Trace.isOn("quant-vts-debug") ){ - Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" ); - } - Node iso_n; - int res = QuantArith::isolate( d_vts_delta, msum, iso_n, n.getKind(), true ); - if( res!=0 ){ - Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; - int index = res==1 ? 0 : 1; - Node slv = iso_n[res==1 ? 1 : 0]; - if( iso_n[index]!=d_vts_delta ){ - if( iso_n[index].getKind()==MULT && iso_n[index].getNumChildren()==2 && iso_n[index][0].isConst() && iso_n[index][1]==d_vts_delta ){ - slv = NodeManager::currentNM()->mkNode( MULT, slv, NodeManager::currentNM()->mkConst( Rational(1)/iso_n[index][0].getConst<Rational>() ) ); + bool rew_inf = false; + bool rew_delta = false; + if( !d_vts_inf.isNull() && containsTerm( n, d_vts_inf ) ){ + rew_inf = true; + }else if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){ + rew_delta = true; + } + if( rew_inf || rew_delta ){ + if( n.getKind()==EQUAL ){ + return d_false; + }else{ + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( n, msum ) ){ + if( Trace.isOn("quant-vts-debug") ){ + Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" ); + } + Node vts_sym = rew_inf ? d_vts_inf : d_vts_delta; + Node iso_n; + int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true ); + if( res!=0 ){ + Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; + int index = res==1 ? 0 : 1; + Node slv = iso_n[res==1 ? 1 : 0]; + if( iso_n[index]!=vts_sym ){ + if( iso_n[index].getKind()==MULT && iso_n[index].getNumChildren()==2 && iso_n[index][0].isConst() && iso_n[index][1]==d_vts_delta ){ + slv = NodeManager::currentNM()->mkNode( MULT, slv, NodeManager::currentNM()->mkConst( Rational(1)/iso_n[index][0].getConst<Rational>() ) ); + }else{ + return n; + } + } + Node nlit; + if( res==1 ){ + if( rew_inf ){ + nlit = d_true; + }else{ + nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv ); + } }else{ - return n; + if( rew_inf ){ + nlit = d_false; + }else{ + nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero ); + } } + Trace("quant-vts-debug") << "Return " << nlit << std::endl; + return nlit; } - Node nlit; - 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; } } - return n; } + return n; }else if( n.getKind()==FORALL ){ //cannot traverse beneath quantifiers - std::vector< Node > delta; - delta.push_back( d_vts_delta ); - std::vector< Node > delta_free; - delta_free.push_back( d_vts_delta_free ); - n = n.substitute( delta.begin(), delta.end(), delta_free.begin(), delta_free.end() ); + std::vector< Node > vars; + std::vector< Node > vars_free; + if( !d_vts_inf.isNull() ){ + vars.push_back( d_vts_inf ); + vars_free.push_back( d_vts_inf_free ); + } + if( !d_vts_delta.isNull() ){ + vars.push_back( d_vts_delta ); + vars_free.push_back( d_vts_delta_free ); + } + n = n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() ); return n; }else{ bool childChanged = false; |