Bug fix fairness for commutative operators in sygus. Minor.

3 files changed, 15 insertions, 11 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 353bd1392..e186c94d1 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -293,7 +293,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
                   if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] ){
                     Trace("sygus-split-debug") << "Check redundancy of " << dt[j].getSygusOp() << " and " << dto[i].getSygusOp() << " under " << parentKind << std::endl;
                     bool rem = false;
-                    if( isPComm && j>i && tnn==tnno ){
+                    if( isPComm && j>i && tnn==tnno && d_sygus_pc_nred[tnno][csIndex][osIndex][j] ){
                       //based on commutativity
                       // use term ordering : constructor index of first argument is not greater than constructor index of second argument
                       rem = true;
@@ -500,9 +500,10 @@ bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pd
         Trace("sygus-split-debug") << "...at argument " << ok_arg << std::endl;
         //other operator be the same type
         if( isTypeMatch( pdt[ok_arg], pdt[arg] ) ){
-          Node co = d_util->getTypeValueOffset( c.getType(), c, offset );
-          Trace("sygus-split-debug") << c << " with offset " << offset << " is " << co << std::endl;
-          if( !co.isNull() ){
+          int status;
+          Node co = d_util->getTypeValueOffset( c.getType(), c, offset, status );
+          Trace("sygus-split-debug") << c << " with offset " << offset << " is " << co << ", status=" << status << std::endl;
+          if( status==0 && !co.isNull() ){
             if( d_util->hasConst( tn, co ) ){
               Trace("sygus-split-debug") << "arg " << arg << " " << c << " in " << parent << " can be treated as " << co << " in " << ok << "..." << std::endl;
               return false;
@@ -1191,21 +1192,25 @@ Node SygusUtil::getTypeMaxValue( TypeNode tn ) {
   }
 }
 
-Node SygusUtil::getTypeValueOffset( TypeNode tn, Node val, int offset ) {
+Node SygusUtil::getTypeValueOffset( TypeNode tn, Node val, int offset, int& status ) {
   std::map< int, Node >::iterator it = d_type_value_offset[tn][val].find( offset );
   if( it==d_type_value_offset[tn][val].end() ){
     Node val_o;
     Node offset_val = getTypeValue( tn, offset );
+    status = -1;
     if( !offset_val.isNull() ){
       if( tn.isInteger() || tn.isReal() ){
         val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, val, offset_val ) );
+        status = 0;
       }else if( tn.isBitVector() ){
         val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( BITVECTOR_PLUS, val, offset_val ) );
       }
     }
     d_type_value_offset[tn][val][offset] = val_o;
+    d_type_value_offset_status[tn][val][offset] = status;
     return val_o;
   }else{
+    status = d_type_value_offset_status[tn][val][offset];
     return it->second;
   }
 }
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 33e9fc54a..db44eaa55 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -154,6 +154,7 @@ private:
   std::map< TypeNode, std::map< int, Node > > d_type_value;
   std::map< TypeNode, Node > d_type_max_value;
   std::map< TypeNode, std::map< Node, std::map< int, Node > > > d_type_value_offset;
+  std::map< TypeNode, std::map< Node, std::map< int, int > > > d_type_value_offset_status;
   /** is assoc */
   bool isAssoc( Kind k );
   /** is comm */
@@ -169,7 +170,7 @@ private:
   /** get value */
   Node getTypeValue( TypeNode tn, int val );
   /** get value */
-  Node getTypeValueOffset( TypeNode tn, Node val, int offset );
+  Node getTypeValueOffset( TypeNode tn, Node val, int offset, int& status );
   /** get value */
   Node getTypeMaxValue( TypeNode tn );
 private:
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 6d604a345..a64362c14 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -67,8 +67,10 @@ void CegInstantiation::CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
         }
       }
     }
-    analyzeSygusConjecture();
     d_syntax_guided = true;
+    if( options::sygusSingleInv() ){
+      analyzeSygusConjecture();
+    }
   }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){
     d_syntax_guided = false;
   }else{
@@ -263,7 +265,6 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() {
 }
 
 bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) {
-  Trace("ajr-temp") << "Process single inv lit " << lit << " " << pol << std::endl;
   if( lit.getKind()==NOT ){
     return processSingleInvLiteral( lit[0], !pol, case_vals );
   }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){
@@ -276,7 +277,6 @@ bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool po
   }else if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
     if( pol ){
       for( unsigned r=0; r<2; r++ ){
-        Trace("ajr-temp") << "Check literal " << lit[r] << " at " << r << std::endl;
         std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[r] );
         if( it!=d_single_inv_map_to_prog.end() ){
           if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){
@@ -379,13 +379,11 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
       Node inst = d_single_inv[1].substitute( vars.begin(), vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
       Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), inst.negate() );
       Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl;
-      /*  inactive for now (until figure out how to use it)
       qe->getOutputChannel().lemma( lem );
       if( Trace.isOn("cegqi-debug") ){
         lem = Rewriter::rewrite( lem );
         Trace("cegqi-debug") << "...rewritten : " << lem << std::endl;
       }
-      */
     }
   }
 }