summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/bounded_integers.h3
-rw-r--r--src/theory/quantifiers/instantiation_engine.h2
-rw-r--r--src/theory/quantifiers/model_engine.cpp104
-rw-r--r--src/theory/quantifiers/model_engine.h2
-rwxr-xr-xsrc/theory/quantifiers/quant_conflict_find.h8
-rw-r--r--src/theory/quantifiers/rewrite_engine.h4
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"; }
};
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback