void TheoryArith::propagate(Effort e) {
d_internal->propagate(e);
}
-
-void TheoryArith::collectModelInfo( TheoryModel* m ){
- d_internal->collectModelInfo(m);
+bool TheoryArith::collectModelInfo(TheoryModel* m)
+{
+ return d_internal->collectModelInfo(m);
}
void TheoryArith::notifyRestart(){
bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp );
- void collectModelInfo( TheoryModel* m );
+ bool collectModelInfo(TheoryModel* m) override;
void shutdown(){ }
return belowMin;
}
-void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){
+bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
+{
AlwaysAssert(d_qflraStatus == Result::SAT);
//AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
Node qNode = mkRationalNode(qmodel);
Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
- m->assertEquality(term, qNode, true);
+ if (!m->assertEquality(term, qNode, true))
+ {
+ return false;
+ }
}else{
Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl;
// m->assertEqualityEngine(&ee);
Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl;
+ return true;
}
bool TheoryArithPrivate::safeToReset() const {
Rational deltaValueForTotalOrder() const;
- void collectModelInfo( TheoryModel* m );
+ bool collectModelInfo(TheoryModel* m);
void shutdown(){ }
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
-
-void TheoryArrays::collectModelInfo( TheoryModel* m )
+bool TheoryArrays::collectModelInfo(TheoryModel* m)
{
set<Node> termSet;
} while (changed);
// Send the equality engine information to the model
- m->assertEqualityEngine(&d_equalityEngine, &termSet);
+ if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ {
+ return false;
+ }
// Build a list of all the relevant reads, indexed by the store representative
std::map<Node, std::vector<Node> > selects;
for (unsigned j = 0; j < reads.size(); ++j) {
rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]);
}
- m->assertEquality(n, rep, true);
+ if (!m->assertEquality(n, rep, true))
+ {
+ return false;
+ }
if (!n.isConst()) {
- m->assertRepresentative(rep);
+ m->assertSkeleton(rep);
}
}
+ return true;
}
/////////////////////////////////////////////////////////////////////////////
private:
public:
+ bool collectModelInfo(TheoryModel* m) override;
- void collectModelInfo(TheoryModel* m);
-
- /////////////////////////////////////////////////////////////////////////////
- // NOTIFICATIONS
- /////////////////////////////////////////////////////////////////////////////
+ /////////////////////////////////////////////////////////////////////////////
+ // NOTIFICATIONS
+ /////////////////////////////////////////////////////////////////////////////
private:
public:
* @param fullModel whether to create a "full model," i.e., add
* constants to equivalence classes that don't already have them
*/
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
void setProofLog( BitVectorProof * bvp );
typedef TNodeSet::const_iterator vars_iterator;
bool assertToSat(TNode node, bool propagate = true);
bool solve();
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
void setProofLog( BitVectorProof * bvp );
};
return true;
}
-void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
AlwaysAssert(!d_useAig && d_bitblaster);
- d_bitblaster->collectModelInfo(m, fullModel);
+ return d_bitblaster->collectModelInfo(m, fullModel);
}
void EagerBitblastSolver::setProofLog(BitVectorProof* bvp) { d_bvp = bvp; }
void turnOffAig();
bool isInitialized();
void initialize();
- void collectModelInfo(theory::TheoryModel* m, bool fullModel);
+ bool collectModelInfo(theory::TheoryModel* m, bool fullModel);
void setProofLog(BitVectorProof* bvp);
private:
}
}
-void BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel) {
- d_bitblaster->collectModelInfo(model, fullModel);
+bool BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel)
+{
+ return d_bitblaster->collectModelInfo(model, fullModel);
}
BVQuickCheck::~BVQuickCheck() {
* @return
*/
uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
- void collectModelInfo(theory::TheoryModel* model, bool fullModel);
+ bool collectModelInfo(theory::TheoryModel* model, bool fullModel);
typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
vars_iterator beginVars();
virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
virtual void preRegister(TNode node) {}
virtual void propagate(Theory::Effort e) {}
- virtual void collectModelInfo(TheoryModel* m, bool fullModel) = 0;
+ virtual bool collectModelInfo(TheoryModel* m, bool fullModel) = 0;
virtual Node getModelValue(TNode var) = 0;
virtual bool isComplete() = 0;
virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) {
return EQUALITY_UNKNOWN;
}
-void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
+bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
+{
Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
AlwaysAssert (!d_quickSolver->inConflict());
set<Node> termSet;
Debug("bitvector-model") << "AlgebraicSolver: " << variables[i] << " => " << subst << "\n";
// Doesn't have to be constant as it may be irrelevant
Assert (subst.getKind() == kind::CONST_BITVECTOR);
- model->assertEquality(variables[i], subst, true);
+ if (!model->assertEquality(variables[i], subst, true))
+ {
+ return false;
+ }
}
-
+ return true;
}
Node AlgebraicSolver::getModelValue(TNode node) {
void preRegister(TNode node) {}
bool check(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions) {Unreachable("AlgebraicSolver does not propagate.\n");}
- EqualityStatus getEqualityStatus(TNode a, TNode b);
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
Node getModelValue(TNode node);
bool isComplete();
virtual void assertFact(TNode fact);
return d_bitblaster->getEqualityStatus(a, b);
}
-void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
return d_bitblaster->collectModelInfo(m, fullModel);
}
bool check(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
EqualityStatus getEqualityStatus(TNode a, TNode b);
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
Node getModelValue(TNode node);
bool isComplete() { return true; }
void bitblastQueue();
return utils::isEqualityTerm(term, seen);
}
-void CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
if (d_useSlicer) {
Unreachable();
}
}
set<Node> termSet;
d_bv->computeRelevantTerms(termSet);
- m->assertEqualityEngine(&d_equalityEngine, &termSet);
+ if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ {
+ return false;
+ }
if (isComplete()) {
Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
Node a = it->first;
Node b = it->second;
Debug("bitvector-model") << "CoreSolver::collectModelInfo modelValues "
- << a << " => " << b <<")\n";
- m->assertEquality(a, b, true);
+ << a << " => " << b <<")\n";
+ if (!m->assertEquality(a, b, true))
+ {
+ return false;
+ }
}
}
+ return true;
}
Node CoreSolver::getModelValue(TNode var) {
void preRegister(TNode node);
bool check(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
Node getModelValue(TNode var);
void addSharedTerm(TNode t) {
d_equalityEngine.addTriggerTerm(t, THEORY_BV);
void InequalitySolver::propagate(Theory::Effort e) {
Assert (false);
}
-
-void InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n";
std::vector<Node> model;
d_inequalityGraph.getAllValuesInModel(model);
for (unsigned i = 0; i < model.size(); ++i) {
Assert (model[i].getKind() == kind::EQUAL);
- m->assertEquality(model[i][0], model[i][1], true);
+ if (!m->assertEquality(model[i][0], model[i][1], true))
+ {
+ return false;
+ }
}
+ return true;
}
Node InequalitySolver::getModelValue(TNode var) {
void propagate(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
bool isComplete() { return d_isComplete; }
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
Node getModelValue(TNode var);
EqualityStatus getEqualityStatus(TNode a, TNode b);
void assertFact(TNode fact);
return utils::mkConst(BitVector(bits.size(), value));
}
-void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
+{
TNodeSet::iterator it = d_variables.begin();
for (; it != d_variables.end(); ++it) {
TNode var = *it;
Debug("bitvector-model")
<< "EagerBitblaster::collectModelInfo (assert (= " << var << " "
<< const_value << "))\n";
- m->assertEquality(var, const_value, true);
+ if (!m->assertEquality(var, const_value, true))
+ {
+ return false;
+ }
}
}
}
+ return true;
}
void EagerBitblaster::setProofLog(BitVectorProof* bvp) {
return utils::mkConst(BitVector(bits.size(), value));
}
-void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
+{
std::set<Node> termSet;
d_bv->computeRelevantTerms(termSet);
Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
<< var << " "
<< const_value << "))\n";
- m->assertEquality(var, const_value, true);
+ if (!m->assertEquality(var, const_value, true))
+ {
+ return false;
+ }
}
}
+ return true;
}
void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){
bool TheoryBV::needsCheckLastEffort() {
return d_needsLastCallCheck;
}
-
-void TheoryBV::collectModelInfo( TheoryModel* m ){
+bool TheoryBV::collectModelInfo(TheoryModel* m)
+{
Assert(!inConflict());
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- d_eagerSolver->collectModelInfo(m, true);
+ if (!d_eagerSolver->collectModelInfo(m, true))
+ {
+ return false;
+ }
}
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
if (d_subtheories[i]->isComplete()) {
- d_subtheories[i]->collectModelInfo(m, true);
- return;
+ return d_subtheories[i]->collectModelInfo(m, true);
}
}
+ return true;
}
Node TheoryBV::getModelValue(TNode var) {
Node explain(TNode n);
- void collectModelInfo( TheoryModel* m );
+ bool collectModelInfo(TheoryModel* m) override;
std::string identify() const { return std::string("TheoryBV"); }
Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
}
-void TheoryDatatypes::collectModelInfo( TheoryModel* m ){
+bool TheoryDatatypes::collectModelInfo(TheoryModel* m)
+{
Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine.consistent() << std::endl;
Trace("dt-model") << std::endl;
printModelDebug( "dt-model" );
getRelevantTerms(termSet);
//combine the equality engine
- m->assertEqualityEngine( &d_equalityEngine, &termSet );
+ if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ {
+ return false;
+ }
//get all constructors
eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
}
if( !neqc.isNull() ){
Trace("dt-cmi") << "Assign : " << neqc << std::endl;
- m->assertEquality( eqc, neqc, true );
+ if (!m->assertEquality(eqc, neqc, true))
+ {
+ return false;
+ }
eqc_cons[ eqc ] = neqc;
}
if( addCons ){
std::map< Node, int > vmap;
Node v = getCodatatypesValue( it->first, eqc_cons, vmap, 0 );
Trace("dt-cmi") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl;
- m->assertEquality( eqc, v, true );
- m->assertRepresentative( v );
+ if (!m->assertEquality(eqc, v, true))
+ {
+ return false;
+ }
+ m->assertSkeleton(v);
}
}else{
Trace("dt-cmi") << "Datatypes : assert representative " << it->second << " for " << it->first << std::endl;
- m->assertRepresentative( it->second );
+ m->assertSkeleton(it->second);
}
}
+ return true;
}
void presolve();
void addSharedTerm(TNode t);
EqualityStatus getEqualityStatus(TNode a, TNode b);
- void collectModelInfo( TheoryModel* m );
+ bool collectModelInfo(TheoryModel* m) override;
void shutdown() { }
std::string identify() const { return std::string("TheoryDatatypes"); }
/** equality engine */
return d_conv.getValue(d_valuation, var);
}
-void TheoryFp::collectModelInfo(TheoryModel *m) {
+bool TheoryFp::collectModelInfo(TheoryModel *m)
+{
std::set<Node> relevantTerms;
Trace("fp-collectModelInfo")
<< "TheoryFp::collectModelInfo(): relevantVariable " << node
<< std::endl;
- m->assertEquality(node, d_conv.getValue(d_valuation, node), true);
+ if (!m->assertEquality(node, d_conv.getValue(d_valuation, node), true))
+ {
+ return false;
+ }
}
- return;
+ return true;
}
bool TheoryFp::NotifyClass::eqNotifyTriggerEquality(TNode equality,
void check(Effort);
Node getModelValue(TNode var);
- void collectModelInfo(TheoryModel* m);
+ bool collectModelInfo(TheoryModel* m) override;
std::string identify() const { return "THEORY_FP"; }
//do nothing
}
-void TheoryQuantifiers::collectModelInfo(TheoryModel* m) {
+bool TheoryQuantifiers::collectModelInfo(TheoryModel* m)
+{
for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
if((*i).assertion.getKind() == kind::NOT) {
Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
- m->assertPredicate((*i).assertion[0], false);
+ if (!m->assertPredicate((*i).assertion[0], false))
+ {
+ return false;
+ }
} else {
Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
- m->assertPredicate(*i, true);
+ if (!m->assertPredicate(*i, true))
+ {
+ return false;
+ }
}
}
+ return true;
}
void TheoryQuantifiers::check(Effort e) {
void check(Effort e);
Node getNextDecisionRequest( unsigned& priority );
Node getValue(TNode n);
- void collectModelInfo( TheoryModel* m );
+ bool collectModelInfo(TheoryModel* m) override;
void shutdown() { }
std::string identify() const { return std::string("TheoryQuantifiers"); }
void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
static_cast<QuantifiersModule::QEffort>(qef);
d_curr_effort_level = quant_e;
//build the model if any module requested it
- if( needsModelE==quant_e && !d_model->isBuilt() ){
- // theory engine's model builder is quantifier engine's builder if it has one
- Assert( !d_builder || d_builder==d_te->getModelBuilder() );
- Trace("quant-engine-debug") << "Build model..." << std::endl;
- if( !d_te->getModelBuilder()->buildModel( d_model ) ){
- //we are done if model building was unsuccessful
- Trace("quant-engine-debug") << "...added lemmas." << std::endl;
- flushLemmas();
+ if (needsModelE == quant_e)
+ {
+ if (!d_model->isBuilt())
+ {
+ // theory engine's model builder is quantifier engine's builder if it
+ // has one
+ Assert(!d_builder || d_builder == d_te->getModelBuilder());
+ Trace("quant-engine-debug") << "Build model..." << std::endl;
+ if (!d_te->getModelBuilder()->buildModel(d_model))
+ {
+ flushLemmas();
+ }
+ }
+ if (!d_model->isBuiltSuccess())
+ {
+ break;
}
}
if( !d_hasAddedLemma ){
//SAT case
if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
- if( options::produceModels() ){
- if( d_model->isBuilt() ){
- Trace("quant-engine-debug") << "Already built model using model builder, finish..." << std::endl;
- }else{
- //use default model builder when no module built the model
- Trace("quant-engine-debug") << "Build the default model..." << std::endl;
- d_te->getModelBuilder()->buildModel( d_model );
- Trace("quant-engine-debug") << "Done building the model." << std::endl;
- }
- }
if( setIncomplete ){
Trace("quant-engine") << "Set incomplete flag." << std::endl;
getOutputChannel().setIncomplete();
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
-
-void TheorySep::collectModelInfo( TheoryModel* m ){
+bool TheorySep::collectModelInfo(TheoryModel* m)
+{
set<Node> termSet;
// Compute terms appearing in assertions and shared terms
computeRelevantTerms(termSet);
// Send the equality engine information to the model
- m->assertEqualityEngine( &d_equalityEngine, &termSet );
+ return m->assertEqualityEngine(&d_equalityEngine, &termSet);
}
void TheorySep::postProcessModel( TheoryModel* m ){
/////////////////////////////////////////////////////////////////////////////
public:
+ bool collectModelInfo(TheoryModel* m) override;
+ void postProcessModel(TheoryModel* m);
- void collectModelInfo(TheoryModel* m);
- void postProcessModel(TheoryModel* m);
-
- /////////////////////////////////////////////////////////////////////////////
- // NOTIFICATIONS
- /////////////////////////////////////////////////////////////////////////////
+ /////////////////////////////////////////////////////////////////////////////
+ // NOTIFICATIONS
+ /////////////////////////////////////////////////////////////////////////////
private:
public:
return d_internal->needsCheckLastEffort();
}
-void TheorySets::collectModelInfo(TheoryModel* m) {
- d_internal->collectModelInfo(m);
+bool TheorySets::collectModelInfo(TheoryModel* m)
+{
+ return d_internal->collectModelInfo(m);
}
void TheorySets::computeCareGraph() {
bool needsCheckLastEffort();
- void collectModelInfo(TheoryModel* m);
+ bool collectModelInfo(TheoryModel* m) override;
void computeCareGraph();
/******************** Model generation ********************/
/******************** Model generation ********************/
-
-void TheorySetsPrivate::collectModelInfo(TheoryModel* m) {
+bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
+{
Trace("sets-model") << "Set collect model info" << std::endl;
set<Node> termSet;
// Compute terms appearing in assertions and shared terms
d_external.computeRelevantTerms(termSet);
// Assert equalities and disequalities to the model
- m->assertEqualityEngine(&d_equalityEngine,&termSet);
-
+ if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ {
+ return false;
+ }
+
std::map< Node, Node > mvals;
for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
Node eqc = d_set_eqc[i];
rep = Rewriter::rewrite( rep );
Trace("sets-model") << "* Assign representative of " << eqc << " to " << rep << std::endl;
mvals[eqc] = rep;
- m->assertEquality( eqc, rep, true );
- m->assertRepresentative( rep );
+ if (!m->assertEquality(eqc, rep, true))
+ {
+ return false;
+ }
+ m->assertSkeleton(rep);
}
}
+ return true;
}
/********************** Helper functions ***************************/
bool needsCheckLastEffort();
- void collectModelInfo(TheoryModel* m);
+ bool collectModelInfo(TheoryModel* m);
void computeCareGraph();
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
-
-void TheoryStrings::collectModelInfo( TheoryModel* m ) {
+bool TheoryStrings::collectModelInfo(TheoryModel* m)
+{
Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl;
Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
// Compute terms appearing in assertions and shared terms
//computeRelevantTerms(termSet);
//m->assertEqualityEngine( &d_equalityEngine, &termSet );
-
- m->assertEqualityEngine( &d_equalityEngine );
-
+
+ if (!m->assertEqualityEngine(&d_equalityEngine))
+ {
+ return false;
+ }
+
// Generate model
std::vector< Node > nodes;
getEquivalenceClasses( nodes );
++sel;
Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl;
processed[pure_eq[j]] = c;
- m->assertEquality( pure_eq[j], c, true );
+ if (!m->assertEquality(pure_eq[j], c, true))
+ {
+ return false;
+ }
}
}
}
Assert( cc.getKind()==kind::CONST_STRING );
Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl;
processed[nodes[i]] = cc;
- m->assertEquality( nodes[i], cc, true );
+ if (!m->assertEquality(nodes[i], cc, true))
+ {
+ return false;
+ }
}
}
//Trace("strings-model") << "String Model : Assigned." << std::endl;
Trace("strings-model") << "String Model : Finished." << std::endl;
+ return true;
}
/////////////////////////////////////////////////////////////////////////////
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
public:
- void collectModelInfo(TheoryModel* m);
+ bool collectModelInfo(TheoryModel* m) override;
- /////////////////////////////////////////////////////////////////////////////
- // NOTIFICATIONS
- /////////////////////////////////////////////////////////////////////////////
+ /////////////////////////////////////////////////////////////////////////////
+ // NOTIFICATIONS
+ /////////////////////////////////////////////////////////////////////////////
public:
void presolve();
void shutdown() { }
* Get all relevant information in this theory regarding the current
* model. This should be called after a call to check( FULL_EFFORT )
* for all theories with no conflicts and no lemmas added.
+ *
+ * This method returns true if and only if the equality engine of m is
+ * consistent as a result of this call.
*/
- virtual void collectModelInfo( TheoryModel* m ){ }
-
+ virtual bool collectModelInfo(TheoryModel* m) { return true; }
/** if theories want to do something with model after building, do it here */
virtual void postProcessModel( TheoryModel* m ){ }
/**
if( theory->needsCheckLastEffort() ){
if( !d_curr_model->isBuilt() ){
if( !d_curr_model_builder->buildModel(d_curr_model) ){
- //model building should fail only if the model builder adds lemmas
- Assert( needCheck() );
break;
}
}
}
if( ! d_inConflict && ! needCheck() ){
if(d_logicInfo.isQuantified()) {
- // quantifiers engine must pass effort last call check
+ // quantifiers engine must check at last call effort
d_quantEngine->check(Theory::EFFORT_LAST_CALL);
- // if returning incomplete or SAT, we have ensured that d_curr_model has been built
- } else if(options::produceModels() && !d_curr_model->isBuilt()) {
+ }
+ }
+ if (!d_inConflict && !needCheck())
+ {
+ if (options::produceModels() && !d_curr_model->isBuilt())
+ {
// must build model at this point
d_curr_model_builder->buildModel(d_curr_model);
}
Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
- //we will answer SAT
+ // case where we are about to answer SAT
if( d_masterEqualityEngine != NULL ){
AlwaysAssert(d_masterEqualityEngine->consistent());
}
- if( options::produceModels() ){
- d_curr_model_builder->debugCheckModel(d_curr_model);
- // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model)
- postProcessModel(d_curr_model);
+ if (d_curr_model->isBuilt())
+ {
+ // model construction should always succeed unless lemmas were added
+ AlwaysAssert(d_curr_model->isBuiltSuccess());
+ if (options::produceModels())
+ {
+ d_curr_model_builder->debugCheckModel(d_curr_model);
+ // Do post-processing of model from the theories (used for THEORY_SEP
+ // to construct heap model)
+ postProcessModel(d_curr_model);
+ }
}
}
} catch(const theory::Interrupted&) {
return true;
}
-void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){
+bool TheoryEngine::collectModelInfo(theory::TheoryModel* m)
+{
//have shared term engine collectModelInfo
// d_sharedTerms.collectModelInfo( m );
// Consult each active theory to get all relevant information
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
if(d_logicInfo.isTheoryEnabled(theoryId)) {
Trace("model-builder") << " CollectModelInfo on theory: " << theoryId << endl;
- d_theoryTable[theoryId]->collectModelInfo( m );
+ if (!d_theoryTable[theoryId]->collectModelInfo(m))
+ {
+ return false;
+ }
}
}
// Get the Boolean variables
value = false;
}
Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl;
- m->assertPredicate(var, value);
+ if (!m->assertPredicate(var, value))
+ {
+ return false;
+ }
}
+ return true;
}
void TheoryEngine::postProcessModel( theory::TheoryModel* m ){
/**
* collect model info
*/
- void collectModelInfo( theory::TheoryModel* m );
+ bool collectModelInfo(theory::TheoryModel* m);
/** post process model */
void postProcessModel( theory::TheoryModel* m );
namespace CVC4 {
namespace theory {
-TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) :
- d_substitutions(c, false), d_modelBuilt(false), d_enableFuncModels(enableFuncModels)
+TheoryModel::TheoryModel(context::Context* c,
+ std::string name,
+ bool enableFuncModels)
+ : d_substitutions(c, false),
+ d_modelBuilt(false),
+ d_modelBuiltSuccess(false),
+ d_enableFuncModels(enableFuncModels)
{
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
void TheoryModel::reset(){
d_modelBuilt = false;
+ d_modelBuiltSuccess = false;
d_modelCache.clear();
d_comment_str.clear();
d_sep_heap = Node::null();
}
/** assert equality */
-void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){
+bool TheoryModel::assertEquality(TNode a, TNode b, bool polarity)
+{
+ Assert(d_equalityEngine->consistent());
if (a == b && polarity) {
- return;
+ return true;
}
Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl;
d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() );
- Assert(d_equalityEngine->consistent());
+ return d_equalityEngine->consistent();
}
/** assert predicate */
-void TheoryModel::assertPredicate(TNode a, bool polarity ){
+bool TheoryModel::assertPredicate(TNode a, bool polarity)
+{
+ Assert(d_equalityEngine->consistent());
if ((a == d_true && polarity) ||
(a == d_false && (!polarity))) {
- return;
+ return true;
}
if (a.getKind() == EQUAL) {
Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl;
} else {
Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl;
d_equalityEngine->assertPredicate( a, polarity, Node::null() );
- Assert(d_equalityEngine->consistent());
}
+ return d_equalityEngine->consistent();
}
/** assert equality engine */
-void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* termSet)
+bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee,
+ set<Node>* termSet)
{
+ Assert(d_equalityEngine->consistent());
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
for (; !eqcs_i.isFinished(); ++eqcs_i) {
Node eqc = (*eqcs_i);
continue;
}
if (predicate) {
- if (predTrue) {
- assertPredicate(*eqc_i, true);
- }
- else if (predFalse) {
- assertPredicate(*eqc_i, false);
+ if (predTrue || predFalse)
+ {
+ if (!assertPredicate(*eqc_i, predTrue))
+ {
+ return false;
+ }
}
else {
if (first) {
else {
Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl;
d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null());
- Assert(d_equalityEngine->consistent());
+ if (!d_equalityEngine->consistent())
+ {
+ return false;
+ }
}
}
} else {
first = false;
}
else {
- assertEquality(*eqc_i, rep, true);
+ if (!assertEquality(*eqc_i, rep, true))
+ {
+ return false;
+ }
}
}
}
}
+ return true;
}
-void TheoryModel::assertRepresentative(TNode n )
+void TheoryModel::assertSkeleton(TNode n)
{
- Trace("model-builder-reps") << "Assert rep : " << n << std::endl;
- Trace("model-builder-reps") << "Rep eqc is : " << getRepresentative( n ) << std::endl;
+ Trace("model-builder-reps") << "Assert skeleton : " << n << std::endl;
+ Trace("model-builder-reps") << "...rep eqc is : " << getRepresentative(n)
+ << std::endl;
d_reps[ n ] = n;
}
*
* These calls may modify the model object using the interface
* functions below, including:
- * - assertEquality, assertPredicate, assertRepresentative,
+ * - assertEquality, assertPredicate, assertSkeleton,
* assertEqualityEngine.
* - assignFunctionDefinition
*
- * During and after this building process, these calls may use
- * interface functions below to guide the model construction:
+ * This class provides several interface functions:
* - hasTerm, getRepresentative, areEqual, areDisequal
* - getEqualityEngine
* - getRepSet
* - hasAssignedFunctionDefinition, getFunctionsToAssign
+ * - getValue
*
- * After this building process, the function getValue can be
- * used to query the value of nodes.
+ * The above functions can be used for a model m after it has been
+ * successfully built, i.e. when m->isBuiltSuccess() returns true.
+ *
+ * Additionally, all of the above functions, with the exception of getValue,
+ * can be used during step (5) of TheoryEngineModelBuilder::buildModel, as
+ * documented in theory_model_builder.h. In particular, we make calls to the
+ * above functions such as getRepresentative() when assigning total
+ * interpretations for uninterpreted functions.
*/
class TheoryModel : public Model
{
virtual void reset();
/** is built
*
- * Have we (attempted to) build this model since the last
+ * Have we attempted to build this model since the last
* call to reset? Notice for model building techniques
* that are not guaranteed to succeed (such as
* when quantified formulas are enabled), a true return
* current assertions.
*/
bool isBuilt() { return d_modelBuilt; }
+ /** is built success
+ *
+ * Was this model successfully built since the last call to reset?
+ */
+ bool isBuiltSuccess() { return d_modelBuiltSuccess; }
//---------------------------- for building the model
/** Adds a substitution from x to t. */
void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
- /** assert equality holds in the model */
- void assertEquality(TNode a, TNode b, bool polarity);
- /** assert predicate holds in the model */
- void assertPredicate(TNode a, bool polarity);
- /** assert all equalities/predicates in equality engine hold in the model */
- void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL);
- /** assert representative
- * This function tells the model that n should be the representative of its equivalence class.
- * It should be called during model generation, before final representatives are chosen. In the
- * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... )
- * functions.
- */
- void assertRepresentative(TNode n);
+ /** assert equality holds in the model
+ *
+ * This method returns true if and only if the equality engine of this model
+ * is consistent after asserting the equality to this model.
+ */
+ bool assertEquality(TNode a, TNode b, bool polarity);
+ /** assert predicate holds in the model
+ *
+ * This method returns true if and only if the equality engine of this model
+ * is consistent after asserting the predicate to this model.
+ */
+ bool assertPredicate(TNode a, bool polarity);
+ /** assert all equalities/predicates in equality engine hold in the model
+ *
+ * This method returns true if and only if the equality engine of this model
+ * is consistent after asserting the equality engine to this model.
+ */
+ bool assertEqualityEngine(const eq::EqualityEngine* ee,
+ std::set<Node>* termSet = NULL);
+ /** assert skeleton
+ *
+ * This method gives a "skeleton" for the model value of the equivalence
+ * class containing n. This should be an application of interpreted function
+ * (e.g. datatype constructor, array store, set union chain). The subterms of
+ * this term that are variables or terms that belong to other theories will
+ * be filled in with model values.
+ *
+ * For example, if we call assertSkeleton on (C x y) where C is a datatype
+ * constructor and x and y are variables, then the equivalence class of
+ * (C x y) will be interpreted in m as (C x^m y^m) where
+ * x^m = m->getValue( x ) and y^m = m->getValue( y ).
+ *
+ * It should be called during model generation, before final representatives
+ * are chosen. In the case of TheoryEngineModelBuilder, it should be called
+ * during Theory's collectModelInfo( ... ) functions.
+ */
+ void assertSkeleton(TNode n);
//---------------------------- end building the model
// ------------------- general equality queries
protected:
/** substitution map for this model */
SubstitutionMap d_substitutions;
- /** whether this model has been built */
+ /** whether we have tried to build this model in the current context */
bool d_modelBuilt;
+ /** whether this model has been built successfully */
+ bool d_modelBuiltSuccess;
/** special local context for our equalityEngine so we can clear it
* independently of search context */
context::Context* d_eeContext;
// mark as built
tm->d_modelBuilt = true;
+ tm->d_modelBuiltSuccess = false;
// Collect model info from the theories
Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
<< std::endl;
- d_te->collectModelInfo(tm);
+ if (!d_te->collectModelInfo(tm))
+ {
+ return false;
+ }
// model-builder specific initialization
if (!preProcessBuildModel(tm))
}
else
{
+ tm->d_modelBuiltSuccess = true;
return true;
}
}
* (4) assign constants to all equivalence classes
* of m's equality engine, through alternating
* iterations of evaluation and enumeration,
- * (5) builder-specific post-processing.
+ * (5) builder-specific processing, which includes assigning total
+ * interpretations to uninterpreted functions.
*
* This function returns false if any of the above
* steps results in a lemma sent on an output channel.
return mkAnd(assumptions);
}
-void TheoryUF::collectModelInfo( TheoryModel* m ){
+bool TheoryUF::collectModelInfo(TheoryModel* m)
+{
Debug("uf") << "UF : collectModelInfo " << std::endl;
set<Node> termSet;
// Compute terms appearing in assertions and shared terms
computeRelevantTerms(termSet);
- m->assertEqualityEngine( &d_equalityEngine, &termSet );
+ if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ {
+ return false;
+ }
if( options::ufHo() ){
for( std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it ){
if( n.getKind()==kind::APPLY_UF ){
// for model-building with ufHo, we require that APPLY_UF is always expanded to HO_APPLY
Node hn = TheoryUfRewriter::getHoApplyForApplyUf( n );
- m->assertEquality( n, hn, true );
+ if (!m->assertEquality(n, hn, true))
+ {
+ return false;
+ }
}
}
}
Debug("uf") << "UF : finish collectModelInfo " << std::endl;
+ return true;
}
void TheoryUF::presolve() {
void preRegisterTerm(TNode term);
Node explain(TNode n);
- void collectModelInfo( TheoryModel* m );
+ bool collectModelInfo(TheoryModel* m) override;
void ppStaticLearn(TNode in, NodeBuilder<>& learned);
void presolve();
projects / cvc5.git / commitdiff