diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 104 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.h | 4 |
6 files changed, 70 insertions, 53 deletions
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 972bdb2ec..4130bffee 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -121,6 +121,9 @@ public: void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); bool isGroundRange(Node f, Node v); + + /** Identify this module */ + std::string identify() const { return "BoundedIntegers"; } }; } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 5f7e26297..394d53d42 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -150,6 +150,8 @@ public: ~Statistics(); }; Statistics d_statistics; + /** Identify this module */ + std::string identify() const { return "InstEngine"; } };/* class InstantiationEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 8b62fc39b..d7b074acc 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -55,68 +55,74 @@ QuantifiersModule( qe ){ void ModelEngine::check( Theory::Effort e ){ if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){ - FirstOrderModel* fm = d_quantEngine->getModel(); - //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers int addedLemmas = 0; - //quantifiers are initialized, we begin an instantiation round - double clSet = 0; - if( Trace.isOn("model-engine") ){ - clSet = double(clock())/double(CLOCKS_PER_SEC); - } - ++(d_statistics.d_inst_rounds); - bool buildAtFullModel = d_builder->optBuildAtFullModel(); - //two effort levels: first try exhaustive instantiation without axioms, then with. - int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; - for( int effort=startEffort; effort<2; effort++ ){ - // for effort = 0, we only instantiate non-axioms - // for effort = 1, we instantiate everything - if( addedLemmas==0 ){ - Trace("model-engine") << "---Model Engine Round---" << std::endl; - //initialize the model - Trace("model-engine-debug") << "Build model..." << std::endl; - d_builder->d_considerAxioms = effort>=1; - d_builder->d_addedLemmas = 0; - d_builder->buildModel( fm, buildAtFullModel ); - addedLemmas += (int)d_builder->d_addedLemmas; - //if builder has lemmas, add and return + bool needsBuild = true; + FirstOrderModel* fm = d_quantEngine->getModel(); + if( fm->getNumAssertedQuantifiers()>0 ){ + //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers + //quantifiers are initialized, we begin an instantiation round + double clSet = 0; + if( Trace.isOn("model-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + } + ++(d_statistics.d_inst_rounds); + bool buildAtFullModel = d_builder->optBuildAtFullModel(); + needsBuild = !buildAtFullModel; + //two effort levels: first try exhaustive instantiation without axioms, then with. + int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; + for( int effort=startEffort; effort<2; effort++ ){ + // for effort = 0, we only instantiate non-axioms + // for effort = 1, we instantiate everything if( addedLemmas==0 ){ - Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; - //let the strong solver verify that the model is minimal - //for debugging, this will if there are terms in the model that the strong solver was not notified of - if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){ - Trace("model-engine-debug") << "Check model..." << std::endl; - d_incomplete_check = false; - //print debug - Debug("fmf-model-complete") << std::endl; - debugPrint("fmf-model-complete"); - //successfully built an acceptable model, now check it - addedLemmas += checkModel(); - }else{ - addedLemmas++; + Trace("model-engine") << "---Model Engine Round---" << std::endl; + //initialize the model + Trace("model-engine-debug") << "Build model..." << std::endl; + d_builder->d_considerAxioms = effort>=1; + d_builder->d_addedLemmas = 0; + d_builder->buildModel( fm, buildAtFullModel ); + addedLemmas += (int)d_builder->d_addedLemmas; + //if builder has lemmas, add and return + if( addedLemmas==0 ){ + Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; + //let the strong solver verify that the model is minimal + //for debugging, this will if there are terms in the model that the strong solver was not notified of + if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){ + Trace("model-engine-debug") << "Check model..." << std::endl; + d_incomplete_check = false; + //print debug + Debug("fmf-model-complete") << std::endl; + debugPrint("fmf-model-complete"); + //successfully built an acceptable model, now check it + addedLemmas += checkModel(); + }else{ + addedLemmas++; + } } } - } - if( addedLemmas==0 ){ - //if we have not added lemmas yet and axiomInstMode=trust, then we are done - if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ - //we must return unknown if an axiom is asserted - if( effort==0 ){ - d_incomplete_check = true; + if( addedLemmas==0 ){ + //if we have not added lemmas yet and axiomInstMode=trust, then we are done + if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ + //we must return unknown if an axiom is asserted + if( effort==0 ){ + d_incomplete_check = true; + } + break; } - break; } } - } - if( Trace.isOn("model-engine") ){ - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; + if( Trace.isOn("model-engine") ){ + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; + } + }else{ + Trace("model-engine-debug") << "No quantified formulas asserted." << std::endl; } if( addedLemmas==0 ){ Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl; //CVC4 will answer SAT or unknown Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - if( options::produceModels() && !buildAtFullModel ){ + if( options::produceModels() && needsBuild ){ // finish building the model d_builder->buildModel( fm, true ); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index cf770a7b9..3b34f7504 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -68,6 +68,8 @@ public: ~Statistics(); }; Statistics d_statistics; + /** Identify this module */ + std::string identify() const { return "ModelEngine"; } };/* class ModelEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 62bd347c7..8a0d956ac 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -116,7 +116,7 @@ public: class QuantInfo {
private:
void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );
- void flatten( Node n, bool beneathQuant ); + void flatten( Node n, bool beneathQuant );
private: //for completing match
std::vector< int > d_unassigned;
std::vector< TypeNode > d_unassigned_tn;
@@ -156,8 +156,8 @@ public: bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );
void revertMatch( std::vector< int >& assigned );
void debugPrintMatch( const char * c );
- bool isConstrainedVar( int v ); -public: + bool isConstrainedVar( int v );
+public:
void getMatch( std::vector< Node >& terms );
};
@@ -274,6 +274,8 @@ public: ~Statistics();
};
Statistics d_statistics;
+ /** Identify this module */
+ std::string identify() const { return "QcfEngine"; }
};
}
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index f85803617..a16a6d598 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -56,7 +56,9 @@ public: void check( Theory::Effort e ); void registerQuantifier( Node f ); - void assertNode( Node n ); + void assertNode( Node n ); + /** Identify this module */ + std::string identify() const { return "RewriteEngine"; } }; } |