// 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(),
// 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(),
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:
inline Node NodeManager::mkNode(TNode opNode,
const std::vector<NodeTemplate<ref_count> >&
children) {
- Assert(kind::metaKindOf(opNode.getKind()) == kind::metakind::PARAMETERIZED);
NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
nb << opNode;
nb.append(children);
/** 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.
}
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 );
}
}
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 */
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); }
| 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); }
+
;
/**
// Bitvector tokens
BITVECTOR_TOK : 'BitVec';
+BV_TOK : 'bv';
CONCAT_TOK : 'concat';
EXTRACT_TOK : 'extract';
BVAND_TOK : 'bvand';
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.
addArithmeticOperators();
break;
+ case THEORY_BITVECTORS:
+ break;
+
default:
Unhandled(theory);
}
addUf();
break;
+ case QF_BV:
+ addTheory(THEORY_BITVECTORS);
+ break;
+
case AUFLIA:
case AUFLIRA:
case AUFNIRA:
case UFNIA:
case QF_AUFBV:
case QF_AUFLIA:
- case QF_BV:
Unhandled(name);
}
}
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
"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"
--- /dev/null
+#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<kind::BITVECTOR_CONCAT, CoreRewriteRules::ExtractWhole>
+ >::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);
+}
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 */
--- /dev/null
+#include <vector>
+#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<Node> 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<Node> 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<Node> 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<BitVector>();
+ for (unsigned k = i + 1; k < j; ++ k) {
+ current = current.concat(node[k].getConst<BitVector>());
+ }
+ // 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<BitVector>();
+
+ 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<Node> 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;
+
+}
--- /dev/null
+#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<Kind kind, typename Rule>
+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
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
--- /dev/null
+#pragma once
+
+#include <vector>
+#include "expr/node_manager.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+namespace utils {
+
+inline unsigned getExtractHigh(TNode node) {
+ return node.getOperator().getConst<BitVectorExtract>().high;
+}
+
+inline unsigned getExtractLow(TNode node) {
+ return node.getOperator().getConst<BitVectorExtract>().low;
+}
+
+inline unsigned getSize(TNode node) {
+ return node.getType().getBitVectorSize();
+}
+
+inline Node mkTrue() {
+ return NodeManager::currentNM()->mkConst<bool>(true);
+}
+
+inline Node mkFalse() {
+ return NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+inline Node mkExtract(TNode node, unsigned high, unsigned low) {
+ Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
+ std::vector<Node> children;
+ children.push_back(node);
+ return NodeManager::currentNM()->mkNode(extractOp, children);
+}
+
+inline Node mkConcat(std::vector<Node>& 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<BitVector>(value);
+}
+
+
+}
+}
+}
+}
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) {}
BitVector& operator =(const BitVector& x) {
if(this == &x)
return *this;
+ d_size = x.d_size;
d_value = x.d_value;
return *this;
}
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 {
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 <code>exp</code>.
*
* @param exp the exponent
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 <code>exp</code>.
*
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[2:1] @ x[0:0] = x[2:0] );
+
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (concat (extract[2:1] x) (extract[0:0] x)) (extract[2:0] x)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[4:2] @ x[1:0] = x[4:0] );
+
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (concat (extract[4:2] x) (extract[1:0] x)) (extract[4:0] x)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[8:4] @ x[3:0] = x[8:0] );
+
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (concat (extract[8:4] x) (extract[3:0] x)) (extract[8:0] x)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[16:8] @ x[7:0] = x[16:0]);
+
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (concat (extract[16:8] x) (extract[7:0] x)) (extract[16:0] x)))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[63:32] = x[31:0]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[62:33] = x[30:1]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[60:3] = x[28:0] @ y[31:3]);
--- /dev/null
+(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))))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[59:4] = x[27:0] @ y[31:4]);
--- /dev/null
+(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))))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[61:34] = x[29:2]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[60:35] = x[28:3]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[31:0] = y[31:0]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[30:1] = y[30:1]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[29:2] = y[29:2]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[28:3] = y[28:3]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[62:1] = x[30:0] @ y[31:1]);
--- /dev/null
+(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))))
+)
--- /dev/null
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[61:2] = x[29:0] @ y[31:2]);
--- /dev/null
+(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))))
+)
--- /dev/null
+QUERY (0bin000111000[6:2] = 0bin01110);
+
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :formula
+(not (= (extract[6:2] bv56[9]) bv14[5]))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[31:0][31:0] = x[31:0]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[31:0][15:1] = x[15:1]);
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (extract[15:1] (extract[31:0] x)) (extract[15:1] x)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[7:2][2:2] = x[4:4]);
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (extract[2:2] (extract[7:2] x)) (extract[4:4] x)))
+)
--- /dev/null
+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
--- /dev/null
+(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)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[31:0][7:2] = x[7:2]);
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (extract[7:2] (extract[31:0] x)) (extract[7:2] x)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[31:0][4:4] = x[4:4]);
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (extract[4:4] (extract[31:0] x)) (extract[4:4] x)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[15:1][14:0] = x[15:1]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[15:1][7:1] = x[8:2]);
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (extract[7:1] (extract[15:1] x)) (extract[8:2] x)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[15:1][3:2] = x[4:3]);
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (extract[3:2] (extract[15:1] x)) (extract[4:3] x)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[15:1][3:3] = x[4:4]);
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (extract[3:3] (extract[15:1] x)) (extract[4:4] x)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[7:2][5:0] = x[7:2]);
--- /dev/null
+(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)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[7:2][3:1] = x[5:3]);
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (extract[3:1] (extract[7:2] x)) (extract[5:3] x)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (0bin0 @ x[31:31] @ x[30:20] @ x[19:10] @ x[9:1] @ x[0:0] @ 0bin0 = 0bin0 @ x @ 0bin0);
--- /dev/null
+(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])))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[31:31] @ x[30:20] @ x[19:10] @ x[9:1] @ x[0:0] = x);
--- /dev/null
+(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))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 = x @ 0bin010101);
+
--- /dev/null
+(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])))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ x = 0bin010101 @ x);
--- /dev/null
+(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)))
+)
--- /dev/null
+x : BITVECTOR(32);
+QUERY (x[31:0] = x);
+
--- /dev/null
+(benchmark B_
+ :logic QF_BV
+ :extrafuns ((x BitVec[32]))
+ :formula
+(not (= (extract[31:0] x) x))
+)
projects / cvc5.git / commitdiff