diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/abstraction.cpp | 1 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblast_strategies_template.h | 1 | ||||
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 1 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 1 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 1 | ||||
-rw-r--r-- | src/theory/bv/kinds | 90 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 1 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 1 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 1 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 1 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 1 |
14 files changed, 71 insertions, 43 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index e6080ed4f..37758ad4a 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -24,6 +24,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" using namespace cvc5; using namespace cvc5::theory; diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h index f5259dc93..f71f82ce1 100644 --- a/src/theory/bv/bitblast/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -25,6 +25,7 @@ #include "theory/bv/bitblast/bitblast_utils.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" namespace cvc5 { diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 32b6dbd7a..ba545e48b 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -27,6 +27,7 @@ #include "context/cdo.h" #include "context/cdqueue.h" #include "context/context.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 3a9e460fe..65c1ec79c 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -29,6 +29,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "util/bitvector.h" using namespace cvc5::context; using namespace cvc5::prop; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 7c97d1bbc..2589418cc 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -23,6 +23,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/ext_theory.h" #include "theory/theory_model.h" +#include "util/rational.h" using namespace std; using namespace cvc5; diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 6af586735..9590d5522 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -13,19 +13,21 @@ properties check propagate presolve ppStaticLearn rewriter ::cvc5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" constant BITVECTOR_TYPE \ - ::cvc5::BitVectorSize \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \ - "util/bitvector.h" \ - "bit-vector type" + struct \ + BitVectorSize \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \ + "util/bitvector.h" \ + "bit-vector type" cardinality BITVECTOR_TYPE \ "::cvc5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \ "theory/bv/theory_bv_type_rules.h" constant CONST_BITVECTOR \ - ::cvc5::BitVector \ - ::cvc5::BitVectorHashFunction \ - "util/bitvector.h" \ - "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class" + class \ + BitVector \ + ::cvc5::BitVectorHashFunction \ + "util/bitvector.h" \ + "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class" enumerator BITVECTOR_TYPE \ "::cvc5::theory::bv::BitVectorEnumerator" \ @@ -101,59 +103,67 @@ operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bi ### parameterized operator kinds ---------------------------------------------- constant BITVECTOR_BITOF_OP \ - ::cvc5::BitVectorBitOf \ - ::cvc5::BitVectorBitOfHashFunction \ - "util/bitvector.h" \ - "operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class" + struct \ + BitVectorBitOf \ + ::cvc5::BitVectorBitOfHashFunction \ + "util/bitvector.h" \ + "operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class" parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term" constant BITVECTOR_EXTRACT_OP \ - ::cvc5::BitVectorExtract \ - ::cvc5::BitVectorExtractHashFunction \ - "util/bitvector.h" \ - "operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class" + struct \ + BitVectorExtract \ + ::cvc5::BitVectorExtractHashFunction \ + "util/bitvector.h" \ + "operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class" parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term" constant BITVECTOR_REPEAT_OP \ - ::cvc5::BitVectorRepeat \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \ - "util/bitvector.h" \ - "operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class" + struct \ + BitVectorRepeat \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \ + "util/bitvector.h" \ + "operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class" parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term" constant BITVECTOR_ROTATE_LEFT_OP \ - ::cvc5::BitVectorRotateLeft \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \ - "util/bitvector.h" \ - "operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class" + struct \ + BitVectorRotateLeft \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \ + "util/bitvector.h" \ + "operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class" parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term" constant BITVECTOR_ROTATE_RIGHT_OP \ - ::cvc5::BitVectorRotateRight \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \ - "util/bitvector.h" \ - "operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class" + struct \ + BitVectorRotateRight \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \ + "util/bitvector.h" \ + "operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class" parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term" constant BITVECTOR_SIGN_EXTEND_OP \ - ::cvc5::BitVectorSignExtend \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \ - "util/bitvector.h" \ - "operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class" + struct \ + BitVectorSignExtend \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \ + "util/bitvector.h" \ + "operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class" parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term" constant BITVECTOR_ZERO_EXTEND_OP \ - ::cvc5::BitVectorZeroExtend \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \ - "util/bitvector.h" \ - "operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class" + struct \ + BitVectorZeroExtend \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \ + "util/bitvector.h" \ + "operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class" parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term" constant INT_TO_BITVECTOR_OP \ - ::cvc5::IntToBitVector \ - "::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \ - "util/bitvector.h" \ - "operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class" + struct \ + IntToBitVector \ + "::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \ + "util/bitvector.h" \ + "operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class" parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term" ### type rules for non-parameterized operator kinds --------------------------- diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index af80ad00b..761f4efb2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -22,6 +22,7 @@ #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 45e313e48..5ead8a215 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -27,6 +27,7 @@ #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index e44d1c9b7..496a625ee 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -23,6 +23,7 @@ #include "options/bv_options.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 1e38aba0f..6d2ed4477 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -24,6 +24,7 @@ #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index d0579703d..476803c59 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -375,9 +375,13 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) { RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite) { - Node resultNode = - LinearRewriteStrategy<RewriteRule<EvalComp>, RewriteRule<BvComp> >::apply( - node); + Node resultNode = LinearRewriteStrategy<RewriteRule<EvalComp>>::apply(node); + + if (node == resultNode && RewriteRule<BvComp>::applies(node)) + { + resultNode = RewriteRule<BvComp>::run<false>(node); + return RewriteResponse(REWRITE_AGAIN, resultNode); + } return RewriteResponse(REWRITE_DONE, resultNode); } diff --git a/src/theory/bv/theory_bv_type_rules.cpp b/src/theory/bv/theory_bv_type_rules.cpp index 304a2b9cf..707b5f8bb 100644 --- a/src/theory/bv/theory_bv_type_rules.cpp +++ b/src/theory/bv/theory_bv_type_rules.cpp @@ -18,6 +18,8 @@ #include <algorithm> #include "expr/type_node.h" +#include "util/bitvector.h" +#include "util/cardinality.h" #include "util/integer.h" namespace cvc5 { diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 927a40b82..bc6096cbb 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -20,6 +20,8 @@ #include "expr/skolem_manager.h" #include "options/theory_options.h" #include "theory/theory.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index fca449917..712f5b822 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -23,6 +23,7 @@ #include <vector> #include "expr/node_manager.h" +#include "util/integer.h" namespace cvc5 { namespace theory { |