This moves model minimization happen in TheoryUF's last call effort check instead of being a custom call in quantifiers finite model finding. This is both a better design and avoids bugs when quantifiers are not enabled (for QF_UF+cardinality constraints).
Fixes #4850.
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
-#include "theory/uf/cardinality_extension.h"
#include "theory/uf/equality_engine.h"
-#include "theory/uf/theory_uf.h"
using namespace std;
using namespace CVC4;
if( doCheck ){
Assert(!d_quantEngine->inConflict());
int addedLemmas = 0;
- FirstOrderModel* fm = d_quantEngine->getModel();
//the following will test that the model satisfies all asserted universal quantifiers by
// (model-based) exhaustive instantiation.
Trace("model-engine") << "---Model Engine Round---" << std::endl;
clSet = double(clock())/double(CLOCKS_PER_SEC);
}
-
- Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
- // Let the cardinality extension verify that the model is minimal.
- // This will if there are terms in the model that the cardinality extension
- // was not notified of.
- uf::CardinalityExtension* ufss =
- static_cast<uf::TheoryUF*>(
- d_quantEngine->getTheoryEngine()->theoryOf(THEORY_UF))
- ->getCardinalityExtension();
- if( !ufss || ufss->debugModel( fm ) ){
- Trace("model-engine-debug") << "Check model..." << std::endl;
- d_incomplete_check = false;
- //print debug
- if( Trace.isOn("fmf-model-complete") ){
- Trace("fmf-model-complete") << std::endl;
- debugPrint("fmf-model-complete");
- }
- //successfully built an acceptable model, now check it
- addedLemmas += checkModel();
- }else{
- addedLemmas++;
+ Trace("model-engine-debug") << "Check model..." << std::endl;
+ d_incomplete_check = false;
+ // print debug
+ if (Trace.isOn("fmf-model-complete"))
+ {
+ Trace("fmf-model-complete") << std::endl;
+ debugPrint("fmf-model-complete");
}
+ // successfully built an acceptable model, now check it
+ addedLemmas += checkModel();
if( Trace.isOn("model-engine") ){
double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
return d_valuation.isSatLiteral(lit);
}
+TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }
+
} // namespace theory
} // namespace CVC4
/** Returns true if lit is a SAT literal. */
virtual bool isSatLiteral(TNode lit) const;
+ /**
+ * Returns pointer to model. This model is only valid during last call effort
+ * check.
+ */
+ TheoryModel* getModel();
protected:
/** Pointer to the SAT context object used by the theory. */
}
}
-bool SortModel::debugModel( TheoryModel* m ){
+bool SortModel::checkLastCall()
+{
+ TheoryModel* m = d_state.getModel();
if( Trace.isOn("uf-ss-warn") ){
std::vector< Node > eqcs;
eq::EqClassesIterator eqcs_i =
/** check */
void CardinalityExtension::check(Theory::Effort level)
{
+ if (level == Theory::EFFORT_LAST_CALL)
+ {
+ // if last call, call last call check for each sort
+ for (std::pair<const TypeNode, SortModel*>& r : d_rep_model)
+ {
+ if (!r.second->checkLastCall())
+ {
+ break;
+ }
+ }
+ return;
+ }
if (!d_state.isInConflict())
{
if (options::ufssMode() == options::UfssMode::FULL)
}
}
-bool CardinalityExtension::debugModel(TheoryModel* m)
-{
- for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
- if( !it->second->debugModel( m ) ){
- return false;
- }
- }
- return true;
-}
-
/** initialize */
void CardinalityExtension::initializeCombinedCardinality()
{
int getMaximumNegativeCardinality() { return d_maxNegCard.get(); }
//print debug
void debugPrint( const char* c );
- /** debug a model */
- bool debugModel( TheoryModel* m );
+ /**
+ * Check at last call effort. This will verify that the model is minimal.
+ * This return lemmas if there are terms in the model that the cardinality
+ * extension was not notified of.
+ *
+ * @return false if current model is not minimal. In this case, lemmas are
+ * sent on the output channel of the UF theory.
+ */
+ bool checkLastCall();
/** get number of regions (for debugging) */
int getNumRegions();
std::string identify() const { return std::string("CardinalityExtension"); }
//print debug
void debugPrint( const char* c );
- /** debug a model */
- bool debugModel( TheoryModel* m );
/** get cardinality for node */
int getCardinality( Node n );
/** get cardinality for type */
//--------------------------------- standard check
+bool TheoryUF::needsCheckLastEffort()
+{
+ // last call effort needed if using finite model finding
+ return d_thss != nullptr;
+}
+
void TheoryUF::postCheck(Effort level)
{
if (d_state.isInConflict())
{
d_thss->check(level);
}
- // check with the higher-order extension
+ // check with the higher-order extension at full effort
if (!d_state.isInConflict() && fullEffort(level))
{
if (options::ufHo())
//--------------------------------- end initialization
//--------------------------------- standard check
+ /** Do we need a check call at last call effort? */
+ bool needsCheckLastEffort() override;
/** Post-check, called after the fact queue of the theory is processed. */
void postCheck(Effort level) override;
/** Pre-notify fact, return true if processed. */
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
std::string identify() const override { return "THEORY_UF"; }
-
- /** get a pointer to the uf with cardinality */
- CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
-
private:
/** Explain why this literal is true by building an explanation */
void explain(TNode literal, Node& exp);
Node getModelValue(TNode var);
/**
- * Returns pointer to model.
+ * Returns pointer to model. This model is only valid during last call effort
+ * check.
*/
TheoryModel* getModel();
--- /dev/null
+(set-logic UFC)
+(set-info :status sat)
+(declare-sort a 0)
+(declare-fun b () a)
+(assert (not (fmf.card b 1)))
+(check-sat)
projects / cvc5.git / commitdiff