diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-10-07 10:02:57 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-10-07 10:02:57 -0500 |
| commit | 2f716d8e5eaf4a75c2cf2e431b96ac1f3c9b8a5f (patch) | |
| tree | d3c3433a21be90a0ef5d03d1844f212f6a22c08a /src/theory/quantifiers | |
| parent | 73917595b8f0a2fadfb9616f38a26e32afc25a32 (diff) | |
Multiple fixes for datatypes theory solver: add support for parametric datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 7 | ||||
| -rw-r--r-- | src/theory/quantifiers/options | 2 |
2 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index cb8cb8154..b1a0c4ed4 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -139,6 +139,11 @@ bool ModelEngine::optOneQuantPerRound(){ int ModelEngine::checkModel(){ FirstOrderModel* fm = d_quantEngine->getModel(); + + //flatten the representatives + //Trace("model-engine-debug") << "Flattening representatives...." << std::endl; + //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps ); + //for debugging if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); @@ -149,7 +154,7 @@ int ModelEngine::checkModel(){ Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); for( size_t i=0; i<it->second.size(); i++ ){ //Trace("model-engine-debug") << it->second[i] << " "; - Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] ); + Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 57211ade7..fd114df04 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -98,7 +98,7 @@ option finiteModelFind --finite-model-find bool :default false option fmfModelBasedInst /--disable-fmf-mbqi bool :default true disable model-based quantifier instantiation for finite model finding -option fmfFullModelCheck --fmf-fmc bool :default false +option fmfFullModelCheck --fmf-fmc bool :default false :read-write enable full model check for finite model finding option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding |