Do not drop patterns during boolean term rewriting. Narrow sygus search space based on commutative operators.

7 files changed, 114 insertions, 76 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 7ab590d89..54a6b5416 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -816,7 +816,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
             }
             Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars);
             Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars);
-            Node quant = nm->mkNode(top.getKind(), boundVarList, body);
+            Node quant;
+            if( top.getNumChildren()==3 ){
+              Node ipl = rewriteBooleanTermsRec(top[2], theory::THEORY_BOOL, quantBoolVars);
+              quant = nm->mkNode(top.getKind(), boundVarList, body, ipl );
+            }else{
+              quant = nm->mkNode(top.getKind(), boundVarList, body);
+            }
             Debug("bt") << "rewrote quantifier to -> " << quant << endl;
             d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant;
             d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff);
@@ -847,16 +853,16 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
                     k != kind::RECORD_SELECT &&
                     k != kind::RECORD_UPDATE &&
                     k != kind::DIVISIBLE &&
-		    // Theory parametric functions go here
-		    k != kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR &&
-		    k != kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT &&
-		    k != kind::FLOATINGPOINT_TO_FP_REAL &&
-		    k != kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR &&
-		    k != kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR &&
-		    k != kind::FLOATINGPOINT_TO_UBV &&
-		    k != kind::FLOATINGPOINT_TO_SBV &&
-		    k != kind::FLOATINGPOINT_TO_REAL
-		    ) {
+        // Theory parametric functions go here
+        k != kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR &&
+        k != kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT &&
+        k != kind::FLOATINGPOINT_TO_FP_REAL &&
+        k != kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR &&
+        k != kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR &&
+        k != kind::FLOATINGPOINT_TO_UBV &&
+        k != kind::FLOATINGPOINT_TO_SBV &&
+        k != kind::FLOATINGPOINT_TO_REAL
+        ) {
             Debug("bt") << "rewriting: " << top.getOperator() << endl;
             result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
             Debug("bt") << "got: " << result.top().getOperator() << endl;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ee09359ad..0e1be30de 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1344,6 +1344,13 @@ void SmtEngine::setDefaults() {
       }
     }
   }
+  
+  //apply counterexample guided instantiation options
+  if( options::ceGuidedInst() ){
+    if( !options::quantConflictFind.wasSetByUser() ){
+      options::quantConflictFind.set( false );
+    }
+  }
 
   //implied options...
   if( options::recurseCbqi() ){
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index cad4aaa48..8192ec067 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -21,6 +21,8 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "util/bitvector.h"
 
+#include "theory/quantifiers/options.h"
+
 using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
@@ -55,10 +57,10 @@ int SygusSplit::getConstArg( TypeNode tn, Node n ){
   return -1;
 }
 
-bool SygusSplit::hasKind( TypeNode tn, Kind k ) { 
+bool SygusSplit::hasKind( TypeNode tn, Kind k ) {
   return getKindArg( tn, k )!=-1;
 }
-bool SygusSplit::hasConst( TypeNode tn, Node n ) { 
+bool SygusSplit::hasConst( TypeNode tn, Node n ) {
   return getConstArg( tn, n )!=-1;
 }
 
@@ -66,7 +68,7 @@ bool SygusSplit::isKindArg( TypeNode tn, int i ) {
   Assert( isRegistered( tn ) );
   std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn );
   if( itt!=d_arg_kind.end() ){
-    return itt->second.find( i )!=itt->second.end(); 
+    return itt->second.find( i )!=itt->second.end();
   }else{
     return false;
   }
@@ -76,79 +78,94 @@ bool SygusSplit::isConstArg( TypeNode tn, int i ) {
   Assert( isRegistered( tn ) );
   std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
   if( itt!=d_arg_const.end() ){
-    return itt->second.find( i )!=itt->second.end(); 
+    return itt->second.find( i )!=itt->second.end();
   }else{
     return false;
   }
 }
 
-void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ) {
+void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas ) {
   Assert( dt.isSygus() );
-  Trace("sygus-split") << "Get sygus splits " << n << std::endl;
-
-  //get the kinds for child datatype
-  TypeNode tnn = n.getType();
-  registerSygusType( tnn, dt );
-
-  //get parent information, if possible
-  int csIndex = -1;
-  int sIndex = -1;
-  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
-    Node op = n.getOperator();
-    Expr selectorExpr = op.toExpr();
-    const Datatype& pdt = Datatype::datatypeOf(selectorExpr);
-    Assert( pdt.isSygus() );
-    csIndex = Datatype::cindexOf(selectorExpr);
-    sIndex = Datatype::indexOf(selectorExpr);
-    TypeNode tnnp = n[0].getType();
-    //register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt
-    registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex );
-    
-    
-    //relationships between arguments
-    /*
-    if( isKindArg( tnnp, csIndex ) ){
-      Kind parentKind = d_arg_kind[tnnp][csIndex];
-      if( isComm( parentKind ) ){
-        //if commutative, normalize based on term ordering (the constructor index of left arg must be less than or equal to the right arg)
-        Trace("sygus-split-debug") << "Commutative operator : " << parentKind << std::endl;
-        if( pdt[csIndex].getNumArgs()==2 ){
-          TypeNode tn1 = TypeNode::fromType( ((SelectorType)pdt[csIndex][0].getType()).getRangeType() );
-          TypeNode tn2 = TypeNode::fromType( ((SelectorType)pdt[csIndex][1].getType()).getRangeType() );
-          if( tn1==tn2 ){
-            if( sIndex==1 ){
+  if( d_splits.find( n )==d_splits.end() ){
+    Trace("sygus-split") << "Get sygus splits " << n << std::endl;
+    //get the kinds for child datatype
+    TypeNode tnn = n.getType();
+    registerSygusType( tnn, dt );
+
+    //get parent information, if possible
+    int csIndex = -1;
+    int sIndex = -1;
+    Node onComm;
+    if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+      Node op = n.getOperator();
+      Expr selectorExpr = op.toExpr();
+      const Datatype& pdt = Datatype::datatypeOf(selectorExpr);
+      Assert( pdt.isSygus() );
+      csIndex = Datatype::cindexOf(selectorExpr);
+      sIndex = Datatype::indexOf(selectorExpr);
+      TypeNode tnnp = n[0].getType();
+      //register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt
+      registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex );
+
+
+      //relationships between arguments
+      if( isKindArg( tnnp, csIndex ) ){
+        Kind parentKind = d_arg_kind[tnnp][csIndex];
+        if( sIndex==1 && isComm( parentKind ) ){
+          //if commutative, normalize based on term ordering (the constructor index of left arg must be less than or equal to the right arg)
+          Trace("sygus-split-debug") << "Commutative operator : " << parentKind << std::endl;
+          if( pdt[csIndex].getNumArgs()==2 ){
+            TypeNode tn1 = TypeNode::fromType( ((SelectorType)pdt[csIndex][0].getType()).getRangeType() );
+            TypeNode tn2 = TypeNode::fromType( ((SelectorType)pdt[csIndex][1].getType()).getRangeType() );
+            if( tn1==tn2 ){
               registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, 0 );
-            }
-            for( unsigned i=1; i<pdt.getNumConstructors(); i++ ){
-              if( d_sygus_pc_nred[tnn][csIndex][i] ){
-                std::vector< Node > lem_c;
-                for( unsigned j=0; j<i; j++ ){
-                  if( d_sygus_pc_nred[tnn][csIndex][j] ){
-                    lem_c.push_back( 
-                  }
-                }
-              }
+              onComm = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] );
             }
           }
         }
       }
+
     }
-    */
-  }
 
-  for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-    bool addSplit = d_sygus_nred[tnn][i];
-    if( addSplit ){
-      if( csIndex!=-1 ){
-        addSplit = d_sygus_pc_nred[tnn][csIndex][sIndex][i];
-      }
+    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+      Trace("sygus-split-debug2") << "Add split " << n << " : constructor " << i << " : ";
+      Assert( d_sygus_nred.find( tnn )!=d_sygus_nred.end() );
+      bool addSplit = d_sygus_nred[tnn][i];
       if( addSplit ){
-        Node test = DatatypesRewriter::mkTester( n, i, dt );
-        splits.push_back( test );
+        if( csIndex!=-1 ){
+          Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() );
+          addSplit = d_sygus_pc_nred[tnn][csIndex][sIndex][i];
+        }
+        if( addSplit ){
+          Node test = DatatypesRewriter::mkTester( n, i, dt );
+          if( options::sygusNormalFormArg() ){
+            //strengthen based on commutativity, if possible
+            if( !onComm.isNull() ){
+              std::vector< Node > lem_c;
+              for( unsigned j=0; j<=i; j++ ){
+                if( d_sygus_pc_nred[tnn][csIndex][0][i] ){
+                  lem_c.push_back( DatatypesRewriter::mkTester( onComm, j, dt ) );
+                }
+              }
+              Assert( !lem_c.empty() );
+              Node commStr = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( OR, lem_c );
+              Trace("sygus-nf") << "...strengthen " << test << " based on commutatitivity : " << commStr << std::endl;
+              test = NodeManager::currentNM()->mkNode( AND, test, commStr );
+            }
+          }
+          d_splits[n].push_back( test );
+          Trace("sygus-split-debug2") << "SUCCESS" << std::endl;
+        }else{
+          Trace("sygus-split-debug2") << "redundant argument" << std::endl;
+        }
+      }else{
+        Trace("sygus-split-debug2") << "redundant operator" << std::endl;
       }
     }
+    Assert( !d_splits[n].empty() );
   }
-  Assert( !splits.empty() );
+  //copy to splits
+  splits.insert( splits.end(), d_splits[n].begin(), d_splits[n].end() );
 }
 
 void SygusSplit::registerSygusType( TypeNode tn, const Datatype& dt ) {
@@ -172,7 +189,7 @@ void SygusSplit::registerSygusType( TypeNode tn, const Datatype& dt ) {
       }
       Trace("sygus-split") << std::endl;
     }
-    
+
     //compute the redundant operators
     for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
       bool nred = true;
@@ -413,7 +430,7 @@ bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pd
       return false;
     }
   }
-  
+
   return true;
 }
 
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index bd7eaad69..46497b586 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -30,6 +30,7 @@ namespace datatypes {
 class SygusSplit
 {
 private:
+  std::map< Node, std::vector< Node > > d_splits;
   std::map< TypeNode, std::vector< bool > > d_sygus_nred;
   std::map< TypeNode, std::map< int, std::map< int, std::vector< bool > > > > d_sygus_pc_nred;
   //information for builtin types
@@ -75,7 +76,7 @@ private:
   int getFirstArgOccurrence( const DatatypeConstructor& c, const Datatype& dt );
 public:
   /** get sygus splits */
-  void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits );
+  void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas );
 };
   
   
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index bbc8837b9..82804e565 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -246,7 +246,12 @@ void TheoryDatatypes::check(Effort e) {
                   Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
                   std::vector< Node > children;
                   if( dt.isSygus() && d_sygus_split ){
-                    d_sygus_split->getSygusSplits( n, dt, children );
+                    std::vector< Node > lemmas;
+                    d_sygus_split->getSygusSplits( n, dt, children, lemmas );
+                    for( unsigned i=0; i<lemmas.size(); i++ ){
+                      Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
+                      d_out->lemma( lemmas[i] );
+                    }
                   }else{
                     for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
                       Node test = DatatypesRewriter::mkTester( n, i, dt );
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 6aeb8cda0..f0edb7106 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -36,7 +36,7 @@ void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
     d.push_back( n );
   }
 }
-  
+
 CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
   d_refine_count = 0;
 }
@@ -72,6 +72,7 @@ Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i
   }else{
     std::map< int, Node >::iterator it = d_lits.find( i );
     if( it==d_lits.end() ){
+      Trace("cegqi-engine") << "******* CEGQI : allocate size literal " << i << std::endl;
       Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i ) ) );
       lit = Rewriter::rewrite( lit );
       d_lits[i] = lit;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index cebc5f245..afa894473 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -200,7 +200,8 @@ option sygusDecompose --sygus-decompose bool :default false
   decompose single invocation synthesis conjectures
 option sygusNormalForm --sygus-normal-form bool :default true
   only search for sygus builtin terms that are in normal form
- 
+option sygusNormalFormArg --sygus-nf-arg bool :default true
+  account for relationship between arguments of operations in sygus normal form
 
 option localTheoryExt --local-t-ext bool :default false
   do instantiation based on local theory extensions