Implement dynamic splitting for quantified formulas. Minor refactoring of reductions in quantifiers engine.

9 files changed, 262 insertions, 92 deletions

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index b72f15a01..d49b37e4c 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -79,7 +79,7 @@ bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
   return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index );
 }
 
-bool AlphaEquivalence::registerQuantifier( Node q ) {
+bool AlphaEquivalence::reduceQuantifier( Node q ) {
   Assert( q.getKind()==FORALL );
   Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
   //construct canonical quantified formula
@@ -99,7 +99,7 @@ bool AlphaEquivalence::registerQuantifier( Node q ) {
   sto.d_tdb = d_qe->getTermDatabase();
   std::sort( typs.begin(), typs.end(), sto );
   Trace("aeq-debug") << "  ";
-  bool ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
+  bool ret = !AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
   Trace("aeq") << "  ...result : " << ret << std::endl;
   return ret;
 }
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index 99517fd2a..18a700842 100644
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -48,7 +48,7 @@ public:
   AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){}
   ~AlphaEquivalence(){}
 
-  bool registerQuantifier( Node q );
+  bool reduceQuantifier( Node q );
 };
 
 }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 272f16be8..6c912cdab 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -36,18 +36,11 @@ d_qe( qe ), d_forall_asserts( c ), d_isModelSet( c, false ){
 
 }
 
-void FirstOrderModel::assertQuantifier( Node n, bool reduced ){
-  if( !reduced ){
-    if( n.getKind()==FORALL ){
-      d_forall_asserts.push_back( n );
-    }else if( n.getKind()==NOT ){
-      Assert( n[0].getKind()==FORALL );
-    }
-  }else{
-    Assert( n.getKind()==FORALL );
-    Assert( d_forall_to_reduce.find( n )==d_forall_to_reduce.end() );
-    d_forall_to_reduce[n] = true;
-    Trace("quant") << "Mark to reduce : " << n << std::endl;
+void FirstOrderModel::assertQuantifier( Node n ){
+  if( n.getKind()==FORALL ){
+    d_forall_asserts.push_back( n );
+  }else if( n.getKind()==NOT ){
+    Assert( n[0].getKind()==FORALL );
   }
 }
 
@@ -122,20 +115,17 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
 
 /** needs check */
 bool FirstOrderModel::checkNeeded() {
-  return d_forall_asserts.size()>0 || !d_forall_to_reduce.empty();
-}
-
-/** mark reduced */
-void FirstOrderModel::markQuantifierReduced( Node q ) {
-  Assert( d_forall_to_reduce.find( q )!=d_forall_to_reduce.end() );
-  d_forall_to_reduce.erase( q );
-  Trace("quant") << "Mark reduced : " << q << std::endl;
+  return d_forall_asserts.size()>0;
 }
 
 void FirstOrderModel::reset_round() {
   d_quant_active.clear();
 }
 
+//bool FirstOrderModel::isQuantifierAsserted( TNode q ) {
+//  return d_forall_asserts.find( q )!=d_forall_asserts.end();
+//}
+
 void FirstOrderModel::setQuantifierActive( TNode q, bool active ) {
   d_quant_active[q] = active;
 }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index d42eb61e3..d5dc62667 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -49,8 +49,6 @@ protected:
   QuantifiersEngine * d_qe;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
-  /** list of quantifiers that have been marked to reduce */
-  std::map< Node, bool > d_forall_to_reduce;
   /** is model set */
   context::CDO< bool > d_isModelSet;
   /** get variable id */
@@ -59,13 +57,11 @@ protected:
   virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
 public: //for Theory Quantifiers:
   /** assert quantifier */
-  void assertQuantifier( Node n, bool reduced = false );
+  void assertQuantifier( Node n );
   /** get number of asserted quantifiers */
   int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
   /** get asserted quantifier */
   Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
-  /** get number to reduce quantifiers */
-  unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); }
   /** initialize model for term */
   void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
   virtual void processInitializeModelForTerm( Node n ) = 0;
@@ -94,14 +90,14 @@ public:
   Node getSomeDomainElement(TypeNode tn);
   /** do we need to do any work? */
   bool checkNeeded();
-  /** mark reduced */
-  void markQuantifierReduced( Node q );
 private:
   //list of inactive quantified formulas
   std::map< TNode, bool > d_quant_active;
 public:
   /** reset round */
   void reset_round();
+  /** is quantified formula asserted */
+  //bool isQuantifierAsserted( TNode q );
   /** set quantified formula active/inactive 
    * a quantified formula may be set inactive if for instance:
    *   - it is entailed by other quantified formulas
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index ad400413e..e6c9b9e6b 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -169,13 +169,15 @@ void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
 bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
-    if( n.getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr( n ) ){
+    if( n.getKind()!=BOUND_VARIABLE && TermDb::hasBoundVarAttr( n ) ){
       if( !inst::Trigger::isCbqiKind( n.getKind() ) ){
         Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n  << std::endl;
         return true;
       }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){
         Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl;
         return true;
+      }else if( n.getKind()==FORALL ){
+        return hasNonCbqiOperator( n[1], visited );
       }else{
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           if( hasNonCbqiOperator( n[i], visited ) ){
@@ -220,9 +222,9 @@ bool InstStrategyCbqi::doCbqi( Node q ){
         }else{
           //if quantifier has a non-arithmetic variable, then do not use cbqi
           //if quantifier has an APPLY_UF term, then do not use cbqi
-          Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+          //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
           std::map< Node, bool > visited;
-          ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+          ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( q[1], visited );
         }
       }
     }
diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index 794032c87..86fbdc7f7 100644
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file quant_util.cpp
+/*! \file local_theory_ext.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: none
@@ -31,69 +31,69 @@ QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){
 }
 
 /** add quantifier */
-bool LtePartialInst::addQuantifier( Node q ) {
-  if( d_do_inst.find( q )!=d_do_inst.end() ){
-    if( d_do_inst[q] ){
-      d_lte_asserts.push_back( q );
-      return true;
+void LtePartialInst::preRegisterQuantifier( Node q ) {
+  if( !q.getAttribute(LtePartialInstAttribute()) ){
+    if( d_do_inst.find( q )!=d_do_inst.end() ){
+      if( d_do_inst[q] ){
+        d_lte_asserts.push_back( q );
+        d_quantEngine->setOwner( q, this );
+      }
     }else{
-      return false;
-    }
-  }else{
-    d_vars[q].clear();
-    d_pat_var_order[q].clear();
-    //check if this quantified formula is eligible for partial instantiation
-    std::map< Node, bool > vars;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      vars[q[0][i]] = false;
-    }
-    getEligibleInstVars( q[1], vars );
-
-    //instantiate only if we would force ground instances
-    std::map< Node, int > var_order;
-    bool doInst = true;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      if( vars[q[0][i]] ){
-        d_vars[q].push_back( q[0][i] );
-        var_order[q[0][i]] = i;
-      }else{
-        Trace("lte-partial-inst-debug") << "...do not consider, variable " << q[0][i] << " was not found in correct position in body." << std::endl;
-        doInst = false;
-        break;
+      d_vars[q].clear();
+      d_pat_var_order[q].clear();
+      //check if this quantified formula is eligible for partial instantiation
+      std::map< Node, bool > vars;
+      for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+        vars[q[0][i]] = false;
       }
-    }
-    if( doInst ){
-      //also needs patterns
-      if( q.getNumChildren()==3 && q[2].getNumChildren()==1 ){
-        for( unsigned i=0; i<q[2][0].getNumChildren(); i++ ){
-          Node pat = q[2][0][i];
-          if( pat.getKind()==APPLY_UF ){
-            for( unsigned j=0; j<pat.getNumChildren(); j++ ){
-              if( !addVariableToPatternList( pat[j], d_pat_var_order[q], var_order ) ){
-                doInst = false;
+      getEligibleInstVars( q[1], vars );
+
+      //instantiate only if we would force ground instances
+      std::map< Node, int > var_order;
+      bool doInst = true;
+      for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+        if( vars[q[0][i]] ){
+          d_vars[q].push_back( q[0][i] );
+          var_order[q[0][i]] = i;
+        }else{
+          Trace("lte-partial-inst-debug") << "...do not consider, variable " << q[0][i] << " was not found in correct position in body." << std::endl;
+          doInst = false;
+          break;
+        }
+      }
+      if( doInst ){
+        //also needs patterns
+        if( q.getNumChildren()==3 && q[2].getNumChildren()==1 ){
+          for( unsigned i=0; i<q[2][0].getNumChildren(); i++ ){
+            Node pat = q[2][0][i];
+            if( pat.getKind()==APPLY_UF ){
+              for( unsigned j=0; j<pat.getNumChildren(); j++ ){
+                if( !addVariableToPatternList( pat[j], d_pat_var_order[q], var_order ) ){
+                  doInst = false;
+                }
               }
+            }else if( !addVariableToPatternList( pat, d_pat_var_order[q], var_order ) ){
+              doInst = false;
+            }
+            if( !doInst ){
+              Trace("lte-partial-inst-debug") << "...do not consider, cannot resolve pattern : " << pat << std::endl;
+              break;
             }
-          }else if( !addVariableToPatternList( pat, d_pat_var_order[q], var_order ) ){
-            doInst = false;
-          }
-          if( !doInst ){
-            Trace("lte-partial-inst-debug") << "...do not consider, cannot resolve pattern : " << pat << std::endl;
-            break;
           }
+        }else{
+          Trace("lte-partial-inst-debug") << "...do not consider (must have exactly one pattern)." << std::endl;
         }
-      }else{
-        Trace("lte-partial-inst-debug") << "...do not consider (must have exactly one pattern)." << std::endl;
+      }
+      
+      
+      Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl;
+      d_do_inst[q] = doInst;
+      if( doInst ){
+        d_lte_asserts.push_back( q );
+        d_needsCheck = true;
+        d_quantEngine->setOwner( q, this );
       }
     }
-    
-    
-    Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl;
-    d_do_inst[q] = doInst;
-    if( doInst ){
-      d_lte_asserts.push_back( q );
-      d_needsCheck = true;
-    }
-    return doInst;
   }
 }
 
@@ -188,7 +188,6 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) {
       Assert( !conj.empty() );
       lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) );
       d_wasInvoked = true;
-      d_quantEngine->getModel()->markQuantifierReduced( q );
     }
   }
 }
diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 6e2ee34af..d802c2cf7 100644
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -55,8 +55,8 @@ private:
   bool addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order );
 public:
   LtePartialInst( QuantifiersEngine * qe, context::Context* c );
-  /** add quantifier : special form of registration */
-  bool addQuantifier( Node q );
+  /** determine whether this quantified formula will be reduced */
+  void preRegisterQuantifier( Node q );
   /** was invoked */
   bool wasInvoked() { return d_wasInvoked; }
   
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
new file mode 100644
index 000000000..e874ee5b8
--- /dev/null
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -0,0 +1,129 @@
+/*********************                                                        */
+/*! \file quant_split.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of local theory ext utilities
+ **/
+
+#include "theory/quantifiers/quant_split.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "options/quantifiers_options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+
+QuantDSplit::QuantDSplit( QuantifiersEngine * qe, context::Context* c ) :
+QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){
+
+}
+
+/** pre register quantifier */
+void QuantDSplit::preRegisterQuantifier( Node q ) {
+  int max_index = -1;
+  int max_score = -1;
+  if( q.getNumChildren()==3 ){
+    return;
+  }
+  Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    TypeNode tn = q[0][i].getType();
+    if( tn.isDatatype() ){
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      if( dt.isRecursiveSingleton() ){
+        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
+      }else{
+        int score = -1;
+        if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
+          score = dt.isFinite() ? 1 : -1;
+        }else if(  options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
+          score = dt.isUFinite() ? 1 : -1;
+        }
+        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << std::endl;
+        if( score>max_score ){
+          max_index = i;
+          max_score = score;
+        }
+      }
+    }
+  }
+
+  if( max_index!=-1 ){
+    Trace("quant-dsplit-debug") << "Will split at index " << max_index << "." << std::endl;
+    d_quant_to_reduce[q] = max_index;
+    d_quantEngine->setOwner( q, this );
+  }
+}
+
+/* whether this module needs to check this round */
+bool QuantDSplit::needsCheck( Theory::Effort e ) {
+  return e>=Theory::EFFORT_FULL;
+}
+/* Call during quantifier engine's check */
+void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
+  //flush lemmas ASAP (they are a reduction)
+  if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
+    std::vector< Node > lemmas;
+    for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) {
+      Node q = it->first;
+      if( d_added_split.find( q )==d_added_split.end() ){
+        d_added_split.insert( q );
+        std::vector< Node > bvs;
+        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+          if( (int)i!=it->second ){
+            bvs.push_back( q[0][i] );
+          }
+        }
+        std::vector< Node > disj;
+        disj.push_back( q.negate() );
+        TNode svar = q[0][it->second];
+        TypeNode tn = svar.getType();
+        if( tn.isDatatype() ){
+          const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+          for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
+            std::vector< Node > vars;
+            for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
+              TypeNode tns = TypeNode::fromType( dt[j][k].getRangeType() );
+              Node v = NodeManager::currentNM()->mkBoundVar( tns );
+              vars.push_back( v );
+            }
+            std::vector< Node > bvs_cmb;
+            bvs_cmb.insert( bvs_cmb.end(), bvs.begin(), bvs.end() );
+            bvs_cmb.insert( bvs_cmb.end(), vars.begin(), vars.end() );
+            vars.insert( vars.begin(), Node::fromExpr( dt[j].getConstructor() ) );
+            Node c = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, vars );
+            TNode ct = c;
+            Node body = q[1].substitute( svar, ct );
+            if( !bvs_cmb.empty() ){
+              body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body );
+            }
+            disj.push_back( body );
+          }
+        }else{
+          Assert( false );
+        }
+        lemmas.push_back( disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ) );
+      }
+    }
+
+    //add lemmas to quantifiers engine
+    for( unsigned i=0; i<lemmas.size(); i++ ){
+      Trace("quant-dsplit") << "QuantDSplit lemma : " << lemmas[i] << std::endl;
+      d_quantEngine->addLemma( lemmas[i], false );
+    }
+  }
+}
+
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
new file mode 100644
index 000000000..f40acc2fd
--- /dev/null
+++ b/src/theory/quantifiers/quant_split.h
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file quant_split.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief dynamic quantifiers splitting
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANT_SPLIT_H
+#define __CVC4__THEORY__QUANT_SPLIT_H
+
+#include "theory/quantifiers_engine.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantDSplit : public QuantifiersModule {
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+private:
+  /** list of relevant quantifiers asserted in the current context */
+  std::map< Node, int > d_quant_to_reduce;
+  /** whether we have instantiated quantified formulas */
+  NodeSet d_added_split;
+public:
+  QuantDSplit( QuantifiersEngine * qe, context::Context* c );
+  /** determine whether this quantified formula will be reduced */
+  void preRegisterQuantifier( Node q );
+  
+  /* whether this module needs to check this round */
+  bool needsCheck( Theory::Effort e );
+  /* Call during quantifier engine's check */
+  void check( Theory::Effort e, unsigned quant_e );
+  /* Called for new quantifiers */
+  void registerQuantifier( Node q ) {}
+  void assertNode( Node n ) {}
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const { return "QuantDSplit"; }
+};
+
+}
+}
+}
+
+#endif