diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-21 14:40:06 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-21 14:40:06 +0200 |
commit | 1ec95c559074ed7575a0165deb16fcee45920e9f (patch) | |
tree | 136c51e992d39da691f13e529662f04998eaa49f | |
parent | fb746fdd4e60e7d166b0fa1e5788bea925d22ee7 (diff) |
Minor changes related to codatatypes for 1.5 release.
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 3 |
2 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 371f27c95..e0a4dc7d8 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1414,11 +1414,15 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Node eqc = it->first; const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); if( dt.isCodatatype() ){ + //until models are implemented for codatatypes + throw Exception("Models for codatatypes are not supported in this version."); + /* std::map< Node, Node > vmap; std::vector< Node > fv; Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap, fv ); Trace("dt-cmi-cdt") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl; //m->assertEquality( eqc, v, true ); + */ } } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index db0328f4f..58f0a265e 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1558,7 +1558,8 @@ void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ bool TermDb::isInductionTerm( Node n ) { if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTermDatatype( n ) ){ - return true; + const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); + return !dt.isCodatatype(); } if( options::intWfInduction() && n.getType().isInteger() ){ return true; |