This PR classifies all internal kinds of incompleteness as identifiers.
It makes it so TheoryEngine records an identifier when its incomplete flag is set.
The next step will be to possibly communicate this value to the user.
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
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;
}
}
else if (d_internal->foundNonlinear())
{
// set incomplete
- d_im.setIncomplete();
+ d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED);
}
}
}
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)
void requirePhase(TNode n, bool phase) override;
- void setIncomplete() override;
+ void setIncomplete(IncompleteId id) override;
void spendResource(ResourceManager::Resource r) override;
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
#include "cvc4_private.h"
-#include <iosfwd>
-
#ifndef CVC4__THEORY__INFERENCE_ID_H
#define CVC4__THEORY__INFERENCE_ID_H
+#include <iosfwd>
+
namespace cvc5 {
namespace theory {
#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"
* 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
}
}
-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;
/** 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 */
}
}
-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 ) {
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;
}
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;
/** identify */
std::string identify() const override { return "Instantiate"; }
/** check incomplete */
- bool checkComplete() override;
+ bool checkComplete(IncompleteId& incId) override;
//--------------------------------------rewrite objects
/** add instantiation rewriter */
*
* 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
#include <vector>
#include "expr/node.h"
+#include "theory/incomplete_id.h"
#include "theory/theory.h"
namespace cvc5 {
/** 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
// 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
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 ){
//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()
//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 "
{
if( setIncomplete ){
Trace("quant-engine") << "Set incomplete flag." << std::endl;
- d_qim.setIncomplete();
+ d_qim.setIncomplete(setIncompleteId);
}
//output debug stats
d_qim.getInstantiate()->debugPrintModel();
if (needAddLemma)
{
- d_im.setIncomplete();
+ d_im.setIncomplete(IncompleteId::SEP);
}
Trace("sep-check") << "Sep::check(): " << level
<< " done, conflict=" << d_state.isInConflict()
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),
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;
// 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
{
fullEffortCheck();
if (!d_state.isInConflict() && !d_im.hasSentLemma()
- && d_full_check_incomplete)
+ && d_fullCheckIncomplete)
{
- d_im.setIncomplete();
+ d_im.setIncomplete(d_fullCheckIncompleteId);
}
}
}
* 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;
}
else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE)
{
- d_im.setIncomplete();
+ d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP);
return ProcessLoopResult::SKIPPED;
}
else if (options::stringProcessLoopMode()
== options::ProcessLoopMode::SIMPLE)
{
- d_im.setIncomplete();
+ d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP);
return ProcessLoopResult::SKIPPED;
}
return true;
}
-void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
-
void InferenceManager::addToExplanation(Node a,
Node b,
std::vector<Node>& exp) const
* 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
/**
else
{
// otherwise we are incomplete
- d_im.setIncomplete();
+ d_im.setIncomplete(IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY);
}
}
if (d_state.isInConflict())
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),
}
}
+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)
{
* 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.
d_out.safePoint(r);
}
-void TheoryInferenceManager::setIncomplete() { d_out.setIncomplete(); }
+void TheoryInferenceManager::setIncomplete(IncompleteId id)
+{
+ d_out.setIncomplete(id);
+}
} // namespace theory
} // namespace cvc5
* Notification from a theory that it realizes it is incomplete at
* this context level.
*/
- void setIncomplete();
+ void setIncomplete(IncompleteId id);
protected:
/**
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;
// are present
if (hasFunctions)
{
- d_im.setIncomplete();
+ d_im.setIncomplete(IncompleteId::UF_HO_EXT_DISABLED);
}
return 0;
}
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
}
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); }
projects / cvc5.git / commitdiff