1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h"
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
rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
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
|
