diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-30 09:49:48 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-30 09:49:48 +0200 |
commit | 4d61b02bd1ab2a2474c896b84cab603713035111 (patch) | |
tree | ecd63750762fcff91baf8985bfb108b1ebd3f1ab /src | |
parent | 6842b50e9e59c89efc21b83faa541df069b5c333 (diff) |
Minor improvement to sygus sol reconstruction.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv_sol.cpp | 35 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 2 |
2 files changed, 34 insertions, 3 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index bac39f22c..8fd935368 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -1072,6 +1072,7 @@ void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) { } void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ) { + Assert( n.getKind()!=k ); //? if( k==AND || k==OR ){ equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) ); equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) ); @@ -1127,13 +1128,43 @@ void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) ); } } - + //inequalities + if( k==GEQ || k==LEQ || k==LT || k==GT || k==NOT ){ + Node atom = n.getKind()==NOT ? n[0] : n; + bool pol = n.getKind()!=NOT; + Kind ak = atom.getKind(); + if( ( ak==GEQ || ak==LEQ || ak==LT || ak==GT ) && ( pol || k!=NOT ) ){ + Node t1 = atom[0]; + Node t2 = atom[1]; + if( !pol ){ + ak = ak==GEQ ? LT : ( ak==LEQ ? GT : ( ak==LT ? GEQ : LEQ ) ); + } + if( k==NOT ){ + equiv.push_back( NodeManager::currentNM()->mkNode( ak==GEQ ? LT : ( ak==LEQ ? GT : ( ak==LT ? GEQ : LEQ ) ), t1, t2 ).negate() ); + }else if( k==ak ){ + equiv.push_back( NodeManager::currentNM()->mkNode( k, t1, t2 ) ); + }else if( (k==GEQ || k==LEQ)==(ak==GEQ || ak==LEQ) ){ + equiv.push_back( NodeManager::currentNM()->mkNode( k, t2, t1 ) ); + }else if( t1.getType().isInteger() && t2.getType().isInteger() ){ + if( (k==GEQ || k==GT)!=(ak==GEQ || ak==GT) ){ + Node ts = t1; + t1 = t2; + t2 = ts; + ak = ak==GEQ ? LEQ : ( ak==LEQ ? GEQ : ( ak==LT ? GT : LT ) ); + } + t2 = NodeManager::currentNM()->mkNode( PLUS, t2, NodeManager::currentNM()->mkConst( Rational( (ak==GT || ak==LEQ) ? 1 : -1 ) ) ); + t2 = Rewriter::rewrite( t2 ); + equiv.push_back( NodeManager::currentNM()->mkNode( k, t1, t2 ) ); + } + } + } + //based on eqt cache std::map< Node, Node >::iterator itet = d_eqt_rep.find( n ); if( itet!=d_eqt_rep.end() ){ Node rn = itet->second; for( unsigned i=0; i<d_eqt_eqc[rn].size(); i++ ){ - if( d_eqt_eqc[rn][i]!=n ){ + if( d_eqt_eqc[rn][i]!=n && d_eqt_eqc[rn][i].getKind()==k ){ if( std::find( equiv.begin(), equiv.end(), d_eqt_eqc[rn][i] )==equiv.end() ){ equiv.push_back( d_eqt_eqc[rn][i] ); } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 753f3f170..ec71e5348 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -226,7 +226,7 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true generalize based on content in global search space narrowing -option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h" +option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h" template mode for sygus invariant synthesis # approach applied to general quantified formulas |