Minor improvement to sygus sol reconstruction.

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