Add more missing inference ids (#6313)

This also makes the relations solver use the inference manager in the standard way.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 508362158ce9c4f007d4e2e820a8a20db43ee093..a4a5ad229d817a060a46931fc9f401dfa68105ea 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4124,7 +4124,7 @@ void TheoryArithPrivate::presolve(){
   for(; i != i_end; ++i){
     TrustNode lem = *i;
     Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
-    outputTrustedLemma(lem, InferenceId::UNKNOWN);
+    outputTrustedLemma(lem, InferenceId::ARITH_UNATE);
   }
 }
 
@@ -4569,11 +4569,11 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
 
         // Output it
         TrustNode trustedClause = d_pfGen->mkTrustNode(clause, clausePf);
-        outputTrustedLemma(trustedClause, InferenceId::UNKNOWN);
+        outputTrustedLemma(trustedClause, InferenceId::ARITH_ROW_IMPL);
       }
       else
       {
-        outputLemma(clause, InferenceId::UNKNOWN);
+        outputLemma(clause, InferenceId::ARITH_ROW_IMPL);
       }
     }else{
       Assert(!implied->negationHasProof());

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 21f2975a86356c02637766a32e38f8c11275a62a..ecb8ba2b4005871ec686c4e37f8a741fdc3430ca 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -243,13 +243,13 @@ TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
                               nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]),
                               nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])),
                    nm->mkNode(kind::EQUAL, res, node[1]));
-    handleLemma(pd);
+    handleLemma(pd, InferenceId::FP_PREPROCESS);
 
     Node z =
         nm->mkNode(kind::IMPLIES,
                    nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
                    nm->mkNode(kind::EQUAL, res, nm->mkConst(Rational(0U))));
-    handleLemma(z);
+    handleLemma(z, InferenceId::FP_PREPROCESS);
 
     // TODO : bounds on the output from largest floats, #1914
   }
@@ -262,7 +262,7 @@ TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
 
     Node nnan =
         nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, res));
-    handleLemma(nnan);
+    handleLemma(nnan, InferenceId::FP_PREPROCESS);
 
     Node z = nm->mkNode(
         kind::IMPLIES,
@@ -271,7 +271,7 @@ TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
                    res,
                    nm->mkConst(FloatingPoint::makeZero(
                        res.getType().getConst<FloatingPointSize>(), false))));
-    handleLemma(z);
+    handleLemma(z, InferenceId::FP_PREPROCESS);
 
     // TODO : rounding-mode specific bounds on floats that don't give infinity
     // BEWARE of directed rounding!   #1914
@@ -346,7 +346,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
               kind::EQUAL,
               nm->mkNode(kind::FLOATINGPOINT_GEQ, concrete[0], floatValue),
               nm->mkNode(kind::GEQ, abstract, concreteValue)));
-      handleLemma(fg);
+      handleLemma(fg, InferenceId::FP_PREPROCESS);
 
       Node fl = nm->mkNode(
           kind::IMPLIES,
@@ -355,7 +355,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
               kind::EQUAL,
               nm->mkNode(kind::FLOATINGPOINT_LEQ, concrete[0], floatValue),
               nm->mkNode(kind::LEQ, abstract, concreteValue)));
-      handleLemma(fl);
+      handleLemma(fl, InferenceId::FP_PREPROCESS);
 
       // Then the backwards constraints
       Node floatAboveAbstract = Rewriter::rewrite(
@@ -373,7 +373,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
               nm->mkNode(
                   kind::FLOATINGPOINT_GEQ, concrete[0], floatAboveAbstract),
               nm->mkNode(kind::GEQ, abstract, abstractValue)));
-      handleLemma(bg);
+      handleLemma(bg, InferenceId::FP_PREPROCESS);
 
       Node floatBelowAbstract = Rewriter::rewrite(
           nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
@@ -390,7 +390,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
               nm->mkNode(
                   kind::FLOATINGPOINT_LEQ, concrete[0], floatBelowAbstract),
               nm->mkNode(kind::LEQ, abstract, abstractValue)));
-      handleLemma(bl);
+      handleLemma(bl, InferenceId::FP_PREPROCESS);
       // TODO : see if the overflow conditions could be improved #1914
 
       return true;
@@ -454,7 +454,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
               kind::EQUAL,
               nm->mkNode(kind::GEQ, concrete[1], realValue),
               nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, concreteValue)));
-      handleLemma(fg);
+      handleLemma(fg, InferenceId::FP_PREPROCESS);
 
       Node fl = nm->mkNode(
           kind::IMPLIES,
@@ -463,7 +463,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
               kind::EQUAL,
               nm->mkNode(kind::LEQ, concrete[1], realValue),
               nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, concreteValue)));
-      handleLemma(fl);
+      handleLemma(fl, InferenceId::FP_PREPROCESS);
 
       // Then the backwards constraints
       if (!abstractValue.getConst<FloatingPoint>().isInfinite())
@@ -480,7 +480,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
                 kind::EQUAL,
                 nm->mkNode(kind::GEQ, concrete[1], realValueOfAbstract),
                 nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, abstractValue)));
-        handleLemma(bg);
+        handleLemma(bg, InferenceId::FP_PREPROCESS);
 
         Node bl = nm->mkNode(
             kind::IMPLIES,
@@ -489,7 +489,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
                 kind::EQUAL,
                 nm->mkNode(kind::LEQ, concrete[1], realValueOfAbstract),
                 nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, abstractValue)));
-        handleLemma(bl);
+        handleLemma(bl, InferenceId::FP_PREPROCESS);
       }
 
       return true;
@@ -536,7 +536,8 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
     NodeManager *nm = NodeManager::currentNM();
 
     handleLemma(
-        nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::BitVector(1U, 1U))));
+        nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::BitVector(1U, 1U))),
+        InferenceId::FP_EQUATE_TERM);
 #endif
 
     ++oldAdditionalAssertions;
@@ -553,11 +554,13 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
 #ifdef SYMFPUPROPISBOOL
       handleLemma(nm->mkNode(kind::EQUAL, node, converted));
 #else
-      handleLemma(nm->mkNode(
-          kind::EQUAL,
-          node,
-          nm->mkNode(
-              kind::EQUAL, converted, nm->mkConst(::cvc5::BitVector(1U, 1U)))));
+      handleLemma(
+          nm->mkNode(kind::EQUAL,
+                     node,
+                     nm->mkNode(kind::EQUAL,
+                                converted,
+                                nm->mkConst(::cvc5::BitVector(1U, 1U)))),
+          InferenceId::FP_EQUATE_TERM);
 #endif
 
     } else {
@@ -569,7 +572,8 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
       Assert(converted.getType().isBitVector());
 
       handleLemma(
-          NodeManager::currentNM()->mkNode(kind::EQUAL, node, converted));
+          NodeManager::currentNM()->mkNode(kind::EQUAL, node, converted),
+          InferenceId::FP_EQUATE_TERM);
     }
   }
 
@@ -640,7 +644,8 @@ void TheoryFp::registerTerm(TNode node) {
         Unreachable() << "Only isNaN, isInf and isZero have aliases";
       }
 
-      handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias));
+      handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias),
+                  InferenceId::FP_REGISTER_TERM);
     }
 
     // Use symfpu to produce an equivalent bit-vector statement

diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index a41bf342c2d56979577c119d292ed8d957d0627a..ada9b39d0d17d453c915377e89c506afed656e27 100644 (file)
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -130,7 +130,7 @@ class TheoryFp : public Theory
   void convertAndEquateTerm(TNode node);
 
   /** Interaction with the rest of the solver **/
-  void handleLemma(Node node, InferenceId id = InferenceId::UNKNOWN);
+  void handleLemma(Node node, InferenceId id);
   /**
    * Called when literal node is inferred by the equality engine. This
    * propagates node on the output channel.

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index ceca32a8d2cce29cea72f082bd75d0bc1110d6b9..fe4ed4c227ba66f1f71c3b055bbc9674e7b432ba 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -39,6 +39,8 @@ const char* toString(InferenceId i)
     case InferenceId::ARITH_BB_LEMMA: return "ARITH_BB_LEMMA";
     case InferenceId::ARITH_DIO_CUT: return "ARITH_DIO_CUT";
     case InferenceId::ARITH_DIO_DECOMPOSITION: return "ARITH_DIO_DECOMPOSITION";
+    case InferenceId::ARITH_UNATE: return "ARITH_UNATE";
+    case InferenceId::ARITH_ROW_IMPL: return "ARITH_ROW_IMPL";
     case InferenceId::ARITH_SPLIT_FOR_NL_MODEL:
       return "ARITH_SPLIT_FOR_NL_MODEL";
     case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS";
@@ -149,6 +151,10 @@ const char* toString(InferenceId i)
       return "DATATYPES_SYGUS_MT_BOUND";
     case InferenceId::DATATYPES_SYGUS_MT_POS: return "DATATYPES_SYGUS_MT_POS";
 
+    case InferenceId::FP_PREPROCESS: return "FP_PREPROCESS";
+    case InferenceId::FP_EQUATE_TERM: return "FP_EQUATE_TERM";
+    case InferenceId::FP_REGISTER_TERM: return "FP_REGISTER_TERM";
+
     case InferenceId::QUANTIFIERS_INST_E_MATCHING:
       return "QUANTIFIERS_INST_E_MATCHING";
     case InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE:
@@ -269,6 +275,7 @@ const char* toString(InferenceId i)
       return "SETS_RELS_PRODUCE_COMPOSE";
     case InferenceId::SETS_RELS_PRODUCT_SPLIT: return "SETS_RELS_PRODUCT_SPLIT";
     case InferenceId::SETS_RELS_TCLOSURE_FWD: return "SETS_RELS_TCLOSURE_FWD";
+    case InferenceId::SETS_RELS_TCLOSURE_UP: return "SETS_RELS_TCLOSURE_UP";
     case InferenceId::SETS_RELS_TRANSPOSE_EQ: return "SETS_RELS_TRANSPOSE_EQ";
     case InferenceId::SETS_RELS_TRANSPOSE_REV: return "SETS_RELS_TRANSPOSE_REV";
     case InferenceId::SETS_RELS_TUPLE_REDUCTION:

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 9e1c781138c1ae3d575e1d104dbf37b17d429e44..169992f417d7317f82dc3cfac0c6ebd7612aeb01 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -67,6 +67,13 @@ enum class InferenceId
   ARITH_BB_LEMMA,
   ARITH_DIO_CUT,
   ARITH_DIO_DECOMPOSITION,
+  // unate lemma during presolve
+  ARITH_UNATE,
+  // row implication
+  ARITH_ROW_IMPL,
+  // a split that occurs when the non-linear solver changes values of arithmetic
+  // variables in a model, but those variables are inconsistent with assignments
+  // from another theory
   ARITH_SPLIT_FOR_NL_MODEL,
   //-------------------- preprocessing
   // equivalence of term and its preprocessed form
@@ -230,6 +237,15 @@ enum class InferenceId
   DATATYPES_SYGUS_MT_POS,
   // ---------------------------------- end datatypes theory
 
+  //-------------------------------------- floating point theory
+  // a lemma sent during TheoryFp::ppRewrite
+  FP_PREPROCESS,
+  // a lemma sent during TheoryFp::convertAndEquateTerm
+  FP_EQUATE_TERM,
+  // a lemma sent during TheoryFp::registerTerm
+  FP_REGISTER_TERM,
+  //-------------------------------------- end floating point theory
+
   //-------------------------------------- quantifiers theory
   //-------------------- types of instantiations.
   // Notice the identifiers in this section cover all the techniques used for
@@ -397,6 +413,7 @@ enum class InferenceId
   SETS_RELS_PRODUCE_COMPOSE,
   SETS_RELS_PRODUCT_SPLIT,
   SETS_RELS_TCLOSURE_FWD,
+  SETS_RELS_TCLOSURE_UP,
   SETS_RELS_TRANSPOSE_EQ,
   SETS_RELS_TRANSPOSE_REV,
   SETS_RELS_TUPLE_REDUCTION,

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 74dfc01baec635086c89ec4f721fccd377d58f2d..69780b04cf615c4fb4d9274eeaec49a64024cc2a 100644 (file)
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -59,9 +59,9 @@ void TheorySetsRels::check(Theory::Effort level)
   {
     collectRelsInfo();
     check();
-    doPendingInfers();
+    d_im.doPendingLemmas();
   }
-  Assert(d_pending.empty());
+  Assert(!d_im.hasPendingLemma());
   Trace("rels") << "\n[sets-rels] ******************************* Done with "
                    "the relational solver *******************************\n"
                 << std::endl;
@@ -596,8 +596,7 @@ void TheorySetsRels::check(Theory::Effort level)
                                   RelsUtils::constructPair(tc_rel, sk_1, sk_2),
                                   tc_rel))));
 
-    Node tc_lemma = nm->mkNode(IMPLIES, reason, conc);
-    d_pending.push_back(tc_lemma);
+    sendInfer(conc, InferenceId::SETS_RELS_TCLOSURE_UP, reason);
   }
 
   bool TheorySetsRels::isTCReachable( Node mem_rep, Node tc_rel ) {
@@ -1118,35 +1117,6 @@ void TheorySetsRels::check(Theory::Effort level)
 
   }
 
-  void TheorySetsRels::doPendingInfers()
-  {
-    // process the inferences in d_pending
-    if (!d_state.isInConflict())
-    {
-      for (const Node& p : d_pending)
-      {
-        if (p.getKind() == IMPLIES)
-        {
-          processInference(p[1], InferenceId::UNKNOWN, p[0]);
-        }
-        else
-        {
-          processInference(p, InferenceId::UNKNOWN, d_trueNode);
-        }
-        if (d_state.isInConflict())
-        {
-          break;
-        }
-      }
-      // if we are still not in conflict, send lemmas
-      if (!d_state.isInConflict())
-      {
-        d_im.doPendingLemmas();
-      }
-    }
-    d_pending.clear();
-  }
-
   void TheorySetsRels::processInference(Node conc, InferenceId id, Node exp)
   {
     Trace("sets-pinfer") << "Process inference: " << exp << " => " << conc
@@ -1355,7 +1325,7 @@ void TheorySetsRels::check(Theory::Effort level)
     Trace("rels-lemma") << "Rels::lemma " << fact << " from " << reason
                         << " by " << id << std::endl;
     Node lemma = NodeManager::currentNM()->mkNode(IMPLIES, reason, fact);
-    d_pending.push_back(lemma);
+    d_im.addPendingLemma(lemma, id);
   }
 }
 }

diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index c30322d07f658e51f8b6b703afe3cbfc172e7db1..89514c64149df34180f3d6d8aaf6dfc71d82ab5a 100644 (file)
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -94,8 +94,6 @@ class TheorySetsRels {
   SkolemCache& d_skCache;
   /** Reference to the term registry */
   TermRegistry& d_treg;
-  /** A list of pending inferences to process */
-  std::vector<Node> d_pending;
   NodeSet                       d_shared_terms;
 
   std::unordered_set<Node> d_rel_nodes;