diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-18 17:54:11 -0500 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-05-18 17:54:11 -0500 |
commit | 20f2510e4a8f0f136b6bba3c936ac63cfc8a61bd (patch) | |
tree | c4b3ba71279d757a99e0cc56052f5a6791108118 /src | |
parent | e2c0e3e939479e87e5e8ad32aebbdb4f1f6aa77f (diff) |
Cache isInterpretedFinite (#1943)
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/type_node.cpp | 59 | ||||
-rw-r--r-- | src/expr/type_node.h | 3 |
2 files changed, 44 insertions, 18 deletions
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index e7775cf7f..02f857568 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -66,41 +66,68 @@ Cardinality TypeNode::getCardinality() const { return kind::getCardinality(*this); } -bool TypeNode::isInterpretedFinite() const { - if( getCardinality().isFinite() ){ - return true; - }else{ - if( options::finiteModelFind() ){ +/** Attribute true for types that are interpreted as finite */ +struct IsInterpretedFiniteTag +{ +}; +struct IsInterpretedFiniteComputedTag +{ +}; +typedef expr::Attribute<IsInterpretedFiniteTag, bool> IsInterpretedFiniteAttr; +typedef expr::Attribute<IsInterpretedFiniteComputedTag, bool> + IsInterpretedFiniteComputedAttr; + +bool TypeNode::isInterpretedFinite() +{ + // check it is already cached + if (!getAttribute(IsInterpretedFiniteComputedAttr())) + { + bool isInterpretedFinite = false; + if (getCardinality().isFinite()) + { + isInterpretedFinite = true; + } + else if (options::finiteModelFind()) + { if( isSort() ){ - return true; + isInterpretedFinite = true; }else if( isDatatype() ){ TypeNode tn = *this; const Datatype& dt = getDatatype(); - return dt.isInterpretedFinite( tn.toType() ); + isInterpretedFinite = dt.isInterpretedFinite(tn.toType()); }else if( isArray() ){ - return getArrayIndexType().isInterpretedFinite() && getArrayConstituentType().isInterpretedFinite(); + isInterpretedFinite = + getArrayIndexType().isInterpretedFinite() + && getArrayConstituentType().isInterpretedFinite(); }else if( isSet() ) { - return getSetElementType().isInterpretedFinite(); + isInterpretedFinite = getSetElementType().isInterpretedFinite(); } else if (isFunction()) { + isInterpretedFinite = true; if (!getRangeType().isInterpretedFinite()) { - return false; + isInterpretedFinite = false; } - std::vector<TypeNode> argTypes = getArgTypes(); - for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) + else { - if (!argTypes[i].isInterpretedFinite()) + std::vector<TypeNode> argTypes = getArgTypes(); + for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) { - return false; + if (!argTypes[i].isInterpretedFinite()) + { + isInterpretedFinite = false; + break; + } } } - return true; } } - return false; + setAttribute(IsInterpretedFiniteAttr(), isInterpretedFinite); + setAttribute(IsInterpretedFiniteComputedAttr(), true); + return isInterpretedFinite; } + return getAttribute(IsInterpretedFiniteAttr()); } bool TypeNode::isFirstClass() const { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 14c4222a6..428b65375 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -427,8 +427,7 @@ public: * If finite model finding is enabled, this assumes all uninterpreted sorts * are interpreted as finite. */ - bool isInterpretedFinite() const; - + bool isInterpretedFinite(); /** * Is this a first-class type? |