Do ITE term bookkeeping when solving Sygus inputs. Add missing script from Sygus comp 2015. Fix bug 665 regarding strings rewriter for contains.

8 files changed, 94 insertions, 72 deletions

diff --git a/contrib/run-script-syguscomp2015 b/contrib/run-script-syguscomp2015
new file mode 100644
index 000000000..aab6851e1
--- /dev/null
+++ b/contrib/run-script-syguscomp2015
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function trywith {
+  ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+trywith --cegqi --cegqi-si-multi-inst-abort --cegqi-si-abort --decision=internal
+trywith --cegqi --no-cegqi-si
+
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index dce9c088c..f01efb5c4 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -87,16 +87,17 @@ void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
     if( !d_syntax_guided ){
       //add immediate lemma
       Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() );
-      Trace("cegqi") << "Add candidate lemma : " << lem << std::endl;
+      Trace("cegqi-lemma") << "Add candidate lemma : " << lem << std::endl;
       qe->getOutputChannel().lemma( lem );
     }else if( d_ceg_si ){
-      Node lem = d_ceg_si->getSingleInvLemma( d_guard );
-      if( !lem.isNull() ){
-        Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl;
-        qe->getOutputChannel().lemma( lem );
+      std::vector< Node > lems;
+      d_ceg_si->getSingleInvLemma( d_guard, lems );
+      for( unsigned i=0; i<lems.size(); i++ ){
+        Trace("cegqi-lemma") << "Add single invocation lemma " << i << " : " << lems[i] << std::endl;
+        qe->getOutputChannel().lemma( lems[i] );
         if( Trace.isOn("cegqi-debug") ){
-          lem = Rewriter::rewrite( lem );
-          Trace("cegqi-debug") << "...rewritten : " << lem << std::endl;
+          Node rlem = Rewriter::rewrite( lems[i] );
+          Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl;
         }
       }
     }
@@ -279,7 +280,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         if( !lems.empty() ){
           d_last_inst_si = true;
           for( unsigned j=0; j<lems.size(); j++ ){
-            Trace("cegqi-lemma") << "Single invocation lemma : " << lems[j] << std::endl;
+            Trace("cegqi-lemma") << "Single invocation instantiation lemma : " << lems[j] << std::endl;
             d_quantEngine->addLemma( lems[j] );
           }
           d_statistics.d_cegqi_si_lemmas += lems.size();
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index f122c63bb..c31ebd9ab 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -59,7 +59,7 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje
   d_sol = new CegConjectureSingleInvSol( qe );
 }
 
-Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
+void CegConjectureSingleInv::getSingleInvLemma( Node guard, std::vector< Node >& lems ) {
   if( !d_single_inv.isNull() ) {
     d_single_inv_var.clear();
     d_single_inv_sk.clear();
@@ -80,13 +80,10 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
     inst = TermDb::simpleNegate( inst );
     Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
 
-    //copy variables to instantiator
-    d_cinst->d_vars.clear();
-    d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
-
-    return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
-  }else{
-    return Node::null();
+    //register with the instantiator
+    Node ginst = NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
+    lems.push_back( ginst );
+    d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk );
   }
 }
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 7df859337..8950b2642 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -113,8 +113,8 @@ public:
   std::map< Node, Node > d_trans_post;
   std::map< Node, std::vector< Node > > d_prog_templ_vars;
 public:
-  //get the single invocation lemma
-  Node getSingleInvLemma( Node guard );
+  //get the single invocation lemma(s)
+  void getSingleInvLemma( Node guard, std::vector< Node >& lems );
   //initialize
   void initialize( Node q );
   //check
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 41c0e276b..073cba525 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Implementation of cbqi instantiation strategies
+ ** \brief Implementation of counterexample-guided quantifier instantiation strategies
  **/
 
 #include "theory/quantifiers/inst_strategy_cbqi.h"
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "util/ite_removal.h"
 
 using namespace std;
 using namespace CVC4;
@@ -28,7 +29,6 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::arith;
-using namespace CVC4::theory::datatypes;
 
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 //#define MBP_STRICT_ASSERTIONS
@@ -1182,6 +1182,37 @@ void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, st
   subs_rhs.push_back( r );
 }
 
+void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
+  Assert( d_vars.empty() );
+  d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
+  IteSkolemMap iteSkolemMap;
+  d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
+  Assert( d_aux_vars.empty() );
+  for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
+    Trace("cbqi-debug") << "  Auxiliary var (from ITE) : " << i->first << std::endl;
+    d_aux_vars.push_back( i->first );
+  }
+  for( unsigned i=0; i<lems.size(); i++ ){
+    Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
+    Node rlem = lems[i];
+    rlem = Rewriter::rewrite( rlem );
+    Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
+    //record the literals that imply auxiliary variables to be equal to terms
+    if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
+      if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){
+        if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][1][0] )!=d_aux_vars.end() ){
+          Node v = lems[i][1][0];
+          for( unsigned r=1; r<=2; r++ ){
+            d_aux_eq[rlem[r]][v] = lems[i][r][1];
+            Trace("cbqi-debug") << "  " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl;
+          }
+        }
+      }
+    }
+    lems[i] = rlem;
+  }
+}
+
 //old implementation
 
 InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :
@@ -1585,9 +1616,6 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q );
   if( it==d_cinst.end() ){
     CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true );
-    for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
-      cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
-    }
     d_cinst[q] = cinst;
     return cinst;
   }else{
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 0056671be..f882da110 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -9,14 +9,14 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief instantiator_arith_instantiator
+ ** \brief counterexample-guided quantifier instantiation
  **/
 
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__INST_STRATEGT_CBQI_H
-#define __CVC4__INST_STRATEGT_CBQI_H
+#ifndef __CVC4__INST_STRATEGY_CBQI_H
+#define __CVC4__INST_STRATEGY_CBQI_H
 
 #include "theory/quantifiers/instantiation_engine.h"
 #include "theory/arith/arithvar.h"
@@ -30,10 +30,6 @@ namespace arith {
   class TheoryArith;
 }
 
-namespace datatypes {
-  class TheoryDatatypes;
-}
-
 namespace quantifiers {
 
 class CegqiOutput
@@ -64,6 +60,12 @@ private:
   std::map< Node, std::vector< Node > > d_curr_eqc;
   std::map< Node, Node > d_curr_rep;
   std::vector< Node > d_curr_arith_eqc;
+  //auxiliary variables
+  std::vector< Node > d_aux_vars;
+  //literals to equalities for aux vars
+  std::map< Node, std::map< Node, Node > > d_aux_eq;
+  //the CE variables
+  std::vector< Node > d_vars;
 private:
   //for adding instantiations during check
   void computeProgVars( Node n );
@@ -87,16 +89,12 @@ private:
   void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r );
 public:
   CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true );
-  //the CE variables
-  std::vector< Node > d_vars;
-  //auxiliary variables
-  std::vector< Node > d_aux_vars;
-  //literals to equalities for aux vars
-  std::map< Node, std::map< Node, Node > > d_aux_eq;
   //check : add instantiations based on valuation of d_vars
   bool check();
   //presolve for quantified formula
   void presolve( Node q );
+  //register the counterexample lemma (stored in lems), modify vector 
+  void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars );
 };
 
 class InstStrategySimplex : public InstStrategy{
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 492b2dedf..699208fba 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -21,7 +21,6 @@
 #include "theory/quantifiers/inst_strategy_e_matching.h"
 #include "theory/quantifiers/inst_strategy_cbqi.h"
 #include "theory/quantifiers/trigger.h"
-#include "util/ite_removal.h"
 
 using namespace std;
 using namespace CVC4;
@@ -108,44 +107,25 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           lem = Rewriter::rewrite( lem );
           Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
 
-          //must explicitly remove ITEs so that we record dependencies
-          IteSkolemMap iteSkolemMap;
-          std::vector< Node > lems;
-          lems.push_back( lem );
-          d_quantEngine->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
-          CegInstantiator * cinst = NULL;
           if( d_i_cegqi ){
-            cinst = d_i_cegqi->getInstantiator( f );
-            Assert( cinst->d_aux_vars.empty() );
-            for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
-              Trace("cbqi-debug") << "  Auxiliary var (from ITE) : " << i->first << std::endl;
-              cinst->d_aux_vars.push_back( i->first );
+            //must register with the instantiator
+            //must explicitly remove ITEs so that we record dependencies
+            std::vector< Node > ce_vars;
+            for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+              ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
             }
-          }
-          for( unsigned i=0; i<lems.size(); i++ ){
-            Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
-            if( !cinst ){
+            std::vector< Node > lems;
+            lems.push_back( lem );
+            CegInstantiator * cinst = d_i_cegqi->getInstantiator( f );
+            cinst->registerCounterexampleLemma( lems, ce_vars );
+            for( unsigned i=0; i<lems.size(); i++ ){
+              Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl;
               d_quantEngine->addLemma( lems[i], false );
-            }else{
-              Node rlem = lems[i];
-              rlem = Rewriter::rewrite( rlem );
-              Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
-              d_quantEngine->addLemma( rlem, false );
-              //record the literals that imply auxiliary variables to be equal to terms
-              if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
-                if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){
-                  if( std::find( cinst->d_aux_vars.begin(), cinst->d_aux_vars.end(), lems[i][1][0] )!=cinst->d_aux_vars.end() ){
-                    Node v = lems[i][1][0];
-                    for( unsigned r=1; r<=2; r++ ){
-                      cinst->d_aux_eq[rlem[r]][v] = lems[i][r][1];
-                      Trace("cbqi-debug") << "  " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl;
-                    }
-                  }
-                }
-              }
             }
+          }else{
+            Trace("cbqi-debug") << "Counterexample lemma  : " << lem << std::endl;
+            d_quantEngine->addLemma( lem, false );
           }
-
           addedLemma = true;
         }
       }
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 7023f7c41..872933cbd 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -948,8 +948,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         bool flag = false;
         unsigned n1 = node[0].getNumChildren();
         unsigned n2 = node[1].getNumChildren();
-        if(n1 - n2) {
-          for(unsigned i=0; i<=n1 - n2; i++) {
+        if( n1>n2 ){
+          unsigned diff = n1-n2;
+          for(unsigned i=0; i<diff; i++) {
             if(node[0][i] == node[1][0]) {
               flag = true;
               for(unsigned j=1; j<n2; j++) {