Fill in missing inference ids in datatypes theory (#5931)

Also updates its inference manager to not track stats since the standard ones are now used.

This also sets up some dependencies in the sygus extension which will be used to implement InferenceId for the sygus extension, to be done on a separate PR.

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index cf93009bb57b97dd130bd2f9de64748a5ccf2c29..8c12258afba571d169044387053b4cb55c0a78ed 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -29,9 +29,6 @@ InferenceManager::InferenceManager(Theory& t,
                                    TheoryState& state,
                                    ProofNodeManager* pnm)
     : InferenceManagerBuffered(t, state, pnm, "theory::datatypes"),
-      d_inferenceLemmas("theory::datatypes::inferenceLemmas"),
-      d_inferenceFacts("theory::datatypes::inferenceFacts"),
-      d_inferenceConflicts("theory::datatypes::inferenceConflicts"),
       d_pnm(pnm),
       d_ipc(pnm == nullptr ? nullptr
                            : new InferProofCons(state.getSatContext(), pnm)),
@@ -41,33 +38,27 @@ InferenceManager::InferenceManager(Theory& t,
                       pnm, state.getUserContext(), "datatypes::lemPg"))
 {
   d_false = NodeManager::currentNM()->mkConst(false);
-  smtStatisticsRegistry()->registerStat(&d_inferenceLemmas);
-  smtStatisticsRegistry()->registerStat(&d_inferenceFacts);
-  smtStatisticsRegistry()->registerStat(&d_inferenceConflicts);
 }
 
 InferenceManager::~InferenceManager()
 {
-  smtStatisticsRegistry()->unregisterStat(&d_inferenceLemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_inferenceFacts);
-  smtStatisticsRegistry()->unregisterStat(&d_inferenceConflicts);
 }
 
 void InferenceManager::addPendingInference(Node conc,
+                                           InferenceId id,
                                            Node exp,
-                                           bool forceLemma,
-                                           InferenceId i)
+                                           bool forceLemma)
 {
   // if we are forcing the inference to be processed as a lemma, or if the
   // inference must be sent as a lemma based on the policy in
   // mustCommunicateFact.
   if (forceLemma || DatatypesInference::mustCommunicateFact(conc, exp))
   {
-    d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, i));
+    d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, id));
   }
   else
   {
-    d_pendingFact.emplace_back(new DatatypesInference(this, conc, exp, i));
+    d_pendingFact.emplace_back(new DatatypesInference(this, conc, exp, id));
   }
 }
 
@@ -87,10 +78,7 @@ void InferenceManager::sendDtLemma(Node lem, InferenceId id, LemmaProperty p)
     return;
   }
   // otherwise send as a normal lemma
-  if (lemma(lem, id, p))
-  {
-    d_inferenceLemmas << id;
-  }
+  lemma(lem, id, p);
 }
 
 void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId id)
@@ -101,15 +89,15 @@ void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId
     prepareDtInference(d_false, exp, id, d_ipc.get());
   }
   conflictExp(id, conf, d_ipc.get());
-  d_inferenceConflicts << id;
 }
 
-bool InferenceManager::sendLemmas(const std::vector<Node>& lemmas)
+bool InferenceManager::sendLemmas(const std::vector<Node>& lemmas,
+                                  InferenceId id)
 {
   bool ret = false;
   for (const Node& lem : lemmas)
   {
-    if (lemma(lem, InferenceId::UNKNOWN))
+    if (lemma(lem, id))
     {
       ret = true;
     }
@@ -151,7 +139,6 @@ TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id)
     }
     d_lemPg->setProofFor(lem, pn);
   }
-  // use trusted lemma
   return TrustNode::mkTrustLemma(lem, d_lemPg.get());
 }
 

diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h
index 9c9a2bcb5fa2827c07903e34b3aa1ee61ba7ba03..ba46d2a423a4b23acf4f66afb1d9adbf03f76f99 100644 (file)
--- a/src/theory/datatypes/inference_manager.h
+++ b/src/theory/datatypes/inference_manager.h
@@ -22,7 +22,6 @@
 #include "theory/datatypes/infer_proof_cons.h"
 #include "theory/datatypes/inference.h"
 #include "theory/inference_manager_buffered.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -45,16 +44,16 @@ class InferenceManager : public InferenceManagerBuffered
    *
    * @param conc The conclusion of the inference
    * @param exp The explanation of the inference
+   * @param id The inference, used for stats and as a hint for constructing
+   * the proof of (conc => exp)
    * @param forceLemma Whether this inference *must* be processed as a lemma.
    * Otherwise, it may be processed as a fact or lemma based on
    * mustCommunicateFact.
-   * @param i The inference, used for stats and as a hint for constructing
-   * the proof of (conc => exp)
    */
   void addPendingInference(Node conc,
+                           InferenceId id,
                            Node exp,
-                           bool forceLemma = false,
-                           InferenceId i = InferenceId::UNKNOWN);
+                           bool forceLemma = false);
   /**
    * Process the current lemmas and facts. This is a custom method that can
    * be seen as overriding the behavior of calling both doPendingLemmas and
@@ -66,17 +65,17 @@ class InferenceManager : public InferenceManagerBuffered
    * Send lemma immediately on the output channel
    */
   void sendDtLemma(Node lem,
-                   InferenceId i = InferenceId::UNKNOWN,
+                   InferenceId id,
                    LemmaProperty p = LemmaProperty::NONE);
   /**
    * Send conflict immediately on the output channel
    */
-  void sendDtConflict(const std::vector<Node>& conf, InferenceId i = InferenceId::UNKNOWN);
+  void sendDtConflict(const std::vector<Node>& conf, InferenceId id);
   /**
    * Send lemmas with property NONE on the output channel immediately.
    * Returns true if any lemma was sent.
    */
-  bool sendLemmas(const std::vector<Node>& lemmas);
+  bool sendLemmas(const std::vector<Node>& lemmas, InferenceId id);
 
  private:
   /** Are proofs enabled? */
@@ -104,13 +103,6 @@ class InferenceManager : public InferenceManagerBuffered
   Node prepareDtInference(Node conc, Node exp, InferenceId id, InferProofCons* ipc);
   /** The false node */
   Node d_false;
-  /**
-   * Counts the number of applications of each type of inference processed by
-   * the above method as facts, lemmas and conflicts.
-   */
-  HistogramStat<InferenceId> d_inferenceLemmas;
-  HistogramStat<InferenceId> d_inferenceFacts;
-  HistogramStat<InferenceId> d_inferenceConflicts;
   /** Pointer to the proof node manager */
   ProofNodeManager* d_pnm;
   /** The inference to proof converter */

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 18b75e6313fb6f4462ae9831c3eddfea34484c92..7efd2a9ac93d309117c92232689a4adb2bd01f24 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -22,12 +22,10 @@
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
-#include "theory/datatypes/theory_datatypes.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4;
@@ -36,16 +34,19 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
-SygusExtension::SygusExtension(TheoryDatatypes* td,
-                                   QuantifiersEngine* qe,
-                                   context::Context* c)
-    : d_td(td),
-      d_tds(qe->getTermDatabaseSygus()),
-      d_ssb(qe),
-      d_testers(c),
-      d_testers_exp(c),
-      d_active_terms(c),
-      d_currTermSize(c)
+SygusExtension::SygusExtension(TheoryState& s,
+                               InferenceManager& im,
+                               quantifiers::TermDbSygus* tds,
+                               DecisionManager* dm)
+    : d_state(s),
+      d_im(im),
+      d_tds(tds),
+      d_dm(dm),
+      d_ssb(tds),
+      d_testers(s.getSatContext()),
+      d_testers_exp(s.getSatContext()),
+      d_active_terms(s.getSatContext()),
+      d_currTermSize(s.getSatContext())
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -1303,12 +1304,11 @@ void SygusExtension::registerSizeTerm(Node e, std::vector<Node>& lemmas)
       d_anchor_to_ag_strategy[e].reset(
           new DecisionStrategySingleton("sygus_enum_active",
                                         ag,
-                                        d_td->getSatContext(),
-                                        d_td->getValuation()));
+                                        d_state.getSatContext(),
+                                        d_state.getValuation()));
     }
-    d_td->getDecisionManager()->registerStrategy(
-        DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE,
-        d_anchor_to_ag_strategy[e].get());
+    d_dm->registerStrategy(DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE,
+                           d_anchor_to_ag_strategy[e].get());
   }
   Node m;
   if (!ag.isNull())
@@ -1387,10 +1387,10 @@ void SygusExtension::registerMeasureTerm( Node m ) {
   if( it==d_szinfo.end() ){
     Trace("sygus-sb") << "Sygus : register measure term : " << m << std::endl;
     d_szinfo[m].reset(new SygusSizeDecisionStrategy(
-        m, d_td->getSatContext(), d_td->getValuation()));
+        m, d_state.getSatContext(), d_state.getValuation()));
     // register this as a decision strategy
-    d_td->getDecisionManager()->registerStrategy(
-        DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE, d_szinfo[m].get());
+    d_dm->registerStrategy(DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE,
+                           d_szinfo[m].get());
   }
 }
 
@@ -1561,7 +1561,7 @@ void SygusExtension::check( std::vector< Node >& lemmas ) {
       Trace("dt-sygus-debug") << "Checking model value of " << prog << "..."
                               << std::endl;
       Assert(prog.getType().isDatatype());
-      Node progv = d_td->getValuation().getModel()->getValue( prog );
+      Node progv = d_state.getValuation().getModel()->getValue(prog);
       if (Trace.isOn("dt-sygus"))
       {
         Trace("dt-sygus") << "* DT model : " << prog << " -> ";
@@ -1578,7 +1578,7 @@ void SygusExtension::check( std::vector< Node >& lemmas ) {
         if (options::sygusFair() == options::SygusFairMode::DT_SIZE)
         {
           Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog );
-          Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz );
+          Node prog_szv = d_state.getValuation().getModel()->getValue(prog_sz);
           Node progv_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, progv );
             
           Trace("sygus-sb") << "  Mv[" << prog << "] = " << progv << ", size = " << prog_szv << std::endl;
@@ -1663,7 +1663,7 @@ bool SygusExtension::checkValue(Node n,
   if (Trace.isOn("sygus-sb-check-value"))
   {
     Node prog_sz = nm->mkNode(DT_SIZE, n);
-    Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz );
+    Node prog_szv = d_state.getValuation().getModel()->getValue(prog_sz);
     for( int i=0; i<ind; i++ ){
       Trace("sygus-sb-check-value") << "  ";
     }
@@ -1676,11 +1676,11 @@ bool SygusExtension::checkValue(Node n,
   // ensure that the expected size bound is met
   int cindex = utils::indexOf(vn.getOperator());
   Node tst = utils::mkTester(n, cindex, dt);
-  bool hastst = d_td->getEqualityEngine()->hasTerm(tst);
+  bool hastst = d_state.getEqualityEngine()->hasTerm(tst);
   Node tstrep;
   if (hastst)
   {
-    tstrep = d_td->getEqualityEngine()->getRepresentative(tst);
+    tstrep = d_state.getEqualityEngine()->getRepresentative(tst);
   }
   if (!hastst || tstrep != d_true)
   {
@@ -1789,7 +1789,8 @@ Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
 
 int SygusExtension::getGuardStatus( Node g ) {
   bool value;
-  if( d_td->getValuation().hasSatValue( g, value ) ) {
+  if (d_state.getValuation().hasSatValue(g, value))
+  {
     if( value ){
       return 1;
     }else{

diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h
index 349ee07c9e128dd78f33c1ad82b087e24a8b477b..99a0f61705e8cb62acc8c690f1aeca5c018d2ab7 100644 (file)
--- a/src/theory/datatypes/sygus_extension.h
+++ b/src/theory/datatypes/sygus_extension.h
@@ -28,6 +28,7 @@
 #include "expr/dtype.h"
 #include "expr/node.h"
 #include "theory/datatypes/sygus_simple_sym.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus_sampler.h"
@@ -37,7 +38,7 @@ namespace CVC4 {
 namespace theory {
 namespace datatypes {
 
-class TheoryDatatypes;
+class InferenceManager;
 
 /**
  * This is the sygus extension of the decision procedure for quantifier-free
@@ -70,9 +71,10 @@ class SygusExtension
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  SygusExtension(TheoryDatatypes* td,
-                   QuantifiersEngine* qe,
-                   context::Context* c);
+  SygusExtension(TheoryState& s,
+                 InferenceManager& im,
+                 quantifiers::TermDbSygus* tds,
+                 DecisionManager* dm);
   ~SygusExtension();
   /**
    * Notify this class that tester for constructor tindex has been asserted for
@@ -106,10 +108,14 @@ class SygusExtension
    */
   void check(std::vector<Node>& lemmas);
  private:
-  /** Pointer to the datatype theory that owns this class. */
-  TheoryDatatypes* d_td;
+  /** The theory state of the datatype theory */
+  TheoryState& d_state;
+  /** The inference manager of the datatype theory */
+  InferenceManager& d_im;
   /** Pointer to the sygus term database */
   quantifiers::TermDbSygus* d_tds;
+  /** Pointer to the decision manager */
+  DecisionManager* d_dm;
   /** the simple symmetry breaking utility */
   SygusSimpleSymBreak d_ssb;
   /**

diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
index 04ac14c11a79aa3b2ca420a4198b22c086a205c4..b7ab9b4f7fc959e8e4a4c0a428c84319778e3fbf 100644 (file)
--- a/src/theory/datatypes/sygus_simple_sym.cpp
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -15,7 +15,6 @@
 #include "theory/datatypes/sygus_simple_sym.h"
 
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -24,8 +23,8 @@ namespace CVC4 {
 namespace theory {
 namespace datatypes {
 
-SygusSimpleSymBreak::SygusSimpleSymBreak(QuantifiersEngine* qe)
-    : d_tds(qe->getTermDatabaseSygus())
+SygusSimpleSymBreak::SygusSimpleSymBreak(quantifiers::TermDbSygus* tds)
+    : d_tds(tds)
 {
 }
 

diff --git a/src/theory/datatypes/sygus_simple_sym.h b/src/theory/datatypes/sygus_simple_sym.h
index c2940512a9df0b8a215a3389876f4c405d1e5a1b..3ca55309bb830d3a758af5d8ce2a28aa10eca5c0 100644 (file)
--- a/src/theory/datatypes/sygus_simple_sym.h
+++ b/src/theory/datatypes/sygus_simple_sym.h
@@ -40,7 +40,7 @@ namespace datatypes {
 class SygusSimpleSymBreak
 {
  public:
-  SygusSimpleSymBreak(QuantifiersEngine* qe);
+  SygusSimpleSymBreak(quantifiers::TermDbSygus* tds);
   ~SygusSimpleSymBreak() {}
   /** consider argument kind
    *

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 8945fb7354494025bd2e778fa49d965646726845..9d3b5a143ab80f04a6fc3f7702e05e63c3ed34f3 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -107,8 +107,10 @@ void TheoryDatatypes::finishInit()
   // this is not done.
   if (getQuantifiersEngine() && options::sygus())
   {
+    quantifiers::TermDbSygus* tds =
+        getQuantifiersEngine()->getTermDatabaseSygus();
     d_sygusExtension.reset(
-        new SygusExtension(this, getQuantifiersEngine(), getSatContext()));
+        new SygusExtension(d_state, d_im, tds, getDecisionManager()));
     // do congruence on evaluation functions
     d_equalityEngine->addFunctionKind(kind::DT_SYGUS_EVAL);
   }
@@ -177,7 +179,7 @@ void TheoryDatatypes::postCheck(Effort level)
     Assert(d_sygusExtension != nullptr);
     std::vector<Node> lemmas;
     d_sygusExtension->check(lemmas);
-    d_im.sendLemmas(lemmas);
+    d_im.sendLemmas(lemmas, InferenceId::UNKNOWN);
     return;
   }
   else if (level == EFFORT_FULL && !d_state.isInConflict()
@@ -252,7 +254,7 @@ void TheoryDatatypes::postCheck(Effort level)
                     assumptions.push_back(assumption);
                     Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions );
                     Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl;
-                    d_im.lemma(lemma, InferenceId::UNKNOWN);
+                    d_im.lemma(lemma, InferenceId::DATATYPES_REC_SINGLETON_EQ);
                   }
                 }
               }else{
@@ -307,7 +309,8 @@ void TheoryDatatypes::postCheck(Effort level)
                   //this may not be necessary?
                   //if only one constructor, then this term must be this constructor
                   Node t = utils::mkTester(n, 0, dt);
-                  d_im.addPendingInference(t, d_true, false, InferenceId::DATATYPES_SPLIT);
+                  d_im.addPendingInference(
+                      t, InferenceId::DATATYPES_SPLIT, d_true);
                   Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl;
                 }else{
                   Assert(consIndex != -1 || dt.isSygus());
@@ -318,7 +321,7 @@ void TheoryDatatypes::postCheck(Effort level)
                     NodeBuilder<> nb(kind::OR);
                     nb << test << test.notNode();
                     Node lemma = nb;
-                    d_im.lemma(lemma, InferenceId::UNKNOWN);
+                    d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT);
                     d_out->requirePhase( test, true );
                   }else{
                     Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
@@ -389,7 +392,7 @@ void TheoryDatatypes::notifyFact(TNode atom,
   {
     std::vector< Node > lemmas;
     d_sygusExtension->assertFact(atom, polarity, lemmas);
-    d_im.sendLemmas(lemmas);
+    d_im.sendLemmas(lemmas, InferenceId::UNKNOWN);
   }
   //add to tester if applicable
   Node t_arg;
@@ -412,7 +415,7 @@ void TheoryDatatypes::notifyFact(TNode atom,
         std::vector< Node > lemmas;
         d_sygusExtension->assertTester(tindex, t_arg, atom, lemmas);
         Trace("dt-tester") << "Done assert tester to sygus." << std::endl;
-        d_im.sendLemmas(lemmas);
+        d_im.sendLemmas(lemmas, InferenceId::UNKNOWN);
       }
     }
   }else{
@@ -472,7 +475,7 @@ void TheoryDatatypes::preRegisterTerm(TNode n)
     {
       std::vector< Node > lemmas;
       d_sygusExtension->preRegisterTerm(n, lemmas);
-      d_im.sendLemmas(lemmas);
+      d_im.sendLemmas(lemmas, InferenceId::UNKNOWN);
     }
     break;
   }
@@ -687,7 +690,8 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
               if( !areEqual( cons1[i], cons2[i] ) ){
                 Node eq = cons1[i].eqNode( cons2[i] );
-                d_im.addPendingInference(eq, unifEq, false, InferenceId::DATATYPES_UNIF);
+                d_im.addPendingInference(
+                    eq, InferenceId::DATATYPES_UNIF, unifEq);
                 Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl;
               }
             }
@@ -849,7 +853,7 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) {
       d_term_sk[n] = k;
       Node eq = k.eqNode( n );
       Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;
-      d_im.addPendingLemma(eq, InferenceId::UNKNOWN);
+      d_im.addPendingLemma(eq, InferenceId::DATATYPES_PURIFY);
       return k;
     }else{
       return (*it).second;
@@ -974,7 +978,7 @@ void TheoryDatatypes::addTester(
                              : utils::mkTester(t_arg, testerIndex, dt);
           Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
           d_im.addPendingInference(
-              t_concl, t_concl_exp, false, InferenceId::DATATYPES_LABEL_EXH);
+              t_concl, InferenceId::DATATYPES_LABEL_EXH, t_concl_exp);
           Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl;
           return;
         }
@@ -1110,7 +1114,8 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
       bool forceLemma = !s.getType().isDatatype();
       Trace("datatypes-infer") << "DtInfer : collapse sel";
       Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl;
-      d_im.addPendingInference(eq, eq_exp, forceLemma, InferenceId::DATATYPES_COLLAPSE_SEL);
+      d_im.addPendingInference(
+          eq, InferenceId::DATATYPES_COLLAPSE_SEL, eq_exp, forceLemma);
     }
   }
 }
@@ -1414,7 +1419,7 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
       Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
       a = v1.eqNode( v2 ).negate();
       //send out immediately as lemma
-      d_im.lemma(a, InferenceId::UNKNOWN);
+      d_im.lemma(a, InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ);
       Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl;
     }
     d_singleton_lemma[index][tn] = a;
@@ -1472,7 +1477,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
     Node lem = nm->mkNode(LEQ, d_zero, n);
     Trace("datatypes-infer")
         << "DtInfer : size geq zero : " << lem << std::endl;
-    d_im.addPendingLemma(lem, InferenceId::UNKNOWN);
+    d_im.addPendingLemma(lem, InferenceId::DATATYPES_SIZE_POS);
   }
   else if (nk == DT_HEIGHT_BOUND && n[1].getConst<Rational>().isZero())
   {
@@ -1497,7 +1502,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
                                           : nm->mkNode(OR, children));
     }
     Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
-    d_im.addPendingLemma(lem, InferenceId::UNKNOWN);
+    d_im.addPendingLemma(lem, InferenceId::DATATYPES_HEIGHT_ZERO);
   }
 }
 
@@ -1564,7 +1569,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
   }
   Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq
                                  << " forceLemma = " << forceLemma << std::endl;
-  d_im.addPendingInference(eq, exp, forceLemma, InferenceId::DATATYPES_INST);
+  d_im.addPendingInference(eq, InferenceId::DATATYPES_INST, exp, forceLemma);
   Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp
                            << std::endl;
 }
@@ -1650,7 +1655,7 @@ void TheoryDatatypes::checkCycles() {
           Trace("dt-cdt") << std::endl;
           Node eq = part_out[i][0].eqNode( part_out[i][j] );
           Node eqExp = NodeManager::currentNM()->mkAnd(exp);
-          d_im.addPendingInference(eq, eqExp, false, InferenceId::DATATYPES_BISIMILAR);
+          d_im.addPendingInference(eq, InferenceId::DATATYPES_BISIMILAR, eqExp);
           Trace("datatypes-infer") << "DtInfer : cdt-bisimilar : " << eq << " by " << eqExp << std::endl;
         }
       }

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index a561cc1b4955b1610f417a9d7c6fd555c5af6472..fda694e3da742c9b540c556a795849e0cdc182c2 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -76,16 +76,27 @@ const char* toString(InferenceId i)
     case InferenceId::BAG_DIFFERENCE_REMOVE: return "BAG_DIFFERENCE_REMOVE";
     case InferenceId::BAG_DUPLICATE_REMOVAL: return "BAG_DUPLICATE_REMOVAL";
 
-    case InferenceId::DATATYPES_UNIF: return "UNIF";
-    case InferenceId::DATATYPES_INST: return "INST";
-    case InferenceId::DATATYPES_SPLIT: return "SPLIT";
-    case InferenceId::DATATYPES_LABEL_EXH: return "LABEL_EXH";
-    case InferenceId::DATATYPES_COLLAPSE_SEL: return "COLLAPSE_SEL";
-    case InferenceId::DATATYPES_CLASH_CONFLICT: return "CLASH_CONFLICT";
-    case InferenceId::DATATYPES_TESTER_CONFLICT: return "TESTER_CONFLICT";
-    case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT: return "TESTER_MERGE_CONFLICT";
-    case InferenceId::DATATYPES_BISIMILAR: return "BISIMILAR";
-    case InferenceId::DATATYPES_CYCLE: return "CYCLE";
+    case InferenceId::DATATYPES_PURIFY: return "DATATYPES_PURIFY";
+    case InferenceId::DATATYPES_UNIF: return "DATATYPES_UNIF";
+    case InferenceId::DATATYPES_INST: return "DATATYPES_INST";
+    case InferenceId::DATATYPES_SPLIT: return "DATATYPES_SPLIT";
+    case InferenceId::DATATYPES_BINARY_SPLIT: return "DATATYPES_BINARY_SPLIT";
+    case InferenceId::DATATYPES_LABEL_EXH: return "DATATYPES_LABEL_EXH";
+    case InferenceId::DATATYPES_COLLAPSE_SEL: return "DATATYPES_COLLAPSE_SEL";
+    case InferenceId::DATATYPES_CLASH_CONFLICT:
+      return "DATATYPES_CLASH_CONFLICT";
+    case InferenceId::DATATYPES_TESTER_CONFLICT:
+      return "DATATYPES_TESTER_CONFLICT";
+    case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT:
+      return "DATATYPES_TESTER_MERGE_CONFLICT";
+    case InferenceId::DATATYPES_BISIMILAR: return "DATATYPES_BISIMILAR";
+    case InferenceId::DATATYPES_REC_SINGLETON_EQ:
+      return "DATATYPES_REC_SINGLETON_EQ";
+    case InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ:
+      return "DATATYPES_REC_SINGLETON_FORCE_DEQ";
+    case InferenceId::DATATYPES_CYCLE: return "DATATYPES_CYCLE";
+    case InferenceId::DATATYPES_SIZE_POS: return "DATATYPES_SIZE_POS";
+    case InferenceId::DATATYPES_HEIGHT_ZERO: return "DATATYPES_HEIGHT_ZERO";
 
     case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP";
     case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP";

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 2891d51322e05ab2bd2e8993536df06a73d579c5..884a7c428e0fa6b9f8e50af637c3e6d4e02d9f96 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -134,12 +134,16 @@ enum class InferenceId
   // ---------------------------------- end bitvector theory
 
   // ---------------------------------- datatypes theory
+  // (= k t) for fresh k
+  DATATYPES_PURIFY,
   // (= (C t1 ... tn) (C s1 .. sn)) => (= ti si)
   DATATYPES_UNIF,
   // ((_ is Ci) t) => (= t (Ci (sel_1 t) ... (sel_n t)))
   DATATYPES_INST,
   // (or ((_ is C1) t) V ... V ((_ is Cn) t))
   DATATYPES_SPLIT,
+  // (or ((_ is Ci) t) V (not ((_ is Ci) t)))
+  DATATYPES_BINARY_SPLIT,
   // (not ((_ is C1) t)) ^ ... [j] ... ^ (not ((_ is Cn) t)) => ((_ is Cj) t)
   DATATYPES_LABEL_EXH,
   // (= t (Ci t1 ... tn)) => (= (sel_j t) rewrite((sel_j (Ci t1 ... tn))))
@@ -152,8 +156,17 @@ enum class InferenceId
   DATATYPES_TESTER_MERGE_CONFLICT,
   // bisimilarity for codatatypes
   DATATYPES_BISIMILAR,
+  // corecursive singleton equality
+  DATATYPES_REC_SINGLETON_EQ,
+  // corecursive singleton equality (not (= k1 k2)) for fresh k1, k2
+  DATATYPES_REC_SINGLETON_FORCE_DEQ,
   // cycle conflict for datatypes
   DATATYPES_CYCLE,
+  //-------------------- datatypes size/height
+  // (>= (dt.size t) 0)
+  DATATYPES_SIZE_POS,
+  // (=> (= (dt.height t) 0) => (and (= (dt.height (sel_1 t)) 0) .... ))
+  DATATYPES_HEIGHT_ZERO,
   // ---------------------------------- end datatypes theory
 
   // ---------------------------------- sep theory