Handle miniscoping of conjunctions in synthesis properties. Refactor construction of sygus datatypes. Expand define-fun in evaluators.

5 files changed, 155 insertions, 90 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 920803c28..d2f38cc82 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -493,6 +493,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
   CommandSequence* seq;
   std::vector<CVC4::Datatype> datatypes;
   std::vector< std::vector<Expr> > ops;
+  std::vector< std::vector< std::string > > cnames;
+  std::vector< std::vector< std::vector< CVC4::Type > > > cargs;
 }
   : /* set the logic */
     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
@@ -599,6 +601,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         sorts.push_back(t);
         datatypes.push_back(Datatype(dname));
         ops.push_back(std::vector<Expr>());
+        cnames.push_back(std::vector<std::string>());
+        cargs.push_back(std::vector<std::vector<CVC4::Type> >());
         if(!PARSER_STATE->isUnresolvedType(dname)) {
           // if not unresolved, must be undeclared
           PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
@@ -606,9 +610,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       }
       // Note the official spec for NTDef is missing the ( parens )
       // but they are necessary to parse SyGuS examples
-      LPAREN_TOK sygusGTerm[fun, datatypes.back(), ops.back()]+ RPAREN_TOK
+      LPAREN_TOK sygusGTerm[fun, ops.back(), cnames.back(), cargs.back()]+ RPAREN_TOK
       RPAREN_TOK
-      { PARSER_STATE->popScope(); }
+      { PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() );
+        PARSER_STATE->popScope(); }
     )+
     RPAREN_TOK
     { PARSER_STATE->popScope();
@@ -691,7 +696,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
 
 // SyGuS grammar term
 // fun is the name of the synth-fun this grammar term is for
-sygusGTerm[std::string& fun, CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops]
+sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs]
 @declarations {
   std::string name;
   Kind k;
@@ -702,24 +707,24 @@ sygusGTerm[std::string& fun, CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops]
 }
   : LPAREN_TOK
     ( builtinOp[k]
-      { ops.push_back(EXPR_MANAGER->operatorOf(k));
+      { Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl;
+        ops.push_back(EXPR_MANAGER->operatorOf(k));
         name = kind::kindToString(k);
-        Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl;
       }
     | symbol[name,CHECK_NONE,SYM_VARIABLE]
       { // what is this sygus term trying to accomplish here, if the
         // symbol isn't yet declared?!  probably the following line will
         // fail, but we need an operator to continue here..
-        Expr bv = PARSER_STATE->getVariable(name);
-        ops.push_back(bv);
-        Debug("parser-sygus") << "Sygus grammar " << fun << " : op : " << name << std::endl;
+        Debug("parser-sygus") << "Sygus grammar " << fun;
+        Debug("parser-sygus") << " : op (declare=" <<  PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl;
+        if( !PARSER_STATE->isDefinedFunction(name) ){
+          PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined."));
+        }
+        ops.push_back( PARSER_STATE->getVariable(name) );
       }
     )
-    { name = dt.getName() + "_" + name;
-      std::string testerId("is-");
-      testerId.append(name);
-      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-      ctor = new CVC4::DatatypeConstructor(name, testerId);
+    { cnames.push_back( name );
+      cargs.push_back( std::vector< CVC4::Type >() );
     }
     ( //sortSymbol[t,CHECK_NONE]
       symbol[sname,CHECK_NONE,SYM_VARIABLE]
@@ -727,75 +732,46 @@ sygusGTerm[std::string& fun, CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops]
         ss << fun << "_" << sname;
         sname = ss.str();
         if( PARSER_STATE->isDeclared(sname, SYM_SORT) ) {
-	  t = PARSER_STATE->getSort(sname);
+          t = PARSER_STATE->getSort(sname);
         } else {
-	  t = PARSER_STATE->mkUnresolvedType(sname);
+          t = PARSER_STATE->mkUnresolvedType(sname);
         }
-        std::stringstream cname;
-        cname << fun << "_" << name << "_" << ++count;
-        ctor->addArg(cname.str(), t);
+        cargs.back().push_back(t);
       } )+ RPAREN_TOK
-    { dt.addConstructor(*ctor);
-      delete ctor; }
   | INTEGER_LITERAL
     { Debug("parser-sygus") << "Sygus grammar " << fun << " : integer literal " << AntlrInput::tokenText($INTEGER_LITERAL) << std::endl;
       ops.push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL))));
-      name = dt.getName() + "_" + AntlrInput::tokenText($INTEGER_LITERAL);
-      std::string testerId("is-");
-      testerId.append(name);
-      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
-      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-      CVC4::DatatypeConstructor c(name, testerId);
-      dt.addConstructor(c);
+      cnames.push_back( AntlrInput::tokenText($INTEGER_LITERAL) );
+      cargs.push_back( std::vector< CVC4::Type >() );
     }
   | HEX_LITERAL
     { Debug("parser-sygus") << "Sygus grammar " << fun << " : hex literal " << AntlrInput::tokenText($HEX_LITERAL) << std::endl;
       assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
       ops.push_back(MK_CONST( BitVector(hexString, 16) ));
-      name = dt.getName() + "_" + AntlrInput::tokenText($HEX_LITERAL);
-      std::string testerId("is-");
-      testerId.append(name);
-      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
-      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-      CVC4::DatatypeConstructor c(name, testerId);
-      dt.addConstructor(c);
+      cnames.push_back( AntlrInput::tokenText($HEX_LITERAL) );
+      cargs.push_back( std::vector< CVC4::Type >() );
     }
   | BINARY_LITERAL
     { Debug("parser-sygus") << "Sygus grammar " << fun << " : binary literal " << AntlrInput::tokenText($BINARY_LITERAL) << std::endl;
       assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
       ops.push_back(MK_CONST( BitVector(binString, 2) ));
-      name = dt.getName() + "_" + AntlrInput::tokenText($BINARY_LITERAL);
-      std::string testerId("is-");
-      testerId.append(name);
-      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
-      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-      CVC4::DatatypeConstructor c(name, testerId);
-      dt.addConstructor(c);
+      cnames.push_back( AntlrInput::tokenText($BINARY_LITERAL) );
+      cargs.push_back( std::vector< CVC4::Type >() );
     }
   | symbol[name,CHECK_NONE,SYM_VARIABLE]
     { if( name[0] == '-' ){  //hack for unary minus
         Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl;
         ops.push_back(MK_CONST(Rational(name)));
-        name = dt.getName() + "_" + name;
-        std::string testerId("is-");
-        testerId.append(name);
-        PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
-        PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-        CVC4::DatatypeConstructor c(name, testerId);
-        dt.addConstructor(c);
+        cnames.push_back( name );
+        cargs.push_back( std::vector< CVC4::Type >() );
       }else{
         Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl;
         Expr bv = PARSER_STATE->getVariable(name);
         ops.push_back(bv);
-        name = dt.getName() + "_" + name;
-        std::string testerId("is-");
-        testerId.append(name);
-        PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
-        PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-        CVC4::DatatypeConstructor c(name, testerId);
-        dt.addConstructor(c);
+        cnames.push_back( name );
+        cargs.push_back( std::vector< CVC4::Type >() );
       }
     }
   ;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d20d48b13..077f385b0 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -504,7 +504,7 @@ void Smt2::includeFile(const std::string& filename) {
 
     //Type t = getExprManager()->mkFunctionType(types, rangeType);
     //Debug("parser-sygus") << "...function type : " << t << std::endl;
-    
+
     Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED);
     Debug("parser-sygus") << "...made function : " << lambda << std::endl;
     std::vector<Expr> applyv;
@@ -524,10 +524,30 @@ void Smt2::includeFile(const std::string& filename) {
   }
 }
 
+void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
+                            std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) {
+  //minimize grammar goes here
+
+  for( unsigned i=0; i<cnames.size(); i++ ){
+    std::string name = dt.getName() + "_" + cnames[i];
+    std::string testerId("is-");
+    testerId.append(name);
+    checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+    checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+    CVC4::DatatypeConstructor c(name, testerId);
+    for( unsigned j=0; j<cargs[i].size(); j++ ){
+      std::stringstream sname;
+      sname << name << "_" << j;
+      c.addArg(sname.str(), cargs[i][j]);
+    }
+    dt.addConstructor(c);
+  }
+}
+
 // i is index in datatypes/ops
 // j is index is datatype
-Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, 
-                              std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms, 
+Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
+                              std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
                               Expr eval, const Datatype& dt, size_t i, size_t j ) {
   const DatatypeConstructor& ctor = dt[j];
   Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl;
@@ -567,7 +587,11 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
   Expr builtTerm;
   //if( ops[i][j].getKind() == kind::BUILTIN ){
   if( !builtApply.empty() ){
-    builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
+    if( ops[i][j].getKind() != kind::BUILTIN ){
+      builtTerm = getExprManager()->mkExpr(kind::APPLY, ops[i][j], builtApply);
+    }else{
+      builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
+    }
   }else{
     builtTerm = ops[i][j];
   }
@@ -577,7 +601,7 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
   pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
   assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern);
   Debug("parser-sygus") << "...made assertion " << assertion << std::endl;
-  
+
   //linearize multiplication if possible
   if( builtTerm.getKind()==kind::MULT ){
     for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index ca1602f36..ed6a5128b 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -183,11 +183,14 @@ public:
   }
 
   void defineSygusFuns();
-  
+
+  void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
+                        std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs );
+
   // i is index in datatypes/ops
   // j is index is datatype
-  Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, 
-                          std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms, 
+  Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
+                          std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
                           Expr eval, const Datatype& dt, size_t i, size_t j );
 
   void addSygusConstraint(Expr constraint) {
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index e6dce35e0..6aeb8cda0 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -27,6 +27,16 @@ using namespace std;
 
 namespace CVC4 {
 
+void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
+  if( n.getKind()==OR ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      collectDisjuncts( n[i], d );
+    }
+  }else{
+    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;
 }
@@ -113,9 +123,17 @@ void CegInstantiation::registerQuantifier( Node q ) {
       d_conj->d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj->d_candidates ) );
       Trace("cegqi") << "Base instantiation is : " << d_conj->d_base_inst << std::endl;
       if( getTermDatabase()->isQAttrSygus( q ) ){
-        if( d_conj->d_base_inst.getKind()==NOT && d_conj->d_base_inst[0].getKind()==FORALL ){
-          for( unsigned j=0; j<d_conj->d_base_inst[0][0].getNumChildren(); j++ ){
-            d_conj->d_inner_vars.push_back( d_conj->d_base_inst[0][0][j] );
+        collectDisjuncts( d_conj->d_base_inst, d_conj->d_base_disj );
+        Trace("cegqi") << "Conjecture has " << d_conj->d_base_disj.size() << " disjuncts." << std::endl;
+        //store the inner variables for each disjunct
+        for( unsigned j=0; j<d_conj->d_base_disj.size(); j++ ){
+          d_conj->d_inner_vars_disj.push_back( std::vector< Node >() );
+          //if the disjunct is an existential, store it
+          if( d_conj->d_base_disj[j].getKind()==NOT && d_conj->d_base_disj[j][0].getKind()==FORALL ){
+            for( unsigned k=0; k<d_conj->d_base_disj[j][0][0].getNumChildren(); k++ ){
+              d_conj->d_inner_vars.push_back( d_conj->d_base_disj[j][0][0][k] );
+              d_conj->d_inner_vars_disj[j].push_back( d_conj->d_base_disj[j][0][0][k] );
+            }
           }
         }
         d_conj->d_syntax_guided = true;
@@ -229,19 +247,38 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         }else{
           //must get a counterexample to the value of the current candidate
           Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
-          inst = Rewriter::rewrite( inst );
-          //if body is existential, immediately skolemize
-          Node inst_sk;
-          if( inst.getKind()==NOT && inst[0].getKind()==FORALL ){
-            inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] ).negate();
-          }else{
-            inst_sk = inst;
+          //check whether we will run CEGIS on inner skolem variables
+          bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 );
+          if( sk_refine ){
+            conj->d_ce_sk.push_back( std::vector< Node >() );
           }
-          Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
-          d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) );
-          if( !conj->isGround() || conj->d_refine_count==0 ){
-            conj->d_ce_sk.push_back( inst[0] );
+          std::vector< Node > ic;
+          ic.push_back( q.negate() );
+          std::vector< Node > d;
+          collectDisjuncts( inst, d );
+          Assert( d.size()==conj->d_base_disj.size() );
+          //immediately skolemize inner existentials
+          for( unsigned i=0; i<d.size(); i++ ){
+            Node dr = Rewriter::rewrite( d[i] );
+            if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
+              ic.push_back( getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
+              if( sk_refine ){
+                conj->d_ce_sk.back().push_back( dr[0] );
+              }
+            }else{
+              ic.push_back( dr );
+              if( sk_refine ){
+                conj->d_ce_sk.back().push_back( Node::null() );
+              }
+              if( !conj->d_inner_vars_disj[i].empty() ){
+                Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl;
+              }
+            }
           }
+          Node lem = NodeManager::currentNM()->mkNode( OR, ic );
+          lem = Rewriter::rewrite( lem );
+          Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
+          d_quantEngine->addLemma( lem );
           Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
         }
       }
@@ -260,19 +297,38 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   }else{
     Trace("cegqi-engine") << "  *** Refine candidate phase..." << std::endl;
     for( unsigned j=0; j<conj->d_ce_sk.size(); j++ ){
-      Node ce_q = conj->d_ce_sk[j];
-      Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[ce_q].size() );
-      std::vector< Node > model_values;
-      if( getModelValues( getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){
-        //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
-        Node inst_ce_refine;
-        if( !conj->d_inner_vars.empty() ){
-          inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(),
-                                                               model_values.begin(), model_values.end() );
+      bool success = true;
+      std::vector< Node > lem_c;
+      Assert( conj->d_ce_sk[j].size()==conj->d_base_disj.size() );
+      for( unsigned k=0; k<conj->d_ce_sk[j].size(); k++ ){
+        Node ce_q = conj->d_ce_sk[j][k];
+        Node c_disj = conj->d_base_disj[k];
+        if( !ce_q.isNull() ){
+          Assert( !conj->d_inner_vars_disj[k].empty() );
+          Assert( conj->d_inner_vars_disj[k].size()==getTermDatabase()->d_skolem_constants[ce_q].size() );
+          std::vector< Node > model_values;
+          if( getModelValues( getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){
+            //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
+            Node inst_ce_refine = conj->d_base_disj[k][0][1].substitute( conj->d_inner_vars_disj[k].begin(), conj->d_inner_vars_disj[k].end(),
+                                                                         model_values.begin(), model_values.end() );
+            lem_c.push_back( inst_ce_refine );
+          }else{
+            success = false;
+            break;
+          }
         }else{
-          inst_ce_refine = conj->d_base_inst.negate();
+          if( conj->d_inner_vars_disj[k].empty() ){
+            lem_c.push_back( conj->d_base_disj[k].negate() );
+          }else{
+            //denegrate case : quantified disjunct was trivially true and does not need to be refined
+            Trace("cegqi-debug") << "*** skip " << conj->d_base_disj[k] << std::endl;
+          }
         }
-        Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine );
+      }
+      if( success ){
+        Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
+        lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), lem );
+        lem = Rewriter::rewrite( lem );
         Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
         Trace("cegqi-engine") << "  ...refine candidate." << std::endl;
         d_quantEngine->addLemma( lem );
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 4f44c121f..8c74b06f6 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -29,6 +29,9 @@ class CegInstantiation : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 private:
+  /** collect disjuncts */
+  static void collectDisjuncts( Node n, std::vector< Node >& ex );
+  /** a synthesis conjecture */
   class CegConjecture {
   public:
     CegConjecture( context::Context* c );
@@ -42,6 +45,8 @@ private:
     Node d_guard;
     /** base instantiation */
     Node d_base_inst;
+    /** expand base inst to disjuncts */
+    std::vector< Node > d_base_disj;
     /** guard split */
     Node d_guard_split;
     /** is syntax-guided */
@@ -49,7 +54,8 @@ private:
     /** list of constants for quantified formula */
     std::vector< Node > d_candidates;
     /** list of variables on inner quantification */
-    std::vector< Node > d_inner_vars;
+    std::vector< Node > d_inner_vars;    
+    std::vector< std::vector< Node > > d_inner_vars_disj;
     /** initialize guard */
     void initializeGuard( QuantifiersEngine * qe );
     /** measure term */
@@ -63,7 +69,7 @@ private:
     /** is assigned */
     bool isAssigned() { return !d_quant.isNull(); }
     /** current extential quantifeirs whose couterexamples we must refine */
-    std::vector< Node > d_ce_sk;
+    std::vector< std::vector< Node > > d_ce_sk;
   public:  //for fairness
     /** the cardinality literals */
     std::map< int, Node > d_lits;