Use quantifiers inference manager for lemma management (#5867)

[cvc5.git] / src / theory / quantifiers / fmf / bounded_integers.cpp

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 2bcb154a05551eda692729afc5e0daada929c55e..0a0d155f9e937f3ae48d4c0018023c179ea81fcf 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -2,10 +2,10 @@
 /*! \file bounded_integers.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Andres Noetzli, Tim King
+ **   Andrew Reynolds, Andres Noetzli, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -84,8 +84,11 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
   return lem;
 }
 
-BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe)
-    : QuantifiersModule(qe)
+BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe,
+                                 QuantifiersState& qs,
+                                 QuantifiersInferenceManager& qim,
+                                 QuantifiersRegistry& qr)
+    : QuantifiersModule(qs, qim, qr, qe)
 {
 }
 
@@ -291,7 +294,7 @@ void BoundedIntegers::check(Theory::Effort e, QEffort quant_e)
     {
       Trace("bound-int-lemma")
           << "*** bound int : proxy lemma : " << prangeLem << std::endl;
-      d_quantEngine->addLemma(prangeLem);
+      d_qim.addPendingLemma(prangeLem);
       addedLemma = true;
     }
   }
@@ -437,11 +440,13 @@ void BoundedIntegers::checkOwnership(Node f)
           }
         }else if( d_bound_type[f][v]==BOUND_FIXED_SET ){
           Trace("bound-int") << "  " << v << " in { ";
-          for( unsigned i=0; i<d_fixed_set_ngr_range[f][v].size(); i++ ){ 
-            Trace("bound-int") << d_fixed_set_ngr_range[f][v][i] << " ";
+          for (TNode fnr : d_fixed_set_ngr_range[f][v])
+          {
+            Trace("bound-int") << fnr << " ";
           }
-          for( unsigned i=0; i<d_fixed_set_gr_range[f][v].size(); i++ ){ 
-            Trace("bound-int") << d_fixed_set_gr_range[f][v][i] << " ";
+          for (TNode fgr : d_fixed_set_gr_range[f][v])
+          {
+            Trace("bound-int") << fgr << " ";
           }
           Trace("bound-int") << "}" << std::endl;
         }else if( d_bound_type[f][v]==BOUND_FINITE ){
@@ -491,8 +496,8 @@ void BoundedIntegers::checkOwnership(Node f)
             d_ranges.push_back( r );
             d_rms[r].reset(
                 new IntRangeDecisionHeuristic(r,
-                                              d_quantEngine->getSatContext(),
-                                              d_quantEngine->getUserContext(),
+                                              d_qstate.getSatContext(),
+                                              d_qstate.getUserContext(),
                                               d_quantEngine->getValuation(),
                                               isProxy));
             d_quantEngine->getTheoryEngine()
@@ -668,13 +673,13 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
       choices.pop_back();
       Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i);
       Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConst(Rational(i)));
-      choice_i = nm->mkNode(CHOICE, bvl, nm->mkNode(OR, cMinCard, cBody));
+      choice_i = nm->mkNode(WITNESS, bvl, nm->mkNode(OR, cMinCard, cBody));
       d_setm_choice[sro].push_back(choice_i);
     }
     Assert(i < d_setm_choice[sro].size());
     choice_i = d_setm_choice[sro][i];
     choices.push_back(choice_i);
-    Node sChoiceI = nm->mkNode(SINGLETON, choice_i);
+    Node sChoiceI = nm->mkSingleton(choice_i.getType(), choice_i);
     if (nsr.isNull())
     {
       nsr = sChoiceI;
@@ -688,8 +693,8 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
   //   e.g.
   // singleton(0) union singleton(1)
   //   becomes
-  // C1 union ( choice y. card(S)<=1 OR ( y in S AND distinct( y, C1 ) ) )
-  // where C1 = ( choice x. card(S)<=0 OR x in S ).
+  // C1 union ( witness y. card(S)<=1 OR ( y in S AND distinct( y, C1 ) ) )
+  // where C1 = ( witness x. card(S)<=0 OR x in S ).
   Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl;
   return nsr;
 }
@@ -705,9 +710,9 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
   for( int i=0; i<vindex; i++) {
     Assert(d_set_nums[q][d_set[q][i]] == i);
     Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
-    int v = rsi->getVariableOrder( i );
-    Assert(q[0][v] == d_set[q][i]);
-    Node t = rsi->getCurrentTerm(v, true);
+    int vo = rsi->getVariableOrder(i);
+    Assert(q[0][vo] == d_set[q][i]);
+    Node t = rsi->getCurrentTerm(vo, true);
     Trace("bound-int-rsi") << "term : " << t << std::endl;
     vars.push_back( d_set[q][i] );
     subs.push_back( t );
@@ -721,7 +726,7 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
       nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
       Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] );
       Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
-      d_quantEngine->getOutputChannel().lemma(lem, false, true);
+      d_quantEngine->getOutputChannel().lemma(lem);
     }
     return false;
   }else{