diff options
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 5 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 25 |
2 files changed, 29 insertions, 1 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index c90419def..4d5e95119 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -309,7 +309,10 @@ operator FUNCTION_TYPE 2: "a function type" cardinality FUNCTION_TYPE \ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -well-founded FUNCTION_TYPE false +well-founded FUNCTION_TYPE \ + "::CVC4::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" enumerator FUNCTION_TYPE \ ::CVC4::theory::builtin::FunctionEnumerator \ "theory/builtin/type_enumerator.h" diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index d49edbc8c..a3d1776e1 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -223,6 +223,31 @@ class FunctionProperties { return valueCard ^ argsCard; } + /** Function type is well-founded if its component sorts are */ + static bool isWellFounded(TypeNode type) + { + for (TypeNode::iterator i = type.begin(), i_end = type.end(); i != i_end; + ++i) + { + if (!(*i).isWellFounded()) + { + return false; + } + } + return true; + } + /** + * Ground term for function sorts is (lambda x. t) where x is the + * canonical variable list for its type and t is the canonical ground term of + * its range. + */ + static Node mkGroundTerm(TypeNode type) + { + NodeManager* nm = NodeManager::currentNM(); + Node bvl = nm->getBoundVarListForFunctionType(type); + Node ret = type.getRangeType().mkGroundTerm(); + return nm->mkNode(kind::LAMBDA, bvl, ret); + } };/* class FuctionProperties */ class SExprProperties { |