diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-08-31 16:48:20 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-08-31 16:48:20 +0000 |
| commit | 3c4935c7c0c6774588af94c82307a960e58a1154 (patch) | |
| tree | e518c60ec182e91300fe53293c42cd4b85e49d29 /src/theory/uf/kinds | |
| parent | ec9e426df607f13e5a0c0f52fbc6ed5dbb79fdf9 (diff) | |
merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
Diffstat (limited to 'src/theory/uf/kinds')
| -rw-r--r-- | src/theory/uf/kinds | 45 |
1 files changed, 1 insertions, 44 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index efad8beb9..1d179248c 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -9,7 +9,7 @@ typechecker "theory/uf/theory_uf_type_rules.h" instantiator ::CVC4::theory::uf::InstantiatorTheoryUf "theory/uf/theory_uf_instantiator.h" properties stable-infinite parametric -properties check propagate ppStaticLearn presolve +properties check propagate ppStaticLearn presolve getNextDecisionRequest rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" @@ -19,47 +19,4 @@ 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 |