Squash implementation of counterexample-guided instantiation (#2423)

2 files changed, 208 insertions, 170 deletions

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index ac76ee31f..9b82c1f4b 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -34,28 +34,58 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
-using namespace CVC4::theory::arith;
 
-#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
+bool CegqiOutputInstStrategy::doAddInstantiation(std::vector<Node>& subs)
+{
+  return d_out->doAddInstantiation(subs);
+}
+
+bool CegqiOutputInstStrategy::isEligibleForInstantiation(Node n)
+{
+  return d_out->isEligibleForInstantiation(n);
+}
 
-InstStrategyCbqi::InstStrategyCbqi(QuantifiersEngine* qe)
+bool CegqiOutputInstStrategy::addLemma(Node lem)
+{
+  return d_out->addLemma(lem);
+}
+
+InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
     : QuantifiersModule(qe),
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
       d_added_cbqi_lemma(qe->getUserContext()),
       d_elim_quants(qe->getSatContext()),
+      d_out(new CegqiOutputInstStrategy(this)),
       d_nested_qe_waitlist_size(qe->getUserContext()),
       d_nested_qe_waitlist_proc(qe->getUserContext())
 //, d_added_inst( qe->getUserContext() )
 {
   d_qid_count = 0;
+  d_small_const =
+      NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000));
+  d_check_vts_lemma_lc = false;
+}
+
+InstStrategyCegqi::~InstStrategyCegqi()
+{
+  for (std::map<Node, CegInstantiator*>::iterator i = d_cinst.begin(),
+                                                  iend = d_cinst.end();
+       i != iend;
+       ++i)
+  {
+    CegInstantiator* instantiator = (*i).second;
+    delete instantiator;
+  }
+  d_cinst.clear();
 }
 
-bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
+bool InstStrategyCegqi::needsCheck(Theory::Effort e)
+{
   return e>=Theory::EFFORT_LAST_CALL;
 }
 
-QuantifiersModule::QEffort InstStrategyCbqi::needsModel(Theory::Effort e)
+QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e)
 {
   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
@@ -66,7 +96,8 @@ QuantifiersModule::QEffort InstStrategyCbqi::needsModel(Theory::Effort e)
   return QEFFORT_NONE;
 }
 
-bool InstStrategyCbqi::registerCbqiLemma( Node q ) {
+bool InstStrategyCegqi::registerCbqiLemma(Node q)
+{
   if( !hasAddedCbqiLemma( q ) ){
     d_added_cbqi_lemma.insert( q );
     Trace("cbqi-debug") << "Do cbqi for " << q << std::endl;
@@ -164,7 +195,8 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) {
   }
 }
 
-void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
+void InstStrategyCegqi::reset_round(Theory::Effort effort)
+{
   d_cbqi_set_quant_inactive = false;
   d_incomplete_check = false;
   d_active_quant.clear();
@@ -238,11 +270,10 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
       Trace("cbqi-debug") << "...done removing." << std::endl;
     }
   }
-  
-  processResetInstantiationRound( effort );
+  d_check_vts_lemma_lc = false;
 }
 
-void InstStrategyCbqi::check(Theory::Effort e, QEffort quant_e)
+void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
 {
   if (quant_e == QEFFORT_STANDARD)
   {
@@ -284,7 +315,8 @@ void InstStrategyCbqi::check(Theory::Effort e, QEffort quant_e)
   }
 }
 
-bool InstStrategyCbqi::checkComplete() {
+bool InstStrategyCegqi::checkComplete()
+{
   if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
     return false;
   }else{
@@ -292,7 +324,8 @@ bool InstStrategyCbqi::checkComplete() {
   }
 }
 
-bool InstStrategyCbqi::checkCompleteFor( Node q ) {
+bool InstStrategyCegqi::checkCompleteFor(Node q)
+{
   std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
   if( it!=d_do_cbqi.end() ){
     return it->second != CEG_UNHANDLED;
@@ -301,7 +334,9 @@ bool InstStrategyCbqi::checkCompleteFor( Node q ) {
   }
 }
 
-Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){
+Node InstStrategyCegqi::getIdMarkedQuantNode(Node n,
+                                             std::map<Node, Node>& visited)
+{
   std::map< Node, Node >::iterator it = visited.find( n );
   if( it==visited.end() ){
     Node ret = n;
@@ -348,7 +383,7 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis
   }
 }
 
-void InstStrategyCbqi::checkOwnership(Node q)
+void InstStrategyCegqi::checkOwnership(Node q)
 {
   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
     if (d_do_cbqi[q] == CEG_HANDLED)
@@ -359,7 +394,7 @@ void InstStrategyCbqi::checkOwnership(Node q)
   }
 }
 
-void InstStrategyCbqi::preRegisterQuantifier(Node q)
+void InstStrategyCegqi::preRegisterQuantifier(Node q)
 {
   // mark all nested quantifiers with id
   if (options::cbqiNestedQE())
@@ -389,13 +424,21 @@ void InstStrategyCbqi::preRegisterQuantifier(Node q)
     }
   }
   if( doCbqi( q ) ){
+    // get the instantiator
+    if (options::cbqiPreRegInst())
+    {
+      getInstantiator(q);
+    }
+    // register the cbqi lemma
     if( registerCbqiLemma( q ) ){
       Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
     }
   }
 }
 
-Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) {
+Node InstStrategyCegqi::doNestedQENode(
+    Node q, Node ceq, Node n, std::vector<Node>& inst_terms, bool doVts)
+{
   // there is a nested quantified formula (forall y. nq[y,x]) such that 
   //    q is (forall y. nq[y,t]) for ground terms t,
   //    ceq is (forall y. nq[y,e]) for CE variables e.
@@ -425,7 +468,12 @@ Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< No
   return ret;
 }
 
-Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) {
+Node InstStrategyCegqi::doNestedQERec(Node q,
+                                      Node n,
+                                      std::map<Node, Node>& visited,
+                                      std::vector<Node>& inst_terms,
+                                      bool doVts)
+{
   if( visited.find( n )==visited.end() ){
     Node ret = n;
     if( n.getKind()==FORALL ){
@@ -482,17 +530,40 @@ Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& vi
   }  
 }
 
-Node InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) {
+Node InstStrategyCegqi::doNestedQE(Node q,
+                                   std::vector<Node>& inst_terms,
+                                   Node lem,
+                                   bool doVts)
+{
   std::map< Node, Node > visited;
   return doNestedQERec( q, lem, visited, inst_terms, doVts );
 }
 
-void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
-  Trace("cbqi-debug") << "Counterexample lemma  : " << lem << std::endl;
-  d_quantEngine->addLemma( lem, false );
+void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
+{
+  // must register with the instantiator
+  // must explicitly remove ITEs so that we record dependencies
+  std::vector<Node> ce_vars;
+  TermUtil* tutil = d_quantEngine->getTermUtil();
+  for (unsigned i = 0, nics = tutil->getNumInstantiationConstants(q); i < nics;
+       i++)
+  {
+    ce_vars.push_back(tutil->getInstantiationConstant(q, i));
+  }
+  std::vector<Node> lems;
+  lems.push_back(lem);
+  CegInstantiator* cinst = getInstantiator(q);
+  cinst->registerCounterexampleLemma(lems, ce_vars);
+  for (unsigned i = 0, size = lems.size(); i < size; i++)
+  {
+    Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i]
+                        << std::endl;
+    d_quantEngine->addLemma(lems[i], false);
+  }
 }
 
-bool InstStrategyCbqi::doCbqi( Node q ){
+bool InstStrategyCegqi::doCbqi(Node q)
+{
   std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
   if( it==d_do_cbqi.end() ){
     CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine);
@@ -503,7 +574,9 @@ bool InstStrategyCbqi::doCbqi( Node q ){
   return it->second != CEG_UNHANDLED;
 }
 
-Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) {
+Node InstStrategyCegqi::getNextDecisionRequestProc(Node q,
+                                                   std::map<Node, bool>& proc)
+{
   if( proc.find( q )==proc.end() ){
     proc[q] = true;
     //first check children
@@ -529,7 +602,8 @@ Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool
   return Node::null(); 
 }
 
-Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){
+Node InstStrategyCegqi::getNextDecisionRequest(unsigned& priority)
+{
   std::map< Node, bool > proc;
   //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
   //  Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
@@ -544,46 +618,6 @@ Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){
   return Node::null();
 }
 
-
-
-//new implementation
-
-bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) {
-  return d_out->doAddInstantiation( subs );
-}
-
-bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) {
-  return d_out->isEligibleForInstantiation( n );
-}
-
-bool CegqiOutputInstStrategy::addLemma( Node lem ) {
-  return d_out->addLemma( lem );
-}
-
-
-InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe )
-  : InstStrategyCbqi( qe ) {
-  d_out = new CegqiOutputInstStrategy( this );
-  d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
-  d_check_vts_lemma_lc = false;
-}
-
-InstStrategyCegqi::~InstStrategyCegqi()
-{
-  delete d_out;
-
-  for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(),
-          iend = d_cinst.end(); i != iend; ++i) {
-    CegInstantiator * instantiator = (*i).second;
-    delete instantiator;
-  }
-  d_cinst.clear();
-}
-
-void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
-  d_check_vts_lemma_lc = false;
-}
-
 void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
   if( e==0 ){
     CegInstantiator * cinst = getInstantiator( q );
@@ -676,7 +710,8 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
 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 );
+    CegInstantiator* cinst =
+        new CegInstantiator(d_quantEngine, d_out.get(), true, true);
     d_cinst[q] = cinst;
     return cinst;
   }else{
@@ -684,37 +719,6 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   }
 }
 
-void InstStrategyCegqi::preRegisterQuantifier(Node q)
-{
-  if( doCbqi( q ) ){
-    // get the instantiator  
-    if( options::cbqiPreRegInst() ){
-      getInstantiator( q );
-    }
-    // register the cbqi lemma
-    if( registerCbqiLemma( q ) ){
-      Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
-    }
-  }
-}
-
-void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) {
-  //must register with the instantiator
-  //must explicitly remove ITEs so that we record dependencies
-  std::vector< Node > ce_vars;
-  for( unsigned i=0; i<d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ); i++ ){
-    ce_vars.push_back( d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ) );
-  }
-  std::vector< Node > lems;
-  lems.push_back( lem );
-  CegInstantiator * cinst = getInstantiator( q );
-  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 );
-  }
-}
-
 void InstStrategyCegqi::presolve() {
   if( options::cbqiPreRegInst() ){
     for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
index 4334652da..433de52a8 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
@@ -18,24 +18,90 @@
 #ifndef __CVC4__INST_STRATEGY_CBQI_H
 #define __CVC4__INST_STRATEGY_CBQI_H
 
-#include "theory/arith/arithvar.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
-#include "theory/quantifiers/ematching/instantiation_engine.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 
-namespace arith {
-  class TheoryArith;
-}
+class InstStrategyCegqi;
 
-namespace quantifiers {
+/**
+ * An output channel class, used by instantiator objects below. The methods
+ * of this class call the corresponding functions of InstStrategyCegqi below.
+ */
+class CegqiOutputInstStrategy : public CegqiOutput
+{
+ public:
+  CegqiOutputInstStrategy(InstStrategyCegqi* out) : d_out(out) {}
+  /** The module whose functions we call. */
+  InstStrategyCegqi* d_out;
+  /** add instantiation */
+  bool doAddInstantiation(std::vector<Node>& subs) override;
+  /** is eligible for instantiation */
+  bool isEligibleForInstantiation(Node n) override;
+  /** add lemma */
+  bool addLemma(Node lem) override;
+};
 
-class InstStrategyCbqi : public QuantifiersModule {
+/**
+ * Counterexample-guided quantifier instantiation module.
+ *
+ * This class manages counterexample-guided instantiation strategies for all
+ * asserted quantified formulas.
+ */
+class InstStrategyCegqi : public QuantifiersModule
+{
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
 
+ public:
+  InstStrategyCegqi(QuantifiersEngine* qe);
+  ~InstStrategyCegqi();
+
+  /** whether to do counterexample-guided instantiation for quantifier q */
+  bool doCbqi(Node q);
+  /** needs check at effort */
+  bool needsCheck(Theory::Effort e) override;
+  /** needs model at effort */
+  QEffort needsModel(Theory::Effort e) override;
+  /** reset round */
+  void reset_round(Theory::Effort e) override;
+  /** check */
+  void check(Theory::Effort e, QEffort quant_e) override;
+  /** check complete */
+  bool checkComplete() override;
+  /** check complete for quantified formula */
+  bool checkCompleteFor(Node q) override;
+  /** check ownership */
+  void checkOwnership(Node q) override;
+  /** identify */
+  std::string identify() const override { return std::string("Cegqi"); }
+  /** get instantiator for quantifier */
+  CegInstantiator* getInstantiator(Node q);
+  /** pre-register quantifier */
+  void preRegisterQuantifier(Node q) override;
+  // presolve
+  void presolve() override;
+  /** get next decision request */
+  Node getNextDecisionRequest(unsigned& priority) override;
+  /** Do nested quantifier elimination. */
+  Node doNestedQE(Node q, std::vector<Node>& inst_terms, Node lem, bool doVts);
+
+  //------------------- interface for CegqiOutputInstStrategy
+  /** Instantiate the current quantified formula forall x. Q with x -> subs. */
+  bool doAddInstantiation(std::vector<Node>& subs);
+  /**
+   * Are we allowed to instantiate the current quantified formula with n? This
+   * includes restrictions such as if n is a variable, it must occur free in
+   * the current quantified formula.
+   */
+  bool isEligibleForInstantiation(Node n);
+  /** Add lemma lem via the output channel of this class. */
+  bool addLemma(Node lem);
+  //------------------- end interface for CegqiOutputInstStrategy
+
  protected:
   /** set quantified formula inactive
    *
@@ -60,18 +126,49 @@ class InstStrategyCbqi : public QuantifiersModule {
   std::map< Node, bool > d_active_quant;
   /** Whether cegqi handles each quantified formula. */
   std::map<Node, CegHandledStatus> d_do_cbqi;
+  /**
+   * An output channel used by instantiators for communicating with this
+   * class.
+   */
+  std::unique_ptr<CegqiOutputInstStrategy> d_out;
+  /**
+   * The instantiator for each quantified formula q registered to this class.
+   * This object is responsible for finding instantiatons for q.
+   */
+  std::map<Node, CegInstantiator*> d_cinst;
+  /** the current quantified formula we are processing */
+  Node d_curr_quant;
+  //---------------------- for vts delta minimization
+  /**
+   * Whether we will use vts delta minimization. If this flag is true, we
+   * add lemmas on demand of the form delta < c^1, delta < c^2, ... where c
+   * is a small (< 1) constant. This heuristic is used in strategies where
+   * vts delta cannot be fully eliminated from assertions (for example, when
+   * using nested quantifiers and a non-innermost instantiation strategy).
+   * The same strategy applies for vts infinity, which we add lemmas of the
+   * form inf > (1/c)^1, inf > (1/c)^2, ....
+   */
+  bool d_check_vts_lemma_lc;
+  /** a small constant, used as a coefficient above */
+  Node d_small_const;
+  //---------------------- end for vts delta minimization
   /** register ce lemma */
   bool registerCbqiLemma( Node q );
-  virtual void registerCounterexampleLemma( Node q, Node lem );
+  /** register counterexample lemma
+   *
+   * This is called when we have constructed lem, the negation of the body of
+   * quantified formula q, skolemized with the instantiation constants of q.
+   * This function is used for setting up the proper information in the
+   * instantiator for q.
+   */
+  void registerCounterexampleLemma(Node q, Node lem);
   /** has added cbqi lemma */
   bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
   /** get next decision request with dependency checking */
   Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc );  
   /** process functions */
-  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
-  virtual void process( Node q, Theory::Effort effort, int e ) = 0;
+  void process(Node q, Theory::Effort effort, int e);
 
- protected:
   //for identification
   uint64_t d_qid_count;
   //nested qe map
@@ -98,71 +195,8 @@ class InstStrategyCbqi : public QuantifiersModule {
   NodeIntMap d_nested_qe_waitlist_proc;
   std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
 
- public:
-  //do nested quantifier elimination
-  Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts );
-
- public:
-  InstStrategyCbqi( QuantifiersEngine * qe );
-
-  /** whether to do CBQI for quantifier q */
-  bool doCbqi( Node q );
-  /** process functions */
-  bool needsCheck(Theory::Effort e) override;
-  QEffort needsModel(Theory::Effort e) override;
-  void reset_round(Theory::Effort e) override;
-  void check(Theory::Effort e, QEffort quant_e) override;
-  bool checkComplete() override;
-  bool checkCompleteFor(Node q) override;
-  void checkOwnership(Node q) override;
-  void preRegisterQuantifier(Node q) override;
-  /** get next decision request */
-  Node getNextDecisionRequest(unsigned& priority) override;
 };
 
-//generalized counterexample guided quantifier instantiation
-
-class InstStrategyCegqi;
-
-class CegqiOutputInstStrategy : public CegqiOutput {
-public:
-  CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
-  InstStrategyCegqi * d_out;
-  bool doAddInstantiation(std::vector<Node>& subs) override;
-  bool isEligibleForInstantiation(Node n) override;
-  bool addLemma(Node lem) override;
-};
-
-class InstStrategyCegqi : public InstStrategyCbqi {
- protected:
-  CegqiOutputInstStrategy * d_out;
-  std::map< Node, CegInstantiator * > d_cinst;
-  Node d_small_const;
-  Node d_curr_quant;
-  bool d_check_vts_lemma_lc;
-  /** process functions */
-  void processResetInstantiationRound(Theory::Effort effort) override;
-  void process(Node f, Theory::Effort effort, int e) override;
-  /** register ce lemma */
-  void registerCounterexampleLemma(Node q, Node lem) override;
-
- public:
-  InstStrategyCegqi( QuantifiersEngine * qe );
-  ~InstStrategyCegqi() override;
-
-  bool doAddInstantiation( std::vector< Node >& subs );
-  bool isEligibleForInstantiation( Node n );
-  bool addLemma( Node lem );
-  /** identify */
-  std::string identify() const override { return std::string("Cegqi"); }
-
-  //get instantiator for quantifier
-  CegInstantiator * getInstantiator( Node q );
-  /** pre-register quantifier */
-  void preRegisterQuantifier(Node q) override;
-  //presolve
-  void presolve() override;
-};
 
 }
 }