From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 21 Aug 2015 12:40:06 +0000 (+0200)
Subject: Minor changes related to codatatypes for 1.5 release.
X-Git-Tag: cvc5-1.0.0~6252^2~11
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ec95c559074ed7575a0165deb16fcee45920e9f;p=cvc5.git

Minor changes related to codatatypes for 1.5 release.
---

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;