From 9bbf41fb6cb5a33cfbfc3a711b82a4783a61b66f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 May 2021 13:39:59 -0500 Subject: [PATCH] Add more missing inference ids (#6313) This also makes the relations solver use the inference manager in the standard way. --- src/theory/arith/theory_arith_private.cpp | 6 +-- src/theory/fp/theory_fp.cpp | 45 +++++++++++++---------- src/theory/fp/theory_fp.h | 2 +- src/theory/inference_id.cpp | 7 ++++ src/theory/inference_id.h | 17 +++++++++ src/theory/sets/theory_sets_rels.cpp | 38 ++----------------- src/theory/sets/theory_sets_rels.h | 2 - 7 files changed, 57 insertions(+), 60 deletions(-) diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 508362158..a4a5ad229 100644 --- 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 " <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 21f2975a8..ecb8ba2b4 100644 --- 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& 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& 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& lems) res, nm->mkConst(FloatingPoint::makeZero( res.getType().getConst(), 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().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 a41bf342c..ada9b39d0 100644 --- 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 ceca32a8d..fe4ed4c22 100644 --- 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 9e1c78113..169992f41 100644 --- 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 74dfc01ba..69780b04c 100644 --- 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 c30322d07..89514c641 100644 --- 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 d_pending; NodeSet d_shared_terms; std::unordered_set d_rel_nodes; -- 2.30.2