diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-13 14:12:32 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-13 14:12:41 +0100 |
commit | 82fbac8829cbc41927216b36ab064b50e50b2fa0 (patch) | |
tree | 346361d002c109b8ac2254f4f215a12dfc7643d2 /src/theory/unconstrained_simplifier.cpp | |
parent | 3ba153b4be4c2fe8ad7decf8ebc7cf5d8815a0e9 (diff) |
Handle recursive singleton case for codatatypes, add regression. Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
Diffstat (limited to 'src/theory/unconstrained_simplifier.cpp')
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index d37aa1b7d..244cb303d 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Clark Barrett ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Tim King, Liana Hadarean, Peter Collingbourne + ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Tim King, Liana Hadarean, Peter Collingbourne, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -197,6 +197,14 @@ void UnconstrainedSimplifier::processUnconstrained() break; } } + if( parent[0].getType().isDatatype() ){ + TypeNode tn = parent[0].getType(); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if( dt.isRecursiveSingleton() ){ + //domain size may be 1 + break; + } + } case kind::BITVECTOR_COMP: case kind::LT: case kind::LEQ: |