From 3075a8e20dba6a784316714543c8a1b262459d9a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Sep 2020 22:13:35 -0500 Subject: [PATCH] Modify lemma vs fact policy for datatype equalities (#5115) This changes the lemma vs fact policy for datatype equalities. Previously, datatype equalities were sent as lemmas unless they were over datatypes that were composed of datatypes only. This is now changed so that equalities that do not involve direct subterms with finite non-datatype types are kept internal. The primary type of equality that this targets are "Instantiate" equalities, e.g. the conclusion of: (is-cons x) => x = (cons (head x) (tail x)) These equalities have been observed to generate large amounts of new terms for many benchmarks. With this PR, the the challenging Facebook benchmark goes from 2 min 45 sec -> 29 sec. If the instantiate rule is disabled altogether, it still correctly solves, and is faster (~14 seconds), which however is not correct in general. This change triggered two other issues: (1) A relations benchmark involving transitive closure now times out. This has been a common issue for the relations solver and should be revisited. (2) A potential issue with doPendingLemmas in InferenceManagerBuffer was uncovered. In rare cases, we can be re-entrant into this method since OutputChannel::lemma may trigger further preregistration of terms, which can trigger a recursive call to doPendingLemmas in the case of datatypes, which causes a segfault due to corrupting an iterator. This PR adds a simple guard for this method. This PR also fixes some existing issues in computing cardinality for parametric datatypes. --- src/expr/dtype_cons.cpp | 91 +++++++++---------- src/expr/dtype_cons.h | 27 ++++++ src/theory/datatypes/inference_manager.cpp | 33 ++++--- src/theory/datatypes/inference_manager.h | 12 ++- src/theory/datatypes/theory_datatypes.cpp | 18 +++- src/theory/inference_manager_buffered.cpp | 9 +- src/theory/inference_manager_buffered.h | 6 ++ test/regress/CMakeLists.txt | 5 +- .../datatypes/dt-different-params.smt2 | 16 ++++ .../regress/regress0/datatypes/list-bool.smt2 | 13 +++ 10 files changed, 160 insertions(+), 70 deletions(-) create mode 100644 test/regress/regress0/datatypes/dt-different-params.smt2 create mode 100644 test/regress/regress0/datatypes/list-bool.smt2 diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 7eec52b19..8e86ba49d 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -153,60 +153,39 @@ Cardinality DTypeConstructor::getCardinality(TypeNode t) const bool DTypeConstructor::isFinite(TypeNode t) const { - Assert(isResolved()); - - TNode self = d_constructor; - // is this already in the cache ? - if (self.getAttribute(DTypeFiniteComputedAttr())) - { - return self.getAttribute(DTypeFiniteAttr()); - } - std::vector instTypes; - std::vector paramTypes; - bool isParam = t.isParametricDatatype(); - if (isParam) - { - paramTypes = t.getDType().getParameters(); - instTypes = TypeNode(t).getParamTypes(); - } - for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++) - { - TypeNode tc = getArgType(i); - if (isParam) - { - tc = tc.substitute(paramTypes.begin(), - paramTypes.end(), - instTypes.begin(), - instTypes.end()); - } - if (!tc.isFinite()) - { - self.setAttribute(DTypeFiniteComputedAttr(), true); - self.setAttribute(DTypeFiniteAttr(), false); - return false; - } - } - self.setAttribute(DTypeFiniteComputedAttr(), true); - self.setAttribute(DTypeFiniteAttr(), true); - return true; + std::pair cinfo = computeCardinalityInfo(t); + return cinfo.first == CardinalityType::FINITE; } bool DTypeConstructor::isInterpretedFinite(TypeNode t) const { - Assert(isResolved()); - TNode self = d_constructor; - // is this already in the cache ? - if (self.getAttribute(DTypeUFiniteComputedAttr())) + std::pair cinfo = computeCardinalityInfo(t); + return cinfo.first != CardinalityType::INFINITE; +} + +bool DTypeConstructor::hasFiniteExternalArgType(TypeNode t) const +{ + std::pair cinfo = computeCardinalityInfo(t); + return cinfo.second; +} + +std::pair +DTypeConstructor::computeCardinalityInfo(TypeNode t) const +{ + std::map >::iterator it = + d_cardInfo.find(t); + if (it != d_cardInfo.end()) { - return self.getAttribute(DTypeUFiniteAttr()); + return it->second; } + std::pair ret(CardinalityType::FINITE, false); std::vector instTypes; std::vector paramTypes; bool isParam = t.isParametricDatatype(); if (isParam) { paramTypes = t.getDType().getParameters(); - instTypes = TypeNode(t).getParamTypes(); + instTypes = t.getParamTypes(); } for (unsigned i = 0, nargs = getNumArgs(); i < nargs; i++) { @@ -218,16 +197,30 @@ bool DTypeConstructor::isInterpretedFinite(TypeNode t) const instTypes.begin(), instTypes.end()); } - if (!tc.isInterpretedFinite()) + if (tc.isFinite()) + { + // do nothing + } + else if (tc.isInterpretedFinite()) + { + if (ret.first == CardinalityType::FINITE) + { + // not simply finite, it depends on uninterpreted sorts being finite + ret.first = CardinalityType::INTERPRETED_FINITE; + } + } + else { - self.setAttribute(DTypeUFiniteComputedAttr(), true); - self.setAttribute(DTypeUFiniteAttr(), false); - return false; + // infinite implies the constructor is infinite cardinality + ret.first = CardinalityType::INFINITE; + continue; } + // if the argument is (interpreted) finite and external, set the flag + // for indicating it has a finite external argument + ret.second = ret.second || !tc.isDatatype(); } - self.setAttribute(DTypeUFiniteComputedAttr(), true); - self.setAttribute(DTypeUFiniteAttr(), true); - return true; + d_cardInfo[t] = ret; + return ret; } bool DTypeConstructor::isResolved() const { return !d_tester.isNull(); } diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h index fc414c756..2dba895e9 100644 --- a/src/expr/dtype_cons.h +++ b/src/expr/dtype_cons.h @@ -158,6 +158,13 @@ class DTypeConstructor * only be called for resolved constructors. */ bool isInterpretedFinite(TypeNode t) const; + /** + * Has finite external argument type. This returns true if this constructor + * has an argument type that is not a datatype and is interpreted as a + * finite type. This function can only be called for resolved constructors. + * + */ + bool hasFiniteExternalArgType(TypeNode t) const; /** * Returns true iff this constructor has already been @@ -229,6 +236,17 @@ class DTypeConstructor void toStream(std::ostream& out) const; private: + /** Constructor cardinality type */ + enum class CardinalityType + { + // the constructor is finite + FINITE, + // the constructor is interpreted-finite (finite under the assumption that + // uninterpreted sorts are finite) + INTERPRETED_FINITE, + // the constructor is infinte + INFINITE + }; /** resolve * * This resolves (initializes) the constructor. For details @@ -286,6 +304,13 @@ class DTypeConstructor std::vector& processing, std::map& gt, bool isValue) const; + /** + * Compute cardinality info, returns a pair where its first component is + * an identifier indicating the cardinality type of this constructor for + * type t, and a Boolean indicating whether the constructor has any arguments + * that have finite external type. + */ + std::pair computeCardinalityInfo(TypeNode t) const; /** compute shared selectors * This computes the maps d_sharedSelectors and d_sharedSelectorIndex. */ @@ -324,6 +349,8 @@ class DTypeConstructor * its argument index for this constructor. */ mutable std::map > d_sharedSelectorIndex; + /** A cache for computeCardinalityInfo. */ + mutable std::map > d_cardInfo; }; /* class DTypeConstructor */ /** diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 45406a9b0..f056b9c5d 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -42,16 +42,13 @@ bool DatatypesInference::mustCommunicateFact(Node n, Node exp) } else if (n.getKind() == EQUAL) { + // Note that equalities due to instantiate are forced as lemmas if + // necessary as they are created. This ensures that terms are shared with + // external theories when necessary. We send the lemma here only if + // the equality is not for datatype terms, which can happen for collapse + // selector / term size or unification. TypeNode tn = n[0].getType(); - if (!tn.isDatatype()) - { - addLemma = true; - } - else - { - const DType& dt = tn.getDType(); - addLemma = dt.involvesExternalType(); - } + addLemma = !tn.isDatatype(); } else if (n.getKind() == LEQ || n.getKind() == OR) { @@ -68,8 +65,10 @@ bool DatatypesInference::mustCommunicateFact(Node n, Node exp) bool DatatypesInference::process(TheoryInferenceManager* im, bool asLemma) { - // check to see if we have to communicate it to the rest of the system - if (mustCommunicateFact(d_conc, d_exp)) + // Check to see if we have to communicate it to the rest of the system. + // The flag asLemma is true when the inference was marked that it must be + // sent as a lemma in addPendingInference below. + if (asLemma || mustCommunicateFact(d_conc, d_exp)) { // send it as an (explained) lemma std::vector exp; @@ -95,9 +94,17 @@ InferenceManager::InferenceManager(Theory& t, void InferenceManager::addPendingInference(Node conc, Node exp, - ProofGenerator* pg) + ProofGenerator* pg, + bool forceLemma) { - d_pendingFact.emplace_back(new DatatypesInference(conc, exp, pg)); + if (forceLemma) + { + d_pendingLem.emplace_back(new DatatypesInference(conc, exp, pg)); + } + else + { + d_pendingFact.emplace_back(new DatatypesInference(conc, exp, pg)); + } } void InferenceManager::process() diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index 91536baab..06c6ff2b5 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -72,8 +72,18 @@ class InferenceManager : public InferenceManagerBuffered /** * Add pending inference, which may be processed as either a fact or * a lemma based on mustCommunicateFact in DatatypesInference above. + * + * @param conc The conclusion of the inference + * @param exp The explanation of the inference + * @param pg The proof generator who can provide a 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. */ - void addPendingInference(Node conc, Node exp, ProofGenerator* pg = nullptr); + void addPendingInference(Node conc, + Node exp, + ProofGenerator* pg = nullptr, + 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 diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9cecb6f27..376dbb1db 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1541,7 +1541,8 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ exp = getLabel(n); tt = exp[0]; } - const DType& dt = tt.getType().getDType(); + TypeNode ttn = tt.getType(); + const DType& dt = ttn.getDType(); // instantiate this equivalence class eqc->d_inst = true; Node tt_cons = getInstantiateCons(tt, dt, index); @@ -1551,10 +1552,17 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ return; } eq = tt.eqNode(tt_cons); - Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq - << std::endl; - d_im.addPendingInference(eq, exp); - Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl; + // Determine if the equality must be sent out as a lemma. Notice that + // we can keep new equalities from the instantiate rule internal as long as + // they are for datatype constructors that have no arguments that have + // finite external type. Such equalities must be sent because they introduce + // selector terms that may contribute to conflicts due to cardinality (good + // examples of this are regress0/datatypes/dt-param-card4-bool-sat.smt2 and + // regress0/datatypes/list-bool.smt2). + bool forceLemma = dt[index].hasFiniteExternalArgType(ttn); + Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq + << " forceLemma = " << forceLemma << std::endl; + d_im.addPendingInference(eq, exp, nullptr, forceLemma); Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl; } diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 1da814116..5699e75ad 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -25,7 +25,7 @@ namespace theory { InferenceManagerBuffered::InferenceManagerBuffered(Theory& t, TheoryState& state, ProofNodeManager* pnm) - : TheoryInferenceManager(t, state, pnm) + : TheoryInferenceManager(t, state, pnm), d_processingPendingLemmas(false) { } @@ -94,12 +94,19 @@ void InferenceManagerBuffered::doPendingFacts() void InferenceManagerBuffered::doPendingLemmas() { + if (d_processingPendingLemmas) + { + // already processing + return; + } + d_processingPendingLemmas = true; for (const std::unique_ptr& plem : d_pendingLem) { // process this lemma plem->process(this, true); } d_pendingLem.clear(); + d_processingPendingLemmas = false; } void InferenceManagerBuffered::doPendingPhaseRequirements() diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index 3d249ea80..74bbcc375 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -134,6 +134,12 @@ class InferenceManagerBuffered : public TheoryInferenceManager std::vector> d_pendingFact; /** A map from literals to their pending phase requirement */ std::map d_pendingReqPhase; + /** + * Whether we are currently processing pending lemmas. This flag ensures + * that we do not call pending lemmas recursively, which may lead to + * segfaults. + */ + bool d_processingPendingLemmas; }; } // namespace theory diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c7bf666d6..fc2167a4a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -415,6 +415,7 @@ set(regress_0_tests regress0/datatypes/datatype3.cvc regress0/datatypes/datatype4.cvc regress0/datatypes/dt-2.6.smt2 + regress0/datatypes/dt-different-params.smt2 regress0/datatypes/dt-match-pat-param-2.6.smt2 regress0/datatypes/dt-param-2.6.smt2 regress0/datatypes/dt-param-2.6-print.smt2 @@ -426,6 +427,7 @@ set(regress_0_tests regress0/datatypes/issue1433.smt2 regress0/datatypes/issue2838.cvc regress0/datatypes/jsat-2.6.smt2 + regress0/datatypes/list-bool.smt2 regress0/datatypes/model-subterms-min.smt2 regress0/datatypes/mutually-recursive.cvc regress0/datatypes/pair-bool-bool.cvc @@ -1676,7 +1678,6 @@ set(regress_1_tests regress1/rels/rel_pressure_0.cvc regress1/rels/rel_tc_10_1.cvc regress1/rels/rel_tc_4.cvc - regress1/rels/rel_tc_4_1.cvc regress1/rels/rel_tc_5_1.cvc regress1/rels/rel_tc_6.cvc regress1/rels/rel_tc_9_1.cvc @@ -2519,6 +2520,8 @@ set(regression_disabled_tests # doing a coverage build with LFSC. regress1/quantifiers/set3.smt2 regress1/rels/garbage_collect.cvc + # times out after dt fact update due to overly eager splitting for tclosure + regress1/rels/rel_tc_4_1.cvc regress1/sets/setofsets-disequal.smt2 regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 regress1/simple-rdl-definefun.smt2 diff --git a/test/regress/regress0/datatypes/dt-different-params.smt2 b/test/regress/regress0/datatypes/dt-different-params.smt2 new file mode 100644 index 000000000..f73d82dc9 --- /dev/null +++ b/test/regress/regress0/datatypes/dt-different-params.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes ((Data 1)) ((par (T) ((data (first T)))))) + +(declare-fun q1 () (Data Int)) +(declare-fun q2 () (Data Int)) +(declare-fun q3 () (Data Int)) + +(assert (distinct q1 q2 q3)) + +(declare-fun p1 () (Data Bool)) +(declare-fun p2 () (Data Bool)) +(declare-fun p3 () (Data Bool)) + +(assert (distinct p1 p2 p3)) +(check-sat) diff --git a/test/regress/regress0/datatypes/list-bool.smt2 b/test/regress/regress0/datatypes/list-bool.smt2 new file mode 100644 index 000000000..adc7ad95a --- /dev/null +++ b/test/regress/regress0/datatypes/list-bool.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((list 0)) ( +((cons (head Bool) (tail list)) (nil)) +)) +(declare-fun x1 () list) +(declare-fun x2 () list) +(declare-fun x3 () list) +(assert (= (tail x1) nil)) +(assert (= (tail x2) nil)) +(assert (= (tail x3) nil)) +(assert (distinct x1 x2 x3 nil)) +(check-sat) -- 2.30.2