* @param polarity Its polarity
* @param fact The original literal that was asserted
* @param isPrereg Whether the assertion is preregistered
+ * @param isInternal Whether the origin of the fact was internal. If this
+ * is false, the fact was asserted via the fact queue of the theory.
* @return true if the theory completely processed this fact, i.e. it does
* not need to assert the fact to its equality engine.
*/
- virtual bool preNotifyFact(TNode atom, bool pol, TNode fact, bool isPrereg);
+ virtual bool preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal);
/**
* Notify fact, called immediately after the fact was pushed into the
* equality engine.
*
* @param atom The atom
* @param polarity Its polarity
- * @param fact The original literal that was asserted
- * @param isInternal Whether the origin of the fact was internal
+ * @param fact The original literal that was asserted.
+ * @param isInternal Whether the origin of the fact was internal. If this
+ * is false, the fact was asserted via the fact queue of the theory.
*/
virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal);
//--------------------------------- end check
* The argument termSet is the set of relevant terms returned by
* computeRelevantTerms.
*/
- virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet);
+ virtual bool collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet);
/** if theories want to do something with model after building, do it here */
virtual void postProcessModel( TheoryModel* m ){ }
//--------------------------------- end collect model info
namespace theory {
namespace uf {
-HoExtension::HoExtension(TheoryUF& p,
- context::Context* c,
- context::UserContext* u)
- : d_parent(p), d_extensionality(u), d_uf_std_skolem(u)
+HoExtension::HoExtension(TheoryUF& p, TheoryState& state)
+ : d_parent(p),
+ d_state(state),
+ d_extensionality(state.getUserContext()),
+ d_uf_std_skolem(state.getUserContext())
{
d_true = NodeManager::currentNM()->mkConst(true);
}
unsigned HoExtension::checkExtensionality(TheoryModel* m)
{
- eq::EqualityEngine* ee = d_parent.getEqualityEngine();
+ eq::EqualityEngine* ee = d_state.getEqualityEngine();
NodeManager* nm = NodeManager::currentNM();
unsigned num_lemmas = 0;
bool isCollectModel = (m != nullptr);
{
Assert(n.getKind() == APPLY_UF);
- eq::EqualityEngine* ee = d_parent.getEqualityEngine();
+ eq::EqualityEngine* ee = d_state.getEqualityEngine();
// must expand into APPLY_HO version if not there already
Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n);
if (!ee->hasTerm(ret) || !ee->areEqual(ret, n))
Trace("uf-ho") << "HoExtension::checkApplyCompletion..." << std::endl;
// compute the operators that are relevant (those for which an HO_APPLY exist)
std::set<TNode> rlvOp;
- eq::EqualityEngine* ee = d_parent.getEqualityEngine();
+ eq::EqualityEngine* ee = d_state.getEqualityEngine();
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
std::map<TNode, std::vector<Node> > apply_uf;
while (!eqcs_i.isFinished())
do
{
num_facts = checkAppCompletion();
- if (d_parent.inConflict())
+ if (d_state.isInConflict())
{
Trace("uf-ho") << "...conflict during app-completion." << std::endl;
return 1;
return 0;
}
-bool HoExtension::collectModelInfoHo(std::set<Node>& termSet, TheoryModel* m)
+bool HoExtension::collectModelInfoHo(TheoryModel* m,
+ const std::set<Node>& termSet)
{
for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it)
{
* so make sure it's initialized first. */
d_thss(nullptr),
d_ho(nullptr),
- d_conflict(c, false),
d_functionsTerms(c),
d_symb(u, instanceName),
d_state(c, u, valuation)
// Initialize the cardinality constraints solver if the logic includes UF,
// finite model finding is enabled, and it is not disabled by
// options::ufssMode().
- if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind()
+ if (options::finiteModelFind()
&& options::ufssMode() != options::UfssMode::NONE)
{
d_thss.reset(new CardinalityExtension(
if (options::ufHo())
{
d_equalityEngine->addFunctionKind(kind::HO_APPLY);
- d_ho.reset(new HoExtension(*this, getSatContext(), getUserContext()));
+ d_ho.reset(new HoExtension(*this, d_state));
}
}
return conjunction;
}/* mkAnd() */
-void TheoryUF::check(Effort level) {
- if (done() && !fullEffort(level)) {
+//--------------------------------- standard check
+
+void TheoryUF::postCheck(Effort level)
+{
+ if (d_state.isInConflict())
+ {
return;
}
- getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep);
- TimerStat::CodeTimer checkTimer(d_checkTime);
-
- while (!done() && !d_conflict)
+ // check with the cardinality constraints extension
+ if (d_thss != nullptr)
{
- // Get all the assertions
- Assertion assertion = get();
- TNode fact = assertion.d_assertion;
-
- Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
- Debug("uf") << "Term's theory: " << theory::Theory::theoryOf(fact.toExpr()) << std::endl;
-
- if (d_thss != NULL) {
- bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
- d_thss->assertNode(fact, isDecision);
- if( d_thss->isConflict() ){
- d_conflict = true;
- return;
- }
+ d_thss->check(level);
+ if (d_thss->isConflict())
+ {
+ d_state.notifyInConflict();
}
+ }
+ // check with the higher-order extension
+ if (!d_state.isInConflict() && fullEffort(level))
+ {
+ if (options::ufHo())
+ {
+ d_ho->check();
+ }
+ }
+}
- // Do the work
- bool polarity = fact.getKind() != kind::NOT;
- TNode atom = polarity ? fact : fact[0];
- if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine->assertEquality(atom, polarity, fact);
- if( options::ufHo() && options::ufHoExt() ){
- if( !polarity && !d_conflict && atom[0].getType().isFunction() ){
- // apply extensionality eagerly using the ho extension
- d_ho->applyExtensionality(fact);
- }
- }
- } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) {
- if( d_thss == NULL ){
- if( !getLogicInfo().hasCardinalityConstraints() ){
- std::stringstream ss;
- ss << "Cardinality constraint " << atom << " was asserted, but the logic does not allow it." << std::endl;
- ss << "Try using a logic containing \"UFC\"." << std::endl;
- throw Exception( ss.str() );
- }else{
- // support for cardinality constraints is not enabled, set incomplete
- d_out->setIncomplete();
- }
+bool TheoryUF::preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+ if (d_thss != nullptr)
+ {
+ bool isDecision =
+ d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
+ d_thss->assertNode(fact, isDecision);
+ if (d_thss->isConflict())
+ {
+ d_state.notifyInConflict();
+ return true;
+ }
+ }
+ if (atom.getKind() == kind::CARDINALITY_CONSTRAINT
+ || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT)
+ {
+ if (d_thss == nullptr)
+ {
+ if (!getLogicInfo().hasCardinalityConstraints())
+ {
+ std::stringstream ss;
+ ss << "Cardinality constraint " << atom
+ << " was asserted, but the logic does not allow it." << std::endl;
+ ss << "Try using a logic containing \"UFC\"." << std::endl;
+ throw Exception(ss.str());
}
- //needed for models
- if( options::produceModels() ){
- d_equalityEngine->assertPredicate(atom, polarity, fact);
+ else
+ {
+ // support for cardinality constraints is not enabled, set incomplete
+ d_out->setIncomplete();
}
- } else {
- d_equalityEngine->assertPredicate(atom, polarity, fact);
}
+ // don't need to assert cardinality constraints if not producing models
+ return !options::produceModels();
}
+ return false;
+}
- if(! d_conflict ){
- // check with the cardinality constraints extension
- if (d_thss != NULL) {
- d_thss->check(level);
- if( d_thss->isConflict() ){
- d_conflict = true;
- }
- }
- // check with the higher-order extension
- if(! d_conflict && fullEffort(level) ){
- if( options::ufHo() ){
- d_ho->check();
+void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
+{
+ if (!d_state.isInConflict() && atom.getKind() == kind::EQUAL)
+ {
+ if (options::ufHo() && options::ufHoExt())
+ {
+ if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction())
+ {
+ // apply extensionality eagerly using the ho extension
+ d_ho->applyExtensionality(fact);
}
}
}
-}/* TheoryUF::check() */
+}
+//--------------------------------- end standard check
TrustNode TheoryUF::expandDefinition(Node node)
{
return TrustNode::null();
}
-void TheoryUF::preRegisterTerm(TNode node) {
+void TheoryUF::preRegisterTerm(TNode node)
+{
Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
if (d_thss != NULL) {
d_equalityEngine->addTerm(node);
break;
}
-}/* TheoryUF::preRegisterTerm() */
+}
bool TheoryUF::propagateLit(TNode literal)
{
Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal << ")"
<< std::endl;
// If already in conflict, no more propagation
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal
<< "): already in conflict" << std::endl;
return false;
// Propagate out
bool ok = d_out->propagate(literal);
if (!ok) {
- d_conflict = true;
+ d_state.notifyInConflict();
}
return ok;
}/* TheoryUF::propagate(TNode) */
return mkAnd(assumptions);
}
-bool TheoryUF::collectModelInfo(TheoryModel* m)
+bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
{
- Debug("uf") << "UF : collectModelInfo " << std::endl;
- set<Node> termSet;
-
- // Compute terms appearing in assertions and shared terms
- computeRelevantTerms(termSet);
-
- if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
- {
- Trace("uf") << "Collect model info fail UF" << std::endl;
- return false;
- }
-
if( options::ufHo() ){
// must add extensionality disequalities for all pairs of (non-disequal)
// function equivalence classes.
- if (!d_ho->collectModelInfoHo(termSet, m))
+ if (!d_ho->collectModelInfoHo(m, termSet))
{
Trace("uf") << "Collect model info fail HO" << std::endl;
return false;
return EQUALITY_FALSE_IN_MODEL;
}
-void TheoryUF::notifySharedTerm(TNode t)
-{
- Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
- d_equalityEngine->addTriggerTerm(t, THEORY_UF);
-}
-
bool TheoryUF::areCareDisequal(TNode x, TNode y){
Assert(d_equalityEngine->hasTerm(x));
Assert(d_equalityEngine->hasTerm(y));
void TheoryUF::conflict(TNode a, TNode b) {
std::shared_ptr<eq::EqProof> pf =
d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr;
- d_conflictNode = explain(a.eqNode(b), pf.get());
+ Node conf = explain(a.eqNode(b), pf.get());
std::unique_ptr<ProofUF> puf(d_proofsEnabled ? new ProofUF(pf) : nullptr);
- d_out->conflict(d_conflictNode, std::move(puf));
- d_conflict = true;
+ d_out->conflict(conf, std::move(puf));
+ d_state.notifyInConflict();
}
void TheoryUF::eqNotifyNewClass(TNode t) {
/** the higher-order solver extension (or nullptr if it does not exist) */
std::unique_ptr<HoExtension> d_ho;
- /** Are we in conflict */
- context::CDO<bool> d_conflict;
-
- /** The conflict node */
- Node d_conflictNode;
-
-
/** node for true */
Node d_true;
void finishInit() override;
//--------------------------------- end initialization
- void check(Effort) override;
+ //--------------------------------- standard check
+ /** Post-check, called after the fact queue of the theory is processed. */
+ void postCheck(Effort level) override;
+ /** Pre-notify fact, return true if processed. */
+ bool preNotifyFact(TNode atom,
+ bool pol,
+ TNode fact,
+ bool isPrereg,
+ bool isInternal) override;
+ /** Notify fact */
+ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+ //--------------------------------- end standard check
+
+ /** Collect model values in m based on the relevant terms given by termSet */
+ bool collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet) override;
+
TrustNode expandDefinition(Node node) override;
void preRegisterTerm(TNode term) override;
TrustNode explain(TNode n) override;
- bool collectModelInfo(TheoryModel* m) override;
void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
void presolve() override;
- void notifySharedTerm(TNode n) override;
void computeCareGraph() override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
/** get a pointer to the uf with cardinality */
CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
- /** are we in conflict? */
- bool inConflict() const { return d_conflict; }
private:
bool areCareDisequal(TNode x, TNode y);
projects / cvc5.git / commitdiff