From 1b30b256a0ec40ff431b83296bfe5aa0e099eb2e Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Mon, 20 Sep 2010 01:08:32 +0000 Subject: [PATCH] bitvector rewriting for the core theory and testcases --- src/expr/node_builder.h | 8 +- src/expr/node_manager.cpp | 2 +- src/expr/node_manager.h | 1 - src/parser/antlr_input.h | 12 +- src/parser/smt/Smt.g | 24 +- src/parser/smt/smt.cpp | 8 +- src/theory/bv/Makefile.am | 4 + src/theory/bv/kinds | 4 +- src/theory/bv/theory_bv.cpp | 60 +++++ src/theory/bv/theory_bv.h | 8 +- src/theory/bv/theory_bv_rewrite_rules.cpp | 249 ++++++++++++++++++ src/theory/bv/theory_bv_rewrite_rules.h | 104 ++++++++ src/theory/bv/theory_bv_type_rules.h | 2 +- src/theory/bv/theory_bv_utils.h | 53 ++++ src/util/bitvector.h | 16 +- src/util/integer_cln_imp.h | 8 + src/util/integer_gmp_imp.h | 3 + .../regress0/bv/core/concat-merge-0.cvc | 3 + .../regress0/bv/core/concat-merge-0.smt | 6 + .../regress0/bv/core/concat-merge-1.cvc | 3 + .../regress0/bv/core/concat-merge-1.smt | 6 + .../regress0/bv/core/concat-merge-2.cvc | 3 + .../regress0/bv/core/concat-merge-2.smt | 6 + .../regress0/bv/core/concat-merge-3.cvc | 3 + .../regress0/bv/core/concat-merge-3.smt | 6 + .../regress0/bv/core/extract-concat-0.cvc | 2 + .../regress0/bv/core/extract-concat-0.smt | 7 + .../regress0/bv/core/extract-concat-1.cvc | 2 + .../regress0/bv/core/extract-concat-1.smt | 7 + .../regress0/bv/core/extract-concat-10.cvc | 2 + .../regress0/bv/core/extract-concat-10.smt | 7 + .../regress0/bv/core/extract-concat-11.cvc | 2 + .../regress0/bv/core/extract-concat-11.smt | 7 + .../regress0/bv/core/extract-concat-2.cvc | 2 + .../regress0/bv/core/extract-concat-2.smt | 7 + .../regress0/bv/core/extract-concat-3.cvc | 2 + .../regress0/bv/core/extract-concat-3.smt | 7 + .../regress0/bv/core/extract-concat-4.cvc | 2 + .../regress0/bv/core/extract-concat-4.smt | 7 + .../regress0/bv/core/extract-concat-5.cvc | 2 + .../regress0/bv/core/extract-concat-5.smt | 7 + .../regress0/bv/core/extract-concat-6.cvc | 2 + .../regress0/bv/core/extract-concat-6.smt | 7 + .../regress0/bv/core/extract-concat-7.cvc | 2 + .../regress0/bv/core/extract-concat-7.smt | 7 + .../regress0/bv/core/extract-concat-8.cvc | 2 + .../regress0/bv/core/extract-concat-8.smt | 7 + .../regress0/bv/core/extract-concat-9.cvc | 2 + .../regress0/bv/core/extract-concat-9.smt | 7 + .../regress0/bv/core/extract-constant.cvc | 2 + .../regress0/bv/core/extract-constant.smt | 5 + .../regress0/bv/core/extract-extract-0.cvc | 2 + .../regress0/bv/core/extract-extract-0.smt | 6 + .../regress0/bv/core/extract-extract-1.cvc | 2 + .../regress0/bv/core/extract-extract-1.smt | 6 + .../regress0/bv/core/extract-extract-10.cvc | 2 + .../regress0/bv/core/extract-extract-10.smt | 6 + .../regress0/bv/core/extract-extract-11.cvc | 2 + .../regress0/bv/core/extract-extract-11.smt | 6 + .../regress0/bv/core/extract-extract-2.cvc | 2 + .../regress0/bv/core/extract-extract-2.smt | 6 + .../regress0/bv/core/extract-extract-3.cvc | 2 + .../regress0/bv/core/extract-extract-3.smt | 6 + .../regress0/bv/core/extract-extract-4.cvc | 2 + .../regress0/bv/core/extract-extract-4.smt | 6 + .../regress0/bv/core/extract-extract-5.cvc | 2 + .../regress0/bv/core/extract-extract-5.smt | 6 + .../regress0/bv/core/extract-extract-6.cvc | 2 + .../regress0/bv/core/extract-extract-6.smt | 6 + .../regress0/bv/core/extract-extract-7.cvc | 2 + .../regress0/bv/core/extract-extract-7.smt | 6 + .../regress0/bv/core/extract-extract-8.cvc | 2 + .../regress0/bv/core/extract-extract-8.smt | 6 + .../regress0/bv/core/extract-extract-9.cvc | 2 + .../regress0/bv/core/extract-extract-9.smt | 6 + .../regress0/bv/core/extract-whole-0.cvc | 2 + .../regress0/bv/core/extract-whole-0.smt | 6 + .../regress0/bv/core/extract-whole-1.cvc | 2 + .../regress0/bv/core/extract-whole-1.smt | 6 + .../regress0/bv/core/extract-whole-2.cvc | 3 + .../regress0/bv/core/extract-whole-2.smt | 6 + .../regress0/bv/core/extract-whole-3.cvc | 2 + .../regress0/bv/core/extract-whole-3.smt | 6 + .../regress0/bv/core/extract-whole-4.cvc | 3 + .../regress0/bv/core/extract-whole-4.smt | 6 + 85 files changed, 830 insertions(+), 25 deletions(-) create mode 100644 src/theory/bv/theory_bv.cpp create mode 100644 src/theory/bv/theory_bv_rewrite_rules.cpp create mode 100644 src/theory/bv/theory_bv_rewrite_rules.h create mode 100644 src/theory/bv/theory_bv_utils.h create mode 100644 test/regress/regress0/bv/core/concat-merge-0.cvc create mode 100644 test/regress/regress0/bv/core/concat-merge-0.smt create mode 100644 test/regress/regress0/bv/core/concat-merge-1.cvc create mode 100644 test/regress/regress0/bv/core/concat-merge-1.smt create mode 100644 test/regress/regress0/bv/core/concat-merge-2.cvc create mode 100644 test/regress/regress0/bv/core/concat-merge-2.smt create mode 100644 test/regress/regress0/bv/core/concat-merge-3.cvc create mode 100644 test/regress/regress0/bv/core/concat-merge-3.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-0.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-0.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-1.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-1.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-10.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-10.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-11.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-11.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-2.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-2.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-3.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-3.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-4.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-4.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-5.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-5.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-6.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-6.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-7.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-7.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-8.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-8.smt create mode 100644 test/regress/regress0/bv/core/extract-concat-9.cvc create mode 100644 test/regress/regress0/bv/core/extract-concat-9.smt create mode 100644 test/regress/regress0/bv/core/extract-constant.cvc create mode 100644 test/regress/regress0/bv/core/extract-constant.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-0.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-0.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-1.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-1.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-10.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-10.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-11.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-11.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-2.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-2.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-3.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-3.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-4.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-4.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-5.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-5.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-6.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-6.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-7.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-7.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-8.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-8.smt create mode 100644 test/regress/regress0/bv/core/extract-extract-9.cvc create mode 100644 test/regress/regress0/bv/core/extract-extract-9.smt create mode 100644 test/regress/regress0/bv/core/extract-whole-0.cvc create mode 100644 test/regress/regress0/bv/core/extract-whole-0.smt create mode 100644 test/regress/regress0/bv/core/extract-whole-1.cvc create mode 100644 test/regress/regress0/bv/core/extract-whole-1.smt create mode 100644 test/regress/regress0/bv/core/extract-whole-2.cvc create mode 100644 test/regress/regress0/bv/core/extract-whole-2.smt create mode 100644 test/regress/regress0/bv/core/extract-whole-3.cvc create mode 100644 test/regress/regress0/bv/core/extract-whole-3.smt create mode 100644 test/regress/regress0/bv/core/extract-whole-4.cvc create mode 100644 test/regress/regress0/bv/core/extract-whole-4.smt diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 4a6dd794e..422cb47a8 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -902,13 +902,13 @@ expr::NodeValue* NodeBuilder::constructNV() { // check that there are the right # of children for this kind Assert(getMetaKind() != kind::metakind::CONSTANT, "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"); - Assert(d_nv->d_nchildren >= kind::metakind::getLowerBoundForKind(getKind()), + Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()), "Nodes with kind %s must have at least %u children (the one under " "construction has %u)", kind::kindToString(getKind()).c_str(), kind::metakind::getLowerBoundForKind(getKind()), getNumChildren()); - Assert(d_nv->d_nchildren <= kind::metakind::getUpperBoundForKind(getKind()), + Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()), "Nodes with kind %s must have at most %u children (the one under " "construction has %u)", kind::kindToString(getKind()).c_str(), @@ -1073,13 +1073,13 @@ expr::NodeValue* NodeBuilder::constructNV() const { // check that there are the right # of children for this kind Assert(getMetaKind() != kind::metakind::CONSTANT, "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"); - Assert(d_nv->d_nchildren >= kind::metakind::getLowerBoundForKind(getKind()), + Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()), "Nodes with kind %s must have at least %u children (the one under " "construction has %u)", kind::kindToString(getKind()).c_str(), kind::metakind::getLowerBoundForKind(getKind()), getNumChildren()); - Assert(d_nv->d_nchildren <= kind::metakind::getUpperBoundForKind(getKind()), + Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()), "Nodes with kind %s must have at most %u children (the one under " "construction has %u)", kind::kindToString(getKind()).c_str(), diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 37ed4fe20..b7bbe2ff8 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -277,7 +277,7 @@ TypeNode NodeManager::getType(TNode n, bool check) case kind::STORE: typeNode = CVC4::theory::arrays::ArrayStoreTypeRule::computeType(this, n, check); break; - case kind::BITVECTOR_CONST: + case kind::CONST_BITVECTOR: typeNode = CVC4::theory::bv::BitVectorConstantTypeRule::computeType(this, n, check); break; case kind::BITVECTOR_AND: diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index baa8de5aa..5c6a05a03 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -916,7 +916,6 @@ template inline Node NodeManager::mkNode(TNode opNode, const std::vector >& children) { - Assert(kind::metaKindOf(opNode.getKind()) == kind::metakind::PARAMETERIZED); NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind())); nb << opNode; nb.append(children); diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 940835a7e..82b15d199 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -175,6 +175,9 @@ public: /** Retrieve a Rational from the text of a token */ static Rational tokenToRational(pANTLR3_COMMON_TOKEN token); + /** Get a bitvector constant from the text of the number and the size token */ + static BitVector tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size); + protected: /** Create an input. This input takes ownership of the given input stream, * and will delete it at destruction time. @@ -230,9 +233,9 @@ inline std::string AntlrInput::tokenTextSubstr(pANTLR3_COMMON_TOKEN token, } start += index; if( n==0 || n >= (size_t) end - start ) { - return std::string( (const char *)start + index, end-start+1 ); + return std::string( (const char *)start, end-start+1 ); } else { - return std::string( (const char *)start + index, n ); + return std::string( (const char *)start, n ); } } @@ -252,6 +255,11 @@ inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) { return Rational::fromDecimal( tokenText(token) ); } +inline BitVector AntlrInput::tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size) { + std::string number_str = tokenTextSubstr(number, 2); + return BitVector(tokenToUnsigned(size), Integer(number_str)); +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index ecb3d39b6..55c158a6f 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -216,12 +216,6 @@ annotatedFormula[CVC4::Expr& expr] RPAREN_TOK { PARSER_STATE->popScope(); } - | /* a variable */ - ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] - | let_identifier[name,CHECK_DECLARED] - | flet_identifier[name,CHECK_DECLARED] ) - { expr = PARSER_STATE->getVariable(name); } - /* constants */ | TRUE_TOK { expr = MK_CONST(true); } | FALSE_TOK { expr = MK_CONST(false); } @@ -230,8 +224,17 @@ annotatedFormula[CVC4::Expr& expr] | RATIONAL_TOK { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } + | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']' + { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); } // NOTE: Theory constants go here /* TODO: quantifiers, arithmetic constants */ + + | /* a variable */ + ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] + | let_identifier[name,CHECK_DECLARED] + | flet_identifier[name,CHECK_DECLARED] ) + { expr = PARSER_STATE->getVariable(name); } + ; /** @@ -553,6 +556,7 @@ XOR_TOK : 'xor'; // Bitvector tokens BITVECTOR_TOK : 'BitVec'; +BV_TOK : 'bv'; CONCAT_TOK : 'concat'; EXTRACT_TOK : 'extract'; BVAND_TOK : 'bvand'; @@ -589,6 +593,14 @@ SIGN_EXTEND_TOK : 'sign_extend'; ROTATE_LEFT_TOK : 'rotate_left'; ROTATE_RIGHT_TOK : 'rotate_right'; +/** + * Mathces a bit-vector constant of the form bv123 + */ +BITVECTOR_BV_CONST + : 'bv' DIGIT+ + ; + + /** * Matches an identifier from the input. An identifier is a sequence of letters, * digits and "_", "'", "." symbols, starting with a letter. diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index fe7d77455..2e0e0087c 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -110,6 +110,9 @@ void Smt::addTheory(Theory theory) { addArithmeticOperators(); break; + case THEORY_BITVECTORS: + break; + default: Unhandled(theory); } @@ -170,6 +173,10 @@ void Smt::setLogic(const std::string& name) { addUf(); break; + case QF_BV: + addTheory(THEORY_BITVECTORS); + break; + case AUFLIA: case AUFLIRA: case AUFNIRA: @@ -177,7 +184,6 @@ void Smt::setLogic(const std::string& name) { case UFNIA: case QF_AUFBV: case QF_AUFLIA: - case QF_BV: Unhandled(name); } } diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index cab90bbdb..ad858ab53 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -7,6 +7,10 @@ noinst_LTLIBRARIES = libbv.la libbv_la_SOURCES = \ theory_bv.h \ + theory_bv.cpp \ + theory_bv_utils.h \ + theory_bv_rewrite_rules.h \ + theory_bv_rewrite_rules.cpp \ theory_bv_type_rules.h EXTRA_DIST = kinds diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index f1b926d24..54f861b76 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -12,13 +12,13 @@ constant BITVECTOR_TYPE \ "util/bitvector.h" \ "bit-vector type" -constant BITVECTOR_CONST \ +constant CONST_BITVECTOR \ ::CVC4::BitVector \ ::CVC4::BitVectorHashStrategy \ "util/bitvector.h" \ "a fixed-width bit-vector constant" -operator BITVECTOR_CONCAT 2 "bit-vector concatenation" +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" diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp new file mode 100644 index 000000000..849740c9a --- /dev/null +++ b/src/theory/bv/theory_bv.cpp @@ -0,0 +1,60 @@ +#include "theory_bv.h" +#include "theory_bv_utils.h" +#include "theory_bv_rewrite_rules.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; + +RewriteResponse TheoryBV::postRewrite(TNode node, bool topLevel) { + + Debug("bitvector") << "postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ")" << std::endl; + + Node result; + + if (node.getKind() == kind::CONST_BITVECTOR /* || isLeaf(n)) */) + result = node; + else { + switch (node.getKind()) { + case kind::BITVECTOR_CONCAT: + result = LinearRewriteStrategy< + // Flatten the top level concatenations + CoreRewriteRules::ConcatFlatten, + // Merge the adjacent extracts on non-constants + CoreRewriteRules::ConcatExtractMerge, + // Merge the adjacent extracts on constants + CoreRewriteRules::ConcatConstantMerge, + // At this point only Extract-Whole could apply, if the result is only one extract + // or at some sub-expression if the result is a concatenation. + ApplyRuleToChildren + >::apply(node); + break; + case kind::BITVECTOR_EXTRACT: + result = LinearRewriteStrategy< + // Extract over a constant gives a constant + CoreRewriteRules::ExtractConstant, + // Extract over an extract is simplified to one extract + CoreRewriteRules::ExtractExtract, + // Extract over a concatenation is distributed to the appropriate concatenations + CoreRewriteRules::ExtractConcat, + // At this point only Extract-Whole could apply + CoreRewriteRules::ExtractWhole + >::apply(node); + break; + case kind::EQUAL: + if (node[0] == node[1]) result = mkTrue(); + else result = node; + break; + default: + // TODO: figure out when this is an operator + result = node; + break; + // Unhandled(); + } + } + + Debug("bitvector") << "postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ") => " << result << std::endl; + + return RewriteComplete(result); +} diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 537e7f5fe..ee331af02 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -33,12 +33,12 @@ public: TheoryBV(int id, context::Context* c, OutputChannel& out) : Theory(id, c, out) { } - - void preRegisterTerm(TNode n) { Unimplemented(); } - void registerTerm(TNode n) { Unimplemented(); } + void preRegisterTerm(TNode n) { } + void registerTerm(TNode n) { } void check(Effort e) {} void propagate(Effort e) {} - void explain(TNode n, Effort e) { Unimplemented(); } + void explain(TNode n, Effort e) { } + RewriteResponse postRewrite(TNode n, bool topLevel); std::string identify() const { return std::string("TheoryBV"); } };/* class TheoryBV */ diff --git a/src/theory/bv/theory_bv_rewrite_rules.cpp b/src/theory/bv/theory_bv_rewrite_rules.cpp new file mode 100644 index 000000000..5473768bb --- /dev/null +++ b/src/theory/bv/theory_bv_rewrite_rules.cpp @@ -0,0 +1,249 @@ +#include +#include "expr/node_builder.h" +#include "theory_bv_rewrite_rules.h" +#include "theory_bv_utils.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; + +bool CoreRewriteRules::ConcatFlatten::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_CONCAT); +} + +Node CoreRewriteRules::ConcatFlatten::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ConcatFlatten(" << node << ")" << endl; + + NodeBuilder<> result(kind::BITVECTOR_CONCAT); + vector processing_stack; + processing_stack.push_back(node); + while (!processing_stack.empty()) { + Node current = processing_stack.back(); + processing_stack.pop_back(); + if (current.getKind() == kind::BITVECTOR_CONCAT) { + for (int i = current.getNumChildren() - 1; i >= 0; i--) + processing_stack.push_back(current[i]); + } else { + result << current; + } + } + + Debug("bitvector") << "ConcatFlatten(" << node << ") => " << result << endl; + + return result; +} + +bool CoreRewriteRules::ConcatExtractMerge::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_CONCAT); +} + +Node CoreRewriteRules::ConcatExtractMerge::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ConcatExtractMerge(" << node << ")" << endl; + + vector mergedExtracts; + + Node current = node[0]; + bool mergeStarted = false; + unsigned currentHigh = 0; + unsigned currentLow = 0; + + for(size_t i = 1, end = node.getNumChildren(); i < end; ++ i) { + // The next candidate for merging + Node next = node[i]; + // If the current is not an extract we just go to the next + if (current.getKind() != kind::BITVECTOR_EXTRACT) { + mergedExtracts.push_back(current); + current = next; + continue; + } + // If it is an extract and the first one, get the extract parameters + else if (!mergeStarted) { + currentHigh = getExtractHigh(current); + currentLow = getExtractLow(current); + } + + // If the next one can be merged, try to merge + bool merged = false; + if (next.getKind() == kind::BITVECTOR_EXTRACT && current[0] == next[0]) { + //x[i : j] @ x[j − 1 : k] -> c x[i : k] + unsigned nextHigh = getExtractHigh(next); + unsigned nextLow = getExtractLow(next); + if(nextHigh + 1 == currentLow) { + currentLow = nextLow; + mergeStarted = true; + merged = true; + } + } + // If we haven't merged anything, add the previous merge and continue with the next + if (!merged) { + if (!mergeStarted) mergedExtracts.push_back(current); + else mergedExtracts.push_back(mkExtract(current[0], currentHigh, currentLow)); + current = next; + mergeStarted = false; + } + } + + // Add the last child + if (!mergeStarted) mergedExtracts.push_back(current); + else mergedExtracts.push_back(mkExtract(current[0], currentHigh, currentLow)); + + // Create the result + Node result = mkConcat(mergedExtracts); + + Debug("bitvector") << "ConcatExtractMerge(" << node << ") =>" << result << endl; + + // Return the result + return result; +} + +bool CoreRewriteRules::ConcatConstantMerge::applies(Node node) { + return node.getKind() == kind::BITVECTOR_CONCAT; +} + +Node CoreRewriteRules::ConcatConstantMerge::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ConcatConstantMerge(" << node << ")" << endl; + + vector mergedConstants; + for (unsigned i = 0, end = node.getNumChildren(); i < end;) { + if (node[i].getKind() != kind::CONST_BITVECTOR) { + // If not a constant, just add it + mergedConstants.push_back(node[i]); + ++i; + } else { + // Find the longest sequence of constants + unsigned j = i + 1; + while (j < end) { + if (node[j].getKind() != kind::CONST_BITVECTOR) { + break; + } else { + ++ j; + } + } + // Append all the constants + BitVector current = node[i].getConst(); + for (unsigned k = i + 1; k < j; ++ k) { + current = current.concat(node[k].getConst()); + } + // Add the new merged constant + mergedConstants.push_back(mkConst(current)); + i = j + 1; + } + } + + Node result = mkConcat(mergedConstants); + + Debug("bitvector") << "ConcatConstantMerge(" << node << ") => " << result << endl; + + return result; +} + +bool CoreRewriteRules::ExtractWhole::applies(Node node) { + if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; + unsigned length = getSize(node[0]); + unsigned extractHigh = getExtractHigh(node); + if (extractHigh != length - 1) return false; + unsigned extractLow = getExtractLow(node); + if (extractLow != 0) return false; + return true; +} + +Node CoreRewriteRules::ExtractWhole::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ExtractWhole(" << node << ")" << endl; + Debug("bitvector") << "ExtractWhole(" << node << ") => " << node[0] << endl; + + return node[0]; +} + +bool CoreRewriteRules::ExtractConstant::applies(Node node) { + if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; + if (node[0].getKind() != kind::CONST_BITVECTOR) return false; + return true; +} + +Node CoreRewriteRules::ExtractConstant::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ExtractConstant(" << node << ")" << endl; + + Node child = node[0]; + BitVector childValue = child.getConst(); + + Node result = mkConst(childValue.extract(getExtractHigh(node), getExtractLow(node))); + + Debug("bitvector") << "ExtractConstant(" << node << ") => " << result << endl; + + return result; +} + +bool CoreRewriteRules::ExtractConcat::applies(Node node) { + if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; + if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false; + return true; +} + +Node CoreRewriteRules::ExtractConcat::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ExtractConcat(" << node << ")" << endl; + + int extract_high = getExtractHigh(node); + int extract_low = getExtractLow(node); + + vector resultChildren; + + Node concat = node[0]; + for (int i = concat.getNumChildren() - 1; i >= 0 && extract_high >= 0; i--) { + Node concatChild = concat[i]; + int concatChildSize = getSize(concatChild); + if (extract_low < concatChildSize) { + int extract_start = extract_low < 0 ? 0 : extract_low; + int extract_end = extract_high < concatChildSize ? extract_high : concatChildSize - 1; + resultChildren.push_back(mkExtract(concatChild, extract_end, extract_start)); + } + extract_low -= concatChildSize; + extract_high -= concatChildSize; + } + + std::reverse(resultChildren.begin(), resultChildren.end()); + + Node result = mkConcat(resultChildren); + + Debug("bitvector") << "ExtractConcat(" << node << ") => " << result << endl; + + return result; +} + +bool CoreRewriteRules::ExtractExtract::applies(Node node) { + if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; + if (node[0].getKind() != kind::BITVECTOR_EXTRACT) return false; + return true; +} + +Node CoreRewriteRules::ExtractExtract::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ExtractExtract(" << node << ")" << endl; + + // x[i:j][k:l] ~> x[k+j:l+j] + Node child = node[0]; + unsigned k = getExtractHigh(node); + unsigned l = getExtractLow(node); + unsigned j = getExtractLow(child); + + Node result = mkExtract(child[0], k + j, l + j); + + Debug("bitvector") << "ExtractExtract(" << node << ") => " << result << endl; + + return result; + +} diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h new file mode 100644 index 000000000..48696ce33 --- /dev/null +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -0,0 +1,104 @@ +#pragma once + +#include "cvc4_private.h" +#include "theory/theory.h" +#include "context/context.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +struct CoreRewriteRules { + + struct EmptyRule { + static inline Node apply(Node node) { return node; } + static inline bool applies(Node node) { return false; } + }; + + struct ConcatFlatten { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ConcatExtractMerge { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ConcatConstantMerge { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ExtractExtract { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ExtractWhole { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ExtractConcat { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ExtractConstant { + static Node apply(Node node); + static bool applies(Node node); + }; + +}; + +template +struct ApplyRuleToChildren { + + static Node apply(Node node) { + if (node.getKind() != kind) { + if (Rule::applies(node)) return Rule::apply(node); + else return node; + } + NodeBuilder<> result(kind); + for (unsigned i = 0, end = node.getNumChildren(); i < end; ++ i) { + if (Rule::applies(node[i])) result << Rule::apply(node[i]); + else result << node[i]; + } + return result; + } + + static bool applies(Node node) { + if (node.getKind() == kind) return true; + return Rule::applies(node); + } + +}; + + +template < + typename R1, + typename R2, + typename R3 = CoreRewriteRules::EmptyRule, + typename R4 = CoreRewriteRules::EmptyRule, + typename R5 = CoreRewriteRules::EmptyRule, + typename R6 = CoreRewriteRules::EmptyRule, + typename R7 = CoreRewriteRules::EmptyRule + > +struct LinearRewriteStrategy { + static Node apply(Node node) { + Node current = node; + if (R1::applies(current)) current = R1::apply(current); + if (R2::applies(current)) current = R2::apply(current); + if (R3::applies(current)) current = R3::apply(current); + if (R4::applies(current)) current = R4::apply(current); + if (R5::applies(current)) current = R5::apply(current); + if (R6::applies(current)) current = R6::apply(current); + if (R7::applies(current)) current = R7::apply(current); + return current; + } +}; + +} // End namespace bv +} // End namespace theory +} // End namespace CVC4 diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 9bb9e61df..7c4ff495e 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -142,7 +142,7 @@ public: TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); for (; it != it_end; ++ it) { - TypeNode t = n[0].getType(check); + TypeNode t = (*it).getType(check); // NOTE: We're throwing a type-checking exception here even // when check is false, bc if we don't check that the arguments // are bit-vectors the result type will be inaccurate diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h new file mode 100644 index 000000000..fa948465d --- /dev/null +++ b/src/theory/bv/theory_bv_utils.h @@ -0,0 +1,53 @@ +#pragma once + +#include +#include "expr/node_manager.h" + +namespace CVC4 { +namespace theory { +namespace bv { +namespace utils { + +inline unsigned getExtractHigh(TNode node) { + return node.getOperator().getConst().high; +} + +inline unsigned getExtractLow(TNode node) { + return node.getOperator().getConst().low; +} + +inline unsigned getSize(TNode node) { + return node.getType().getBitVectorSize(); +} + +inline Node mkTrue() { + return NodeManager::currentNM()->mkConst(true); +} + +inline Node mkFalse() { + return NodeManager::currentNM()->mkConst(false); +} + +inline Node mkExtract(TNode node, unsigned high, unsigned low) { + Node extractOp = NodeManager::currentNM()->mkConst(BitVectorExtract(high, low)); + std::vector children; + children.push_back(node); + return NodeManager::currentNM()->mkNode(extractOp, children); +} + +inline Node mkConcat(std::vector& children) { + if (children.size() > 1) + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children); + else + return children[0]; +} + +inline Node mkConst(const BitVector& value) { + return NodeManager::currentNM()->mkConst(value); +} + + +} +} +} +} diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 0b5952481..5c05bd6a7 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -35,10 +35,11 @@ private: unsigned d_size; Integer d_value; - BitVector(unsigned size, const Integer& val) : d_size(size), d_value(val) {} - public: + BitVector(unsigned size, const Integer& val) + : d_size(size), d_value(val) {} + BitVector(unsigned size = 0) : d_size(size), d_value(0) {} @@ -58,6 +59,7 @@ public: BitVector& operator =(const BitVector& x) { if(this == &x) return *this; + d_size = x.d_size; d_value = x.d_value; return *this; } @@ -92,8 +94,16 @@ public: return BitVector(d_size, d_value); } + BitVector concat (const BitVector& other) const { + return BitVector(d_size + other.d_size, (d_value * Integer(2).pow(other.d_size)) + other.d_value); + } + + BitVector extract(unsigned high, unsigned low) { + return BitVector(high - low + 1, (d_value % (Integer(2).pow(high + 1))) / Integer(2).pow(low)); + } + size_t hash() const { - return d_value.hash(); + return d_value.hash() + d_size; } std::string toString(unsigned int base = 2) const { diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 8551d0a6a..233b3aa08 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -152,6 +152,14 @@ public: return Integer( d_value * y.d_value ); } + Integer operator/(const Integer& y) const { + return Integer( cln::floor1(d_value, y.d_value) ); + } + + Integer operator%(const Integer& y) const { + return Integer( cln::floor2(d_value, y.d_value).remainder ); + } + /** Raise this Integer to the power exp. * * @param exp the exponent diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index b065dca23..4b2ab1a79 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -123,6 +123,9 @@ public: Integer operator/(const Integer& y) const { return Integer( d_value / y.d_value ); } + Integer operator%(const Integer& y) const { + return Integer( d_value % y.d_value ); + } /** Raise this Integer to the power exp. * diff --git a/test/regress/regress0/bv/core/concat-merge-0.cvc b/test/regress/regress0/bv/core/concat-merge-0.cvc new file mode 100644 index 000000000..60341c03b --- /dev/null +++ b/test/regress/regress0/bv/core/concat-merge-0.cvc @@ -0,0 +1,3 @@ +x : BITVECTOR(32); +QUERY (x[2:1] @ x[0:0] = x[2:0] ); + diff --git a/test/regress/regress0/bv/core/concat-merge-0.smt b/test/regress/regress0/bv/core/concat-merge-0.smt new file mode 100644 index 000000000..c68d4ec53 --- /dev/null +++ b/test/regress/regress0/bv/core/concat-merge-0.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (concat (extract[2:1] x) (extract[0:0] x)) (extract[2:0] x))) +) diff --git a/test/regress/regress0/bv/core/concat-merge-1.cvc b/test/regress/regress0/bv/core/concat-merge-1.cvc new file mode 100644 index 000000000..af0e8387b --- /dev/null +++ b/test/regress/regress0/bv/core/concat-merge-1.cvc @@ -0,0 +1,3 @@ +x : BITVECTOR(32); +QUERY (x[4:2] @ x[1:0] = x[4:0] ); + diff --git a/test/regress/regress0/bv/core/concat-merge-1.smt b/test/regress/regress0/bv/core/concat-merge-1.smt new file mode 100644 index 000000000..4b6702598 --- /dev/null +++ b/test/regress/regress0/bv/core/concat-merge-1.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (concat (extract[4:2] x) (extract[1:0] x)) (extract[4:0] x))) +) diff --git a/test/regress/regress0/bv/core/concat-merge-2.cvc b/test/regress/regress0/bv/core/concat-merge-2.cvc new file mode 100644 index 000000000..8ad7f2aa3 --- /dev/null +++ b/test/regress/regress0/bv/core/concat-merge-2.cvc @@ -0,0 +1,3 @@ +x : BITVECTOR(32); +QUERY (x[8:4] @ x[3:0] = x[8:0] ); + diff --git a/test/regress/regress0/bv/core/concat-merge-2.smt b/test/regress/regress0/bv/core/concat-merge-2.smt new file mode 100644 index 000000000..2350d6d8b --- /dev/null +++ b/test/regress/regress0/bv/core/concat-merge-2.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (concat (extract[8:4] x) (extract[3:0] x)) (extract[8:0] x))) +) diff --git a/test/regress/regress0/bv/core/concat-merge-3.cvc b/test/regress/regress0/bv/core/concat-merge-3.cvc new file mode 100644 index 000000000..d46da1a55 --- /dev/null +++ b/test/regress/regress0/bv/core/concat-merge-3.cvc @@ -0,0 +1,3 @@ +x : BITVECTOR(32); +QUERY (x[16:8] @ x[7:0] = x[16:0]); + diff --git a/test/regress/regress0/bv/core/concat-merge-3.smt b/test/regress/regress0/bv/core/concat-merge-3.smt new file mode 100644 index 000000000..303357541 --- /dev/null +++ b/test/regress/regress0/bv/core/concat-merge-3.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (concat (extract[16:8] x) (extract[7:0] x)) (extract[16:0] x))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-0.cvc b/test/regress/regress0/bv/core/extract-concat-0.cvc new file mode 100644 index 000000000..9aa608265 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-0.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[63:32] = x[31:0]); diff --git a/test/regress/regress0/bv/core/extract-concat-0.smt b/test/regress/regress0/bv/core/extract-concat-0.smt new file mode 100644 index 000000000..c4d6c7e02 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-0.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[63:32] (concat x y)) (extract[31:0] x))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-1.cvc b/test/regress/regress0/bv/core/extract-concat-1.cvc new file mode 100644 index 000000000..e192f159c --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-1.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[62:33] = x[30:1]); diff --git a/test/regress/regress0/bv/core/extract-concat-1.smt b/test/regress/regress0/bv/core/extract-concat-1.smt new file mode 100644 index 000000000..0f5a2c187 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-1.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[62:33] (concat x y)) (extract[30:1] x))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-10.cvc b/test/regress/regress0/bv/core/extract-concat-10.cvc new file mode 100644 index 000000000..8d3b88fba --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-10.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[60:3] = x[28:0] @ y[31:3]); diff --git a/test/regress/regress0/bv/core/extract-concat-10.smt b/test/regress/regress0/bv/core/extract-concat-10.smt new file mode 100644 index 000000000..ed44a9abb --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-10.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[60:3] (concat x y)) (concat (extract[28:0] x) (extract[31:3] y)))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-11.cvc b/test/regress/regress0/bv/core/extract-concat-11.cvc new file mode 100644 index 000000000..2290eef04 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-11.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[59:4] = x[27:0] @ y[31:4]); diff --git a/test/regress/regress0/bv/core/extract-concat-11.smt b/test/regress/regress0/bv/core/extract-concat-11.smt new file mode 100644 index 000000000..ed1f6275e --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-11.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[59:4] (concat x y)) (concat (extract[27:0] x) (extract[31:4] y)))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-2.cvc b/test/regress/regress0/bv/core/extract-concat-2.cvc new file mode 100644 index 000000000..bd1e3ff30 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-2.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[61:34] = x[29:2]); diff --git a/test/regress/regress0/bv/core/extract-concat-2.smt b/test/regress/regress0/bv/core/extract-concat-2.smt new file mode 100644 index 000000000..fb8c61464 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-2.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[61:34] (concat x y)) (extract[29:2] x))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-3.cvc b/test/regress/regress0/bv/core/extract-concat-3.cvc new file mode 100644 index 000000000..4e225be42 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-3.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[60:35] = x[28:3]); diff --git a/test/regress/regress0/bv/core/extract-concat-3.smt b/test/regress/regress0/bv/core/extract-concat-3.smt new file mode 100644 index 000000000..f89115ecf --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-3.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[60:35] (concat x y)) (extract[28:3] x))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-4.cvc b/test/regress/regress0/bv/core/extract-concat-4.cvc new file mode 100644 index 000000000..8ecf96e6f --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-4.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[31:0] = y[31:0]); diff --git a/test/regress/regress0/bv/core/extract-concat-4.smt b/test/regress/regress0/bv/core/extract-concat-4.smt new file mode 100644 index 000000000..29ea62916 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-4.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[31:0] (concat x y)) (extract[31:0] y))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-5.cvc b/test/regress/regress0/bv/core/extract-concat-5.cvc new file mode 100644 index 000000000..378ca5d2a --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-5.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[30:1] = y[30:1]); diff --git a/test/regress/regress0/bv/core/extract-concat-5.smt b/test/regress/regress0/bv/core/extract-concat-5.smt new file mode 100644 index 000000000..8f137ef05 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-5.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[30:1] (concat x y)) (extract[30:1] y))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-6.cvc b/test/regress/regress0/bv/core/extract-concat-6.cvc new file mode 100644 index 000000000..41499b55b --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-6.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[29:2] = y[29:2]); diff --git a/test/regress/regress0/bv/core/extract-concat-6.smt b/test/regress/regress0/bv/core/extract-concat-6.smt new file mode 100644 index 000000000..0ef6e2ee6 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-6.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[29:2] (concat x y)) (extract[29:2] y))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-7.cvc b/test/regress/regress0/bv/core/extract-concat-7.cvc new file mode 100644 index 000000000..838017f55 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-7.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[28:3] = y[28:3]); diff --git a/test/regress/regress0/bv/core/extract-concat-7.smt b/test/regress/regress0/bv/core/extract-concat-7.smt new file mode 100644 index 000000000..f1a9bf161 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-7.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[28:3] (concat x y)) (extract[28:3] y))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-8.cvc b/test/regress/regress0/bv/core/extract-concat-8.cvc new file mode 100644 index 000000000..68982b0a6 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-8.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[62:1] = x[30:0] @ y[31:1]); diff --git a/test/regress/regress0/bv/core/extract-concat-8.smt b/test/regress/regress0/bv/core/extract-concat-8.smt new file mode 100644 index 000000000..c317e94e1 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-8.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[62:1] (concat x y)) (concat (extract[30:0] x) (extract[31:1] y)))) +) diff --git a/test/regress/regress0/bv/core/extract-concat-9.cvc b/test/regress/regress0/bv/core/extract-concat-9.cvc new file mode 100644 index 000000000..5f0e690cb --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-9.cvc @@ -0,0 +1,2 @@ +x, y : BITVECTOR(32); +QUERY ((x @ y)[61:2] = x[29:0] @ y[31:2]); diff --git a/test/regress/regress0/bv/core/extract-concat-9.smt b/test/regress/regress0/bv/core/extract-concat-9.smt new file mode 100644 index 000000000..668842dfc --- /dev/null +++ b/test/regress/regress0/bv/core/extract-concat-9.smt @@ -0,0 +1,7 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :formula +(not (= (extract[61:2] (concat x y)) (concat (extract[29:0] x) (extract[31:2] y)))) +) diff --git a/test/regress/regress0/bv/core/extract-constant.cvc b/test/regress/regress0/bv/core/extract-constant.cvc new file mode 100644 index 000000000..e70ccbf5e --- /dev/null +++ b/test/regress/regress0/bv/core/extract-constant.cvc @@ -0,0 +1,2 @@ +QUERY (0bin000111000[6:2] = 0bin01110); + diff --git a/test/regress/regress0/bv/core/extract-constant.smt b/test/regress/regress0/bv/core/extract-constant.smt new file mode 100644 index 000000000..a36bb6ea7 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-constant.smt @@ -0,0 +1,5 @@ +(benchmark B_ + :logic QF_BV + :formula +(not (= (extract[6:2] bv56[9]) bv14[5])) +) diff --git a/test/regress/regress0/bv/core/extract-extract-0.cvc b/test/regress/regress0/bv/core/extract-extract-0.cvc new file mode 100644 index 000000000..7d1a4542c --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-0.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[31:0][31:0] = x[31:0]); diff --git a/test/regress/regress0/bv/core/extract-extract-0.smt b/test/regress/regress0/bv/core/extract-extract-0.smt new file mode 100644 index 000000000..971ad9e8d --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-0.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(let (?cvc_0 (extract[31:0] x)) (not (= (extract[31:0] ?cvc_0) ?cvc_0))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-1.cvc b/test/regress/regress0/bv/core/extract-extract-1.cvc new file mode 100644 index 000000000..86158e1cb --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-1.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[31:0][15:1] = x[15:1]); diff --git a/test/regress/regress0/bv/core/extract-extract-1.smt b/test/regress/regress0/bv/core/extract-extract-1.smt new file mode 100644 index 000000000..098e417b9 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-1.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (extract[15:1] (extract[31:0] x)) (extract[15:1] x))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-10.cvc b/test/regress/regress0/bv/core/extract-extract-10.cvc new file mode 100644 index 000000000..4710aa65a --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-10.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[7:2][2:2] = x[4:4]); diff --git a/test/regress/regress0/bv/core/extract-extract-10.smt b/test/regress/regress0/bv/core/extract-extract-10.smt new file mode 100644 index 000000000..d277f5fdb --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-10.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (extract[2:2] (extract[7:2] x)) (extract[4:4] x))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-11.cvc b/test/regress/regress0/bv/core/extract-extract-11.cvc new file mode 100644 index 000000000..27c7e1baa --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-11.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[30:1][28:2][26:3][23:4][19:5][14:6][8:7][0:0] = x[28:28]); \ No newline at end of file diff --git a/test/regress/regress0/bv/core/extract-extract-11.smt b/test/regress/regress0/bv/core/extract-extract-11.smt new file mode 100644 index 000000000..189c7ef47 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-11.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (extract[0:0] (extract[8:7] (extract[14:6] (extract[19:5] (extract[23:4] (extract[26:3] (extract[28:2] (extract[30:1] x)))))))) (extract[28:28] x))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-2.cvc b/test/regress/regress0/bv/core/extract-extract-2.cvc new file mode 100644 index 000000000..fc90ab275 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-2.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[31:0][7:2] = x[7:2]); diff --git a/test/regress/regress0/bv/core/extract-extract-2.smt b/test/regress/regress0/bv/core/extract-extract-2.smt new file mode 100644 index 000000000..f423ec9ad --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-2.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (extract[7:2] (extract[31:0] x)) (extract[7:2] x))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-3.cvc b/test/regress/regress0/bv/core/extract-extract-3.cvc new file mode 100644 index 000000000..3344c0359 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-3.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[31:0][4:4] = x[4:4]); diff --git a/test/regress/regress0/bv/core/extract-extract-3.smt b/test/regress/regress0/bv/core/extract-extract-3.smt new file mode 100644 index 000000000..e614c4c92 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-3.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (extract[4:4] (extract[31:0] x)) (extract[4:4] x))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-4.cvc b/test/regress/regress0/bv/core/extract-extract-4.cvc new file mode 100644 index 000000000..0ad43466b --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-4.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[15:1][14:0] = x[15:1]); diff --git a/test/regress/regress0/bv/core/extract-extract-4.smt b/test/regress/regress0/bv/core/extract-extract-4.smt new file mode 100644 index 000000000..2b9c92946 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-4.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(let (?cvc_0 (extract[15:1] x)) (not (= (extract[14:0] ?cvc_0) ?cvc_0))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-5.cvc b/test/regress/regress0/bv/core/extract-extract-5.cvc new file mode 100644 index 000000000..0d6690527 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-5.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[15:1][7:1] = x[8:2]); diff --git a/test/regress/regress0/bv/core/extract-extract-5.smt b/test/regress/regress0/bv/core/extract-extract-5.smt new file mode 100644 index 000000000..0623ce997 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-5.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (extract[7:1] (extract[15:1] x)) (extract[8:2] x))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-6.cvc b/test/regress/regress0/bv/core/extract-extract-6.cvc new file mode 100644 index 000000000..4c344f619 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-6.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[15:1][3:2] = x[4:3]); diff --git a/test/regress/regress0/bv/core/extract-extract-6.smt b/test/regress/regress0/bv/core/extract-extract-6.smt new file mode 100644 index 000000000..851bd6f68 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-6.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (extract[3:2] (extract[15:1] x)) (extract[4:3] x))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-7.cvc b/test/regress/regress0/bv/core/extract-extract-7.cvc new file mode 100644 index 000000000..f911226bc --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-7.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[15:1][3:3] = x[4:4]); diff --git a/test/regress/regress0/bv/core/extract-extract-7.smt b/test/regress/regress0/bv/core/extract-extract-7.smt new file mode 100644 index 000000000..e6a2acc13 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-7.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (extract[3:3] (extract[15:1] x)) (extract[4:4] x))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-8.cvc b/test/regress/regress0/bv/core/extract-extract-8.cvc new file mode 100644 index 000000000..9b782a70e --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-8.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[7:2][5:0] = x[7:2]); diff --git a/test/regress/regress0/bv/core/extract-extract-8.smt b/test/regress/regress0/bv/core/extract-extract-8.smt new file mode 100644 index 000000000..7a808f31a --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-8.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(let (?cvc_0 (extract[7:2] x)) (not (= (extract[5:0] ?cvc_0) ?cvc_0))) +) diff --git a/test/regress/regress0/bv/core/extract-extract-9.cvc b/test/regress/regress0/bv/core/extract-extract-9.cvc new file mode 100644 index 000000000..85c0acf49 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-9.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[7:2][3:1] = x[5:3]); diff --git a/test/regress/regress0/bv/core/extract-extract-9.smt b/test/regress/regress0/bv/core/extract-extract-9.smt new file mode 100644 index 000000000..7a3c8e3da --- /dev/null +++ b/test/regress/regress0/bv/core/extract-extract-9.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (extract[3:1] (extract[7:2] x)) (extract[5:3] x))) +) diff --git a/test/regress/regress0/bv/core/extract-whole-0.cvc b/test/regress/regress0/bv/core/extract-whole-0.cvc new file mode 100644 index 000000000..ea7e991cd --- /dev/null +++ b/test/regress/regress0/bv/core/extract-whole-0.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (0bin0 @ x[31:31] @ x[30:20] @ x[19:10] @ x[9:1] @ x[0:0] @ 0bin0 = 0bin0 @ x @ 0bin0); diff --git a/test/regress/regress0/bv/core/extract-whole-0.smt b/test/regress/regress0/bv/core/extract-whole-0.smt new file mode 100644 index 000000000..83025250f --- /dev/null +++ b/test/regress/regress0/bv/core/extract-whole-0.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (concat (concat (concat (concat (concat (concat bv0[1] (extract[31:31] x)) (extract[30:20] x)) (extract[19:10] x)) (extract[9:1] x)) (extract[0:0] x)) bv0[1]) (concat (concat bv0[1] x) bv0[1]))) +) diff --git a/test/regress/regress0/bv/core/extract-whole-1.cvc b/test/regress/regress0/bv/core/extract-whole-1.cvc new file mode 100644 index 000000000..8115c20b4 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-whole-1.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (x[31:31] @ x[30:20] @ x[19:10] @ x[9:1] @ x[0:0] = x); diff --git a/test/regress/regress0/bv/core/extract-whole-1.smt b/test/regress/regress0/bv/core/extract-whole-1.smt new file mode 100644 index 000000000..bc74e0ca9 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-whole-1.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (concat (concat (concat (concat (extract[31:31] x) (extract[30:20] x)) (extract[19:10] x)) (extract[9:1] x)) (extract[0:0] x)) x)) +) diff --git a/test/regress/regress0/bv/core/extract-whole-2.cvc b/test/regress/regress0/bv/core/extract-whole-2.cvc new file mode 100644 index 000000000..c6eb38be1 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-whole-2.cvc @@ -0,0 +1,3 @@ +x : BITVECTOR(32); +QUERY (x @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 = x @ 0bin010101); + diff --git a/test/regress/regress0/bv/core/extract-whole-2.smt b/test/regress/regress0/bv/core/extract-whole-2.smt new file mode 100644 index 000000000..c661678eb --- /dev/null +++ b/test/regress/regress0/bv/core/extract-whole-2.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (concat (concat (concat (concat (concat (concat x bv0[1]) bv1[1]) bv0[1]) bv1[1]) bv0[1]) bv1[1]) (concat x bv21[6]))) +) diff --git a/test/regress/regress0/bv/core/extract-whole-3.cvc b/test/regress/regress0/bv/core/extract-whole-3.cvc new file mode 100644 index 000000000..689383b7a --- /dev/null +++ b/test/regress/regress0/bv/core/extract-whole-3.cvc @@ -0,0 +1,2 @@ +x : BITVECTOR(32); +QUERY (0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ x = 0bin010101 @ x); diff --git a/test/regress/regress0/bv/core/extract-whole-3.smt b/test/regress/regress0/bv/core/extract-whole-3.smt new file mode 100644 index 000000000..2767384af --- /dev/null +++ b/test/regress/regress0/bv/core/extract-whole-3.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (concat (concat (concat (concat (concat (concat bv0[1] bv1[1]) bv0[1]) bv1[1]) bv0[1]) bv1[1]) x) (concat bv21[6] x))) +) diff --git a/test/regress/regress0/bv/core/extract-whole-4.cvc b/test/regress/regress0/bv/core/extract-whole-4.cvc new file mode 100644 index 000000000..1a3f367a0 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-whole-4.cvc @@ -0,0 +1,3 @@ +x : BITVECTOR(32); +QUERY (x[31:0] = x); + diff --git a/test/regress/regress0/bv/core/extract-whole-4.smt b/test/regress/regress0/bv/core/extract-whole-4.smt new file mode 100644 index 000000000..41d2f0594 --- /dev/null +++ b/test/regress/regress0/bv/core/extract-whole-4.smt @@ -0,0 +1,6 @@ +(benchmark B_ + :logic QF_BV + :extrafuns ((x BitVec[32])) + :formula +(not (= (extract[31:0] x) x)) +) -- 2.30.2