diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-12 18:30:15 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-12 18:30:15 +0000 |
| commit | 65798541fa437278cde0c759ab70fd9fa4fe9638 (patch) | |
| tree | 27341327b8159e58a5ce6371bede6129bf67beb3 /src/theory/uf/kinds | |
| parent | 78d8b3ce56a1fd243acb54d2aaaf6d716e3b9788 (diff) | |
merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
Diffstat (limited to 'src/theory/uf/kinds')
| -rw-r--r-- | src/theory/uf/kinds | 44 |
1 files changed, 43 insertions, 1 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index ec353dc59..ce8785f86 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -17,7 +17,49 @@ parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule operator CARDINALITY_CONSTRAINT 2 "cardinality constraint" - typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule +# +# For compact function models +# There are three cases for FUNCTION_MODEL nodes: +# (1) The node has two children, the first being of kind FUNCTION_CASE_SPLIT. The second child specifies a default value. +# (2) The node has one child of kind FUNCTION_CASE_SPLIT. +# (3) The node has one child, it's default value. +# +# Semantics of FUNCTION_MODEL kind-ed nodes. The value of n applied to arguments args is +# +# getValueFM( n, args, 0 ), where: +# +# Node getValueFM( n, args, argIndex ) +# if n.getKind()!=FUNCTION_MODEL +# return n; +# else if (1) +# val = getValueFCS( n[0], args, argIndex ); +# if !val.isNull() +# return val; +# else +# return getValueFM( n[1], args, argIndex+1 ); +# else if (2) +# return getValueFCS( n[0], args, argIndex ); +# else if (3) +# return getValueFM( n[0], args, argIndex+1 ); +# +# Node getValueFCS( n, args, argIndex ) : +# //n.getKind()==FUNCTION_CASE_SPLIT +# //n[j].getKind()==FUNCTION_CASE for all 0<=j<n.getNumChildren() +# if( args[argIndex]=n[i][0] for some i) +# return getValueFM( n[i][1], args, argIndex+1 ); +# else +# return null; +# + +operator FUNCTION_MODEL 1:2 "function model" +typerule FUNCTION_MODEL ::CVC4::theory::uf::FunctionModelTypeRule + +operator FUNCTION_CASE_SPLIT 1: "function case split" +typerule FUNCTION_CASE_SPLIT ::CVC4::theory::uf::FunctionCaseSplitTypeRule + +operator FUNCTION_CASE 2 "function case" +typerule FUNCTION_CASE ::CVC4::theory::uf::FunctionCaseTypeRule + endtheory |