diff options
34 files changed, 216 insertions, 50 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4db7b202e..918c5a45a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -632,6 +632,8 @@ libcvc4_add_sources( theory/fp/theory_fp_type_rules.cpp theory/fp/type_enumerator.h theory/interrupted.h + theory/incomplete_id.cpp + theory/incomplete_id.h theory/inference_id.cpp theory/inference_id.h theory/inference_manager_buffered.cpp diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 03563006b..16142886f 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -489,7 +489,7 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termS Trace("nl-ext") << "...failed to send lemma in " "NonLinearExtension, set incomplete" << std::endl; - d_containing.getOutputChannel().setIncomplete(); + d_containing.getOutputChannel().setIncomplete(IncompleteId::ARITH_NL); return Result::Sat::SAT_UNKNOWN; } } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e68ff7d11..2c339cd0c 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -206,7 +206,7 @@ void TheoryArith::postCheck(Effort level) else if (d_internal->foundNonlinear()) { // set incomplete - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED); } } } diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index 08fa0164b..709ecbfa1 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -139,10 +139,10 @@ void EngineOutputChannel::requirePhase(TNode n, bool phase) d_engine->getPropEngine()->requirePhase(n, phase); } -void EngineOutputChannel::setIncomplete() +void EngineOutputChannel::setIncomplete(IncompleteId id) { - Trace("theory") << "setIncomplete()" << std::endl; - d_engine->setIncomplete(d_theory); + Trace("theory") << "setIncomplete(" << id << ")" << std::endl; + d_engine->setIncomplete(d_theory, id); } void EngineOutputChannel::spendResource(ResourceManager::Resource r) diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index 8b497547b..a9bae38a3 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -58,7 +58,7 @@ class EngineOutputChannel : public theory::OutputChannel void requirePhase(TNode n, bool phase) override; - void setIncomplete() override; + void setIncomplete(IncompleteId id) override; void spendResource(ResourceManager::Resource r) override; diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp new file mode 100644 index 000000000..340e2c208 --- /dev/null +++ b/src/theory/incomplete_id.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \file incomplete_id.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 + ** + ** \brief Implementation of incompleteness enumeration. + **/ + +#include "theory/incomplete_id.h" + +#include <iostream> + +namespace cvc5 { +namespace theory { + +const char* toString(IncompleteId i) +{ + switch (i) + { + case IncompleteId::ARITH_NL_DISABLED: return "ARITH_NL_DISABLED"; + case IncompleteId::ARITH_NL: return "ARITH_NL"; + case IncompleteId::QUANTIFIERS: return "QUANTIFIERS"; + case IncompleteId::QUANTIFIERS_SYGUS_NO_VERIFY: + return "QUANTIFIERS_SYGUS_NO_VERIFY"; + case IncompleteId::QUANTIFIERS_CEGQI: return "QUANTIFIERS_CEGQI"; + case IncompleteId::QUANTIFIERS_FMF: return "QUANTIFIERS_FMF"; + case IncompleteId::QUANTIFIERS_RECORDED_INST: + return "QUANTIFIERS_RECORDED_INST"; + case IncompleteId::SEP: return "SEP"; + case IncompleteId::SETS_RELS_CARD: return "SETS_RELS_CARD"; + case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP"; + case IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY: + return "STRINGS_REGEXP_NO_SIMPLIFY"; + case IncompleteId::UF_HO_EXT_DISABLED: return "UF_HO_EXT_DISABLED"; + case IncompleteId::UF_CARD_DISABLED: return "UF_CARD_DISABLED"; + case IncompleteId::UF_CARD_MODE: return "UF_CARD_MODE"; + case IncompleteId::UNKNOWN: return "UNKNOWN"; + default: return "?IncompleteId?"; + } +} + +std::ostream& operator<<(std::ostream& out, IncompleteId i) +{ + out << toString(i); + return out; +} + +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h new file mode 100644 index 000000000..67754b67d --- /dev/null +++ b/src/theory/incomplete_id.h @@ -0,0 +1,83 @@ +/********************* */ +/*! \file incomplete_id.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 + ** + ** \brief Incompleteness enumeration. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__INCOMPLETE_ID_H +#define CVC4__THEORY__INCOMPLETE_ID_H + +#include <iosfwd> + +namespace cvc5 { +namespace theory { + +/** + * Reasons for incompleteness in CVC4. + */ +enum class IncompleteId +{ + // the non-linear arithmetic solver was disabled + ARITH_NL_DISABLED, + // the non-linear arithmetic solver was incomplete + ARITH_NL, + // incomplete due to lack of a complete quantifiers strategy + QUANTIFIERS, + // we failed to verify the correctness of a candidate solution in SyGuS + QUANTIFIERS_SYGUS_NO_VERIFY, + // incomplete due to counterexample-guided instantiation not being complete + QUANTIFIERS_CEGQI, + // incomplete due to finite model finding not being complete + QUANTIFIERS_FMF, + // incomplete due to explicitly recorded instantiations + QUANTIFIERS_RECORDED_INST, + // incomplete due to separation logic + SEP, + // relations were used in combination with set cardinality constraints + SETS_RELS_CARD, + // we skipped processing a looping word equation + STRINGS_LOOP_SKIP, + // we could not simplify a regular expression membership + STRINGS_REGEXP_NO_SIMPLIFY, + // HO extensionality axiom was disabled + UF_HO_EXT_DISABLED, + // UF+cardinality solver was disabled + UF_CARD_DISABLED, + // UF+cardinality solver used in an incomplete mode + UF_CARD_MODE, + + //-------------------------------------- unknown + UNKNOWN +}; + +/** + * Converts an incompleteness id to a string. + * + * @param i The incompleteness identifier + * @return The name of the incompleteness identifier + */ +const char* toString(IncompleteId i); + +/** + * Writes an incompleteness identifier to a stream. + * + * @param out The stream to write to + * @param i The incompleteness identifier to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, IncompleteId i); + +} // namespace theory +} // namespace cvc5 + +#endif /* CVC4__THEORY__INCOMPLETE_ID_H */ diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 89957ded6..3e91bff44 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -14,11 +14,11 @@ #include "cvc4_private.h" -#include <iosfwd> - #ifndef CVC4__THEORY__INFERENCE_ID_H #define CVC4__THEORY__INFERENCE_ID_H +#include <iosfwd> + namespace cvc5 { namespace theory { diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index b86a4d647..0a3fa3904 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -19,6 +19,7 @@ #ifndef CVC4__THEORY__OUTPUT_CHANNEL_H #define CVC4__THEORY__OUTPUT_CHANNEL_H +#include "theory/incomplete_id.h" #include "theory/trust_node.h" #include "util/resource_manager.h" @@ -150,7 +151,7 @@ class OutputChannel { * this context level. If SAT is later determined by the * TheoryEngine, it should actually return an UNKNOWN result. */ - virtual void setIncomplete() = 0; + virtual void setIncomplete(IncompleteId id) = 0; /** * "Spend" a "resource." The meaning is specific to the context in diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 74469e7de..5afea1e9b 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -296,9 +296,10 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) } } -bool InstStrategyCegqi::checkComplete() +bool InstStrategyCegqi::checkComplete(IncompleteId& incId) { if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ + incId = IncompleteId::QUANTIFIERS_CEGQI; return false; }else{ return true; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 6d4ee047f..85724a915 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -85,7 +85,7 @@ class InstStrategyCegqi : public QuantifiersModule /** check */ void check(Theory::Effort e, QEffort quant_e) override; /** check complete */ - bool checkComplete() override; + bool checkComplete(IncompleteId& incId) override; /** check complete for quantified formula */ bool checkCompleteFor(Node q) override; /** check ownership */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 1c46e425d..5fa139681 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -112,8 +112,14 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e) } } -bool ModelEngine::checkComplete() { - return !d_incomplete_check; +bool ModelEngine::checkComplete(IncompleteId& incId) +{ + if (d_incomplete_check) + { + incId = IncompleteId::QUANTIFIERS_FMF; + return false; + } + return true; } bool ModelEngine::checkCompleteFor( Node q ) { diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 2547f2831..5a983d726 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -55,7 +55,7 @@ public: QEffort needsModel(Theory::Effort e) override; void reset_round(Theory::Effort e) override; void check(Theory::Effort e, QEffort quant_e) override; - bool checkComplete() override; + bool checkComplete(IncompleteId& incId) override; bool checkCompleteFor(Node q) override; void registerQuantifier(Node f) override; void assertNode(Node f) override; diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 62376bff6..8fc1c4d13 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -74,12 +74,13 @@ bool Instantiate::reset(Theory::Effort e) } void Instantiate::registerQuantifier(Node q) {} -bool Instantiate::checkComplete() +bool Instantiate::checkComplete(IncompleteId& incId) { if (!d_recordedInst.empty()) { Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl; + incId = IncompleteId::QUANTIFIERS_RECORDED_INST; return false; } return true; diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index b3c056506..b56938fd1 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -117,7 +117,7 @@ class Instantiate : public QuantifiersUtil /** identify */ std::string identify() const override { return "Instantiate"; } /** check incomplete */ - bool checkComplete() override; + bool checkComplete(IncompleteId& incId) override; //--------------------------------------rewrite objects /** add instantiation rewriter */ diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index e6d5eee76..01a51ccff 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -104,8 +104,11 @@ class QuantifiersModule * * This is called just before the quantifiers engine will return * with no lemmas added during a LAST_CALL effort check. + * + * If this method returns false, it should update incId to the reason for + * why the module was incomplete. */ - virtual bool checkComplete() { return true; } + virtual bool checkComplete(IncompleteId& incId) { return true; } /** Check was complete for quantified formula q * * If for each quantified formula q, some module returns true for diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 7cd89c7d8..90955226c 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -22,6 +22,7 @@ #include <vector> #include "expr/node.h" +#include "theory/incomplete_id.h" #include "theory/theory.h" namespace cvc5 { @@ -49,9 +50,10 @@ public: /** Check complete? * * Returns false if the utility's reasoning was globally incomplete - * (e.g. "sat" must be replaced with "incomplete"). + * (e.g. "sat" must be replaced with "incomplete"). If this method returns + * false, it should update incId to the reason for incompleteness. */ - virtual bool checkComplete() { return true; } + virtual bool checkComplete(IncompleteId& incId) { return true; } }; class QuantPhaseReq diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 6db632b11..c9ef1205c 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -616,7 +616,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) // We should set incomplete, since a "sat" answer should not be // interpreted as "infeasible", which would make a difference in the rare // case where e.g. we had a finite grammar and exhausted the grammar. - d_qim.setIncomplete(); + d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_NO_VERIFY); return false; } // otherwise we are unsat, and we will process the solution below diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0bcf1d19c..21c82e9eb 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -205,6 +205,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_qim.reset(); bool setIncomplete = false; + IncompleteId setIncompleteId = IncompleteId::QUANTIFIERS; Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl; if( needsCheck ){ @@ -354,7 +355,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ //sources of incompleteness for (QuantifiersUtil*& util : d_util) { - if (!util->checkComplete()) + if (!util->checkComplete(setIncompleteId)) { Trace("quant-engine-debug") << "Set incomplete because utility " << util->identify().c_str() @@ -372,7 +373,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ //check if we should set the incomplete flag for (QuantifiersModule*& mdl : d_modules) { - if (!mdl->checkComplete()) + if (!mdl->checkComplete(setIncompleteId)) { Trace("quant-engine-debug") << "Set incomplete because module " @@ -447,7 +448,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ { if( setIncomplete ){ Trace("quant-engine") << "Set incomplete flag." << std::endl; - d_qim.setIncomplete(); + d_qim.setIncomplete(setIncompleteId); } //output debug stats d_qim.getInstantiate()->debugPrintModel(); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 5585b36ab..db842e5a8 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -899,7 +899,7 @@ void TheorySep::postCheck(Effort level) if (needAddLemma) { - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::SEP); } Trace("sep-check") << "Sep::check(): " << level << " done, conflict=" << d_state.isInConflict() diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 3aa97672d..5001b51dd 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -41,7 +41,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, SkolemCache& skc) : d_deq(state.getSatContext()), d_termProcessed(state.getUserContext()), - d_full_check_incomplete(false), + d_fullCheckIncomplete(false), + d_fullCheckIncompleteId(IncompleteId::UNKNOWN), d_external(external), d_state(state), d_im(im), @@ -208,7 +209,8 @@ bool TheorySetsPrivate::areCareDisequal(Node a, Node b) void TheorySetsPrivate::fullEffortReset() { Assert(d_equalityEngine->consistent()); - d_full_check_incomplete = false; + d_fullCheckIncomplete = false; + d_fullCheckIncompleteId = IncompleteId::UNKNOWN; d_most_common_type.clear(); d_most_common_type_term.clear(); d_card_enabled = false; @@ -295,7 +297,8 @@ void TheorySetsPrivate::fullEffortCheck() // some kinds of cardinality we cannot handle if (d_rels->isRelationKind(nk0)) { - d_full_check_incomplete = true; + d_fullCheckIncomplete = true; + d_fullCheckIncompleteId = IncompleteId::SETS_RELS_CARD; Trace("sets-incomplete") << "Sets : incomplete because of " << n << "." << std::endl; // TODO (#1124): The issue can be divided into 4 parts @@ -789,9 +792,9 @@ void TheorySetsPrivate::postCheck(Theory::Effort level) { fullEffortCheck(); if (!d_state.isInConflict() && !d_im.hasSentLemma() - && d_full_check_incomplete) + && d_fullCheckIncomplete) { - d_im.setIncomplete(); + d_im.setIncomplete(d_fullCheckIncompleteId); } } } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index c2f266971..3c3469b07 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -122,7 +122,9 @@ class TheorySetsPrivate { * is incomplete for some reason (for instance, if we combine cardinality * with a relation or extended function kind). */ - bool d_full_check_incomplete; + bool d_fullCheckIncomplete; + /** The reason we set the above flag to true */ + IncompleteId d_fullCheckIncompleteId; std::map< Node, TypeNode > d_most_common_type; std::map< Node, Node > d_most_common_type_term; diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 6a461cb7a..f38acfac2 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1778,7 +1778,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, } else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE) { - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP); return ProcessLoopResult::SKIPPED; } @@ -1931,7 +1931,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, else if (options::stringProcessLoopMode() == options::ProcessLoopMode::SIMPLE) { - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP); return ProcessLoopResult::SKIPPED; } diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index ff3803b7e..8a0429fae 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -241,8 +241,6 @@ bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq) return true; } -void InferenceManager::setIncomplete() { d_out.setIncomplete(); } - void InferenceManager::addToExplanation(Node a, Node b, std::vector<Node>& exp) const diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index cb5560f2b..cfb8614ca 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -201,12 +201,6 @@ class InferenceManager : public InferenceManagerBuffered * otherwise. A split is trivial if a=b rewrites to a constant. */ bool sendSplit(Node a, Node b, InferenceId infer, bool preq = true); - /** - * Set that we are incomplete for the current set of assertions (in other - * words, we must answer "unknown" instead of "sat"); this calls the output - * channel's setIncomplete method. - */ - void setIncomplete(); //----------------------------constructing antecedants /** diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 7510b26ca..85d66cd54 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -303,7 +303,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) else { // otherwise we are incomplete - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY); } } if (d_state.isInConflict()) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2210caf6a..dd130e28a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -234,6 +234,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_inSatMode(false), d_hasShutDown(false), d_incomplete(context, false), + d_incompleteTheory(context, THEORY_BUILTIN), + d_incompleteId(context, IncompleteId::UNKNOWN), d_propagationMap(context), d_propagationMapTimestamp(context, 0), d_propagatedLiterals(context), @@ -1454,6 +1456,14 @@ void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId) } } +void TheoryEngine::setIncomplete(theory::TheoryId theory, + theory::IncompleteId id) +{ + d_incomplete = true; + d_incompleteTheory = theory; + d_incompleteId = id; +} + theory::TrustNode TheoryEngine::getExplanation( std::vector<NodeTheoryPair>& explanationVector) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 8960b324d..cc3de2e50 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -199,13 +199,14 @@ class TheoryEngine { * context level or below). */ context::CDO<bool> d_incomplete; + /** The theory and identifier that (most recently) set incomplete */ + context::CDO<theory::TheoryId> d_incompleteTheory; + context::CDO<theory::IncompleteId> d_incompleteId; /** * Called by the theories to notify that the current branch is incomplete. */ - void setIncomplete(theory::TheoryId theory) { - d_incomplete = true; - } + void setIncomplete(theory::TheoryId theory, theory::IncompleteId id); /** * Mapping of propagations from recievers to senders. diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index e7c89e703..1ca866871 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -517,7 +517,10 @@ void TheoryInferenceManager::safePoint(ResourceManager::Resource r) d_out.safePoint(r); } -void TheoryInferenceManager::setIncomplete() { d_out.setIncomplete(); } +void TheoryInferenceManager::setIncomplete(IncompleteId id) +{ + d_out.setIncomplete(id); +} } // namespace theory } // namespace cvc5 diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index e911fb41e..380ba6e48 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -370,7 +370,7 @@ class TheoryInferenceManager * Notification from a theory that it realizes it is incomplete at * this context level. */ - void setIncomplete(); + void setIncomplete(IncompleteId id); protected: /** diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index eb6145f9c..6ba459452 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1432,7 +1432,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){ // cardinality constraint from user input, set incomplete Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl; - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::UF_CARD_MODE); } } Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl; diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index ee3753e92..78171349d 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -227,7 +227,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) // are present if (hasFunctions) { - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::UF_HO_EXT_DISABLED); } return 0; } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9cb37a26d..e23bc0c45 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -177,7 +177,7 @@ bool TheoryUF::preNotifyFact( else { // support for cardinality constraints is not enabled, set incomplete - d_im.setIncomplete(); + d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED); } } // don't need to assert cardinality constraints if not producing models diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 9be954059..425e61bc2 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -137,7 +137,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel } void requirePhase(TNode, bool) override {} - void setIncomplete() override {} + void setIncomplete(theory::IncompleteId id) override {} void handleUserAttribute(const char* attr, theory::Theory* t) override {} void splitLemma(TNode n, bool removable = false) override { push(LEMMA, n); } |