From 5f096cbd59afa98e8b3c7e7e7aa0b6df3c7e01b0 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 6 Mar 2017 00:25:26 -0800 Subject: Adding support for bool-to-bv Squashed commit of the following: commit 5197a663eb262afbeb7740f53b5bd27479dccea0 Author: Clark Barrett Date: Mon Mar 6 00:16:16 2017 -0800 Remove IFF case commit 2119b25a30ed42eca54f632e7232c9f76ae5755a Author: guykatzz Date: Mon Feb 20 12:37:06 2017 -0800 proof support for bvcomp commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22 Author: Clark Barrett Date: Fri Feb 17 21:09:04 2017 -0800 Added missing cases to operator<< for bv rewrite rules. commit 0ed797c31d0e66cadc35b2397716c841d1aff270 Author: Clark Barrett Date: Fri Feb 17 11:43:51 2017 -0800 Added rewrite rules for new bitvector kinds. commit 3b23dffb317de5559f8a95118fef633f711c114a Author: Clark Barrett Date: Mon Feb 13 14:41:49 2017 -0800 First draft of bool-to-bv pass. --- src/theory/bv/kinds | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'src/theory/bv/kinds') diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 0ab33379f..da2833ca0 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -61,6 +61,7 @@ operator BITVECTOR_UREM_TOTAL 2 "unsigned remainder from truncating division of operator BITVECTOR_SHL 2 "bit-vector shift left (the two bit-vector parameters must have same width)" operator BITVECTOR_LSHR 2 "bit-vector logical shift right (the two bit-vector parameters must have same width)" operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)" + operator BITVECTOR_ULT 2 "bit-vector unsigned less than (the two bit-vector parameters must have same width)" operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal (the two bit-vector parameters must have same width)" operator BITVECTOR_UGT 2 "bit-vector unsigned greater than (the two bit-vector parameters must have same width)" @@ -70,6 +71,10 @@ 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_ULTBV 2 "bit-vector unsigned less than but returns bv of size 1 instead of boolean" +operator BITVECTOR_SLTBV 2 "bit-vector signed less than but returns bv of size 1 instead of boolean" +operator BITVECTOR_ITE 3 "same semantics as regular ITE, but condition is bv of size 1 instead of Boolean" + operator BITVECTOR_REDOR 1 "bit-vector redor" operator BITVECTOR_REDAND 1 "bit-vector redand" @@ -145,8 +150,6 @@ typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompTypeRule - typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorFixedWidthTypeRule @@ -174,6 +177,11 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorBVPredTypeRule +typerule BITVECTOR_ULTBV ::CVC4::theory::bv::BitVectorBVPredTypeRule +typerule BITVECTOR_SLTBV ::CVC4::theory::bv::BitVectorBVPredTypeRule +typerule BITVECTOR_ITE ::CVC4::theory::bv::BitVectorITETypeRule + typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule -- cgit v1.2.3