diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-19 12:39:07 -0400 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-19 12:39:07 -0400 |
| commit | 7de5f26ca35f6b3b11dc8a7465f7a15e5d0d2e50 (patch) | |
| tree | a0c0cd831361d7e872618fc9e8739f63db9760bb /src/theory/quantifiers/sygus | |
| parent | 9fa66413709fbdb1a02f8986d0c332934523b110 (diff) | |
Fixes for sygus with datatypes (#3103)
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 01d08dad8..af8c93e45 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -874,8 +874,13 @@ void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, un // do not recurse to non-datatype types return; } + const Datatype& dt = tn.getDatatype(); + if( !dt.isSygus() ) + { + // do not recurse to non-sygus datatype types + return; + } d_min_type_depth[root_tn][tn] = type_depth; - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); //compute for connected types for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ |