diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-12-22 13:44:05 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-12-22 13:44:05 +0100 |
commit | 75003d97ad485f8840310e652a74872f5950538d (patch) | |
tree | 0d7b44ff11ffdf48495ed5c165f7344671e0c3b5 /src/theory | |
parent | bd6a13bbb46c272561c01b7783f62ff7be091c2c (diff) |
Always split on constructor types for datatypes involving uninterpreted sorts when finite model finding is enabled, add regressions.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 |
3 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 1962d2e31..77733904d 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -244,7 +244,7 @@ void TheoryDatatypes::check(Effort e) { if( consIndex==-1 ){ consIndex = j; } - if( !dt[ j ].isFinite() ) { + if( !dt[ j ].isFinite() && ( !options::finiteModelFind() || !dt.involvesUninterpretedType() ) ) { if( !eqc || !eqc->d_selectors ){ needSplit = false; } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 095e7868e..027a4573b 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -688,6 +688,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { }else{ //make the condition Node cond = d_models[op]->d_cond[i]; + Trace("fmc-model-func") << "...cond : " << cond << std::endl; std::vector< Node > children; for( unsigned j=0; j<cond.getNumChildren(); j++) { TypeNode tn = vars[j].getType(); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5ccb794f7..36b24c51b 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1029,7 +1029,7 @@ Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { bool TermDb::isClosedEnumerableType( TypeNode tn ) { std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn ); if( it==d_typ_closed_enum.end() ){ - d_typ_closed_enum[tn] = false; + d_typ_closed_enum[tn] = true; bool ret = true; if( tn.isArray() || tn.isSort() || tn.isCodatatype() ){ ret = false; |