diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
| commit | f62d9456b41bf17df1d339e46776c9213cb3705a (patch) | |
| tree | 01d3448b3c9fe89ead56c72b18f8516292092e13 /src/theory/bv/kinds | |
| parent | 7943953741c67d8246f983e193d26812d959b4cd (diff) | |
Squashed merge of SygusComp 2015 branch.
Diffstat (limited to 'src/theory/bv/kinds')
| -rw-r--r-- | src/theory/bv/kinds | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index b4ecc1d3d..3cbc45cd1 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -70,6 +70,9 @@ operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vect operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)" operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)" +operator BITVECTOR_REDOR 1 "bit-vector redor" +operator BITVECTOR_REDAND 1 "bit-vector redand" + operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)" operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)" operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)" @@ -171,6 +174,10 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule +typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule + + typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule |