#include "mtl/Sort.h"
#include "core/Solver.h"
#include <iostream>
+#include "util/output.h"
using namespace BVMinisat;
// NOTE: assumptions passed in member-variable 'assumptions'.
lbool Solver::solve_()
{
+ Debug("bvminisat") <<"BVMinisat::Solving learned clauses " << learnts.size() <<"\n";
+ Debug("bvminisat") <<"BVMinisat::Solving assumptions " << assumptions.size() <<"\n";
model.clear();
conflict.clear();
if (!ok) return l_False;
// Initialize the next region to a size corresponding to the estimated utilization degree. This
// is not precise but should avoid some unnecessary reallocations for the new region:
ClauseAllocator to(ca.size() - ca.wasted());
-
+ Debug("bvminisat") << " BVMinisat::Garbage collection \n";
relocAll(to);
if (verbosity >= 2)
printf("| Garbage collection: %12d bytes => %12d bytes |\n",
void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
Debug("sat::minisat") << "Add clause " << clause <<"\n";
BVMinisat::vec<BVMinisat::Lit> minisat_clause;
- toMinisatClause(clause, minisat_clause);
+ toMinisatClause(clause, minisat_clause);
+ // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
+ // d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true);
+ // }
d_minisat->addClause(minisat_clause);
}
}
Debug("sat::minisat") <<"\n";
- SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump));
+ SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump));
return result;
}
for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
d_assertionsToCheck[i] = theory::Rewriter::rewrite(d_assertionsToCheck[i]);
}
+
}
void SmtEnginePrivate::staticLearning() {
theory_bv.cpp \
theory_bv_rewrite_rules.h \
theory_bv_rewrite_rules_core.h \
- theory_bv_rewrite_rules_arith.h \
+ theory_bv_rewrite_rules_operator_elimination.h \
+ theory_bv_rewrite_rules_constant_evaluation.h \
+ theory_bv_rewrite_rules_normalization.h \
+ theory_bv_rewrite_rules_simplification.h \
theory_bv_type_rules.h \
theory_bv_rewriter.h \
theory_bv_rewriter.cpp \
Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) {
- Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
+ Trace("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
<< node.getKind() << "\n";
Unreachable();
}
Unimplemented();
}
+// Node DefaultSltBB(TNode node, Bitblaster* bb){
+// Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+// // shoudl be rewritten in terms of ult
+// Unimplemented();
+// }
+
+// Node DefaultSleBB(TNode node, Bitblaster* bb){
+// Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+// // shoudl be rewritten in terms of ule
+// Unimplemented();
+// }
+
+
Node DefaultSltBB(TNode node, Bitblaster* bb){
Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
/// Term bitblasting strategies
void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) {
- Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
+ Trace("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
<< node.getKind() << "\n";
Unreachable();
}
/// other modes
Node AdderUltBB(TNode node, Bitblaster* bb);
-
+Node SltBB(TNode node, Bitblaster* bb);
+Node SleBB(TNode node, Bitblaster* bb);
/**
return;
}
+ BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+
// the bitblasted definition of the atom
Node atom_bb = d_atomBBStrategies[node.getKind()](node, this);
// asserting that the atom is true iff the definition holds
getBBTerm(node, bits);
return;
}
-
+ BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
d_termBBStrategies[node.getKind()] (node, bits,this);
Assert (bits.size() == utils::getSize(node));
*/
void Bitblaster::bitblast(TNode node) {
TimerStat::CodeTimer codeTimer(d_statistics.d_bitblastTimer);
-
+
/// strip the not
if (node.getKind() == kind::NOT) {
node = node[0];
if (node.getKind() == kind::EQUAL ||
node.getKind() == kind::BITVECTOR_ULT ||
+ node.getKind() == kind::BITVECTOR_ULE ||
node.getKind() == kind::BITVECTOR_SLT ||
- node.getKind() == kind::BITVECTOR_ULE ||
- node.getKind() == kind::BITVECTOR_SLE )
+ node.getKind() == kind::BITVECTOR_SLE)
{
bbAtom(node);
}
atom = lit;
}
- Assert (hasBBAtom(atom));
+ Assert (hasBBAtom(atom));
+ Node rewr_atom = Rewriter::rewrite(atom);
SatLiteral markerLit = d_cnfStream->getLiteral(atom);
if(lit.getKind() == kind::NOT) {
*/
bool Bitblaster::solve() {
+ Trace("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
return SatValTrue == d_satSolver->solve(d_assertedAtoms);
}
AtomSet d_bitblastedAtoms;
context::CDList<prop::SatLiteral> d_assertedAtoms; /**< context dependent list storing the atoms
- currently asserted by the DPLL SAT solver. */
+ currently asserted by the DPLL SAT solver. */
/// helper methods
bool hasBBAtom(TNode node);
}
TheoryBV::Statistics::Statistics():
d_avgConflictSize("theory::bv::AvgBVConflictSize"),
- d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0)
+ d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
+ d_solveTimer("theory::bv::solveTimer")
{
StatisticsRegistry::registerStat(&d_avgConflictSize);
StatisticsRegistry::registerStat(&d_solveSubstitutions);
+ StatisticsRegistry::registerStat(&d_solveTimer);
}
TheoryBV::Statistics::~Statistics() {
StatisticsRegistry::unregisterStat(&d_avgConflictSize);
StatisticsRegistry::unregisterStat(&d_solveSubstitutions);
+ StatisticsRegistry::unregisterStat(&d_solveTimer);
}
void TheoryBV::preRegisterTerm(TNode node) {
-
BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
//marker literal: bitblast all terms before we start
- d_bitblaster->bitblast(node);
+ //d_bitblaster->bitblast(node);
}
void TheoryBV::check(Effort e) {
- BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
- if (fullEffort(e)) {
- std::vector<TNode> assertions;
+ if (fullEffort(e) && !done()) {
+ Trace("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl;
+ std::vector<TNode> assertions;
+
while (!done()) {
TNode assertion = get();
- Debug("bitvector") << "assertion " << assertion << "\n";
- assertions.push_back(assertion);
+ Trace("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n";
d_bitblaster->bitblast(assertion);
+ d_bitblaster->assertToSat(assertion);
}
-
- std::vector<TNode>::const_iterator it = assertions.begin();
- for (; it != assertions.end(); ++it) {
- d_bitblaster->assertToSat(*it);
- }
+
+ TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
bool res = d_bitblaster->solve();
if (res == false) {
std::vector<TNode> conflictAtoms;
d_bitblaster->getConflict(conflictAtoms);
-
d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
Node conflict = mkConjunction(conflictAtoms);
d_out->conflict(conflict);
+ Trace("bitvector") << "TheoryBV::check returns conflict. \n ";
return;
}
}
class Statistics {
public:
AverageStat d_avgConflictSize;
- IntStat d_solveSubstitutions;
+ IntStat d_solveSubstitutions;
+ TimerStat d_solveTimer;
Statistics();
~Statistics();
};
/*! \file theory_bv_rewrite_rules.h
** \verbatim
** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: lianah
** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
namespace bv {
enum RewriteRuleId {
- /// core rewrite rules
+
+ /// core normalization rules
EmptyRule,
ConcatFlatten,
ConcatExtractMerge,
FailEq,
SimplifyEq,
ReflexivityEq,
+
/// operator elimination rules
- UgtToUlt,
- UgeToUle,
- SgeToSle,
- SgtToSlt,
+ UgtEliminate,
+ UgeEliminate,
+ SgeEliminate,
+ SgtEliminate,
+ SubEliminate,
+ SltEliminate,
+ SleEliminate,
+ CompEliminate,
RepeatEliminate,
RotateLeftEliminate,
RotateRightEliminate,
NandEliminate,
NorEliminate,
+ XnorEliminate,
SdivEliminate,
UdivEliminate,
SmodEliminate,
SremEliminate,
ZeroExtendEliminate,
- // division by zero guards: rewrite a / b as b!=0 => a/b = ...
- DivZeroGuard
+ SignExtendEliminate,
+ /// ground term evaluation
+ EvalEquals,
+ EvalConcat,
+ EvalAnd,
+ EvalOr,
+ EvalXor,
+ EvalNot,
+ EvalMult,
+ EvalPlus,
+ EvalUdiv,
+ EvalUrem,
+ EvalShl,
+ EvalLshr,
+ EvalAshr,
+ EvalUlt,
+ EvalUle,
+ EvalExtract,
+ EvalSignExtend,
+ EvalRotateLeft,
+ EvalRotateRight,
+ EvalNeg,
+
+ /// simplification rules
+ /// all of these rules decrease formula size
+ ShlByConst,
+ LshrByConst,
+ AshrByConst,
+ BitwiseIdemp,
+ AndZero,
+ AndOne,
+ OrZero,
+ OrOne,
+ XorDuplicate,
+ XorOne,
+ XorZero,
+ BitwiseNotAnd,
+ BitwiseNotOr,
+ XorNot,
+ NotIdemp,
+ LtSelf,
+ LteSelf,
+ UltZero,
+ UltSelf,
+ UleZero,
+ UleSelf,
+ ZeroUle,
+ UleMax,
+ NotUlt,
+ NotUle,
+ MultOne,
+ MultZero,
+ MultPow2,
+ PlusZero,
+ PlusSelf,
+ PlusNegSelf,
+ NegIdemp,
+ UdivPow2,
+ UdivOne,
+ UdivSelf,
+ UremPow2,
+ UremOne,
+ UremSelf,
+ ShiftZero,
+
+ /// normalization rules
+ ExtractBitwise,
+ ExtractNot,
+ ExtractArith,
+ ExtractArith2,
+ DoubleNeg,
+ NotConcat,
+ NotAnd, // not sure why this would help (not done)
+ NotOr, // not sure why this would help (not done)
+ NotXor // not sure why this would help (not done)
};
inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
case FailEq: out << "FailEq"; return out;
case SimplifyEq: out << "SimplifyEq"; return out;
case ReflexivityEq: out << "ReflexivityEq"; return out;
- case UgtToUlt: out << "UgtToUlt"; return out;
- case SgtToSlt: out << "SgtToSlt"; return out;
- case UgeToUle: out << "UgeToUle"; return out;
- case SgeToSle: out << "SgeToSle"; return out;
+ case UgtEliminate: out << "UgtEliminate"; return out;
+ case SgtEliminate: out << "SgtEliminate"; return out;
+ case UgeEliminate: out << "UgeEliminate"; return out;
+ case SgeEliminate: out << "SgeEliminate"; return out;
case RepeatEliminate: out << "RepeatEliminate"; return out;
case RotateLeftEliminate: out << "RotateLeftEliminate"; return out;
case RotateRightEliminate:out << "RotateRightEliminate";return out;
case SdivEliminate : out << "SdivEliminate"; return out;
case SremEliminate : out << "SremEliminate"; return out;
case SmodEliminate : out << "SmodEliminate"; return out;
- case ZeroExtendEliminate :out << "ZeroExtendEliminate"; return out;
- case DivZeroGuard : out << "DivZeroGuard"; return out;
+ case ZeroExtendEliminate :out << "ZeroExtendEliminate"; return out;
+ case EvalEquals : out << "EvalEquals"; return out;
+ case EvalConcat : out << "EvalConcat"; return out;
+ case EvalAnd : out << "EvalAnd"; return out;
+ case EvalOr : out << "EvalOr"; return out;
+ case EvalXor : out << "EvalXor"; return out;
+ case EvalNot : out << "EvalNot"; return out;
+ case EvalMult : out << "EvalMult"; return out;
+ case EvalPlus : out << "EvalPlus"; return out;
+ case EvalUdiv : out << "EvalUdiv"; return out;
+ case EvalUrem : out << "EvalUrem"; return out;
+ case EvalShl : out << "EvalShl"; return out;
+ case EvalLshr : out << "EvalLshr"; return out;
+ case EvalAshr : out << "EvalAshr"; return out;
+ case EvalUlt : out << "EvalUlt"; return out;
+ case EvalUle : out << "EvalUle"; return out;
+ case EvalExtract : out << "EvalExtract"; return out;
+ case EvalSignExtend : out << "EvalSignExtend"; return out;
+ case EvalRotateLeft : out << "EvalRotateLeft"; return out;
+ case EvalRotateRight : out << "EvalRotateRight"; return out;
+ case EvalNeg : out << "EvalNeg"; return out;
+ case ShlByConst : out << "ShlByConst"; return out;
+ case LshrByConst : out << "LshrByConst"; return out;
+ case AshrByConst : out << "AshrByConst"; return out;
+ case ExtractBitwise : out << "ExtractBitwise"; return out;
+ case ExtractNot : out << "ExtractNot"; return out;
+ case ExtractArith : out << "ExtractArith"; return out;
+ case ExtractArith2 : out << "ExtractArith2"; return out;
+ case DoubleNeg : out << "DoubleNeg"; return out;
+ case NotConcat : out << "NotConcat"; return out;
+ case NotAnd : out << "NotAnd"; return out;
+ case NotOr : out << "NotOr"; return out;
+ case NotXor : out << "NotXor"; return out;
+ case BitwiseIdemp : out << "BitwiseIdemp"; return out;
+ case XorDuplicate : out << "XorDuplicate"; return out;
+ case BitwiseNotAnd : out << "BitwiseNotAnd"; return out;
+ case BitwiseNotOr : out << "BitwiseNotOr"; return out;
+ case XorNot : out << "XorNot"; return out;
+ case LtSelf : out << "LtSelf"; return out;
+ case LteSelf : out << "LteSelf"; return out;
+ case UltZero : out << "UltZero"; return out;
+ case UleZero : out << "UleZero"; return out;
+ case ZeroUle : out << "ZeroUle"; return out;
+ case NotUlt : out << "NotUlt"; return out;
+ case NotUle : out << "NotUle"; return out;
+ case UleMax : out << "UleMax"; return out;
+ case SltEliminate : out << "SltEliminate"; return out;
+ case SleEliminate : out << "SleEliminate"; return out;
+ case AndZero : out << "AndZero"; return out;
+ case AndOne : out << "AndOne"; return out;
+ case OrZero : out << "OrZero"; return out;
+ case OrOne : out << "OrOne"; return out;
+ case XorOne : out << "XorOne"; return out;
+ case XorZero : out << "XorZero"; return out;
+ case MultOne : out << "MultOne"; return out;
+ case MultZero : out << "MultZero"; return out;
+ case MultPow2 : out << "MultPow2"; return out;
+ case PlusZero : out << "PlusZero"; return out;
+ case PlusSelf : out << "PlusSelf"; return out;
+ case PlusNegSelf : out << "PlusNegSelf"; return out;
+ case NegIdemp : out << "NegIdemp"; return out;
+ case UdivPow2 : out << "UdivPow2"; return out;
+ case UdivOne : out << "UdivOne"; return out;
+ case UdivSelf : out << "UdivSelf"; return out;
+ case UremPow2 : out << "UremPow2"; return out;
+ case UremOne : out << "UremOne"; return out;
+ case UremSelf : out << "UremSelf"; return out;
+ case ShiftZero : out << "ShiftZero"; return out;
+ case SubEliminate : out << "SubEliminate"; return out;
+ case CompEliminate : out << "CompEliminate"; return out;
+ case XnorEliminate : out << "XnorEliminate"; return out;
+ case SignExtendEliminate : out << "SignExtendEliminate"; return out;
+ case NotIdemp : out << "NotIdemp"; return out;
+ case UleSelf: out << "UleSelf"; return out;
default:
Unreachable();
}
template <RewriteRuleId rule>
class RewriteRule {
- class RuleStatistics {
+ // class RuleStatistics {
- /** The name of the rule prefixed with the prefix */
- static std::string getStatName(const char* prefix) {
- std::stringstream statName;
- statName << prefix << rule;
- return statName.str();
- }
+ // /** The name of the rule prefixed with the prefix */
+ // static std::string getStatName(const char* prefix) {
+ // std::stringstream statName;
+ // statName << prefix << rule;
+ // return statName.str();
+ // }
- public:
+ // public:
- /** Number of applications of this rule */
- IntStat d_ruleApplications;
+ // /** Number of applications of this rule */
+ // IntStat d_ruleApplications;
- /** Constructor */
- RuleStatistics()
- : d_ruleApplications(getStatName("theory::bv::RewriteRules::count"), 0) {
- StatisticsRegistry::registerStat(&d_ruleApplications);
- }
+ // /** Constructor */
+ // RuleStatistics()
+ // : d_ruleApplications(getStatName("theory::bv::RewriteRules::count"), 0) {
+ // StatisticsRegistry::registerStat(&d_ruleApplications);
+ // }
- /** Destructor */
- ~RuleStatistics() {
- StatisticsRegistry::unregisterStat(&d_ruleApplications);
- }
- };
+ // /** Destructor */
+ // ~RuleStatistics() {
+ // StatisticsRegistry::unregisterStat(&d_ruleApplications);
+ // }
+ // };
- /* Statistics about the rule */
- // NOTE: Cannot have static fields like this, or else you can't have
- // two SmtEngines in the process (the second-to-be-destroyed will
- // have a dangling pointer and segfault). If this statistic is needed,
- // fix the rewriter by making it an instance per-SmtEngine (instead of
- // static).
- //static RuleStatistics* s_statistics;
+ // /* Statistics about the rule */
+ // // NOTE: Cannot have static fields like this, or else you can't have
+ // // two SmtEngines in the process (the second-to-be-destroyed will
+ // // have a dangling pointer and segfault). If this statistic is needed,
+ // // fix the rewriter by making it an instance per-SmtEngine (instead of
+ // // static).
+ // static RuleStatistics* s_statistics;
/** Actually apply the rewrite rule */
static inline Node apply(Node node) {
public:
RewriteRule() {
- /*
- if (s_statistics == NULL) {
- s_statistics = new RuleStatistics();
- }
- */
+
+ // if (s_statistics == NULL) {
+ // s_statistics = new RuleStatistics();
+ // }
+
}
~RewriteRule() {
- /*
- delete s_statistics;
- s_statistics = NULL;
- */
+
+ // delete s_statistics;
+ // s_statistics = NULL;
+
}
static inline bool applies(Node node) {
}
};
-/*
-template<RewriteRuleId rule>
-typename RewriteRule<rule>::RuleStatistics* RewriteRule<rule>::s_statistics = NULL;
-*/
+
+ // template<RewriteRuleId rule>
+ // typename RewriteRule<rule>::RuleStatistics* RewriteRule<rule>::s_statistics = NULL;
+
/** Have to list all the rewrite rules to get the statistics out */
struct AllRewriteRules {
-
RewriteRule<EmptyRule> rule00;
RewriteRule<ConcatFlatten> rule01;
RewriteRule<ConcatExtractMerge> rule02;
RewriteRule<FailEq> rule08;
RewriteRule<SimplifyEq> rule09;
RewriteRule<ReflexivityEq> rule10;
- RewriteRule<UgtToUlt> rule11;
- RewriteRule<SgtToSlt> rule12;
- RewriteRule<UgeToUle> rule13;
- RewriteRule<SgeToSle> rule14;
+ RewriteRule<UgtEliminate> rule11;
+ RewriteRule<SgtEliminate> rule12;
+ RewriteRule<UgeEliminate> rule13;
+ RewriteRule<SgeEliminate> rule14;
RewriteRule<RepeatEliminate> rule17;
RewriteRule<RotateLeftEliminate> rule18;
RewriteRule<RotateRightEliminate> rule19;
RewriteRule<SdivEliminate> rule22;
RewriteRule<SremEliminate> rule23;
RewriteRule<SmodEliminate> rule24;
- RewriteRule<DivZeroGuard> rule25;
-
+ RewriteRule<EvalConcat> rule25;
+ RewriteRule<EvalAnd> rule26;
+ RewriteRule<EvalOr> rule27;
+ RewriteRule<EvalXor> rule28;
+ RewriteRule<EvalNot> rule29;
+ RewriteRule<EvalMult> rule31;
+ RewriteRule<EvalPlus> rule32;
+ RewriteRule<EvalUdiv> rule34;
+ RewriteRule<EvalUrem> rule35;
+ RewriteRule<EvalShl> rule36;
+ RewriteRule<EvalLshr> rule37;
+ RewriteRule<EvalAshr> rule38;
+ RewriteRule<EvalUlt> rule39;
+ RewriteRule<EvalUle> rule40;
+ RewriteRule<EvalExtract> rule43;
+ RewriteRule<EvalSignExtend> rule44;
+ RewriteRule<EvalRotateLeft> rule45;
+ RewriteRule<EvalRotateRight> rule46;
+ RewriteRule<EvalEquals> rule47;
+ RewriteRule<EvalNeg> rule48;
+ RewriteRule<ShlByConst> rule50;
+ RewriteRule<LshrByConst> rule51;
+ RewriteRule<AshrByConst> rule52;
+ RewriteRule<ExtractBitwise> rule53;
+ RewriteRule<ExtractNot> rule54;
+ RewriteRule<ExtractArith> rule55;
+ RewriteRule<DoubleNeg> rule56;
+ RewriteRule<NotConcat> rule57;
+ RewriteRule<NotAnd> rule58;
+ RewriteRule<NotOr> rule59;
+ RewriteRule<NotXor> rule60;
+ RewriteRule<BitwiseIdemp> rule61;
+ RewriteRule<XorDuplicate> rule62;
+ RewriteRule<BitwiseNotAnd> rule63;
+ RewriteRule<BitwiseNotOr> rule64;
+ RewriteRule<XorNot> rule65;
+ RewriteRule<LtSelf> rule66;
+ RewriteRule<LtSelf> rule67;
+ RewriteRule<UltZero> rule68;
+ RewriteRule<UleZero> rule69;
+ RewriteRule<ZeroUle> rule70;
+ RewriteRule<NotUlt> rule71;
+ RewriteRule<NotUle> rule72;
+ RewriteRule<ZeroExtendEliminate> rule73;
+ RewriteRule<UleMax> rule74;
+ RewriteRule<LteSelf> rule75;
+ RewriteRule<SltEliminate> rule76;
+ RewriteRule<SleEliminate> rule77;
+ RewriteRule<AndZero> rule78;
+ RewriteRule<AndOne> rule79;
+ RewriteRule<OrZero> rule80;
+ RewriteRule<OrOne> rule81;
+ RewriteRule<SubEliminate> rule82;
+ RewriteRule<XorOne> rule83;
+ RewriteRule<XorZero> rule84;
+ RewriteRule<MultOne> rule85;
+ RewriteRule<MultZero> rule86;
+ RewriteRule<MultPow2> rule87;
+ RewriteRule<PlusZero> rule88;
+ RewriteRule<PlusSelf> rule89;
+ RewriteRule<PlusNegSelf> rule90;
+ RewriteRule<NegIdemp> rule91;
+ RewriteRule<UdivPow2> rule92;
+ RewriteRule<UdivOne> rule93;
+ RewriteRule<UdivSelf> rule94;
+ RewriteRule<UremPow2> rule95;
+ RewriteRule<UremOne> rule96;
+ RewriteRule<UremSelf> rule97;
+ RewriteRule<ShiftZero> rule98;
+ RewriteRule<CompEliminate> rule99;
+ RewriteRule<XnorEliminate> rule100;
+ RewriteRule<SignExtendEliminate> rule101;
+ RewriteRule<NotIdemp> rule102;
+ RewriteRule<UleSelf> rule103;
};
template<>
template<>
Node RewriteRule<EmptyRule>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EmptyRule> for " << node.getKind() <<"\n";
Unreachable();
return node;
}
template <
typename R1,
- typename R2 = RewriteRule<EmptyRule>,
- typename R3 = RewriteRule<EmptyRule>,
- typename R4 = RewriteRule<EmptyRule>,
- typename R5 = RewriteRule<EmptyRule>,
- typename R6 = RewriteRule<EmptyRule>,
- typename R7 = RewriteRule<EmptyRule>,
- typename R8 = RewriteRule<EmptyRule>
+ typename R2 = RewriteRule<EmptyRule>,
+ typename R3 = RewriteRule<EmptyRule>,
+ typename R4 = RewriteRule<EmptyRule>,
+ typename R5 = RewriteRule<EmptyRule>,
+ typename R6 = RewriteRule<EmptyRule>,
+ typename R7 = RewriteRule<EmptyRule>,
+ typename R8 = RewriteRule<EmptyRule>,
+ typename R9 = RewriteRule<EmptyRule>,
+ typename R10 = RewriteRule<EmptyRule>,
+ typename R11 = RewriteRule<EmptyRule>,
+ typename R12 = RewriteRule<EmptyRule>,
+ typename R13 = RewriteRule<EmptyRule>,
+ typename R14 = RewriteRule<EmptyRule>,
+ typename R15 = RewriteRule<EmptyRule>,
+ typename R16 = RewriteRule<EmptyRule>,
+ typename R17 = RewriteRule<EmptyRule>,
+ typename R18 = RewriteRule<EmptyRule>,
+ typename R19 = RewriteRule<EmptyRule>,
+ typename R20 = RewriteRule<EmptyRule>
>
struct LinearRewriteStrategy {
static Node apply(Node node) {
Node current = node;
- if (R1::applies(current)) current = R1::template run<false>(current);
- if (R2::applies(current)) current = R2::template run<false>(current);
- if (R3::applies(current)) current = R3::template run<false>(current);
- if (R4::applies(current)) current = R4::template run<false>(current);
- if (R5::applies(current)) current = R5::template run<false>(current);
- if (R6::applies(current)) current = R6::template run<false>(current);
- if (R7::applies(current)) current = R7::template run<false>(current);
- if (R8::applies(current)) current = R8::template run<false>(current);
+ if (R1::applies(current)) current = R1::template run<false>(current);
+ if (R2::applies(current)) current = R2::template run<false>(current);
+ if (R3::applies(current)) current = R3::template run<false>(current);
+ if (R4::applies(current)) current = R4::template run<false>(current);
+ if (R5::applies(current)) current = R5::template run<false>(current);
+ if (R6::applies(current)) current = R6::template run<false>(current);
+ if (R7::applies(current)) current = R7::template run<false>(current);
+ if (R8::applies(current)) current = R8::template run<false>(current);
+ if (R9::applies(current)) current = R9::template run<false>(current);
+ if (R10::applies(current)) current = R10::template run<false>(current);
+ if (R11::applies(current)) current = R11::template run<false>(current);
+ if (R12::applies(current)) current = R12::template run<false>(current);
+ if (R13::applies(current)) current = R13::template run<false>(current);
+ if (R14::applies(current)) current = R14::template run<false>(current);
+ if (R15::applies(current)) current = R15::template run<false>(current);
+ if (R16::applies(current)) current = R16::template run<false>(current);
+ if (R17::applies(current)) current = R17::template run<false>(current);
+ if (R18::applies(current)) current = R18::template run<false>(current);
+ if (R19::applies(current)) current = R19::template run<false>(current);
+ if (R20::applies(current)) current = R20::template run<false>(current);
return current;
}
};
+template <
+ typename R1,
+ typename R2 = RewriteRule<EmptyRule>,
+ typename R3 = RewriteRule<EmptyRule>,
+ typename R4 = RewriteRule<EmptyRule>,
+ typename R5 = RewriteRule<EmptyRule>,
+ typename R6 = RewriteRule<EmptyRule>,
+ typename R7 = RewriteRule<EmptyRule>,
+ typename R8 = RewriteRule<EmptyRule>,
+ typename R9 = RewriteRule<EmptyRule>,
+ typename R10 = RewriteRule<EmptyRule>,
+ typename R11 = RewriteRule<EmptyRule>,
+ typename R12 = RewriteRule<EmptyRule>,
+ typename R13 = RewriteRule<EmptyRule>,
+ typename R14 = RewriteRule<EmptyRule>,
+ typename R15 = RewriteRule<EmptyRule>,
+ typename R16 = RewriteRule<EmptyRule>,
+ typename R17 = RewriteRule<EmptyRule>,
+ typename R18 = RewriteRule<EmptyRule>,
+ typename R19 = RewriteRule<EmptyRule>,
+ typename R20 = RewriteRule<EmptyRule>
+ >
+struct FixpointRewriteStrategy {
+ static Node apply(Node node) {
+ Node previous = node;
+ Node current = node;
+ do {
+ previous = current;
+ if (R1::applies(current)) current = R1::template run<false>(current);
+ if (R2::applies(current)) current = R2::template run<false>(current);
+ if (R3::applies(current)) current = R3::template run<false>(current);
+ if (R4::applies(current)) current = R4::template run<false>(current);
+ if (R5::applies(current)) current = R5::template run<false>(current);
+ if (R6::applies(current)) current = R6::template run<false>(current);
+ if (R7::applies(current)) current = R7::template run<false>(current);
+ if (R8::applies(current)) current = R8::template run<false>(current);
+ if (R9::applies(current)) current = R9::template run<false>(current);
+ if (R10::applies(current)) current = R10::template run<false>(current);
+ if (R11::applies(current)) current = R11::template run<false>(current);
+ if (R12::applies(current)) current = R12::template run<false>(current);
+ if (R13::applies(current)) current = R13::template run<false>(current);
+ if (R14::applies(current)) current = R14::template run<false>(current);
+ if (R15::applies(current)) current = R15::template run<false>(current);
+ if (R16::applies(current)) current = R16::template run<false>(current);
+ if (R17::applies(current)) current = R17::template run<false>(current);
+ if (R18::applies(current)) current = R18::template run<false>(current);
+ if (R19::applies(current)) current = R19::template run<false>(current);
+ if (R20::applies(current)) current = R20::template run<false>(current);
+ } while (previous != current);
+
+ return current;
+ }
+};
+
+
} // End namespace bv
} // End namespace theory
} // End namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file theory_bv_rewrite_rules_core.h
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include "theory/bv/theory_bv_rewrite_rules.h"
-#include "theory/bv/theory_bv_utils.h"
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-template<>
-bool RewriteRule<UgtToUlt>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_UGT);
-}
-
-template<>
-Node RewriteRule<UgtToUlt>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<UgtToUlt>(" << node << ")" << std::endl;
- TNode a = node[0];
- TNode b = node[1];
- Node result = utils::mkNode(kind::BITVECTOR_ULT, b, a);
- return result;
-}
-
-
-template<>
-bool RewriteRule<UgeToUle>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_UGE);
-}
-
-template<>
-Node RewriteRule<UgeToUle>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<UgeToUle>(" << node << ")" << std::endl;
- TNode a = node[0];
- TNode b = node[1];
- Node result = utils::mkNode(kind::BITVECTOR_ULE, b, a);
- return result;
-}
-
-
-template<>
-bool RewriteRule<SgtToSlt>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_SGT);
-}
-
-template<>
-Node RewriteRule<SgtToSlt>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<UgtToUlt>(" << node << ")" << std::endl;
- TNode a = node[0];
- TNode b = node[1];
- Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a);
- return result;
-}
-
-
-template<>
-bool RewriteRule<SgeToSle>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_SGE);
-}
-
-template<>
-Node RewriteRule<SgeToSle>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<SgeToSle>(" << node << ")" << std::endl;
- TNode a = node[0];
- TNode b = node[1];
- Node result = utils::mkNode(kind::BITVECTOR_SLE, b, a);
- return result;
-}
-
-template<>
-bool RewriteRule<RepeatEliminate>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_REPEAT);
-}
-
-template<>
-Node RewriteRule<RepeatEliminate>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
- TNode a = node[0];
- unsigned amount = node.getOperator().getConst<BitVectorRepeat>().repeatAmount;
- Assert(amount >= 1);
- if(amount == 1) {
- return a;
- }
- NodeBuilder<> result(kind::BITVECTOR_CONCAT);
- for(unsigned i = 0; i < amount; ++i) {
- result << node[0];
- }
- Node resultNode = result;
- return resultNode;
-}
-
-template<>
-bool RewriteRule<RotateLeftEliminate>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_ROTATE_LEFT);
-}
-
-template<>
-Node RewriteRule<RotateLeftEliminate>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
- TNode a = node[0];
- unsigned amount = node.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
- amount = amount % utils::getSize(a);
- if (amount == 0) {
- return a;
- }
-
- Node left = utils::mkExtract(a, utils::getSize(a)-1 - amount, 0);
- Node right = utils::mkExtract(a, utils::getSize(a) -1, utils::getSize(a) - amount);
- Node result = utils::mkConcat(left, right);
-
- return result;
-}
-
-template<>
-bool RewriteRule<RotateRightEliminate>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT);
-}
-
-template<>
-Node RewriteRule<RotateRightEliminate>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
- TNode a = node[0];
- unsigned amount = node.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
- amount = amount % utils::getSize(a);
- if (amount == 0) {
- return a;
- }
-
- Node left = utils::mkExtract(a, amount - 1, 0);
- Node right = utils::mkExtract(a, utils::getSize(a)-1, amount);
- Node result = utils::mkConcat(left, right);
-
- return result;
-}
-
-template<>
-bool RewriteRule<NandEliminate>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_NAND);
-}
-
-template<>
-Node RewriteRule<NandEliminate>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" << std::endl;
- TNode a = node[0];
- TNode b = node[1];
- Node andNode = utils::mkNode(kind::BITVECTOR_AND, a, b);
- Node result = utils::mkNode(kind::BITVECTOR_NOT, andNode);
- return result;
-}
-
-template<>
-bool RewriteRule<NorEliminate>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_NOR);
-}
-
-template<>
-Node RewriteRule<NorEliminate>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" << std::endl;
- TNode a = node[0];
- TNode b = node[1];
- Node orNode = utils::mkNode(kind::BITVECTOR_OR, a, b);
- Node result = utils::mkNode(kind::BITVECTOR_NOT, orNode);
- return result;
-}
-
-template<>
-bool RewriteRule<SdivEliminate>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_SDIV);
-}
-
-template<>
-Node RewriteRule<SdivEliminate>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" << std::endl;
-
- TNode a = node[0];
- TNode b = node[1];
- unsigned size = utils::getSize(a);
-
- Node one = utils::mkConst(1, 1);
- Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one);
- Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one);
- Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
- Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
-
- Node a_udiv_b = utils::mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b);
- Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b);
-
- Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0);
- Node result = utils::mkNode(kind::ITE, condition, neg_result, a_udiv_b);
-
- return result;
-}
-
-
-template<>
-bool RewriteRule<SremEliminate>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_SREM);
-}
-
-template<>
-Node RewriteRule<SremEliminate>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" << std::endl;
- TNode a = node[0];
- TNode b = node[1];
- unsigned size = utils::getSize(a);
-
- Node one = utils::mkConst(1, 1);
- Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one);
- Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one);
- Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
- Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
-
- Node a_urem_b = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
- Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b);
-
- Node result = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);
-
- return result;
-}
-
-template<>
-bool RewriteRule<SmodEliminate>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_SMOD);
-}
-
-template<>
-Node RewriteRule<SmodEliminate>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" << std::endl;
- TNode a = node[0];
- TNode b = node[1];
- unsigned size = utils::getSize(a);
-
- Node one = utils::mkConst(1, 1);
- Node zero = utils::mkConst(1, 0);
- Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one);
- Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one);
-
- Node a_gte_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), zero);
- Node b_gte_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), zero);
-
- Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
- Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
-
- Node a_urem_b = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
- Node neg_rem = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b);
-
-
- Node aneg_bpos = utils::mkNode(kind::AND, a_lt_0, b_gte_0);
- Node apos_bneg = utils::mkNode(kind::AND, a_gte_0, b_lt_0);
- Node aneg_bneg = utils::mkNode(kind::AND, a_lt_0, b_lt_0);
-
- Node result = utils::mkNode(kind::ITE, aneg_bpos, utils::mkNode(kind::BITVECTOR_PLUS, neg_rem, b),
- utils::mkNode(kind::ITE, apos_bneg, utils::mkNode(kind::BITVECTOR_PLUS, a_urem_b, b),
- utils::mkNode(kind::ITE, aneg_bneg, neg_rem,
- a_urem_b)));
- return result;
-}
-
-
-template<>
-bool RewriteRule<ZeroExtendEliminate>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND);
-}
-
-template<>
-Node RewriteRule<ZeroExtendEliminate>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
-
- TNode bv = node[0];
- unsigned amount = node.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
-
- Node zero = utils::mkConst(amount, 0);
- Node result = utils::mkConcat(zero, node[0]);
-
- return result;
-}
-
-
-template<>
-bool RewriteRule<DivZeroGuard>::applies(Node node) {
- return (node.getKind() == kind::BITVECTOR_UDIV ||
- node.getKind() == kind::BITVECTOR_UREM ||
- node.getKind() == kind::BITVECTOR_SDIV ||
- node.getKind() == kind::BITVECTOR_SREM ||
- node.getKind() == kind::BITVECTOR_SMOD);
-}
-
-template<>
-Node RewriteRule<DivZeroGuard>::apply(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<DivZeroGuard>(" << node << ")" << std::endl;
-
- Unimplemented();
-
-}
-
-
-
-
-}
-}
-}
--- /dev/null
+/********************* */
+/*! \file theory_bv_rewrite_rules_core.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "theory/bv/theory_bv_rewrite_rules.h"
+#include "theory/bv/theory_bv_utils.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+template<>
+bool RewriteRule<EvalAnd>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_AND &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalAnd>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+ BitVector res = a & b;
+
+ return utils::mkConst(res);
+}
+
+template<>
+bool RewriteRule<EvalOr>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_OR &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalOr>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+ BitVector res = a | b;
+
+ return utils::mkConst(res);
+}
+
+template<>
+bool RewriteRule<EvalXor>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_XOR &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalXor>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+ BitVector res = a ^ b;
+
+ return utils::mkConst(res);
+}
+
+// template<>
+// bool RewriteRule<EvalXnor>::applies(Node node) {
+// return (node.getKind() == kind::BITVECTOR_XNOR &&
+// utils::isBVGroundTerm(node));
+// }
+
+// template<>
+// Node RewriteRule<EvalXnor>::apply(Node node) {
+// BVDebug("bv-rewrite") << "RewriteRule<EvalXnor>(" << node << ")" << std::endl;
+// BitVector a = node[0].getConst<BitVector>();
+// BitVector b = node[1].getConst<BitVector>();
+// BitVector res = ~ (a ^ b);
+
+// return utils::mkConst(res);
+// }
+template<>
+bool RewriteRule<EvalNot>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_NOT &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalNot>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector res = ~ a;
+ return utils::mkConst(res);
+}
+
+// template<>
+// bool RewriteRule<EvalComp>::applies(Node node) {
+// return (node.getKind() == kind::BITVECTOR_COMP &&
+// utils::isBVGroundTerm(node));
+// }
+
+// template<>
+// Node RewriteRule<EvalComp>::apply(Node node) {
+// BVDebug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl;
+// BitVector a = node[0].getConst<BitVector>();
+// BitVector b = node[1].getConst<BitVector>();
+// BitVector res;
+// if (a == b) {
+// res = BitVector(1, Integer(1));
+// } else {
+// res = BitVector(1, Integer(0));
+// }
+
+// return utils::mkConst(res);
+// }
+
+template<>
+bool RewriteRule<EvalMult>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_MULT &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalMult>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+ BitVector res = a * b;
+
+ return utils::mkConst(res);
+}
+
+template<>
+bool RewriteRule<EvalPlus>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_PLUS &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalPlus>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+ BitVector res = a + b;
+
+ return utils::mkConst(res);
+}
+
+// template<>
+// bool RewriteRule<EvalSub>::applies(Node node) {
+// return (node.getKind() == kind::BITVECTOR_SUB &&
+// utils::isBVGroundTerm(node));
+// }
+
+// template<>
+// Node RewriteRule<EvalSub>::apply(Node node) {
+// BVDebug("bv-rewrite") << "RewriteRule<EvalSub>(" << node << ")" << std::endl;
+// BitVector a = node[0].getConst<BitVector>();
+// BitVector b = node[1].getConst<BitVector>();
+// BitVector res = a - b;
+
+// return utils::mkConst(res);
+// }
+template<>
+bool RewriteRule<EvalNeg>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_NEG &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalNeg>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalNeg>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector res = - a;
+
+ return utils::mkConst(res);
+}
+template<>
+bool RewriteRule<EvalUdiv>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_UDIV &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalUdiv>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+ BitVector res = a.unsignedDiv(b);
+
+ return utils::mkConst(res);
+}
+template<>
+bool RewriteRule<EvalUrem>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_UREM &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalUrem>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+ BitVector res = a.unsignedRem(b);
+ return utils::mkConst(res);
+}
+
+template<>
+bool RewriteRule<EvalShl>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SHL &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalShl>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalShl>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+
+ BitVector res = a.leftShift(b);
+ return utils::mkConst(res);
+}
+
+template<>
+bool RewriteRule<EvalLshr>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_LSHR &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalLshr>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalLshr>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+
+ BitVector res = a.logicalRightShift(b);
+ return utils::mkConst(res);
+}
+
+template<>
+bool RewriteRule<EvalAshr>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ASHR &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalAshr>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalAshr>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+
+ BitVector res = a.arithRightShift(b);
+ return utils::mkConst(res);
+}
+
+template<>
+bool RewriteRule<EvalUlt>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ULT &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalUlt>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalUlt>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+
+ if (a.unsignedLessThan(b)) {
+ return utils::mkTrue();
+ }
+ return utils::mkFalse();
+}
+
+// template<>
+// bool RewriteRule<EvalSlt>::applies(Node node) {
+// return (node.getKind() == kind::BITVECTOR_SLT &&
+// utils::isBVGroundTerm(node));
+// }
+
+// template<>
+// Node RewriteRule<EvalSlt>::apply(Node node) {
+// BVDebug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl;
+// BitVector a = node[0].getConst<BitVector>();
+// BitVector b = node[1].getConst<BitVector>();
+
+// if (a.signedLessThan(b)) {
+// return utils::mkTrue();
+// }
+// return utils::mkFalse();
+
+// }
+
+template<>
+bool RewriteRule<EvalUle>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ULE &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalUle>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalUle>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+
+ if (a.unsignedLessThanEq(b)) {
+ return utils::mkTrue();
+ }
+ return utils::mkFalse();
+}
+
+// template<>
+// bool RewriteRule<EvalSle>::applies(Node node) {
+// return (node.getKind() == kind::BITVECTOR_SLE &&
+// utils::isBVGroundTerm(node));
+// }
+
+// template<>
+// Node RewriteRule<EvalSle>::apply(Node node) {
+// BVDebug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl;
+// BitVector a = node[0].getConst<BitVector>();
+// BitVector b = node[1].getConst<BitVector>();
+
+// if (a.signedLessThanEq(b)) {
+// return utils::mkTrue();
+// }
+// return utils::mkFalse();
+// }
+
+template<>
+bool RewriteRule<EvalExtract>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_EXTRACT &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalExtract>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalExtract>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ unsigned lo = utils::getExtractLow(node);
+ unsigned hi = utils::getExtractHigh(node);
+
+ BitVector res = a.extract(hi, lo);
+ return utils::mkConst(res);
+}
+
+
+template<>
+bool RewriteRule<EvalConcat>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_CONCAT &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalConcat>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalConcat>(" << node << ")" << std::endl;
+ unsigned num = node.getNumChildren();
+ BitVector res = node[0].getConst<BitVector>();
+ for(unsigned i = 1; i < num; ++i ) {
+ BitVector a = node[i].getConst<BitVector>();
+ res = res.concat(a);
+ }
+ return utils::mkConst(res);
+}
+
+template<>
+bool RewriteRule<EvalSignExtend>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalSignExtend>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+ BitVector res = a.signExtend(amount);
+
+ return utils::mkConst(res);
+}
+
+template<>
+bool RewriteRule<EvalEquals>::applies(Node node) {
+ return (node.getKind() == kind::EQUAL &&
+ utils::isBVGroundTerm(node));
+}
+
+template<>
+Node RewriteRule<EvalEquals>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<EvalEquals>(" << node << ")" << std::endl;
+ BitVector a = node[0].getConst<BitVector>();
+ BitVector b = node[1].getConst<BitVector>();
+ if (a == b) {
+ return utils::mkTrue();
+ }
+ return utils::mkFalse();
+
+}
+
+
+}
+}
+}
}
}
Node resultNode = result;
+ BVDebug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << resultNode << ")" << std::endl;
return resultNode;
}
template<>
bool RewriteRule<ExtractConcat>::applies(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
+ //BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false;
return true;
template<>
bool RewriteRule<FailEq>::applies(Node node) {
- BVDebug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
+ //BVDebug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
if (node.getKind() != kind::EQUAL) return false;
if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
if (node[1].getKind() != kind::CONST_BITVECTOR) return false;
template<>
Node RewriteRule<FailEq>::apply(Node node) {
- return utils::mkFalse();
+ return utils::mkFalse();
}
template<>
--- /dev/null
+/********************* */
+/*! \file theory_bv_rewrite_rules_normalization.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "theory/bv/theory_bv_rewrite_rules.h"
+#include "theory/bv/theory_bv_utils.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+/**
+ * ExtractBitwise
+ * (x bvop y) [i:j] ==> x[i:j] bvop y[i:j]
+ * where bvop is bvand,bvor, bvxor
+ */
+template<>
+bool RewriteRule<ExtractBitwise>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_EXTRACT &&
+ (node[0].getKind() == kind::BITVECTOR_AND ||
+ node[0].getKind() == kind::BITVECTOR_OR ||
+ node[0].getKind() == kind::BITVECTOR_XOR ));
+}
+
+template<>
+Node RewriteRule<ExtractBitwise>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
+ unsigned high = utils::getExtractHigh(node);
+ unsigned low = utils::getExtractLow(node);
+ Node a = utils::mkExtract(node[0][0], high, low);
+ Node b = utils::mkExtract(node[0][1], high, low);
+ Kind kind = node[0].getKind();
+ return utils::mkNode(kind, a, b);
+}
+
+/**
+ * ExtractNot
+ *
+ * (~ a) [i:j] ==> ~ (a[i:j])
+ */
+template<>
+bool RewriteRule<ExtractNot>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_EXTRACT &&
+ node[0].getKind() == kind::BITVECTOR_NOT);
+}
+
+template<>
+Node RewriteRule<ExtractNot>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl;
+ unsigned low = utils::getExtractLow(node);
+ unsigned high = utils::getExtractHigh(node);
+ Node a = utils::mkExtract(node[0][0], high, low);
+ return utils::mkNode(kind::BITVECTOR_NOT, a);
+}
+
+/**
+ * ExtractArith
+ *
+ * (a bvop b) [k:0] ==> (a[k:0] bvop b[k:0])
+ */
+
+template<>
+bool RewriteRule<ExtractArith>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_EXTRACT &&
+ utils::getExtractLow(node) == 0 &&
+ (node[0].getKind() == kind::BITVECTOR_PLUS ||
+ node[0].getKind() == kind::BITVECTOR_MULT));
+}
+
+template<>
+Node RewriteRule<ExtractArith>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" << std::endl;
+ unsigned low = utils::getExtractLow(node);
+ Assert (low == 0);
+ unsigned high = utils::getExtractHigh(node);
+ Node a = utils::mkExtract(node[0][0], high, low);
+ Node b = utils::mkExtract(node[0][1], high, low);
+
+ Kind kind = node[0].getKind();
+ return utils::mkNode(kind, a, b);
+
+}
+
+/**
+ * ExtractArith2
+ *
+ * (a bvop b) [i:j] ==> (a[i:0] bvop b[i:0]) [i:j]
+ */
+
+// careful not to apply in a loop
+template<>
+bool RewriteRule<ExtractArith2>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_EXTRACT &&
+ (node[0].getKind() == kind::BITVECTOR_PLUS ||
+ node[0].getKind() == kind::BITVECTOR_MULT));
+}
+
+template<>
+Node RewriteRule<ExtractArith2>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl;
+ unsigned low = utils::getExtractLow(node);
+ unsigned high = utils::getExtractHigh(node);
+ Node a = utils::mkExtract(node[0][0], high, 0);
+ Node b = utils::mkExtract(node[0][1], high, 0);
+
+ Kind kind = node[0].getKind();
+ Node a_op_b = utils::mkNode(kind, a, b);
+
+ return utils::mkExtract(a_op_b, high, low);
+}
+
+
+// template<>
+// bool RewriteRule<>::applies(Node node) {
+// return (node.getKind() == kind::BITVECTOR_CONCAT);
+// }
+
+// template<>
+// Node RewriteRule<>::apply(Node node) {
+// BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
+// return resultNode;
+// }
+
+
+
+}
+}
+}
--- /dev/null
+/********************* */
+/*! \file theory_bv_rewrite_rules_core.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "theory/bv/theory_bv_rewrite_rules.h"
+#include "theory/bv/theory_bv_utils.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+template<>
+bool RewriteRule<UgtEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_UGT);
+}
+
+template<>
+Node RewriteRule<UgtEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ TNode b = node[1];
+ Node result = utils::mkNode(kind::BITVECTOR_ULT, b, a);
+ return result;
+}
+
+
+template<>
+bool RewriteRule<UgeEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_UGE);
+}
+
+template<>
+Node RewriteRule<UgeEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ TNode b = node[1];
+ Node result = utils::mkNode(kind::BITVECTOR_ULE, b, a);
+ return result;
+}
+
+
+template<>
+bool RewriteRule<SgtEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SGT);
+}
+
+template<>
+Node RewriteRule<SgtEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RgewriteRule<UgtEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ TNode b = node[1];
+ Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a);
+ return result;
+}
+
+
+template<>
+bool RewriteRule<SgeEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SGE);
+}
+
+template<>
+Node RewriteRule<SgeEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ TNode b = node[1];
+ Node result = utils::mkNode(kind::BITVECTOR_SLE, b, a);
+ return result;
+}
+
+template <>
+bool RewriteRule<SltEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SLT);
+}
+
+template <>
+Node RewriteRule<SltEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")" << std::endl;
+
+ unsigned size = utils::getSize(node[0]);
+ Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1)));
+ Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two);
+ Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two);
+
+ return utils::mkNode(kind::BITVECTOR_ULT, a, b);
+
+}
+
+template <>
+bool RewriteRule<SleEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SLE);
+}
+
+template <>
+Node RewriteRule<SleEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl;
+
+ unsigned size = utils::getSize(node[0]);
+ Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1)));
+ Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two);
+ Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two);
+
+ return utils::mkNode(kind::BITVECTOR_ULE, a, b);
+
+}
+
+template <>
+bool RewriteRule<CompEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_COMP);
+}
+
+template <>
+Node RewriteRule<CompEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")" << std::endl;
+ Node comp = utils::mkNode(kind::EQUAL, node[0], node[1]);
+ Node one = utils::mkConst(1, 1);
+ Node zero = utils::mkConst(1, 0);
+
+ return utils::mkNode(kind::ITE, comp, one, zero);
+}
+
+template <>
+bool RewriteRule<SubEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SUB);
+}
+
+template <>
+Node RewriteRule<SubEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")" << std::endl;
+ Node negb = utils::mkNode(kind::BITVECTOR_NEG, node[1]);
+ Node a = node[0];
+
+ return utils::mkNode(kind::BITVECTOR_PLUS, a, negb);
+}
+
+
+template<>
+bool RewriteRule<RepeatEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_REPEAT);
+}
+
+template<>
+Node RewriteRule<RepeatEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ unsigned amount = node.getOperator().getConst<BitVectorRepeat>().repeatAmount;
+ Assert(amount >= 1);
+ if(amount == 1) {
+ return a;
+ }
+ NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+ for(unsigned i = 0; i < amount; ++i) {
+ result << node[0];
+ }
+ Node resultNode = result;
+ return resultNode;
+}
+
+template<>
+bool RewriteRule<RotateLeftEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ROTATE_LEFT);
+}
+
+template<>
+Node RewriteRule<RotateLeftEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ unsigned amount = node.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
+ amount = amount % utils::getSize(a);
+ if (amount == 0) {
+ return a;
+ }
+
+ Node left = utils::mkExtract(a, utils::getSize(a)-1 - amount, 0);
+ Node right = utils::mkExtract(a, utils::getSize(a) -1, utils::getSize(a) - amount);
+ Node result = utils::mkConcat(left, right);
+
+ return result;
+}
+
+template<>
+bool RewriteRule<RotateRightEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT);
+}
+
+template<>
+Node RewriteRule<RotateRightEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ unsigned amount = node.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
+ amount = amount % utils::getSize(a);
+ if (amount == 0) {
+ return a;
+ }
+
+ Node left = utils::mkExtract(a, amount - 1, 0);
+ Node right = utils::mkExtract(a, utils::getSize(a)-1, amount);
+ Node result = utils::mkConcat(left, right);
+
+ return result;
+}
+
+template<>
+bool RewriteRule<NandEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_NAND);
+}
+
+template<>
+Node RewriteRule<NandEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ TNode b = node[1];
+ Node andNode = utils::mkNode(kind::BITVECTOR_AND, a, b);
+ Node result = utils::mkNode(kind::BITVECTOR_NOT, andNode);
+ return result;
+}
+
+template<>
+bool RewriteRule<NorEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_NOR);
+}
+
+template<>
+Node RewriteRule<NorEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ TNode b = node[1];
+ Node orNode = utils::mkNode(kind::BITVECTOR_OR, a, b);
+ Node result = utils::mkNode(kind::BITVECTOR_NOT, orNode);
+ return result;
+}
+
+template<>
+bool RewriteRule<XnorEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_XNOR);
+}
+
+template<>
+Node RewriteRule<XnorEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ TNode b = node[1];
+ Node xorNode = utils::mkNode(kind::BITVECTOR_XOR, a, b);
+ return utils::mkNode(kind::BITVECTOR_NOT, xorNode);
+}
+
+
+template<>
+bool RewriteRule<SdivEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SDIV);
+}
+
+template<>
+Node RewriteRule<SdivEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" << std::endl;
+
+ TNode a = node[0];
+ TNode b = node[1];
+ unsigned size = utils::getSize(a);
+
+ Node one = utils::mkConst(1, 1);
+ Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one);
+ Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one);
+ Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
+ Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
+
+ Node a_udiv_b = utils::mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b);
+ Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b);
+
+ Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0);
+ Node result = utils::mkNode(kind::ITE, condition, neg_result, a_udiv_b);
+
+ return result;
+}
+
+
+template<>
+bool RewriteRule<SremEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SREM);
+}
+
+template<>
+Node RewriteRule<SremEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ TNode b = node[1];
+ unsigned size = utils::getSize(a);
+
+ Node one = utils::mkConst(1, 1);
+ Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one);
+ Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one);
+ Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
+ Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
+
+ Node a_urem_b = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
+ Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b);
+
+ Node result = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);
+
+ return result;
+}
+
+template<>
+bool RewriteRule<SmodEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SMOD);
+}
+
+template<>
+Node RewriteRule<SmodEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ TNode b = node[1];
+ unsigned size = utils::getSize(a);
+
+ Node one = utils::mkConst(1, 1);
+ Node zero = utils::mkConst(1, 0);
+ Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one);
+ Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one);
+
+ Node a_gte_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), zero);
+ Node b_gte_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), zero);
+
+ Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
+ Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
+
+ Node a_urem_b = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
+ Node neg_rem = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b);
+
+
+ Node aneg_bpos = utils::mkNode(kind::AND, a_lt_0, b_gte_0);
+ Node apos_bneg = utils::mkNode(kind::AND, a_gte_0, b_lt_0);
+ Node aneg_bneg = utils::mkNode(kind::AND, a_lt_0, b_lt_0);
+
+ Node result = utils::mkNode(kind::ITE, aneg_bpos, utils::mkNode(kind::BITVECTOR_PLUS, neg_rem, b),
+ utils::mkNode(kind::ITE, apos_bneg, utils::mkNode(kind::BITVECTOR_PLUS, a_urem_b, b),
+ utils::mkNode(kind::ITE, aneg_bneg, neg_rem,
+ a_urem_b)));
+ return result;
+}
+
+
+template<>
+bool RewriteRule<ZeroExtendEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND);
+}
+
+template<>
+Node RewriteRule<ZeroExtendEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
+
+ TNode bv = node[0];
+ unsigned amount = node.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
+ if (amount == 0) {
+ return node[0];
+ }
+ Node zero = utils::mkConst(amount, 0);
+ Node result = utils::mkConcat(zero, node[0]);
+
+ return result;
+}
+
+template<>
+bool RewriteRule<SignExtendEliminate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND);
+}
+
+template<>
+Node RewriteRule<SignExtendEliminate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
+
+ unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+ if(amount == 0) {
+ return node[0];
+ }
+ unsigned size = utils::getSize(node[0]);
+ Node sign_bit = utils::mkExtract(node[0], size-1, size-1);
+ Node extension = utils::mkConcat(sign_bit, amount);
+
+ return utils::mkConcat(extension, node[0]);
+}
+
+
+}
+}
+}
--- /dev/null
+/********************* */
+/*! \file theory_bv_rewrite_rules_simplification.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "theory/bv/theory_bv_rewrite_rules.h"
+#include "theory/bv/theory_bv_utils.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+// FIXME: this rules subsume the constant evaluation ones
+
+
+/**
+ * ShlByConst
+ *
+ * Left Shift by constant amount
+ */
+template<>
+bool RewriteRule<ShlByConst>::applies(Node node) {
+ // if the shift amount is constant
+ return (node.getKind() == kind::BITVECTOR_SHL &&
+ node[1].getKind() == kind::CONST_BITVECTOR);
+}
+
+template<>
+Node RewriteRule<ShlByConst>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
+ Integer amount = node[1].getConst<BitVector>().toInteger();
+
+ Node a = node[0];
+ uint32_t size = utils::getSize(a);
+
+
+ if (amount >= Integer(size)) {
+ // if we are shifting more than the length of the bitvector return 0
+ return utils::mkConst(BitVector(size, Integer(0)));
+ }
+
+ // make sure we do not lose information casting
+ Assert(amount < Integer(1).multiplyByPow2(32));
+
+ uint32_t uint32_amount = amount.toUnsignedInt();
+ Node left = utils::mkExtract(a, size - 1 - uint32_amount, 0);
+ Node right = utils::mkConst(BitVector(uint32_amount, Integer(0)));
+ return utils::mkConcat(left, right);
+}
+
+/**
+ * LshrByConst
+ *
+ * Right Logical Shift by constant amount
+ */
+
+template<>
+bool RewriteRule<LshrByConst>::applies(Node node) {
+ // if the shift amount is constant
+ return (node.getKind() == kind::BITVECTOR_LSHR &&
+ node[1].getKind() == kind::CONST_BITVECTOR);
+}
+
+template<>
+Node RewriteRule<LshrByConst>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
+ Integer amount = node[1].getConst<BitVector>().toInteger();
+
+ Node a = node[0];
+ uint32_t size = utils::getSize(a);
+
+
+ if (amount >= Integer(size)) {
+ // if we are shifting more than the length of the bitvector return 0
+ return utils::mkConst(BitVector(size, Integer(0)));
+ }
+
+ // make sure we do not lose information casting
+ Assert(amount < Integer(1).multiplyByPow2(32));
+
+ uint32_t uint32_amount = amount.toUnsignedInt();
+ Node right = utils::mkExtract(a, size - 1, uint32_amount);
+ Node left = utils::mkConst(BitVector(uint32_amount, Integer(0)));
+ return utils::mkConcat(left, right);
+}
+
+/**
+ * AshrByConst
+ *
+ * Right Arithmetic Shift by constant amount
+ */
+
+template<>
+bool RewriteRule<AshrByConst>::applies(Node node) {
+ // if the shift amount is constant
+ return (node.getKind() == kind::BITVECTOR_ASHR &&
+ node[1].getKind() == kind::CONST_BITVECTOR);
+}
+
+template<>
+Node RewriteRule<AshrByConst>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
+ Integer amount = node[1].getConst<BitVector>().toInteger();
+
+ Node a = node[0];
+ uint32_t size = utils::getSize(a);
+ Node sign_bit = utils::mkExtract(a, size-1, size-1);
+
+ if (amount >= Integer(size)) {
+ // if we are shifting more than the length of the bitvector return n repetitions
+ // of the first bit
+ return utils::mkConcat(sign_bit, size);
+ }
+
+ // make sure we do not lose information casting
+ Assert(amount < Integer(1).multiplyByPow2(32));
+
+ uint32_t uint32_amount = amount.toUnsignedInt();
+ if (uint32_amount == 0) {
+ return a;
+ }
+
+ Node left = utils::mkConcat(sign_bit, uint32_amount);
+ Node right = utils::mkExtract(a, size - 1, uint32_amount);
+ return utils::mkConcat(left, right);
+}
+
+/**
+ * BitwiseIdemp
+ *
+ * (a bvand a) ==> a
+ * (a bvor a) ==> a
+ */
+
+template<>
+bool RewriteRule<BitwiseIdemp>::applies(Node node) {
+ return ((node.getKind() == kind::BITVECTOR_AND ||
+ node.getKind() == kind::BITVECTOR_OR) &&
+ node[0] == node[1]);
+}
+
+template<>
+Node RewriteRule<BitwiseIdemp>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
+ return node[0];
+}
+
+/**
+ * AndZero
+ *
+ * (a bvand 0) ==> 0
+ */
+
+template<>
+bool RewriteRule<AndZero>::applies(Node node) {
+ unsigned size = utils::getSize(node);
+ return (node.getKind() == kind::BITVECTOR_AND &&
+ (node[0] == utils::mkConst(size, 0) ||
+ node[1] == utils::mkConst(size, 0)));
+}
+
+template<>
+Node RewriteRule<AndZero>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
+ return utils::mkConst(utils::getSize(node), 0);
+}
+
+/**
+ * AndOne
+ *
+ * (a bvand 1) ==> a
+ */
+
+template<>
+bool RewriteRule<AndOne>::applies(Node node) {
+ unsigned size = utils::getSize(node);
+ Node ones = utils::mkOnes(size);
+ return (node.getKind() == kind::BITVECTOR_AND &&
+ (node[0] == ones ||
+ node[1] == ones));
+}
+
+template<>
+Node RewriteRule<AndOne>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
+ unsigned size = utils::getSize(node);
+
+ if (node[0] == utils::mkOnes(size)) {
+ return node[1];
+ } else {
+ Assert (node[1] == utils::mkOnes(size));
+ return node[0];
+ }
+}
+
+/**
+ * OrZero
+ *
+ * (a bvor 0) ==> a
+ */
+
+template<>
+bool RewriteRule<OrZero>::applies(Node node) {
+ unsigned size = utils::getSize(node);
+ return (node.getKind() == kind::BITVECTOR_OR &&
+ (node[0] == utils::mkConst(size, 0) ||
+ node[1] == utils::mkConst(size, 0)));
+}
+
+template<>
+Node RewriteRule<OrZero>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
+
+ unsigned size = utils::getSize(node);
+ if (node[0] == utils::mkConst(size, 0)) {
+ return node[1];
+ } else {
+ Assert(node[1] == utils::mkConst(size, 0));
+ return node[0];
+ }
+}
+
+/**
+ * OrOne
+ *
+ * (a bvor 1) ==> 1
+ */
+
+template<>
+bool RewriteRule<OrOne>::applies(Node node) {
+ unsigned size = utils::getSize(node);
+ Node ones = utils::mkOnes(size);
+ return (node.getKind() == kind::BITVECTOR_OR &&
+ (node[0] == ones ||
+ node[1] == ones));
+}
+
+template<>
+Node RewriteRule<OrOne>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
+ return utils::mkOnes(utils::getSize(node));
+}
+
+
+/**
+ * XorDuplicate
+ *
+ * (a bvxor a) ==> 0
+ */
+
+template<>
+bool RewriteRule<XorDuplicate>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_XOR &&
+ node[0] == node[1]);
+}
+
+template<>
+Node RewriteRule<XorDuplicate>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
+ return utils::mkConst(BitVector(utils::getSize(node), Integer(0)));
+}
+
+/**
+ * XorOne
+ *
+ * (a bvxor 1) ==> ~a
+ */
+
+template<>
+bool RewriteRule<XorOne>::applies(Node node) {
+ Node ones = utils::mkOnes(utils::getSize(node));
+ return (node.getKind() == kind::BITVECTOR_XOR &&
+ (node[0] == ones ||
+ node[1] == ones));
+}
+
+template<>
+Node RewriteRule<XorOne>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
+ Node ones = utils::mkOnes(utils::getSize(node));
+ Node a;
+ if (node[0] == ones) {
+ a = node[1];
+ } else {
+ Assert(node[1] == ones);
+ a = node[0];
+ }
+
+ return utils::mkNode(kind::BITVECTOR_NOT, a);
+}
+
+
+/**
+ * XorZero
+ *
+ * (a bvxor 0) ==> a
+ */
+
+template<>
+bool RewriteRule<XorZero>::applies(Node node) {
+ Node zero = utils::mkConst(utils::getSize(node), 0);
+ return (node.getKind() == kind::BITVECTOR_XOR &&
+ (node[0] == zero ||
+ node[1] == zero));
+}
+
+template<>
+Node RewriteRule<XorZero>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
+ Node zero = utils::mkConst(utils::getSize(node), 0);
+ if (node[0] == zero) {
+ return node[1];
+ }
+
+ Assert(node[1] == zero);
+ return node[0];
+}
+
+
+/**
+ * BitwiseNotAnd
+ *
+ * (a bvand (~ a)) ==> 0
+ */
+
+template<>
+bool RewriteRule<BitwiseNotAnd>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_AND &&
+ ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
+ (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0])));
+}
+
+template<>
+Node RewriteRule<BitwiseNotAnd>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
+ return utils::mkConst(BitVector(utils::getSize(node), Integer(0)));
+}
+
+/**
+ * BitwiseNegOr
+ *
+ * (a bvor (~ a)) ==> 1
+ */
+
+template<>
+bool RewriteRule<BitwiseNotOr>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_OR &&
+ ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
+ (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0])));
+}
+
+template<>
+Node RewriteRule<BitwiseNotOr>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
+ uint32_t size = utils::getSize(node);
+ Integer ones = Integer(1).multiplyByPow2(size) - 1;
+ return utils::mkConst(BitVector(size, ones));
+}
+
+/**
+ * XorNot
+ *
+ * ((~ a) bvxor (~ b)) ==> (a bvxor b)
+ */
+
+template<>
+bool RewriteRule<XorNot>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_XOR &&
+ node[0].getKind() == kind::BITVECTOR_NOT &&
+ node[1].getKind() == kind::BITVECTOR_NOT);
+}
+
+template<>
+Node RewriteRule<XorNot>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
+ Node a = node[0][0];
+ Node b = node[1][0];
+ return utils::mkNode(kind::BITVECTOR_XOR, a, b);
+}
+
+/**
+ * NotXor
+ *
+ * ~(a bvxor b) ==> (~ a bvxor b)
+ */
+
+template<>
+bool RewriteRule<NotXor>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_NOT &&
+ node[0].getKind() == kind::BITVECTOR_XOR);
+}
+
+template<>
+Node RewriteRule<NotXor>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
+ Node a = node[0][0];
+ Node b = node[0][1];
+ Node nota = utils::mkNode(kind::BITVECTOR_NOT, a);
+ return utils::mkNode(kind::BITVECTOR_XOR, nota, b);
+}
+
+/**
+ * NotIdemp
+ *
+ * ~ (~ a) ==> a
+ */
+
+template<>
+bool RewriteRule<NotIdemp>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_NOT &&
+ node[0].getKind() == kind::BITVECTOR_NOT);
+}
+
+template<>
+Node RewriteRule<NotIdemp>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl;
+ return node[0][0];
+}
+
+
+
+/**
+ * LtSelf
+ *
+ * a < a ==> false
+ */
+
+template<>
+bool RewriteRule<LtSelf>::applies(Node node) {
+ return ((node.getKind() == kind::BITVECTOR_ULT ||
+ node.getKind() == kind::BITVECTOR_SLT) &&
+ node[0] == node[1]);
+}
+
+template<>
+Node RewriteRule<LtSelf>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
+ return utils::mkFalse();
+}
+
+/**
+ * LteSelf
+ *
+ * a <= a ==> true
+ */
+
+template<>
+bool RewriteRule<LteSelf>::applies(Node node) {
+ return ((node.getKind() == kind::BITVECTOR_ULE ||
+ node.getKind() == kind::BITVECTOR_SLE) &&
+ node[0] == node[1]);
+}
+
+template<>
+Node RewriteRule<LteSelf>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
+ return utils::mkTrue();
+}
+
+/**
+ * UltZero
+ *
+ * a < 0 ==> false
+ */
+
+template<>
+bool RewriteRule<UltZero>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ULT &&
+ node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+}
+
+template<>
+Node RewriteRule<UltZero>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
+ return utils::mkFalse();
+}
+
+/**
+ * UltSelf
+ *
+ * a < a ==> false
+ */
+
+template<>
+bool RewriteRule<UltSelf>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ULT &&
+ node[1] == node[0]);
+}
+
+template<>
+Node RewriteRule<UltSelf>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
+ return utils::mkFalse();
+}
+
+
+/**
+ * UleZero
+ *
+ * a <= 0 ==> a = 0
+ */
+
+template<>
+bool RewriteRule<UleZero>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ULE &&
+ node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+}
+
+template<>
+Node RewriteRule<UleZero>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
+ return utils::mkNode(kind::EQUAL, node[0], node[1]);
+}
+
+/**
+ * UleSelf
+ *
+ * a <= a ==> true
+ */
+
+template<>
+bool RewriteRule<UleSelf>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ULE &&
+ node[1] == node[0]);
+}
+
+template<>
+Node RewriteRule<UleSelf>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
+ return utils::mkTrue();
+}
+
+
+/**
+ * ZeroUle
+ *
+ * 0 <= a ==> true
+ */
+
+template<>
+bool RewriteRule<ZeroUle>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_ULE &&
+ node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+}
+
+template<>
+Node RewriteRule<ZeroUle>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
+ return utils::mkTrue();
+}
+
+/**
+ * UleMax
+ *
+ * a <= 11..1 ==> true
+ */
+
+template<>
+bool RewriteRule<UleMax>::applies(Node node) {
+ if (node.getKind()!= kind::BITVECTOR_ULE) {
+ return false;
+ }
+ uint32_t size = utils::getSize(node[0]);
+ Integer ones = Integer(1).multiplyByPow2(size) -1;
+ return (node.getKind() == kind::BITVECTOR_ULE &&
+ node[1] == utils::mkConst(BitVector(size, ones)));
+}
+
+template<>
+Node RewriteRule<UleMax>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
+ return utils::mkTrue();
+}
+
+/**
+ * NotUlt
+ *
+ * ~ ( a < b) ==> b <= a
+ */
+
+template<>
+bool RewriteRule<NotUlt>::applies(Node node) {
+ return (node.getKind() == kind::NOT &&
+ node[0].getKind() == kind::BITVECTOR_ULT);
+}
+
+template<>
+Node RewriteRule<NotUlt>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
+ Node ult = node[0];
+ Node a = ult[0];
+ Node b = ult[1];
+ return utils::mkNode(kind::BITVECTOR_ULE, b, a);
+}
+
+/**
+ * NotUle
+ *
+ * ~ ( a <= b) ==> b < a
+ */
+
+template<>
+bool RewriteRule<NotUle>::applies(Node node) {
+ return (node.getKind() == kind::NOT &&
+ node[0].getKind() == kind::BITVECTOR_ULE);
+}
+
+template<>
+Node RewriteRule<NotUle>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
+ Node ult = node[0];
+ Node a = ult[0];
+ Node b = ult[1];
+ return utils::mkNode(kind::BITVECTOR_ULT, b, a);
+}
+
+/**
+ * MultOne
+ *
+ * (a * 1) ==> a
+ */
+
+template<>
+bool RewriteRule<MultOne>::applies(Node node) {
+ unsigned size = utils::getSize(node);
+ return (node.getKind() == kind::BITVECTOR_MULT &&
+ (node[0] == utils::mkConst(size, 1) ||
+ node[1] == utils::mkConst(size, 1)));
+}
+
+template<>
+Node RewriteRule<MultOne>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<MultOne>(" << node << ")" << std::endl;
+ unsigned size = utils::getSize(node);
+ if (node[0] == utils::mkConst(size, 1)) {
+ return node[1];
+ }
+ Assert(node[1] == utils::mkConst(size, 1));
+ return node[0];
+}
+
+/**
+ * MultZero
+ *
+ * (a * 0) ==> 0
+ */
+
+template<>
+bool RewriteRule<MultZero>::applies(Node node) {
+ unsigned size = utils::getSize(node);
+ return (node.getKind() == kind::BITVECTOR_MULT &&
+ (node[0] == utils::mkConst(size, 0) ||
+ node[1] == utils::mkConst(size, 0)));
+}
+
+template<>
+Node RewriteRule<MultZero>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<MultZero>(" << node << ")" << std::endl;
+ return utils::mkConst(utils::getSize(node), 0);
+}
+
+/**
+ * MultPow2
+ *
+ * (a * 2^k) ==> a[n-k-1:0] 0_k
+ */
+
+template<>
+bool RewriteRule<MultPow2>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_MULT &&
+ (utils::isPow2Const(node[0]) ||
+ utils::isPow2Const(node[1])));
+}
+
+template<>
+Node RewriteRule<MultPow2>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
+ Node a;
+ unsigned power;
+ power = utils::isPow2Const(node[0]);
+
+ if (power != 0) {
+ a = node[1];
+ // isPow2Const returns the power + 1
+ --power;
+ } else {
+ power = utils::isPow2Const(node[1]);
+ Assert(power != 0);
+ a = node[0];
+ power--;
+ }
+
+ Node extract = utils::mkExtract(a, utils::getSize(node) - power - 1, 0);
+ Node zeros = utils::mkConst(power, 0);
+ return utils::mkConcat(extract, zeros);
+}
+
+/**
+ * PlusZero
+ *
+ * (a + 0) ==> a
+ */
+
+template<>
+bool RewriteRule<PlusZero>::applies(Node node) {
+ Node zero = utils::mkConst(utils::getSize(node), 0);
+ return (node.getKind() == kind::BITVECTOR_PLUS &&
+ (node[0] == zero ||
+ node[1] == zero));
+}
+
+template<>
+Node RewriteRule<PlusZero>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<PlusZero>(" << node << ")" << std::endl;
+ Node zero = utils::mkConst(utils::getSize(node), 0);
+ if (node[0] == zero) {
+ return node[1];
+ }
+
+ return node[0];
+}
+
+/**
+ * NegIdemp
+ *
+ * -(-a) ==> a
+ */
+
+template<>
+bool RewriteRule<NegIdemp>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_NEG &&
+ node[0].getKind() == kind::BITVECTOR_NEG);
+}
+
+template<>
+Node RewriteRule<NegIdemp>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
+ return node[0][0];
+}
+
+/**
+ * UdivPow2
+ *
+ * (a udiv 2^k) ==> 0_k a[n-1: k]
+ */
+
+template<>
+bool RewriteRule<UdivPow2>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_UDIV &&
+ utils::isPow2Const(node[1]));
+}
+
+template<>
+Node RewriteRule<UdivPow2>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
+ Node a = node[0];
+ unsigned power = utils::isPow2Const(node[1]) -1;
+
+ Node extract = utils::mkExtract(a, utils::getSize(node) - 1, power);
+ Node zeros = utils::mkConst(power, 0);
+
+ return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract);
+}
+
+/**
+ * UdivOne
+ *
+ * (a udiv 1) ==> a
+ */
+
+template<>
+bool RewriteRule<UdivOne>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_UDIV &&
+ node[1] == utils::mkConst(utils::getSize(node), 1));
+}
+
+template<>
+Node RewriteRule<UdivOne>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
+ return node[0];
+}
+
+/**
+ * UdivSelf
+ *
+ * (a udiv a) ==> 1
+ */
+
+template<>
+bool RewriteRule<UdivSelf>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_UDIV &&
+ node[0] == node[1]);
+}
+
+template<>
+Node RewriteRule<UdivSelf>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl;
+ return utils::mkConst(utils::getSize(node), 1);
+}
+
+/**
+ * UremPow2
+ *
+ * (a urem 2^k) ==> 0_(n-k) a[k-1:0]
+ */
+
+template<>
+bool RewriteRule<UremPow2>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_UREM &&
+ utils::isPow2Const(node[1]));
+}
+
+template<>
+Node RewriteRule<UremPow2>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ unsigned power = utils::isPow2Const(node[1]) - 1;
+ Node extract = utils::mkExtract(a, power - 1, 0);
+ Node zeros = utils::mkConst(utils::getSize(node) - power, 0);
+ return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract);
+}
+
+/**
+ * UremOne
+ *
+ * (a urem 1) ==> 0
+ */
+
+template<>
+bool RewriteRule<UremOne>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_UREM &&
+ node[1] == utils::mkConst(utils::getSize(node), 1));
+}
+
+template<>
+Node RewriteRule<UremOne>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
+ return utils::mkConst(utils::getSize(node), 0);
+}
+
+/**
+ * UremSelf
+ *
+ * (a urem a) ==> 0
+ */
+
+template<>
+bool RewriteRule<UremSelf>::applies(Node node) {
+ return (node.getKind() == kind::BITVECTOR_UREM &&
+ node[0] == node[1]);
+}
+
+template<>
+Node RewriteRule<UremSelf>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
+ return utils::mkConst(utils::getSize(node), 0);
+}
+
+/**
+ * ShiftZero
+ *
+ * (0_k >> a) ==> 0_k
+ */
+
+template<>
+bool RewriteRule<ShiftZero>::applies(Node node) {
+ return ((node.getKind() == kind::BITVECTOR_SHL ||
+ node.getKind() == kind::BITVECTOR_LSHR ||
+ node.getKind() == kind::BITVECTOR_ASHR) &&
+ node[0] == utils::mkConst(utils::getSize(node), 0));
+}
+
+template<>
+Node RewriteRule<ShiftZero>::apply(Node node) {
+ BVDebug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
+ return node[0];
+}
+
+// /**
+// *
+// *
+// *
+// */
+
+// template<>
+// bool RewriteRule<>::applies(Node node) {
+// return (node.getKind() == );
+// }
+
+// template<>
+// Node RewriteRule<>::apply(Node node) {
+// BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
+// return ;
+// }
+
+
+
+}
+}
+}
#include "theory/bv/theory_bv_rewriter.h"
#include "theory/bv/theory_bv_rewrite_rules.h"
#include "theory/bv/theory_bv_rewrite_rules_core.h"
-#include "theory/bv/theory_bv_rewrite_rules_arith.h"
+#include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
+#include "theory/bv/theory_bv_rewrite_rules_constant_evaluation.h"
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
+#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
using namespace CVC4;
using namespace CVC4::theory;
using namespace CVC4::theory::bv;
+
+// CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL;
+// CVC4_THREADLOCAL(TimerStat*) TheoryBVRewriter::d_rewriteTimer = NULL;
+CVC4_THREADLOCAL(RewriteFunction) TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND];
+void TheoryBVRewriter::init() {
+ // s_allRules = new AllRewriteRules;
+ // d_rewriteTimer = new TimerStat("theory::bv::rewriteTimer");
+ // StatisticsRegistry::registerStat(d_rewriteTimer);
+ initializeRewrites();
+
+}
+
+void TheoryBVRewriter::shutdown() {
+ // delete s_allRules;
+ // StatisticsRegistry::unregisterStat(d_rewriteTimer);
+ //delete d_rewriteTimer;
+}
+
+RewriteResponse TheoryBVRewriter::preRewrite(TNode node) {
+ Debug("bitvector-rewrite") << "TheoryBV::preRewrite(" << node << ")" << std::endl;
+ //return d_rewriteTable[node.getKind()](node);
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
+ //TimerStat::CodeTimer codeTimer(*d_rewriteTimer);
+ Debug("bitvector-rewrite") << "TheoryBV::postRewrite(" << node << ")" << std::endl;
+ RewriteResponse res = d_rewriteTable[node.getKind()](node);
+ return res;
+}
+
+RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalUlt>,
+ // if both arguments are constants evaluates
+ RewriteRule<UltZero>
+ // a < 0 rewrites to false
+ >::apply(node);
- BVDebug("bitvector") << "TheoryBV::postRewrite(" << node << ")" << std::endl;
-
- Node result = node;
- if (node.getKind() == kind::CONST_BITVECTOR || (node.getKind() != kind::EQUAL && Theory::isLeafOf(node, THEORY_BV))) {
- result = node;
- } else {
- switch (node.getKind()) {
- case kind::BITVECTOR_CONCAT:
- result = LinearRewriteStrategy<
- // Flatten the top level concatenations
- RewriteRule<ConcatFlatten>,
- // Merge the adjacent extracts on non-constants
- RewriteRule<ConcatExtractMerge>,
- // Merge the adjacent extracts on constants
- RewriteRule<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, ExtractWhole>
- >::apply(node);
- break;
- case kind::BITVECTOR_EXTRACT:
- result = LinearRewriteStrategy<
- // Extract over a concatenation is distributed to the appropriate concatenations
- RewriteRule<ExtractConcat>,
- // Extract over a constant gives a constant
- RewriteRule<ExtractConstant>,
- // We could get another extract over extract
- RewriteRule<ExtractExtract>,
- // At this point only Extract-Whole could apply
- RewriteRule<ExtractWhole>
- >::apply(node);
- break;
- case kind::EQUAL:
- result = LinearRewriteStrategy<
- // Two distinct values rewrite to false
- RewriteRule<FailEq>,
- // If both sides are equal equality is true
- RewriteRule<SimplifyEq>,
- // Eliminate the equalities
- RewriteRule<ReflexivityEq>
- >::apply(node);
- break;
- case kind::BITVECTOR_UGT:
- result = LinearRewriteStrategy <
- RewriteRule<UgtToUlt>
- >::apply(node);
- break;
-
- case kind::BITVECTOR_UGE:
- result = LinearRewriteStrategy <
- RewriteRule<UgeToUle>
- >::apply(node);
- break;
- case kind::BITVECTOR_SGT:
- result = LinearRewriteStrategy <
- RewriteRule<SgtToSlt>
- >::apply(node);
- break;
- case kind::BITVECTOR_SGE:
- result = LinearRewriteStrategy <
- RewriteRule<SgeToSle>
- >::apply(node);
- break;
- case kind::BITVECTOR_REPEAT:
- result = LinearRewriteStrategy <
- RewriteRule<RepeatEliminate>
- >::apply(node);
- break;
- case kind::BITVECTOR_ROTATE_RIGHT:
- result = LinearRewriteStrategy <
- RewriteRule<RotateRightEliminate>
- >::apply(node);
- break;
- case kind::BITVECTOR_ROTATE_LEFT:
- result = LinearRewriteStrategy <
- RewriteRule<RotateLeftEliminate>
- >::apply(node);
- break;
- case kind::BITVECTOR_NAND:
- result = LinearRewriteStrategy <
- RewriteRule<NandEliminate>
- >::apply(node);
- break;
- case kind::BITVECTOR_NOR:
- result = LinearRewriteStrategy <
- RewriteRule<NorEliminate>
- >::apply(node);
- break;
-
- case kind::BITVECTOR_SDIV:
- result = LinearRewriteStrategy <
- RewriteRule<SdivEliminate>
- >::apply(node);
- break;
- case kind::BITVECTOR_SREM:
- result = LinearRewriteStrategy <
- RewriteRule<SremEliminate>
- >::apply(node);
- break;
- case kind::BITVECTOR_SMOD:
- result = LinearRewriteStrategy <
- RewriteRule<SmodEliminate>
- >::apply(node);
- break;
- case kind::BITVECTOR_ZERO_EXTEND:
- result = LinearRewriteStrategy <
- RewriteRule<ZeroExtendEliminate>
- >::apply(node);
- break;
-
- default:
- // TODO: figure out when this is an operator
- result = node;
- break;
- // Unhandled();
- }
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node){
+ return RewriteResponse(REWRITE_DONE, node);
+ // Node resultNode = LinearRewriteStrategy
+ // < RewriteRule < SltEliminate >
+ // // a <_s b ==> a + 2^{n-1} <_u b + 2^{n-1}
+ // >::apply(node);
+
+ // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteUle(TNode node){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalUle>,
+ RewriteRule<UleMax>,
+ RewriteRule<ZeroUle>,
+ RewriteRule<UleZero>,
+ RewriteRule<UleSelf>
+ >::apply(node);
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteSle(TNode node){
+ return RewriteResponse(REWRITE_DONE, node);
+ // Node resultNode = LinearRewriteStrategy
+ // < RewriteRule<SleEliminate>
+ // >::apply(node);
+
+ // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<UgtEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<SgtEliminate>
+ //RewriteRule<SltEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteUge(TNode node){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<UgeEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteSge(TNode node){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<SgeEliminate>
+ // RewriteRule<SleEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteNot(TNode node){
+ Node resultNode = node;
+ if(RewriteRule<NotXor>::applies(node)) {
+ resultNode = RewriteRule<NotXor>::run<false>(node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
}
+ resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalNot>,
+ RewriteRule<NotIdemp>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
- BVDebug("bitvector") << "TheoryBV::postRewrite(" << node << ") => " << result << std::endl;
+RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node) {
+ Node resultNode = node;
+ if (RewriteRule<ExtractConcat>::applies(node)) {
+ resultNode = RewriteRule<ExtractConcat>::run<false>(node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
- return RewriteResponse(REWRITE_DONE, result);
+ if (RewriteRule<ExtractBitwise>::applies(node)) {
+ resultNode = RewriteRule<ExtractBitwise>::run<false>(node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
+ if (RewriteRule<ExtractNot>::applies(node)) {
+ resultNode = RewriteRule<ExtractNot>::run<false>(node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
+ if (RewriteRule<ExtractArith>::applies(node)) {
+ resultNode = RewriteRule<ExtractArith>::run<false>(node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
+ resultNode = LinearRewriteStrategy
+ < RewriteRule<ExtractConstant>,
+ RewriteRule<ExtractExtract>,
+ // We could get another extract over extract
+ RewriteRule<ExtractWhole>
+ // At this point only Extract-Whole could apply
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
}
-CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL;
-void TheoryBVRewriter::init() {
- s_allRules = new AllRewriteRules;
+RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<ConcatFlatten>,
+ // Flatten the top level concatenations
+ RewriteRule<ConcatExtractMerge>,
+ // Merge the adjacent extracts on non-constants
+ RewriteRule<ConcatConstantMerge>,
+ // Merge the adjacent extracts on constants
+ ApplyRuleToChildren<kind::BITVECTOR_CONCAT, ExtractWhole>
+ >::apply(node);
+ return RewriteResponse(REWRITE_DONE, resultNode);
}
-void TheoryBVRewriter::shutdown() {
- delete s_allRules;
+RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalAnd>,
+ RewriteRule<BitwiseIdemp>,
+ RewriteRule<AndZero>,
+ RewriteRule<AndOne>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteOr(TNode node){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalOr>,
+ RewriteRule<BitwiseIdemp>,
+ RewriteRule<OrZero>,
+ RewriteRule<OrOne>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteXor(TNode node) {
+ Node resultNode = node;
+ if (RewriteRule<XorOne>::applies(node)) {
+ resultNode = RewriteRule<XorOne>::run<false> (node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+ resultNode = LinearRewriteStrategy
+ < RewriteRule<XorNot>,
+ RewriteRule<EvalXor>,
+ RewriteRule<XorDuplicate>,
+ RewriteRule<XorZero>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<XnorEliminate>
+ >::apply(node);
+ // need to rewrite two levels in
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
}
+
+RewriteResponse TheoryBVRewriter::RewriteNand(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<NandEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteNor(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<NorEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteComp(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<CompEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteMult(TNode node) {
+ Node resultNode = node;
+ if(RewriteRule<MultPow2>::applies(node)) {
+ resultNode = RewriteRule<MultPow2>::run <false> (node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
+ resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalMult>,
+ RewriteRule<MultOne>,
+ RewriteRule<MultZero>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewritePlus(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalPlus>,
+ RewriteRule<PlusZero>
+ // RewriteRule<PlusSelf>,
+ // RewriteRule<PlusNegSelf>
+ // RewriteRule<PlusLiftConcat>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteSub(TNode node){
+ return RewriteResponse(REWRITE_DONE, node);
+ // Node resultNode = LinearRewriteStrategy
+ // < RewriteRule<SubEliminate>
+ // >::apply(node);
+
+ // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalNeg>,
+ RewriteRule<NegIdemp>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node){
+ Node resultNode = node;
+ if(RewriteRule<UdivPow2>::applies(node)) {
+ resultNode = RewriteRule<UdivPow2>::run <false> (node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
+ resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalUdiv>,
+ RewriteRule<UdivOne>,
+ RewriteRule<UdivSelf>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node) {
+ Node resultNode = node;
+ if(RewriteRule<UremPow2>::applies(node)) {
+ resultNode = RewriteRule<UremPow2>::run <false> (node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
+ resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalUrem>,
+ RewriteRule<UremOne>,
+ RewriteRule<UremSelf>
+ >::apply(node);
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<SmodEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<SdivEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<SremEliminate>
+ >::apply(node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteShl(TNode node) {
+ Node resultNode = node;
+ if(RewriteRule<ShlByConst>::applies(node)) {
+ resultNode = RewriteRule<ShlByConst>::run <false> (node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
+ resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalShl>,
+ RewriteRule<ShiftZero>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node) {
+ Node resultNode = node;
+ if(RewriteRule<LshrByConst>::applies(node)) {
+ resultNode = RewriteRule<LshrByConst>::run <false> (node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
+ resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalLshr>,
+ RewriteRule<ShiftZero>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node) {
+ Node resultNode = node;
+ if(RewriteRule<AshrByConst>::applies(node)) {
+ resultNode = RewriteRule<AshrByConst>::run <false> (node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
+ resultNode = LinearRewriteStrategy
+ < RewriteRule<EvalAshr>,
+ RewriteRule<ShiftZero>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+
+RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<RepeatEliminate >
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<ZeroExtendEliminate >
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node) {
+ // Node resultNode = LinearRewriteStrategy
+ // < RewriteRule<SignExtendEliminate >
+ // >::apply(node);
+
+ // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
+
+RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<RotateRightEliminate >
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<RotateLeftEliminate >
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node) {
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<FailEq>,
+ RewriteRule<SimplifyEq>,
+ RewriteRule<ReflexivityEq>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
+
+RewriteResponse TheoryBVRewriter::IdentityRewrite(TNode node) {
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
+RewriteResponse TheoryBVRewriter::UndefinedRewrite(TNode node) {
+ Debug("bv-rewrite") << "TheoryBV::UndefinedRewrite for" << node;
+ Unimplemented();
+}
+
+
+
+void TheoryBVRewriter::initializeRewrites() {
+
+ for(unsigned i = 0; i < kind::LAST_KIND; ++i) {
+ d_rewriteTable[i] = IdentityRewrite; //UndefinedRewrite;
+ }
+
+ d_rewriteTable [ kind::EQUAL ] = RewriteEqual;
+ d_rewriteTable [ kind::BITVECTOR_ULT ] = RewriteUlt;
+ d_rewriteTable [ kind::BITVECTOR_SLT ] = RewriteSlt;
+ d_rewriteTable [ kind::BITVECTOR_ULE ] = RewriteUle;
+ d_rewriteTable [ kind::BITVECTOR_SLE ] = RewriteSle;
+ d_rewriteTable [ kind::BITVECTOR_UGT ] = RewriteUgt;
+ d_rewriteTable [ kind::BITVECTOR_SGT ] = RewriteSgt;
+ d_rewriteTable [ kind::BITVECTOR_UGE ] = RewriteUge;
+ d_rewriteTable [ kind::BITVECTOR_SGE ] = RewriteSge;
+ d_rewriteTable [ kind::BITVECTOR_NOT ] = RewriteNot;
+ d_rewriteTable [ kind::BITVECTOR_CONCAT ] = RewriteConcat;
+ d_rewriteTable [ kind::BITVECTOR_AND ] = RewriteAnd;
+ d_rewriteTable [ kind::BITVECTOR_OR ] = RewriteOr;
+ d_rewriteTable [ kind::BITVECTOR_XOR] = RewriteXor;
+ d_rewriteTable [ kind::BITVECTOR_XNOR ] = RewriteXnor;
+ d_rewriteTable [ kind::BITVECTOR_NAND ] = RewriteNand;
+ d_rewriteTable [ kind::BITVECTOR_NOR ] = RewriteNor;
+ d_rewriteTable [ kind::BITVECTOR_COMP ] = RewriteComp;
+ d_rewriteTable [ kind::BITVECTOR_MULT ] = RewriteMult;
+ d_rewriteTable [ kind::BITVECTOR_PLUS ] = RewritePlus;
+ d_rewriteTable [ kind::BITVECTOR_SUB ] = RewriteSub;
+ d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg;
+ d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv;
+ d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem;
+ d_rewriteTable [ kind::BITVECTOR_SMOD ] = RewriteSmod;
+ d_rewriteTable [ kind::BITVECTOR_SDIV ] = RewriteSdiv;
+ d_rewriteTable [ kind::BITVECTOR_SREM ] = RewriteSrem;
+ d_rewriteTable [ kind::BITVECTOR_SHL ] = RewriteShl;
+ d_rewriteTable [ kind::BITVECTOR_LSHR ] = RewriteLshr;
+ d_rewriteTable [ kind::BITVECTOR_ASHR ] = RewriteAshr;
+ d_rewriteTable [ kind::BITVECTOR_EXTRACT ] = RewriteExtract;
+ d_rewriteTable [ kind::BITVECTOR_REPEAT ] = RewriteRepeat;
+ d_rewriteTable [ kind::BITVECTOR_ZERO_EXTEND ] = RewriteZeroExtend;
+ d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend;
+ d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight;
+ d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft;
+}
+
+
+
+
#define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
#include "theory/rewriter.h"
+#include "util/stats.h"
namespace CVC4 {
namespace theory {
namespace bv {
struct AllRewriteRules;
+typedef RewriteResponse (*RewriteFunction) (TNode);
class TheoryBVRewriter {
+ // static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
+ // static CVC4_THREADLOCAL(TimerStat*) d_rewriteTimer;
+ static CVC4_THREADLOCAL(RewriteFunction) d_rewriteTable[kind::LAST_KIND];
- static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
+ static RewriteResponse IdentityRewrite(TNode node);
+ static RewriteResponse UndefinedRewrite(TNode node);
+
+ static void initializeRewrites();
+
+ static RewriteResponse RewriteEqual(TNode node);
+ static RewriteResponse RewriteUlt(TNode node);
+ static RewriteResponse RewriteSlt(TNode node);
+ static RewriteResponse RewriteUle(TNode node);
+ static RewriteResponse RewriteSle(TNode node);
+ static RewriteResponse RewriteUgt(TNode node);
+ static RewriteResponse RewriteSgt(TNode node);
+ static RewriteResponse RewriteUge(TNode node);
+ static RewriteResponse RewriteSge(TNode node);
+ static RewriteResponse RewriteNot(TNode node);
+ static RewriteResponse RewriteConcat(TNode node);
+ static RewriteResponse RewriteAnd(TNode node);
+ static RewriteResponse RewriteOr(TNode node);
+ static RewriteResponse RewriteXnor(TNode node);
+ static RewriteResponse RewriteXor(TNode node);
+ static RewriteResponse RewriteNand(TNode node);
+ static RewriteResponse RewriteNor(TNode node);
+ static RewriteResponse RewriteComp(TNode node);
+ static RewriteResponse RewriteMult(TNode node);
+ static RewriteResponse RewritePlus(TNode node);
+ static RewriteResponse RewriteSub(TNode node);
+ static RewriteResponse RewriteNeg(TNode node);
+ static RewriteResponse RewriteUdiv(TNode node);
+ static RewriteResponse RewriteUrem(TNode node);
+ static RewriteResponse RewriteSmod(TNode node);
+ static RewriteResponse RewriteSdiv(TNode node);
+ static RewriteResponse RewriteSrem(TNode node);
+ static RewriteResponse RewriteShl(TNode node);
+ static RewriteResponse RewriteLshr(TNode node);
+ static RewriteResponse RewriteAshr(TNode node);
+ static RewriteResponse RewriteExtract(TNode node);
+ static RewriteResponse RewriteRepeat(TNode node);
+ static RewriteResponse RewriteZeroExtend(TNode node);
+ static RewriteResponse RewriteSignExtend(TNode node);
+ static RewriteResponse RewriteRotateRight(TNode node);
+ static RewriteResponse RewriteRotateLeft(TNode node);
public:
static RewriteResponse postRewrite(TNode node);
- static inline RewriteResponse preRewrite(TNode node) {
- return postRewrite(node);
- }
+ static RewriteResponse preRewrite(TNode node);
static inline Node rewriteEquality(TNode node) {
+ Debug("bitvector") << "TheoryBV::rewriteEquality(" << node << ")" << std::endl;
return postRewrite(node).node;
}
static void init();
static void shutdown();
+
};/* class TheoryBVRewriter */
}/* CVC4::theory::bv namespace */
#define BVDebug(x) if (false) Debug(x)
#endif
+
+
namespace CVC4 {
namespace theory {
namespace bv {
}
+
+inline Node mkConcat(Node node, unsigned repeat) {
+ Assert (repeat);
+ if(repeat == 1) {
+ return node;
+ }
+ NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+ for (unsigned i = 0; i < repeat; ++i) {
+ result << node;
+ }
+ Node resultNode = result;
+ return resultNode;
+}
+
inline Node mkConcat(std::vector<Node>& children) {
if (children.size() > 1)
return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children);
return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2);
}
+inline Node mkOnes(unsigned size) {
+ BitVector val = BitVector(1, Integer(1)).signExtend(size-1);
+ return NodeManager::currentNM()->mkConst<BitVector>(val);
+}
inline Node mkConst(unsigned size, unsigned int value) {
BitVector val(size, value);
return conjunction;
}
+
+inline unsigned isPow2Const(TNode node) {
+ if (node.getKind() != kind::CONST_BITVECTOR) {
+ return false;
+ }
+
+ BitVector bv = node.getConst<BitVector>();
+ return bv.isPow2();
+}
+
+// neeed a better name, this is not technically a ground term
+inline bool isBVGroundTerm(TNode node) {
+ if (node.getNumChildren() == 0) {
+ return node.isConst();
+ }
+
+ for (size_t i = 0; i < node.getNumChildren(); ++i) {
+ if(! node[i].isConst()) {
+ return false;
+ }
+ }
+ return true;
+}
+
inline bool isBVPredicate(TNode node) {
if (node.getKind() == kind::EQUAL ||
node.getKind() == kind::BITVECTOR_ULT ||
private:
+ /*
+ Class invariants:
+ * no overflows: 2^d_size < d_value
+ * no negative numbers: d_value >= 0
+ */
unsigned d_size;
Integer d_value;
+ Integer toSignedInt() const {
+ // returns Integer corresponding to two's complement interpretation of bv
+ unsigned size = d_size;
+ Integer sign_bit = d_value.extractBitRange(1,size-1);
+ Integer val = d_value.extractBitRange(size-1, 0);
+ Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
+ return res;
+ }
+
+
public:
- BitVector(unsigned size, const Integer& val)
- : d_size(size), d_value(val) {}
-
+ BitVector(unsigned size, const Integer& val):
+ d_size(size),
+ d_value(val.modByPow2(size))
+ {}
+
BitVector(unsigned size = 0)
- : d_size(size), d_value(0) {}
+ : d_size(size), d_value(0) {}
BitVector(unsigned size, unsigned int z)
- : d_size(size), d_value(z) {}
-
+ : d_size(size), d_value(z) {
+ d_value = d_value.modByPow2(size);
+ }
+
BitVector(unsigned size, unsigned long int z)
- : d_size(size), d_value(z) {}
+ : d_size(size), d_value(z) {
+ d_value = d_value.modByPow2(size);
+ }
BitVector(unsigned size, const BitVector& q)
- : d_size(size), d_value(q.d_value) {}
-
+ : d_size(size), d_value(q.d_value) {}
+
BitVector(const std::string& num, unsigned base = 2);
~BitVector() {}
+ Integer toInteger() const {
+ return d_value;
+ }
+
BitVector& operator =(const BitVector& x) {
if(this == &x)
return *this;
}
bool operator ==(const BitVector& y) const {
- if (d_size != y.d_size) return false;
+ if (d_size != y.d_size) return false;
return d_value == y.d_value;
}
bool operator !=(const BitVector& y) const {
- if (d_size == y.d_size) return false;
+ if (d_size != y.d_size) return true;
return d_value != y.d_value;
}
+ BitVector equals(const BitVector& y) const {
+ Assert(d_size == y.d_size);
+ return d_value == y.d_value;
+ }
+
+ BitVector concat (const BitVector& other) const {
+ return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
+ }
+
+ BitVector extract(unsigned high, unsigned low) const {
+ return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
+ }
+
+ /*
+ Bitwise operations on BitVectors
+ */
+
+ // xor
+ BitVector operator ^(const BitVector& y) const {
+ Assert (d_size == y.d_size);
+ return BitVector(d_size, d_value.bitwiseXor(y.d_value));
+ }
+
+ // or
+ BitVector operator |(const BitVector& y) const {
+ Assert (d_size == y.d_size);
+ return BitVector(d_size, d_value.bitwiseOr(y.d_value));
+ }
+
+ // and
+ BitVector operator &(const BitVector& y) const {
+ Assert (d_size == y.d_size);
+ return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
+ }
+
+ // not
+ BitVector operator ~() const {
+ return BitVector(d_size, d_value.bitwiseNot());
+ }
+
+ /*
+ Arithmetic operations on BitVectors
+ */
+
+
+ bool operator <(const BitVector& y) const {
+ return d_value < y.d_value;
+ }
+
+ bool operator >(const BitVector& y) const {
+ return d_value > y.d_value ;
+ }
+
+ bool operator <=(const BitVector& y) const {
+ return d_value <= y.d_value;
+ }
+
+ bool operator >=(const BitVector& y) const {
+ return d_value >= y.d_value ;
+ }
+
+
BitVector operator +(const BitVector& y) const {
- return BitVector(std::max(d_size, y.d_size), d_value + y.d_value);
+ Assert (d_size == y.d_size);
+ Integer sum = d_value + y.d_value;
+ return BitVector(d_size, sum);
}
BitVector operator -(const BitVector& y) const {
- return *this + ~y + 1;
+ Assert (d_size == y.d_size);
+ // to maintain the invariant that we are only adding BitVectors of the
+ // same size
+ BitVector one(d_size, Integer(1));
+ return *this + ~y + one;
}
BitVector operator -() const {
- return ~(*this) + 1;
+ BitVector one(d_size, Integer(1));
+ return ~(*this) + one;
}
BitVector operator *(const BitVector& y) const {
- return BitVector(d_size, d_value * y.d_value);
+ Assert (d_size == y.d_size);
+ Integer prod = d_value * y.d_value;
+ return BitVector(d_size, prod);
+ }
+
+ BitVector unsignedDiv (const BitVector& y) const {
+ Assert (d_size == y.d_size);
+ Assert (d_value >= 0 && y.d_value > 0);
+ return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
}
- BitVector operator ~() const {
- //is this right? it looks like a no-op?
- return BitVector(d_size, d_value);
+ BitVector unsignedRem(const BitVector& y) const {
+ Assert (d_size == y.d_size);
+ Assert (d_value >= 0 && y.d_value > 0);
+ return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
+ }
+
+
+ bool signedLessThan(const BitVector& y) const {
+ Assert(d_size == y.d_size);
+ Assert(d_value >= 0 && y.d_value >= 0);
+ Integer a = (*this).toSignedInt();
+ Integer b = y.toSignedInt();
+
+ return a < b;
}
- BitVector concat (const BitVector& other) const {
- return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
- //return BitVector(d_size + other.d_size, (d_value * Integer(2).pow(other.d_size)) + other.d_value);
+ bool unsignedLessThan(const BitVector& y) const {
+ Assert(d_size == y.d_size);
+ Assert(d_value >= 0 && y.d_value >= 0);
+ return d_value < y.d_value;
}
- BitVector extract(unsigned high, unsigned low) const {
- return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
- //return BitVector(high - low + 1, (d_value % (Integer(2).pow(high + 1))) / Integer(2).pow(low));
+ bool signedLessThanEq(const BitVector& y) const {
+ Assert(d_size == y.d_size);
+ Assert(d_value >= 0 && y.d_value >= 0);
+ Integer a = (*this).toSignedInt();
+ Integer b = y.toSignedInt();
+
+ return a <= b;
+ }
+
+ bool unsignedLessThanEq(const BitVector& y) const {
+ Assert(d_size == y.d_size);
+ Assert(d_value >= 0 && y.d_value >= 0);
+ return d_value <= y.d_value;
+ }
+
+
+ /*
+ Extend operations
+ */
+
+ BitVector zeroExtend(unsigned amount) const {
+ return BitVector(d_size + amount, d_value);
+ }
+
+ BitVector signExtend(unsigned amount) const {
+ Integer sign_bit = d_value.extractBitRange(1, d_size -1);
+ if(sign_bit == Integer(0)) {
+ return BitVector(d_size + amount, d_value);
+ } else {
+ Integer val = d_value.oneExtend(d_size, amount);
+ return BitVector(d_size+ amount, val);
+ }
+ }
+
+ /*
+ Shifts on BitVectors
+ */
+
+ BitVector leftShift(const BitVector& y) const {
+ if (y.d_value > Integer(d_size)) {
+ return BitVector(d_size, Integer(0));
+ }
+ if (y.d_value == 0) {
+ return *this;
+ }
+
+ // making sure we don't lose information casting
+ Assert(y.d_value < Integer(1).multiplyByPow2(32));
+ uint32_t amount = y.d_value.toUnsignedInt();
+ Integer res = d_value.multiplyByPow2(amount);
+ return BitVector(d_size, res);
}
+ BitVector logicalRightShift(const BitVector& y) const {
+ if(y.d_value > Integer(d_size)) {
+ return BitVector(d_size, Integer(0));
+ }
+
+ // making sure we don't lose information casting
+ Assert(y.d_value < Integer(1).multiplyByPow2(32));
+ uint32_t amount = y.d_value.toUnsignedInt();
+ Integer res = d_value.divByPow2(amount);
+ return BitVector(d_size, res);
+ }
+
+ BitVector arithRightShift(const BitVector& y) const {
+ Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
+ if(y.d_value > Integer(d_size)) {
+ if(sign_bit == Integer(0)) {
+ return BitVector(d_size, Integer(0));
+ } else {
+ return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 );
+ }
+ }
+
+ if (y.d_value == 0) {
+ return *this;
+ }
+
+ // making sure we don't lose information casting
+ Assert(y.d_value < Integer(1).multiplyByPow2(32));
+
+ uint32_t amount = y.d_value.toUnsignedInt();
+ Integer rest = d_value.divByPow2(amount);
+
+ if(sign_bit == Integer(0)) {
+ return BitVector(d_size, rest);
+ }
+ Integer res = rest.oneExtend(d_size - amount, amount);
+ return BitVector(d_size, res);
+ }
+
+
+ /*
+ Convenience functions
+ */
+
size_t hash() const {
return d_value.hash() + d_size;
}
const Integer& getValue() const {
return d_value;
}
+
+ /**
+ Returns k is the integer is equal to 2^k and zero
+ otherwise
+ @return k if the integer is equal to 2^k and zero otherwise
+ */
+ unsigned isPow2() {
+ return d_value.isPow2();
+ }
+
};/* class BitVector */
+
+
inline BitVector::BitVector(const std::string& num, unsigned base) {
AlwaysAssert( base == 2 || base == 16 );
if( base == 2 ) {
d_size = num.size();
-// d_value = Integer(num,2);
-/*
- for( string::const_iterator it = num.begin(); it != num.end(); ++it ) {
- if( *it != '0' || *it != '1' ) {
- IllegalArgument(num, "BitVector argument is not a binary string.");
- }
- z = (Integer(2) * z) + (*it == '1');
- d_value = mpz_class(z.get_mpz());
- }
-*/
} else if( base == 16 ) {
d_size = num.size() * 4;
-// // Use a stream to decode the hex string
-// stringstream ss;
-// ss.setf(ios::hex, ios::basefield);
-// ss << num;
-// ss >> z;
-// d_value = mpz_class(z);
-// break;
} else {
Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
}
}
*/
+
+ Integer bitwiseOr(const Integer& y) const {
+ return Integer(cln::logior(d_value, y.d_value));
+ }
+
+ Integer bitwiseAnd(const Integer& y) const {
+ return Integer(cln::logand(d_value, y.d_value));
+ }
+
+ Integer bitwiseXor(const Integer& y) const {
+ return Integer(cln::logxor(d_value, y.d_value));
+ }
+
+ Integer bitwiseNot() const {
+ return Integer(cln::lognot(d_value));
+ }
+
+
/**
* Return this*(2^pow).
*/
return Integer( d_value << ipow);
}
+ Integer oneExtend(uint32_t size, uint32_t amount) const {
+ Assert((*this) < Integer(1).multiplyByPow2(size));
+ cln::cl_byte range(amount, size);
+ cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1
+ Integer temp(allones);
+
+ return Integer(cln::deposit_field(allones, d_value, range));
+ }
+
+ uint32_t toUnsignedInt() const {
+ return cln::cl_I_to_uint(d_value);
+ }
+
+
/** See CLN Documentation. */
Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
cln::cl_byte range(bitCount, low);
return Integer( cln::exquo(d_value, y.d_value) );
}
+ Integer modByPow2(uint32_t exp) const {
+ cln::cl_byte range(exp, 0);
+ return Integer(cln::ldb(d_value, range));
+ }
+
+ Integer divByPow2(uint32_t exp) const {
+ return d_value >> exp;
+ }
+
/**
* Raise this Integer to the power <code>exp</code>.
*
return cln::logbitp(n, d_value);
}
+ /**
+ * Returns k if the integer is equal to 2^(k-1)
+ * @return k if the integer is equal to 2^(k-1) and 0 otherwise
+ */
+ unsigned isPow2() const {
+ if (d_value <= 0) return 0;
+ // power2p returns n such that d_value = 2^(n-1)
+ return cln::power2p(d_value);
+ }
+
/**
* If x != 0, returns the unique n s.t. 2^{n-1} <= abs(x) < 2^{n}.
* If x == 0, returns 1.
return *this;
}
+ Integer bitwiseOr(const Integer& y) const {
+ mpz_class result;
+ mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
+ return Integer(result);
+ }
+
+ Integer bitwiseAnd(const Integer& y) const {
+ mpz_class result;
+ mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
+ return Integer(result);
+ }
+
+ Integer bitwiseXor(const Integer& y) const {
+ mpz_class result;
+ mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
+ return Integer(result);
+ }
+
+ Integer bitwiseNot() const {
+ mpz_class result;
+ mpz_com(result.get_mpz_t(), d_value.get_mpz_t());
+ return Integer(result);
+ }
+
/**
* Return this*(2^pow).
*/
return Integer( result );
}
+ /**
+ * Returns the integer with the binary representation of size bits
+ * extended with amount 1's
+ */
+ Integer oneExtend(uint32_t size, uint32_t amount) const {
+ // check that the size is accurate
+ Assert ((*this) < Integer(1).multiplyByPow2(size));
+ mpz_class res = d_value;
+
+ for (unsigned i = size; i < size + amount; ++i) {
+ mpz_setbit(res.get_mpz_t(), i);
+ }
+
+ return Integer(res);
+ }
+
+ uint32_t toUnsignedInt() const {
+ return mpz_get_ui(d_value.get_mpz_t());
+ }
+
/** See GMP Documentation. */
Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
// bitCount = high-low+1
}
/**
- * Computes a floor quoient and remainder for x divided by y.
+ * Computes a floor quotient and remainder for x divided by y.
*/
static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
mpz_fdiv_qr(q.d_value.get_mpz_t(), r.d_value.get_mpz_t(), x.d_value.get_mpz_t(), y.d_value.get_mpz_t());
return Integer( q );
}
+ /**
+ * Returns y mod 2^exp
+ */
+ Integer modByPow2(uint32_t exp) const {
+ mpz_class res;
+ mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
+ return Integer(res);
+ }
+
+ /**
+ * Returns y / 2^exp
+ */
+ Integer divByPow2(uint32_t exp) const {
+ mpz_class res;
+ mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
+ return Integer(res);
+ }
+
+
int sgn() const {
return mpz_sgn(d_value.get_mpz_t());
}
long si = d_value.get_si();
// ensure there wasn't overflow
AlwaysAssert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0,
- "Overflow when extracting long from multiprecision integer");
+ "Overflow detected in Integer::getLong()");
return si;
}
unsigned long getUnsignedLong() const {
unsigned long ui = d_value.get_ui();
// ensure there wasn't overflow
AlwaysAssert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0,
- "Overflow when extracting unsigned long from multiprecision integer");
+ "Overflow detected in Integer::getUnsignedLong()");
return ui;
}
return mpz_tstbit(d_value.get_mpz_t(), n);
}
+ /**
+ * Returns k if the integer is equal to 2^(k-1)
+ * @return k if the integer is equal to 2^(k-1) and 0 otherwise
+ */
+ unsigned isPow2() const {
+ if (d_value <= 0) return 0;
+ // check that the number of ones in the binary represenation is 1
+ if (mpz_popcount(d_value.get_mpz_t()) == 1) {
+ // return the index of the first one plus 1
+ return mpz_scan1(d_value.get_mpz_t(), 0) + 1;
+ }
+ return 0;
+ }
+
+
/**
* If x != 0, returns the smallest n s.t. 2^{n-1} <= abs(x) < 2^{n}.
* If x == 0, returns 1.
projects / cvc5.git / commitdiff