ite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8eb6664ca94d5553ca6d40a6707307e7a337b6b8..e7b3daa2b0e15efbecd5631d438d9463e126a913 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1427,17 +1427,27 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
   return node;
 }
 
+
+struct ContainsQuantAttributeId {};
+typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute;
+
 // check if the given node contains a universal quantifier
 static bool containsQuantifiers(Node n) {
-  if(n.getKind() == kind::FORALL) {
+  if( n.hasAttribute(ContainsQuantAttribute()) ){
+    return n.getAttribute(ContainsQuantAttribute())==1;
+  } else if(n.getKind() == kind::FORALL) {
     return true;
   } else {
-    for(unsigned i = 0; i < n.getNumChildren(); ++i) {
-      if(containsQuantifiers(n[i])) {
-        return true;
+    bool cq = false;
+    for( unsigned i = 0; i < n.getNumChildren(); ++i ){
+      if( containsQuantifiers(n[i]) ){
+        cq = true;
+        break;
       }
     }
-    return false;
+    ContainsQuantAttribute cqa;
+    n.setAttribute(cqa, cq ? 1 : 0);
+    return cq;
   }
 }
 
@@ -1498,43 +1508,36 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
     }
   }else{
     //check if it contains a quantifier as a subterm
-    bool containsQuant = false;
-    if( n.getType().isBoolean() ){
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        if( containsQuantifiers( n[i] ) ){
-          containsQuant = true;
-          break;
-        }
-      }
-    }
     //if so, we will write this node
-    if( containsQuant ){
-      if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
-        Node nn;
-        //must remove structure
-        if( n.getKind()==kind::ITE ){
-          nn = NodeManager::currentNM()->mkNode( kind::AND,
-                 NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
-                 NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
-        }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
-          nn = NodeManager::currentNM()->mkNode( kind::AND,
-                 NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
-                 NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
-        }else if( n.getKind()==kind::IMPLIES ){
-          nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
-        }
-        return preSkolemizeQuantifiers( nn, polarity, fvs );
-      }else{
-        Assert( n.getKind() == kind::AND || n.getKind() == kind::OR );
-        vector< Node > children;
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
+    if( containsQuantifiers( n ) ){
+      if( n.getType().isBoolean() ){
+        if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
+          Node nn;
+          //must remove structure
+          if( n.getKind()==kind::ITE ){
+            nn = NodeManager::currentNM()->mkNode( kind::AND,
+                   NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
+                   NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
+          }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+            nn = NodeManager::currentNM()->mkNode( kind::AND,
+                   NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
+                   NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
+          }else if( n.getKind()==kind::IMPLIES ){
+            nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
+          }
+          return preSkolemizeQuantifiers( nn, polarity, fvs );
+        }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
+          vector< Node > children;
+          for( int i=0; i<(int)n.getNumChildren(); i++ ){
+            children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
+          }
+          return NodeManager::currentNM()->mkNode( n.getKind(), children );
+        }else{
+          //must pull ite's
         }
-        return NodeManager::currentNM()->mkNode( n.getKind(), children );
       }
-    }else{
-      return n;
     }
+    return n;
   }
 }
 

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 85a96f90aa1b27cb1938e3330f76ce57fe843f06..5a80512cdbcada4bab0113d62ca7a087f648b269 100644 (file)
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -140,7 +140,7 @@ void InstMatch::set(TNode var, TNode n){
        //var.getType() == n.getType()
        !n.getType().isSubtypeOf( var.getType() ) ){
     Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
-    Trace("inst-match-warn") << var << " " << var.getType() << n << " " << n.getType() << std::endl ;
+    Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
     Assert(false);
   }
   d_map[var] = n;

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 5484e25e9a3aa9a2c86880f2fbf6b9de1e4498aa..dd8588b52375a31ed067fa1426adbd4dba36ecb8 100644 (file)
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -74,7 +74,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
     int childMatchPolicy = MATCH_GEN_DEFAULT;
     for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
       if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
-        if( d_match_pattern[i].getKind()!=INST_CONSTANT ){
+        if( d_match_pattern[i].getKind()!=INST_CONSTANT && !Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
           InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy );
           d_children.push_back( cimg );
           d_children_index.push_back( i );
@@ -115,7 +115,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
       d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
     }else{
       d_cg = new CandidateGeneratorQueue;
-      if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
+      if( !Trigger::isArithmeticTrigger( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
         Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
         //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
         d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
@@ -155,14 +155,20 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
     //first, check if ground arguments are not equal, or a match is in conflict
     for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
       if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
-        if( d_match_pattern[i].getKind()==INST_CONSTANT ){
-          if( !m.setMatch( q, d_match_pattern[i], t[i] ) ){
+        if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
+          Node vv = d_match_pattern[i];
+          Node tt = t[i];
+          if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
+            vv = d_match_pattern[i][0];
+            tt = NodeManager::currentNM()->mkConst(q->areEqual( tt, d_match_pattern[i][1] ));
+          }
+          if( !m.setMatch( q, vv, tt ) ){
             //match is in conflict
-            Debug("matching-debug") << "Match in conflict " << t[i] << " and "
-                                    << d_match_pattern[i] << " because "
-                                    << m.get(d_match_pattern[i])
+            Debug("matching-debug") << "Match in conflict " << tt << " and "
+                                    << vv << " because "
+                                    << m.get(vv)
                                     << std::endl;
-            Debug("matching-fail") << "Match fail: " << m.get(d_match_pattern[i]) << " and " << t[i] << std::endl;
+            Debug("matching-fail") << "Match fail: " << m.get(vv) << " and " << tt << std::endl;
             success = false;
             break;
           }

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 3f5cc76660e6e6b72a328bd1219831feeeb6cb11..0915f59a532a98b3fc0ef9c62e257c68e9cac166 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -145,6 +145,10 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
     if( gen ){
       generateTriggers( f, effort, e, status );
     }
+    //if( e==4 ){
+    //  d_processed_trigger.clear();
+    //  d_quantEngine->getEqualityQuery()->setLiberal( true );
+    //}
     Debug("quant-uf-strategy")  << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;
     //Notice() << "Try auto-generated triggers..." << std::endl;
     for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){
@@ -171,6 +175,9 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
         }
       }
     }
+    //if( e==4 ){
+    //  d_quantEngine->getEqualityQuery()->setLiberal( false );
+    //}
     Debug("quant-uf-strategy") << "done." << std::endl;
     //Notice() << "done" << std::endl;
     return status;

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 7a3687dd589d9ed81ee5591a77391611f854a7f0..222fc4425e62622f98ca41724a8e4e594981adda 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -36,7 +36,8 @@ option cnfQuant --cnf-quant bool :default false
 #   forall x. P( x ) => f( S( x ) ) = x
 option preSkolemQuant --pre-skolem-quant bool :default false
  apply skolemization eagerly to bodies of quantified formulas
-
+option iteRemoveQuant --ite-remove-quant bool :default false
+ apply ite removal to bodies of quantifiers
 # Whether to perform agressive miniscoping
 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
@@ -48,7 +49,7 @@ option macrosQuant --macros-quant bool :default false
 option smartTriggers /--disable-smart-triggers bool :default true
  disable smart triggers
 # Whether to use relevent triggers
-option relevantTriggers --relevant-triggers bool :default true
+option relevantTriggers /--disable-relevant-triggers bool :default true
  prefer triggers that are more relevant based on SInE style analysis
 
 # Whether to consider terms in the bodies of quantifiers for matching

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 85602dbab0b96575da8b1e0e5ffc817e248cf6aa..0b4f2654b7fdeaefe6b39e8a7950e6de00d24c6f 100644 (file)
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -91,6 +91,8 @@ public:
   virtual eq::EqualityEngine* getEngine() = 0;
   /** get the equivalence class of a */
   virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
+
+  virtual void setLiberal( bool l ) = 0;
 };/* class EqualityQuery */
 
 }

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index cff28f243d2770d17d27a868dd539fe4e7b2e82a..125829e06167837909dc307c024965fe4c47ed31 100644 (file)
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -226,17 +226,24 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
 
 bool Trigger::isUsable( Node n, Node f ){
   if( n.getAttribute(InstConstantAttribute())==f ){
-    if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){
-      std::map< Node, Node > coeffs;
-      return getPatternArithmetic( f, n, coeffs );
-    }else{
+    if( isAtomicTrigger( n ) ){
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
         if( !isUsable( n[i], f ) ){
           return false;
         }
       }
       return true;
+    }else if( n.getKind()==INST_CONSTANT ){
+      return true;
+    }else{
+      std::map< Node, Node > coeffs;
+      if( isArithmeticTrigger( f, n, coeffs ) ){
+        return true;
+      }else if( isBooleanTermTrigger( n ) ){
+        return true;
+      }
     }
+    return false;
   }else{
     return true;
   }
@@ -368,7 +375,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
   }
 }
 
-bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){
+bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ){
   if( n.getKind()==PLUS ){
     Assert( coeffs.empty() );
     NodeBuilder<> t(kind::PLUS);
@@ -381,7 +388,7 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
             coeffs.clear();
             return false;
           }
-        }else if( !getPatternArithmetic( f, n[i], coeffs ) ){
+        }else if( !isArithmeticTrigger( f, n[i], coeffs ) ){
           coeffs.clear();
           return false;
         }
@@ -413,6 +420,22 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
   return false;
 }
 
+bool Trigger::isBooleanTermTrigger( Node n ) {
+  if( n.getKind()==ITE ){
+    //check for boolean term converted to ITE
+    if( n[0].getKind()==INST_CONSTANT &&
+        n[1].getKind()==CONST_BITVECTOR &&
+        n[2].getKind()==CONST_BITVECTOR ){
+      if( ((BitVectorType)n[1].getType().toType()).getSize()==1 &&
+          n[1].getConst<BitVector>().toInteger()==1 &&
+          n[2].getConst<BitVector>().toInteger()==0 ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
 Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
   if( nodes.empty() ){
     return d_tr;

diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 93731283bc77982c0d2b1c53c365448009ee0f8b..9ecac0120cad3224da99cd6eedb14ae7bde6ccf8 100644 (file)
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -109,7 +109,8 @@ public:
   static bool isAtomicTrigger( Node n );
   static bool isSimpleTrigger( Node n );
   /** get pattern arithmetic */
-  static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs );
+  static bool isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs );
+  static bool isBooleanTermTrigger( Node n );
 
   inline void toStream(std::ostream& out) const {
     out << "TRIGGER( ";

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a11cc85c0c3536013b5fa2ae4240c31ada451224..f12143bbe821579d2a214f89d798d2d8ba11a2c2 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -583,12 +583,16 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
     return true;
   }else{
     eq::EqualityEngine* ee = getEngine();
-    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-      if( ee->areEqual( a, b ) ){
-        return true;
+    if( d_liberal ){
+      return true;//!areDisequal( a, b );
+    }else{
+      if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+        if( ee->areEqual( a, b ) ){
+          return true;
+        }
       }
+      return false;
     }
-    return false;
   }
 }
 

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 9f520f4201385b71c60d327646132947963c29d1..5f288a186b3ad2202dc7df6af7e3b07caf5ac9fe 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -272,6 +272,8 @@ private:
   std::map< Node, int > d_rep_score;
   /** reset count */
   int d_reset_count;
+
+  bool d_liberal;
 private:
   /** node contains */
   Node getInstance( Node n, std::vector< Node >& eqc );
@@ -280,7 +282,7 @@ private:
   /** choose rep based on sort inference */
   bool optInternalRepSortInference();
 public:
-  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
+  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
   ~EqualityQueryQuantifiersEngine(){}
   /** reset */
   void reset();
@@ -296,6 +298,8 @@ public:
       not contain instantiation constants, if such a term exists.
    */
   Node getInternalRepresentative( Node a, Node f, int index );
+
+  void setLiberal( bool l ) { d_liberal = l; }
 }; /* EqualityQueryQuantifiersEngine */
 
 }/* CVC4::theory namespace */

diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 240e5a0cf55773192ef58568275abcdb21fe9eb7..de7ae2e9710edbc52c54083053ec6841e518bacd 100644 (file)
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -19,6 +19,7 @@
 #include "util/ite_removal.h"
 #include "theory/rewriter.h"
 #include "expr/command.h"
+#include "theory/quantifiers/options.h"
 
 using namespace CVC4;
 using namespace std;
@@ -28,12 +29,13 @@ namespace CVC4 {
 void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
 {
   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
-    output[i] = run(output[i], output, iteSkolemMap);
+    std::vector<Node> quantVar;
+    output[i] = run(output[i], output, iteSkolemMap, quantVar);
   }
 }
 
 Node RemoveITE::run(TNode node, std::vector<Node>& output,
-                    IteSkolemMap& iteSkolemMap) {
+                    IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) {
   // Current node
   Debug("ite") << "removeITEs(" << node << ")" << endl;
 
@@ -50,8 +52,23 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   if(node.getKind() == kind::ITE) {
     TypeNode nodeType = node.getType();
     if(!nodeType.isBoolean()) {
+      Node skolem;
       // Make the skolem to represent the ITE
-      Node skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
+      if( quantVar.empty() ){
+        skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
+      }else{
+        //if in the scope of free variables, make a skolem operator
+        vector< TypeNode > argTypes;
+        for( size_t i=0; i<quantVar.size(); i++ ){
+          argTypes.push_back( quantVar[i].getType() );
+        }
+        TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, nodeType );
+        Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" );
+        vector< Node > funcArgs;
+        funcArgs.push_back( op );
+        funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() );
+        skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
+      }
 
       // The new assertion
       Node newAssertion =
@@ -63,7 +80,16 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
       d_iteCache[node] = skolem;
 
       // Remove ITEs from the new assertion, rewrite it and push it to the output
-      newAssertion = run(newAssertion, output, iteSkolemMap);
+      newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
+
+      if( !quantVar.empty() ){
+        //if in the scope of free variables, it is a quantified assertion
+        vector< Node > children;
+        children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) );
+        children.push_back( newAssertion );
+        newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children );
+      }
+
       iteSkolemMap[skolem] = output.size();
       output.push_back(newAssertion);
 
@@ -73,9 +99,16 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   }
 
   // If not an ITE, go deep
-  if( node.getKind() != kind::FORALL &&
+  if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) &&
       node.getKind() != kind::EXISTS &&
       node.getKind() != kind::REWRITE_RULE ) {
+    std::vector< Node > newQuantVar;
+    newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() );
+    if( node.getKind()==kind::FORALL ){
+      for( size_t i=0; i<node[0].getNumChildren(); i++ ){
+        newQuantVar.push_back( node[0][i] );
+      }
+    }
     vector<Node> newChildren;
     bool somethingChanged = false;
     if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
@@ -83,7 +116,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
     }
     // Remove the ITEs from the children
     for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
-      Node newChild = run(*it, output, iteSkolemMap);
+      Node newChild = run(*it, output, iteSkolemMap, newQuantVar);
       somethingChanged |= (newChild != *it);
       newChildren.push_back(newChild);
     }

diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 77e9c39db9986608528e81b76efd3d52b6a720d0..6c0c74cd49ce5b4f14787688578bdc8f3ef01837 100644 (file)
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -55,7 +55,7 @@ public:
    * ite created in conjunction with that skolem variable.
    */
   Node run(TNode node, std::vector<Node>& additionalAssertions,
-           IteSkolemMap& iteSkolemMap);
+           IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar);
 
 };/* class RemoveTTE */