diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/builtin/kinds | 10 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 27 | ||||
-rw-r--r-- | src/theory/bv/kinds | 12 | ||||
-rw-r--r-- | src/theory/uf/kinds | 4 |
4 files changed, 44 insertions, 9 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index d3b9d12fb..47ee8cbfc 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -112,8 +112,14 @@ theory builtin ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h" # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's # not stored that way. If you ask for the operator of (EQUAL a b), # you'll get a special, singleton (BUILTIN EQUAL) Node. -constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \ - "expr/kind.h" "The kind of nodes representing built-in operators" +constant BUILTIN \ + ::CVC4::Kind \ + ::CVC4::kind::KindHashStrategy \ + "expr/kind.h" \ + "The kind of nodes representing built-in operators" + +variable FUNCTION "function" +parameterized APPLY FUNCTION 1: "defined function application" operator EQUAL 2 "equality" operator DISTINCT 2: "disequality" diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 2ff92e788..aee147eff 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -31,6 +31,33 @@ namespace CVC4 { namespace theory { namespace builtin { +class ApplyTypeRule { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate) { + TNode f = n.getOperator(); + TypeNode fType = f.getType(check); + if( !fType.isFunction() ) { + throw TypeCheckingExceptionPrivate(n, "operator does not have function type"); + } + if( check ) { + if (n.getNumChildren() != fType.getNumChildren() - 1) { + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); + } + TNode::iterator argument_it = n.begin(); + TNode::iterator argument_it_end = n.end(); + TypeNode::iterator argument_type_it = fType.begin(); + for(; argument_it != argument_it_end; ++argument_it) { + if((*argument_it).getType() != *argument_type_it) { + throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + } + } + } + return fType.getRangeType(); + } +};/* class ApplyTypeRule */ + + class EqualityTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index cc6fe0c20..e7374284e 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -17,11 +17,11 @@ constant CONST_BITVECTOR \ ::CVC4::BitVectorHashStrategy \ "util/bitvector.h" \ "a fixed-width bit-vector constant" - + operator BITVECTOR_CONCAT 2: "bit-vector concatenation" operator BITVECTOR_AND 2 "bitwise and" -operator BITVECTOR_OR 2 "bitwise or" -operator BITVECTOR_XOR 2 "bitwise xor" +operator BITVECTOR_OR 2 "bitwise or" +operator BITVECTOR_XOR 2 "bitwise xor" operator BITVECTOR_NOT 2 "bitwise not" operator BITVECTOR_NAND 2 "bitwise nand" operator BITVECTOR_NOR 2 "bitwise nor" @@ -31,8 +31,8 @@ operator BITVECTOR_MULT 2 "bit-vector multiplication" operator BITVECTOR_PLUS 2 "bit-vector addition" operator BITVECTOR_SUB 2 "bit-vector subtraction" operator BITVECTOR_NEG 1 "bit-vector unary negation" -operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)" -operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)" +operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)" +operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)" operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division" operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)" operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)" @@ -83,7 +83,7 @@ constant BITVECTOR_ROTATE_RIGHT_OP \ "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateRight >" \ "util/bitvector.h" \ "operator for the bit-vector rotate right" - + parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract" parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat" parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend" diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 13cd5e91b..8cd6aec70 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -7,4 +7,6 @@ theory ::CVC4::theory::uf::TheoryUF "theory_uf.h" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" -variable SORT_TYPE "sort type" + +variable SORT_TAG "sort tag" +parameterized SORT_TYPE SORT_TAG 0: "sort type" |