diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 196 | ||||
-rw-r--r-- | src/theory/bv/bitblaster.h | 93 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 29 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 17 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 10 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 203 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.h | 28 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 87 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.h | 30 | ||||
-rw-r--r-- | src/theory/bv/kinds | 11 | ||||
-rw-r--r-- | src/theory/bv/options | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 72 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 20 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 51 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 17 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 196 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 28 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 2 |
20 files changed, 644 insertions, 465 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 8579012ab..d17dd588f 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -12,7 +12,7 @@ ** \brief [[ Add one-line brief description here ]] ** ** [[ Add lengthier description here ]] - ** + ** **/ #include "bitblaster.h" @@ -29,7 +29,7 @@ using namespace std; using namespace CVC4::theory::bv::utils; -using namespace CVC4::context; +using namespace CVC4::context; using namespace CVC4::prop; namespace CVC4 { @@ -37,20 +37,20 @@ namespace theory { namespace bv{ std::string toString(Bits& bits) { - ostringstream os; + ostringstream os; for (int i = bits.size() - 1; i >= 0; --i) { TNode bit = bits[i]; if (bit.getKind() == kind::CONST_BOOLEAN) { os << (bit.getConst<bool>() ? "1" : "0"); } else { - os << bit<< " "; + os << bit<< " "; } } os <<"\n"; - - return os.str(); + + return os.str(); } -/////// Bitblaster +/////// Bitblaster Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : d_bv(bv), @@ -64,38 +64,41 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context()); MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv); - d_satSolver->setNotify(notify); + d_satSolver->setNotify(notify); // initializing the bit-blasting strategies - initAtomBBStrategies(); - initTermBBStrategies(); + initAtomBBStrategies(); + initTermBBStrategies(); } Bitblaster::~Bitblaster() { delete d_cnfStream; - delete d_satSolver; + delete d_satSolver; } -/** +/** * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver * NOTE: duplicate clauses are not detected because of marker literal * @param node the atom to be bitblasted - * + * */ void Bitblaster::bbAtom(TNode node) { node = node.getKind() == kind::NOT? node[0] : node; - + if (hasBBAtom(node)) { - return; + return; } // make sure it is marked as an atom - addAtom(node); + addAtom(node); - Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; + Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numAtoms; // the bitblasted definition of the atom - Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this)); + Node normalized = Rewriter::rewrite(node); + Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ? + Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) : + normalized; // asserting that the atom is true iff the definition holds Node atom_definition = mkNode(kind::IFF, node, atom_bb); @@ -123,14 +126,14 @@ void Bitblaster::bbTerm(TNode node, Bits& bits) { return; } - Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; + Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numTerms; d_termBBStrategies[node.getKind()] (node, bits,this); - + Assert (bits.size() == utils::getSize(node)); - cacheTermDef(node, bits); + cacheTermDef(node, bits); } Node Bitblaster::bbOptimize(TNode node) { @@ -139,21 +142,21 @@ Node Bitblaster::bbOptimize(TNode node) { if (node.getKind() == kind::BITVECTOR_PLUS) { if (RewriteRule<BBPlusNeg>::applies(node)) { Node res = RewriteRule<BBPlusNeg>::run<false>(node); - return res; + return res; } // if (RewriteRule<BBFactorOut>::applies(node)) { // Node res = RewriteRule<BBFactorOut>::run<false>(node); - // return res; - // } + // return res; + // } } else if (node.getKind() == kind::BITVECTOR_MULT) { if (RewriteRule<MultPow2>::applies(node)) { Node res = RewriteRule<MultPow2>::run<false>(node); - return res; + return res; } } - - return node; + + return node; } /// Public methods @@ -170,31 +173,31 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) { std::vector<SatLiteral> literal_explanation; d_satSolver->explain(d_cnfStream->getLiteral(atom), literal_explanation); for (unsigned i = 0; i < literal_explanation.size(); ++i) { - explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); + explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); } } -/** +/* * Asserts the clauses corresponding to the atom to the Sat Solver * by turning on the marker literal (i.e. setting it to false) * @param node the atom to be asserted - * + * */ - + bool Bitblaster::propagate() { return d_satSolver->propagate() == prop::SAT_VALUE_TRUE; } bool Bitblaster::assertToSat(TNode lit, bool propagate) { // strip the not - TNode atom; + TNode atom; if (lit.getKind() == kind::NOT) { - atom = lit[0]; + atom = lit[0]; } else { - atom = lit; + atom = lit; } - + Assert (hasBBAtom(atom)); SatLiteral markerLit = d_cnfStream->getLiteral(atom); @@ -202,9 +205,9 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) { if(lit.getKind() == kind::NOT) { markerLit = ~markerLit; } - + Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n"; - Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n"; + Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n"; SatValue ret = d_satSolver->assertAssumption(markerLit, propagate); @@ -214,13 +217,13 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) { return ret == prop::SAT_VALUE_TRUE; } -/** - * Calls the solve method for the Sat Solver. +/** + * Calls the solve method for the Sat Solver. * passing it the marker literals to be asserted - * + * * @return true for sat, and false for unsat */ - + bool Bitblaster::solve(bool quick_solve) { if (Trace.isOn("bitvector")) { Trace("bitvector") << "Bitblaster::solve() asserted atoms "; @@ -229,24 +232,24 @@ bool Bitblaster::solve(bool quick_solve) { Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; } } - Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; - return SAT_VALUE_TRUE == d_satSolver->solve(); + Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; + return SAT_VALUE_TRUE == d_satSolver->solve(); } void Bitblaster::getConflict(std::vector<TNode>& conflict) { SatClause conflictClause; d_satSolver->getUnsatCore(conflictClause); - + for (unsigned i = 0; i < conflictClause.size(); i++) { - SatLiteral lit = conflictClause[i]; + SatLiteral lit = conflictClause[i]; TNode atom = d_cnfStream->getNode(lit); - Node not_atom; + Node not_atom; if (atom.getKind() == kind::NOT) { not_atom = atom[0]; } else { - not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); + not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); } - conflict.push_back(not_atom); + conflict.push_back(not_atom); } } @@ -256,9 +259,9 @@ void Bitblaster::getConflict(std::vector<TNode>& conflict) { void Bitblaster::initAtomBBStrategies() { for (int i = 0 ; i < kind::LAST_KIND; ++i ) { - d_atomBBStrategies[i] = UndefinedAtomBBStrategy; + d_atomBBStrategies[i] = UndefinedAtomBBStrategy; } - + /// setting default bb strategies for atoms d_atomBBStrategies [ kind::EQUAL ] = DefaultEqBB; d_atomBBStrategies [ kind::BITVECTOR_ULT ] = DefaultUltBB; @@ -269,7 +272,7 @@ void Bitblaster::initAtomBBStrategies() { d_atomBBStrategies [ kind::BITVECTOR_SLE ] = DefaultSleBB; d_atomBBStrategies [ kind::BITVECTOR_SGT ] = DefaultSgtBB; d_atomBBStrategies [ kind::BITVECTOR_SGE ] = DefaultSgeBB; - + } void Bitblaster::initTermBBStrategies() { @@ -278,7 +281,7 @@ void Bitblaster::initTermBBStrategies() { for (int i = 0 ; i < kind::LAST_KIND; ++i ) { d_termBBStrategies[i] = DefaultVarBB; } - + /// setting default bb strategies for terms: // d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB; d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB; @@ -295,13 +298,13 @@ void Bitblaster::initTermBBStrategies() { d_termBBStrategies [ kind::BITVECTOR_PLUS ] = DefaultPlusBB; d_termBBStrategies [ kind::BITVECTOR_SUB ] = DefaultSubBB; d_termBBStrategies [ kind::BITVECTOR_NEG ] = DefaultNegBB; - d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy; d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ] = DefaultUdivBB; d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ] = DefaultUremBB; - d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy; d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB; d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB; d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB; @@ -313,22 +316,22 @@ void Bitblaster::initTermBBStrategies() { d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ] = DefaultRotateLeftBB; } - + bool Bitblaster::hasBBAtom(TNode atom) const { return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end(); } void Bitblaster::cacheTermDef(TNode term, Bits def) { Assert (d_termCache.find(term) == d_termCache.end()); - d_termCache[term] = def; + d_termCache[term] = def; } bool Bitblaster::hasBBTerm(TNode node) const { - return d_termCache.find(node) != d_termCache.end(); + return d_termCache.find(node) != d_termCache.end(); } void Bitblaster::getBBTerm(TNode node, Bits& bits) const { - Assert (hasBBTerm(node)); + Assert (hasBBTerm(node)); // copy? bits = d_termCache.find(node)->second; } @@ -337,7 +340,7 @@ Bitblaster::Statistics::Statistics() : d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0), d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0), d_numTerms("theory::bv::NumberOfBitblastedTerms", 0), - d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0), + d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0), d_bitblastTimer("theory::bv::BitblastTimer") { StatisticsRegistry::registerStat(&d_numTermClauses); @@ -374,7 +377,7 @@ void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) { }; void Bitblaster::MinisatNotify::safePoint() { - d_bv->d_out->safePoint(); + d_bv->d_out->safePoint(); } EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) { @@ -417,70 +420,77 @@ EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) { bool Bitblaster::isSharedTerm(TNode node) { - return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); + return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } bool Bitblaster::hasValue(TNode a) { - Assert (d_termCache.find(a) != d_termCache.end()); + Assert (d_termCache.find(a) != d_termCache.end()); Bits bits = d_termCache[a]; for (int i = bits.size() -1; i >= 0; --i) { - SatValue bit_value; - if (d_cnfStream->hasLiteral(bits[i])) { + SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { SatLiteral bit = d_cnfStream->getLiteral(bits[i]); bit_value = d_satSolver->value(bit); if (bit_value == SAT_VALUE_UNKNOWN) - return false; + return false; } else { - return false; + return false; } } - return true; + return true; } -/** +/** * Returns the value a is currently assigned to in the SAT solver - * or null if the value is completely unassigned. - * - * @param a - * - * @return + * or null if the value is completely unassigned. + * + * @param a + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them + * + * @return */ -Node Bitblaster::getVarValue(TNode a) { +Node Bitblaster::getVarValue(TNode a, bool fullModel) { if (d_termCache.find(a) == d_termCache.end()) { Assert(isSharedTerm(a)); - return Node(); + return Node(); } Bits bits = d_termCache[a]; - Integer value(0); + Integer value(0); for (int i = bits.size() -1; i >= 0; --i) { SatValue bit_value; - if (d_cnfStream->hasLiteral(bits[i])) { + if (d_cnfStream->hasLiteral(bits[i])) { SatLiteral bit = d_cnfStream->getLiteral(bits[i]); bit_value = d_satSolver->value(bit); - Assert (bit_value != SAT_VALUE_UNKNOWN); + Assert (bit_value != SAT_VALUE_UNKNOWN); } else { - // the bit is unconstrainted so we can give it an arbitrary value + //TODO: return Node() if fullModel=false? + // the bit is unconstrainted so we can give it an arbitrary value bit_value = SAT_VALUE_FALSE; } - Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0); - value = value * 2 + bit_int; + Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0); + value = value * 2 + bit_int; } - return utils::mkConst(BitVector(bits.size(), value)); + return utils::mkConst(BitVector(bits.size(), value)); } -void Bitblaster::collectModelInfo(TheoryModel* m) { +void Bitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin(); for (; it!= d_variables.end(); ++it) { TNode var = *it; if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { - Node const_value = getVarValue(var); + Node const_value = getVarValue(var, fullModel); if(const_value == Node()) { - // if the value is unassigned just set it to zero - const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); + if( fullModel ){ + // if the value is unassigned just set it to zero + const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); + } + } + if(const_value != Node()) { + Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; + m->assertEquality(var, const_value, true); } - Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " - << var << " " - << const_value << "))\n"; - m->assertEquality(var, const_value, true); } } } diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index c122c407d..6fab0369c 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -55,14 +55,14 @@ namespace bv { typedef std::vector<Node> Bits; -std::string toString (Bits& bits); +std::string toString (Bits& bits); class TheoryBV; -/** - * The Bitblaster that manages the mapping between Nodes - * and their bitwise definition - * +/** + * The Bitblaster that manages the mapping between Nodes + * and their bitwise definition + * */ class Bitblaster { @@ -79,26 +79,26 @@ class Bitblaster { void notify(prop::SatClause& clause); void safePoint(); }; - - + + typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction > TermDefMap; typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> VarSet; - - typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*); - typedef Node (*AtomBBStrategy) (TNode, Bitblaster*); + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> VarSet; + + typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*); + typedef Node (*AtomBBStrategy) (TNode, Bitblaster*); TheoryBV *d_bv; - + // sat solver used for bitblasting and associated CnfStream theory::OutputChannel* d_bvOutput; - prop::BVSatSolverInterface* d_satSolver; + prop::BVSatSolverInterface* d_satSolver; prop::CnfStream* d_cnfStream; // caches and mappings TermDefMap d_termCache; AtomSet d_bitblastedAtoms; - VarSet d_variables; + VarSet d_variables; context::CDList<prop::SatLiteral> d_assertedAtoms; /**< context dependent list storing the atoms currently asserted by the DPLL SAT solver. */ @@ -111,79 +111,80 @@ class Bitblaster { /// function tables for the various bitblasting strategies indexed by node kind TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; - AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; + AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; // helper methods to initialize function tables void initAtomBBStrategies(); - void initTermBBStrategies(); + void initTermBBStrategies(); // returns a node that might be easier to bitblast - Node bbOptimize(TNode node); - - void addAtom(TNode atom); + Node bbOptimize(TNode node); + + void addAtom(TNode atom); // division is bitblasted in terms of constraints // so it needs to use private bitblaster interface void bbUdiv(TNode node, Bits& bits); void bbUrem(TNode node, Bits& bits); - bool hasValue(TNode a); + bool hasValue(TNode a); public: void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division void bbTerm(TNode node, Bits& bits); void bbAtom(TNode node); - - Bitblaster(context::Context* c, bv::TheoryBV* bv); + + Bitblaster(context::Context* c, bv::TheoryBV* bv); ~Bitblaster(); bool assertToSat(TNode node, bool propagate = true); bool propagate(); bool solve(bool quick_solve = false); - void getConflict(std::vector<TNode>& conflict); + void getConflict(std::vector<TNode>& conflict); void explain(TNode atom, std::vector<TNode>& explanation); EqualityStatus getEqualityStatus(TNode a, TNode b); - /** + /** * Return a constant Node representing the value of a variable - * in the current model. - * @param a - * - * @return + * in the current model. + * @param a + * + * @return */ - Node getVarValue(TNode a); - /** - * Adds a constant value for each bit-blasted variable in the model. - * - * @param m the model + Node getVarValue(TNode a, bool fullModel=true); + /** + * Adds a constant value for each bit-blasted variable in the model. + * + * @param m the model + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them */ - void collectModelInfo(TheoryModel* m); - /** - * Stores the variable (or non-bv term) and its corresponding bits. - * - * @param var - * @param bits + void collectModelInfo(TheoryModel* m, bool fullModel); + /** + * Stores the variable (or non-bv term) and its corresponding bits. + * + * @param var */ void storeVariable(TNode var) { - d_variables.insert(var); + d_variables.insert(var); } bool isSharedTerm(TNode node); uint64_t computeAtomWeight(TNode node); private: - + class Statistics { public: IntStat d_numTermClauses, d_numAtomClauses; - IntStat d_numTerms, d_numAtoms; + IntStat d_numTerms, d_numAtoms; TimerStat d_bitblastTimer; Statistics(); - ~Statistics(); - }; - + ~Statistics(); + }; + Statistics d_statistics; }; -} /* bv namespace */ +} /* bv namespace */ } /* theory namespace */ diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 8374a3f75..0b0551283 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -9,7 +9,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Algebraic solver. + ** \brief Algebraic solver. ** ** Algebraic solver. **/ @@ -46,7 +46,7 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { out << "BV_CORE_SUBTHEORY"; break; case SUB_INEQUALITY: - out << "BV_INEQUALITY_SUBTHEORY"; + out << "BV_INEQUALITY_SUBTHEORY"; default: Unreachable(); break; @@ -55,13 +55,10 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { } -const bool d_useEqualityEngine = true; -const bool d_useSatPropagation = true; +// forward declaration +class TheoryBV; -// forward declaration -class TheoryBV; - -typedef context::CDQueue<Node> AssertionQueue; +typedef context::CDQueue<Node> AssertionQueue; /** * Abstract base class for bit-vector subtheory solvers * @@ -78,7 +75,7 @@ protected: AssertionQueue d_assertionQueue; context::CDO<uint32_t> d_assertionIndex; public: - + SubtheorySolver(context::Context* c, TheoryBV* bv) : d_context(c), d_bv(bv), @@ -86,24 +83,24 @@ public: d_assertionIndex(c, 0) {} virtual ~SubtheorySolver() {} - virtual bool check(Theory::Effort e) = 0; + virtual bool check(Theory::Effort e) = 0; virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0; virtual void preRegister(TNode node) {} virtual void propagate(Theory::Effort e) {} - virtual void collectModelInfo(TheoryModel* m) = 0; - virtual Node getModelValue(TNode var) = 0; + virtual void collectModelInfo(TheoryModel* m, bool fullModel) = 0; + virtual Node getModelValue(TNode var) = 0; virtual bool isComplete() = 0; virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0; - virtual void addSharedTerm(TNode node) {} + virtual void addSharedTerm(TNode node) {} bool done() { return d_assertionQueue.size() == d_assertionIndex; } TNode get() { - Assert (!done()); + Assert (!done()); TNode res = d_assertionQueue[d_assertionIndex]; d_assertionIndex = d_assertionIndex + 1; - return res; + return res; } virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); } -}; +}; } } diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 2308f36a3..5a0c17134 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -34,7 +34,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) d_bitblaster(new Bitblaster(c, bv)), d_bitblastQueue(c), d_statistics(), - d_validModelCache(c, true) + d_validModelCache(c, true), + d_useSatPropagation(options::bvPropagate()) {} BitblastSolver::~BitblastSolver() { @@ -83,20 +84,20 @@ void BitblastSolver::bitblastQueue() { } bool BitblastSolver::check(Theory::Effort e) { - Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; + Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; Assert(!options::bitvectorEagerBitblast()); - ++(d_statistics.d_numCallstoCheck); + ++(d_statistics.d_numCallstoCheck); //// Lazy bit-blasting // bit-blast enqueued nodes bitblastQueue(); - // Processing assertions + // Processing assertions while (!done()) { TNode fact = get(); d_validModelCache = false; - Debug("bv-bitblast") << " fact " << fact << ")\n"; + Debug("bv-bitblast") << " fact " << fact << ")\n"; if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) { // Some atoms have not been bit-blasted yet d_bitblaster->bbAtom(fact); @@ -143,8 +144,8 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) { return d_bitblaster->getEqualityStatus(a, b); } -void BitblastSolver::collectModelInfo(TheoryModel* m) { - return d_bitblaster->collectModelInfo(m); +void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) { + return d_bitblaster->collectModelInfo(m, fullModel); } Node BitblastSolver::getModelValue(TNode node) @@ -188,5 +189,5 @@ Node BitblastSolver::getModelValueRec(TNode node) Assert(val.isConst()); d_modelCache[node] = val; Debug("bitvector-model") << node << " => " << val <<"\n"; - return val; + return val; } diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 819b3d62c..f1204dbdf 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -19,7 +19,6 @@ #pragma once #include "theory/bv/bv_subtheory.h" -#include "theory/substitutions.h" namespace CVC4 { namespace theory { namespace bv { @@ -33,20 +32,21 @@ class BitblastSolver : public SubtheorySolver { struct Statistics { IntStat d_numCallstoCheck; Statistics(); - ~Statistics(); - }; + ~Statistics(); + }; /** Bitblaster */ Bitblaster* d_bitblaster; /** Nodes that still need to be bit-blasted */ context::CDQueue<TNode> d_bitblastQueue; - Statistics d_statistics; + Statistics d_statistics; typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_modelCache; context::CDO<bool> d_validModelCache; Node getModelValueRec(TNode node); + bool d_useSatPropagation; public: BitblastSolver(context::Context* c, TheoryBV* bv); ~BitblastSolver(); @@ -55,7 +55,7 @@ public: bool check(Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); EqualityStatus getEqualityStatus(TNode a, TNode b); - void collectModelInfo(TheoryModel* m); + void collectModelInfo(TheoryModel* m, bool fullModel); Node getModelValue(TNode node); bool isComplete() { return true; } void bitblastQueue(); diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index c0546f892..45946b8c8 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -37,53 +37,48 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv) d_isCoreTheory(c, true), d_reasons(c) { - if (d_useEqualityEngine) { - - // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); - } + + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); } CoreSolver::~CoreSolver() { - delete d_slicer; + delete d_slicer; } void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); } void CoreSolver::preRegister(TNode node) { - if (!d_useEqualityEngine) - return; - if (node.getKind() == kind::EQUAL) { d_equalityEngine.addTriggerEquality(node); if (options::bitvectorCoreSolver()) { @@ -109,51 +104,51 @@ Node CoreSolver::getBaseDecomposition(TNode a) { std::vector<Node> a_decomp; d_slicer->getBaseDecomposition(a, a_decomp); Node new_a = utils::mkConcat(a_decomp); - Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n"; - return new_a; + Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n"; + return new_a; } bool CoreSolver::decomposeFact(TNode fact) { - Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl; + Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl; // assert decompositions since the equality engine does not know the semantics of // concat: // a == a_1 concat ... concat a_k // b == b_1 concat ... concat b_k - Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl; - // FIXME: are this the right things to assert? + Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl; + // FIXME: are this the right things to assert? // assert decompositions since the equality engine does not know the semantics of // concat: // a == a_1 concat ... concat a_k // b == b_1 concat ... concat b_k - TNode eq = fact.getKind() == kind::NOT? fact[0] : fact; + TNode eq = fact.getKind() == kind::NOT? fact[0] : fact; TNode a = eq[0]; TNode b = eq[1]; Node new_a = getBaseDecomposition(a); - Node new_b = getBaseDecomposition(b); - + Node new_b = getBaseDecomposition(b); + Assert (utils::getSize(new_a) == utils::getSize(new_b) && - utils::getSize(new_a) == utils::getSize(a)); - + utils::getSize(new_a) == utils::getSize(a)); + NodeManager* nm = NodeManager::currentNM(); Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a); Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b); bool ok = true; ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue()); - if (!ok) return false; + if (!ok) return false; ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue()); - if (!ok) return false; + if (!ok) return false; ok = assertFactToEqualityEngine(fact, fact); if (!ok) return false; - + if (fact.getKind() == kind::EQUAL) { // assert the individual equalities as well // a_i == b_i if (new_a.getKind() == kind::BITVECTOR_CONCAT && new_b.getKind() == kind::BITVECTOR_CONCAT) { - - Assert (new_a.getNumChildren() == new_b.getNumChildren()); + + Assert (new_a.getNumChildren() == new_b.getNumChildren()); for (unsigned i = 0; i < new_a.getNumChildren(); ++i) { Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]); ok = assertFactToEqualityEngine(eq_i, fact); @@ -161,23 +156,23 @@ bool CoreSolver::decomposeFact(TNode fact) { } } } - return true; + return true; } bool CoreSolver::check(Theory::Effort e) { Trace("bitvector::core") << "CoreSolver::check \n"; Assert (!d_bv->inConflict()); - ++(d_statistics.d_numCallstoCheck); - bool ok = true; + ++(d_statistics.d_numCallstoCheck); + bool ok = true; std::vector<Node> core_eqs; while (! done()) { - TNode fact = get(); - + TNode fact = get(); + // update whether we are in the core fragment if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) { - d_isCoreTheory = false; + d_isCoreTheory = false; } - + // only reason about equalities if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) { if (options::bitvectorCoreSolver()) { @@ -186,31 +181,31 @@ bool CoreSolver::check(Theory::Effort e) { ok = assertFactToEqualityEngine(fact, fact); } } else { - ok = assertFactToEqualityEngine(fact, fact); + ok = assertFactToEqualityEngine(fact, fact); } if (!ok) - return false; + return false; } - + if (Theory::fullEffort(e) && isComplete()) { buildModel(); } - + return true; } void CoreSolver::buildModel() { if (options::bitvectorCoreSolver()) { // FIXME - Unreachable(); - return; + Unreachable(); + return; } - Debug("bv-core") << "CoreSolver::buildModel() \n"; - d_modelValues.clear(); + Debug("bv-core") << "CoreSolver::buildModel() \n"; + d_modelValues.clear(); TNodeSet constants; - TNodeSet constants_in_eq_engine; + TNodeSet constants_in_eq_engine; // collect constants in equality engine - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); while (!eqcs_i.isFinished()) { TNode repr = *eqcs_i; if (repr.getKind() == kind::CONST_BITVECTOR) { @@ -218,39 +213,39 @@ void CoreSolver::buildModel() { eq::EqClassIterator it(repr, &d_equalityEngine); if (!(++it).isFinished() || true) { constants.insert(repr); - constants_in_eq_engine.insert(repr); + constants_in_eq_engine.insert(repr); } } - ++eqcs_i; + ++eqcs_i; } // build repr to value map - + eqcs_i = eq::EqClassesIterator(&d_equalityEngine); while (!eqcs_i.isFinished()) { TNode repr = *eqcs_i; ++eqcs_i; - + if (repr.getKind() != kind::VARIABLE && repr.getKind() != kind::SKOLEM && repr.getKind() != kind::CONST_BITVECTOR && !d_bv->isSharedTerm(repr)) { - continue; + continue; } - - TypeNode type = repr.getType(); + + TypeNode type = repr.getType(); if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) { - Debug("bv-core-model") << " processing " << repr <<"\n"; + Debug("bv-core-model") << " processing " << repr <<"\n"; // we need to assign a value for it TypeEnumerator te(type); - Node val; + Node val; do { - val = *te; + val = *te; ++te; // Debug("bv-core-model") << " trying value " << val << "\n"; // Debug("bv-core-model") << " is in set? " << constants.count(val) << "\n"; - // Debug("bv-core-model") << " enumerator done? " << te.isFinished() << "\n"; + // Debug("bv-core-model") << " enumerator done? " << te.isFinished() << "\n"; } while (constants.count(val) != 0 && !(te.isFinished())); - + if (te.isFinished() && constants.count(val) != 0) { // if we cannot enumerate anymore values we just return the lemma stating that // at least two of the representatives are equal. @@ -259,15 +254,15 @@ void CoreSolver::buildModel() { for (TNodeSet::const_iterator it = constants_in_eq_engine.begin(); it != constants_in_eq_engine.end(); ++it) { - TNode constant = *it; + TNode constant = *it; if (utils::getSize(constant) == utils::getSize(repr)) { - representatives.push_back(constant); + representatives.push_back(constant); } } for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { representatives.push_back(it->first); } - std::vector<Node> equalities; + std::vector<Node> equalities; for (unsigned i = 0; i < representatives.size(); ++i) { for (unsigned j = i + 1; j < representatives.size(); ++j) { TNode a = representatives[i]; @@ -279,19 +274,19 @@ void CoreSolver::buildModel() { } Node lemma = utils::mkOr(equalities); d_bv->lemma(lemma); - Debug("bv-core") << " lemma: " << lemma << "\n"; - return; + Debug("bv-core") << " lemma: " << lemma << "\n"; + return; } Debug("bv-core-model") << " " << repr << " => " << val <<"\n" ; constants.insert(val); - d_modelValues[repr] = val; + d_modelValues[repr] = val; } } } bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { - // Notify the equality engine - if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) { + // Notify the equality engine + if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) { Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl; // Debug("bv-slicer-eq") << " reason=" << reason << endl; bool negated = fact.getKind() == kind::NOT; @@ -315,8 +310,8 @@ bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { // checking for a conflict if (d_bv->inConflict()) { return false; - } - return true; + } + return true; } bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) { @@ -361,10 +356,10 @@ void CoreSolver::conflict(TNode a, TNode b) { d_bv->setConflict(conflict); } -void CoreSolver::collectModelInfo(TheoryModel* m) { +void CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) { if (options::bitvectorCoreSolver()) { Unreachable(); - return; + return; } if (Debug.isOn("bitvector-model")) { context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin(); @@ -377,11 +372,11 @@ void CoreSolver::collectModelInfo(TheoryModel* m) { d_bv->computeRelevantTerms(termSet); m->assertEqualityEngine(&d_equalityEngine, &termSet); if (isComplete()) { - Debug("bitvector-model") << "CoreSolver::collectModelInfo complete."; + Debug("bitvector-model") << "CoreSolver::collectModelInfo complete."; for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { Node a = it->first; Node b = it->second; - m->assertEquality(a, b, true); + m->assertEquality(a, b, true); } } } @@ -390,23 +385,23 @@ Node CoreSolver::getModelValue(TNode var) { // we don't need to evaluate bv expressions and only look at variable values // because this only gets called when the core theory is complete (i.e. no other bv // function symbols are currently asserted) - Assert (d_slicer->isCoreTerm(var)); - - Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")"; + Assert (d_slicer->isCoreTerm(var)); + + Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")"; Assert (isComplete()); TNode repr = d_equalityEngine.getRepresentative(var); - Node result = Node(); + Node result = Node(); if (repr.getKind() == kind::CONST_BITVECTOR) { - result = repr; + result = repr; } else if (d_modelValues.find(repr) == d_modelValues.end()) { // it may be a shared term that never gets asserted // result is just Null Assert(d_bv->isSharedTerm(var)); } else { - result = d_modelValues[repr]; + result = d_modelValues[repr]; } - Debug("bitvector-model") << " => " << result <<"\n"; - return result; + Debug("bitvector-model") << " => " << result <<"\n"; + return result; } CoreSolver::Statistics::Statistics() diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 423408a7c..b886bbdd5 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -25,21 +25,21 @@ namespace CVC4 { namespace theory { namespace bv { -class Slicer; -class Base; +class Slicer; +class Base; /** * Bitvector equality solver */ class CoreSolver : public SubtheorySolver { typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; struct Statistics { IntStat d_numCallstoCheck; Statistics(); - ~Statistics(); - }; - + ~Statistics(); + }; + // NotifyClass: handles call-back from congruence closure module class NotifyClass : public eq::EqualityEngineNotify { CoreSolver& d_solver; @@ -59,13 +59,13 @@ class CoreSolver : public SubtheorySolver { /** The notify class for d_equalityEngine */ NotifyClass d_notify; - + /** Equality engine */ eq::EqualityEngine d_equalityEngine; /** Store a propagation to the bv solver */ bool storePropagation(TNode literal); - + /** Store a conflict from merging two constants */ void conflict(TNode a, TNode b); @@ -74,12 +74,12 @@ class CoreSolver : public SubtheorySolver { /** To make sure we keep the explanations */ context::CDHashSet<Node, NodeHashFunction> d_reasons; ModelValue d_modelValues; - void buildModel(); - bool assertFactToEqualityEngine(TNode fact, TNode reason); + void buildModel(); + bool assertFactToEqualityEngine(TNode fact, TNode reason); bool decomposeFact(TNode fact); Node getBaseDecomposition(TNode a); - Statistics d_statistics; -public: + Statistics d_statistics; +public: CoreSolver(context::Context* c, TheoryBV* bv); ~CoreSolver(); bool isComplete() { return d_isCoreTheory; } @@ -87,8 +87,8 @@ public: void preRegister(TNode node); bool check(Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); - void collectModelInfo(TheoryModel* m); - Node getModelValue(TNode var); + void collectModelInfo(TheoryModel* m, bool fullModel); + Node getModelValue(TNode var); void addSharedTerm(TNode t) { d_equalityEngine.addTriggerTerm(t, THEORY_BV); } diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index f45250f5b..a3970c9e3 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -29,17 +29,17 @@ using namespace CVC4::theory::bv::utils; bool InequalitySolver::check(Theory::Effort e) { Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n"; ++(d_statistics.d_numCallstoCheck); - - bool ok = true; + + bool ok = true; while (!done() && ok) { TNode fact = get(); - Debug("bv-subtheory-inequality") << " "<< fact <<"\n"; + Debug("bv-subtheory-inequality") << " "<< fact <<"\n"; if (fact.getKind() == kind::EQUAL) { TNode a = fact[0]; TNode b = fact[1]; ok = d_inequalityGraph.addInequality(a, b, false, fact); if (ok) - ok = d_inequalityGraph.addInequality(b, a, false, fact); + ok = d_inequalityGraph.addInequality(b, a, false, fact); } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) { TNode a = fact[0][0]; TNode b = fact[0][1]; @@ -47,40 +47,40 @@ bool InequalitySolver::check(Theory::Effort e) { } if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) { TNode a = fact[0][1]; - TNode b = fact[0][0]; + TNode b = fact[0][0]; ok = d_inequalityGraph.addInequality(a, b, true, fact); // propagate // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) { - // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); + // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); // d_bv->storePropagation(neq, SUB_INEQUALITY); // d_explanations[neq] = fact; // } } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) { TNode a = fact[0][1]; - TNode b = fact[0][0]; + TNode b = fact[0][0]; ok = d_inequalityGraph.addInequality(a, b, false, fact); } else if (fact.getKind() == kind::BITVECTOR_ULT) { TNode a = fact[0]; - TNode b = fact[1]; + TNode b = fact[1]; ok = d_inequalityGraph.addInequality(a, b, true, fact); // propagate // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) { - // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); + // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); // d_bv->storePropagation(neq, SUB_INEQUALITY); // d_explanations[neq] = fact; // } } else if (fact.getKind() == kind::BITVECTOR_ULE) { TNode a = fact[0]; - TNode b = fact[1]; + TNode b = fact[1]; ok = d_inequalityGraph.addInequality(a, b, false, fact); } } - + if (!ok) { std::vector<TNode> conflict; - d_inequalityGraph.getConflict(conflict); + d_inequalityGraph.getConflict(conflict); d_bv->setConflict(utils::flattenAnd(conflict)); - return false; + return false; } if (isComplete() && Theory::fullEffort(e)) { @@ -89,36 +89,39 @@ bool InequalitySolver::check(Theory::Effort e) { std::vector<Node> lemmas; d_inequalityGraph.checkDisequalities(lemmas); for(unsigned i = 0; i < lemmas.size(); ++i) { - d_bv->lemma(lemmas[i]); + d_bv->lemma(lemmas[i]); } } - return true; + return true; } EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) { + if (!isComplete()) + return EQUALITY_UNKNOWN; + Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b); Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a); // if an inequality containing the terms has been asserted then we know // the equality is false if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a)) { - return EQUALITY_FALSE; + return EQUALITY_FALSE; } - + if (!d_inequalityGraph.hasValueInModel(a) || !d_inequalityGraph.hasValueInModel(b)) { - return EQUALITY_UNKNOWN; + return EQUALITY_UNKNOWN; } // TODO: check if this disequality is entailed by inequalities via transitivity - + BitVector a_val = d_inequalityGraph.getValueInModel(a); BitVector b_val = d_inequalityGraph.getValueInModel(b); - + if (a_val == b_val) { - return EQUALITY_TRUE_IN_MODEL; + return EQUALITY_TRUE_IN_MODEL; } else { - return EQUALITY_FALSE_IN_MODEL; + return EQUALITY_FALSE_IN_MODEL; } } @@ -126,19 +129,19 @@ void InequalitySolver::assertFact(TNode fact) { d_assertionQueue.push_back(fact); d_assertionSet.insert(fact); if (!isInequalityOnly(fact)) { - d_isComplete = false; + d_isComplete = false; } } bool InequalitySolver::isInequalityOnly(TNode node) { if (d_ineqTermCache.find(node) != d_ineqTermCache.end()) { - return d_ineqTermCache[node]; + return d_ineqTermCache[node]; } - + if (node.getKind() == kind::NOT) { - node = node[0]; + node = node[0]; } - + if (node.getKind() != kind::EQUAL && node.getKind() != kind::BITVECTOR_ULT && node.getKind() != kind::BITVECTOR_ULE && @@ -146,50 +149,50 @@ bool InequalitySolver::isInequalityOnly(TNode node) { node.getKind() != kind::SELECT && node.getKind() != kind::STORE && node.getMetaKind() != kind::metakind::VARIABLE) { - return false; + return false; } - bool res = true; + bool res = true; for (unsigned i = 0; i < node.getNumChildren(); ++i) { res = res && isInequalityOnly(node[i]); } - d_ineqTermCache[node] = res; - return res; + d_ineqTermCache[node] = res; + return res; } void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) { Assert (d_explanations.find(literal) != d_explanations.end()); TNode explanation = d_explanations[literal]; assumptions.push_back(explanation); - Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n"; + Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n"; } void InequalitySolver::propagate(Theory::Effort e) { - Assert (false); + Assert (false); } -void InequalitySolver::collectModelInfo(TheoryModel* m) { - Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n"; +void InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel) { + Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n"; std::vector<Node> model; d_inequalityGraph.getAllValuesInModel(model); for (unsigned i = 0; i < model.size(); ++i) { - Assert (model[i].getKind() == kind::EQUAL); - m->assertEquality(model[i][0], model[i][1], true); + Assert (model[i].getKind() == kind::EQUAL); + m->assertEquality(model[i][0], model[i][1], true); } } Node InequalitySolver::getModelValue(TNode var) { - Assert (isInequalityOnly(var)); - Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")"; + Assert (isInequalityOnly(var)); + Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")"; Assert (isComplete()); - Node result = Node(); + Node result = Node(); if (!d_inequalityGraph.hasValueInModel(var)) { Assert (d_bv->isSharedTerm(var)); } else { BitVector val = d_inequalityGraph.getValueInModel(var); result = utils::mkConst(val); } - Debug("bitvector-model") << " => " << result <<"\n"; - return result; + Debug("bitvector-model") << " => " << result <<"\n"; + return result; } InequalitySolver::Statistics::Statistics() diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 390a329ff..6e0139e09 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -9,7 +9,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Algebraic solver. + ** \brief Algebraic solver. ** ** Algebraic solver. **/ @@ -31,16 +31,16 @@ class InequalitySolver: public SubtheorySolver { struct Statistics { IntStat d_numCallstoCheck; Statistics(); - ~Statistics(); - }; + ~Statistics(); + }; - context::CDHashSet<Node, NodeHashFunction> d_assertionSet; + context::CDHashSet<Node, NodeHashFunction> d_assertionSet; InequalityGraph d_inequalityGraph; - context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; + context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; context::CDO<bool> d_isComplete; - __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache; - bool isInequalityOnly(TNode node); - Statistics d_statistics; + __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache; + bool isInequalityOnly(TNode node); + Statistics d_statistics; public: InequalitySolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), @@ -51,19 +51,19 @@ public: d_ineqTermCache(), d_statistics() {} - + bool check(Theory::Effort e); - void propagate(Theory::Effort e); + void propagate(Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); bool isComplete() { return d_isComplete; } - void collectModelInfo(TheoryModel* m); - Node getModelValue(TNode var); + void collectModelInfo(TheoryModel* m, bool fullModel); + Node getModelValue(TNode var); EqualityStatus getEqualityStatus(TNode a, TNode b); - void assertFact(TNode fact); -}; + void assertFact(TNode fact); +}; } } } -#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ +#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 052e477ea..aeae1073e 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -120,6 +120,14 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign- parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left" parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right" +constant INT_TO_BITVECTOR_OP \ + ::CVC4::IntToBitVector \ + "::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \ + "util/bitvector.h" \ + "operator for the integer conversion to bit-vector" +parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector" +operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer" + typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule @@ -166,4 +174,7 @@ typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule +typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule +typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule + endtheory diff --git a/src/theory/bv/options b/src/theory/bv/options index 7b87baa21..077299d1f 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -22,5 +22,11 @@ option bitvectorCoreSolver --bv-core-solver bool option bvToBool --bv-to-bool bool lift bit-vectors of size 1 to booleans when possible + +option bvPropagate --bv-propagate bool :default true + use bit-vector propagation in the bit-blaster + +option bvEquality --bv-eq bool :default true + use the equality engine for the bit-vector theory endmodule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index cb68a0f65..a2de951aa 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -49,29 +49,32 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_literalsToPropagateIndex(c, 0), d_propagatedBy(c) { - SubtheorySolver* core_solver = new CoreSolver(c, this); - d_subtheories.push_back(core_solver); - d_subtheoryMap[SUB_CORE] = core_solver; - + if (options::bvEquality()) { + SubtheorySolver* core_solver = new CoreSolver(c, this); + d_subtheories.push_back(core_solver); + d_subtheoryMap[SUB_CORE] = core_solver; + } if (options::bitvectorInequalitySolver()) { - SubtheorySolver* ineq_solver = new InequalitySolver(c, this); + SubtheorySolver* ineq_solver = new InequalitySolver(c, this); d_subtheories.push_back(ineq_solver); d_subtheoryMap[SUB_INEQUALITY] = ineq_solver; } - - SubtheorySolver* bb_solver = new BitblastSolver(c, this); + + SubtheorySolver* bb_solver = new BitblastSolver(c, this); d_subtheories.push_back(bb_solver); d_subtheoryMap[SUB_BITBLAST] = bb_solver; } TheoryBV::~TheoryBV() { for (unsigned i = 0; i < d_subtheories.size(); ++i) { - delete d_subtheories[i]; + delete d_subtheories[i]; } } void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { - dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq); + if (options::bvEquality()) { + dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq); + } } TheoryBV::Statistics::Statistics(): @@ -110,7 +113,7 @@ void TheoryBV::preRegisterTerm(TNode node) { return; } for (unsigned i = 0; i < d_subtheories.size(); ++i) { - d_subtheories[i]->preRegister(node); + d_subtheories[i]->preRegister(node); } } @@ -131,22 +134,22 @@ void TheoryBV::checkForLemma(TNode fact) { if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) { TNode urem = fact[0]; TNode result = fact[1]; - TNode divisor = urem[1]; + TNode divisor = urem[1]; Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); Node divisor_eq_0 = mkNode(kind::EQUAL, divisor, - mkConst(BitVector(getSize(divisor), 0u))); + mkConst(BitVector(getSize(divisor), 0u))); Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); lemma(split); } if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) { TNode urem = fact[1]; TNode result = fact[0]; - TNode divisor = urem[1]; + TNode divisor = urem[1]; Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); Node divisor_eq_0 = mkNode(kind::EQUAL, divisor, - mkConst(BitVector(getSize(divisor), 0u))); + mkConst(BitVector(getSize(divisor), 0u))); Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); lemma(split); } @@ -162,9 +165,9 @@ void TheoryBV::check(Effort e) } if (Theory::fullEffort(e)) { - ++(d_statistics.d_numCallsToCheckFullEffort); + ++(d_statistics.d_numCallsToCheckFullEffort); } else { - ++(d_statistics.d_numCallsToCheckStandardEffort); + ++(d_statistics.d_numCallsToCheckStandardEffort); } // if we are already in conflict just return the conflict if (inConflict()) { @@ -174,28 +177,29 @@ void TheoryBV::check(Effort e) while (!done()) { TNode fact = get().assertion; - checkForLemma(fact); + checkForLemma(fact); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { - d_subtheories[i]->assertFact(fact); + d_subtheories[i]->assertFact(fact); } } bool ok = true; bool complete = false; for (unsigned i = 0; i < d_subtheories.size(); ++i) { - Assert (!inConflict()); + Assert (!inConflict()); ok = d_subtheories[i]->check(e); - complete = d_subtheories[i]->isComplete(); + complete = d_subtheories[i]->isComplete(); if (!ok) { // if we are in a conflict no need to check with other theories Assert (inConflict()); sendConflict(); - return; + return; } if (complete) { // if the last subtheory was complete we stop - return; + return; } } } @@ -205,8 +209,8 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ // Assert (fullModel); // can only query full model for (unsigned i = 0; i < d_subtheories.size(); ++i) { if (d_subtheories[i]->isComplete()) { - d_subtheories[i]->collectModelInfo(m); - return; + d_subtheories[i]->collectModelInfo(m, fullModel); + return; } } } @@ -215,10 +219,10 @@ Node TheoryBV::getModelValue(TNode var) { Assert(!inConflict()); for (unsigned i = 0; i < d_subtheories.size(); ++i) { if (d_subtheories[i]->isComplete()) { - return d_subtheories[i]->getModelValue(var); + return d_subtheories[i]->getModelValue(var); } } - Unreachable(); + Unreachable(); } void TheoryBV::propagate(Effort e) { @@ -236,7 +240,7 @@ void TheoryBV::propagate(Effort e) { bool ok = true; for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - // temporary fix for incremental bit-blasting + // temporary fix for incremental bit-blasting if (d_valuation.isSatLiteral(literal)) { Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n"; ok = d_out->propagate(literal); @@ -286,14 +290,14 @@ Node TheoryBV::ppRewrite(TNode t) if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { std::vector<Node> equalities; Slicer::splitEqualities(t, equalities); - return utils::mkAnd(equalities); + return utils::mkAnd(equalities); } - + return t; } void TheoryBV::presolve() { - Debug("bitvector") << "TheoryBV::presolve" << endl; + Debug("bitvector") << "TheoryBV::presolve" << endl; } bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) @@ -318,7 +322,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) // Safe to ignore this one, subtheory should produce a conflict return true; } - + d_propagatedBy[literal] = subtheory; } @@ -366,7 +370,7 @@ Node TheoryBV::explain(TNode node) { void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); - if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) { + if (!options::bitvectorEagerBitblast() && options::bvEquality()) { for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->addSharedTerm(t); } @@ -379,11 +383,11 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) if (options::bitvectorEagerBitblast()) { return EQUALITY_UNKNOWN; } - + for (unsigned i = 0; i < d_subtheories.size(); ++i) { EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); if (status != EQUALITY_UNKNOWN) { - return status; + return status; } } return EQUALITY_UNKNOWN; ; diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index baaf7e133..8426afb59 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -66,6 +66,9 @@ enum RewriteRuleId { SremEliminate, ZeroExtendEliminate, SignExtendEliminate, + BVToNatEliminate, + IntToBVEliminate, + /// ground term evaluation EvalEquals, EvalConcat, @@ -173,13 +176,15 @@ 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 UgtEliminate: out << "UgtEliminate"; return out; - case SgtEliminate: out << "SgtEliminate"; return out; - case UgeEliminate: out << "UgeEliminate"; return out; - case SgeEliminate: out << "SgeEliminate"; 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 BVToNatEliminate: out << "BVToNatEliminate"; return out; + case IntToBVEliminate: out << "IntToBVEliminate"; return out; case NandEliminate: out << "NandEliminate"; return out; case NorEliminate : out << "NorEliminate"; return out; case SdivEliminate : out << "SdivEliminate"; return out; @@ -214,7 +219,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { 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 ExtractArith2 : out << "ExtractArith2"; return out; case DoubleNeg : out << "DoubleNeg"; return out; case NotConcat : out << "NotConcat"; return out; case NotAnd : out << "NotAnd"; return out; @@ -226,7 +231,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { 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 LteSelf : out << "LteSelf"; return out; case UltZero : out << "UltZero"; return out; case UleZero : out << "UleZero"; return out; case ZeroUle : out << "ZeroUle"; return out; @@ -491,7 +496,8 @@ struct AllRewriteRules { RewriteRule<BitwiseEq> rule113; RewriteRule<UltOne> rule114; RewriteRule<SltZero> rule115; - + RewriteRule<BVToNatEliminate> rule116; + RewriteRule<IntToBVEliminate> rule117; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index a5368d2c9..9f3d12415 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -198,8 +198,9 @@ Node RewriteRule<EvalNeg>::apply(TNode node) { } template<> inline bool RewriteRule<EvalUdiv>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && - utils::isBVGroundTerm(node)); + return (utils::isBVGroundTerm(node) && + (node.getKind() == kind::BITVECTOR_UDIV_TOTAL || + (node.getKind() == kind::BITVECTOR_UDIV && node[1].isConst()))); } template<> inline @@ -213,8 +214,9 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) { } template<> inline bool RewriteRule<EvalUrem>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && - utils::isBVGroundTerm(node)); + return (utils::isBVGroundTerm(node) && + (node.getKind() == kind::BITVECTOR_UREM_TOTAL || + (node.getKind() == kind::BITVECTOR_UREM && node[1].isConst()))); } template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index cf36633fa..b513dbf90 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -231,6 +231,57 @@ Node RewriteRule<RotateRightEliminate>::apply(TNode node) { } template<> +bool RewriteRule<BVToNatEliminate>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_TO_NAT); +} + +template<> +Node RewriteRule<BVToNatEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<BVToNatEliminate>(" << node << ")" << std::endl; + + const unsigned size = utils::getSize(node[0]); + NodeManager* const nm = NodeManager::currentNM(); + const Node z = nm->mkConst(Rational(0)); + const Node bvone = nm->mkConst(BitVector(1u, 1u)); + + NodeBuilder<> result(kind::PLUS); + Integer i = 1; + for(unsigned bit = 0; bit < size; ++bit, i *= 2) { + Node cond = nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]), bvone); + result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z); + } + + return Node(result); +} + +template<> +bool RewriteRule<IntToBVEliminate>::applies(TNode node) { + return (node.getKind() == kind::INT_TO_BITVECTOR); +} + +template<> +Node RewriteRule<IntToBVEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<IntToBVEliminate>(" << node << ")" << std::endl; + + const unsigned size = node.getOperator().getConst<IntToBitVector>().size; + NodeManager* const nm = NodeManager::currentNM(); + const Node bvzero = nm->mkConst(BitVector(1u, 0u)); + const Node bvone = nm->mkConst(BitVector(1u, 1u)); + + std::vector<Node> v; + Integer i = 2; + while(v.size() < size) { + Node cond = nm->mkNode(kind::GEQ, nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))), nm->mkConst(Rational(i, 2))); + v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero)); + i *= 2; + } + + NodeBuilder<> result(kind::BITVECTOR_CONCAT); + result.append(v.rbegin(), v.rend()); + return Node(result); +} + +template<> bool RewriteRule<NandEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_NAND && node.getNumChildren() == 2); diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index d660dde29..ff7d67cb0 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -45,7 +45,9 @@ template<> inline Node RewriteRule<ShlByConst>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl; Integer amount = node[1].getConst<BitVector>().toInteger(); - + if (amount == 0) { + return node[0]; + } Node a = node[0]; uint32_t size = utils::getSize(a); @@ -59,6 +61,7 @@ Node RewriteRule<ShlByConst>::apply(TNode node) { 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); @@ -81,6 +84,9 @@ template<> inline Node RewriteRule<LshrByConst>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl; Integer amount = node[1].getConst<BitVector>().toInteger(); + if (amount == 0) { + return node[0]; + } Node a = node[0]; uint32_t size = utils::getSize(a); @@ -117,7 +123,10 @@ template<> inline Node RewriteRule<AshrByConst>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl; Integer amount = node[1].getConst<BitVector>().toInteger(); - + if (amount == 0) { + return node[0]; + } + Node a = node[0]; uint32_t size = utils::getSize(a); Node sign_bit = utils::mkExtract(a, size-1, size-1); @@ -812,7 +821,9 @@ Node RewriteRule<UdivPow2>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl; Node a = node[0]; unsigned power = utils::isPow2Const(node[1]) -1; - + if (power == 0) { + return a; + } Node extract = utils::mkExtract(a, utils::getSize(node) - 1, power); Node zeros = utils::mkConst(power, 0); diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 7844e5b92..2467ae3f1 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -70,7 +70,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { return res; } -RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool prerewrite) { // reduce common subexpressions on both sides Node resultNode = LinearRewriteStrategy < RewriteRule<EvalUlt>, @@ -82,7 +82,7 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule < EvalSlt > >::apply(node); @@ -97,7 +97,7 @@ RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){ // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<EvalUle>, RewriteRule<UleMax>, @@ -109,7 +109,7 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule <EvalSle>, RewriteRule <SleEliminate> @@ -117,7 +117,7 @@ RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<UgtEliminate> >::apply(node); @@ -125,7 +125,7 @@ RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){ return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<SgtEliminate> //RewriteRule<SltEliminate> @@ -134,7 +134,7 @@ RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool preregister){ return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<UgeEliminate> >::apply(node); @@ -142,7 +142,7 @@ RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool preregister){ return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<SgeEliminate> // RewriteRule<SleEliminate> @@ -151,7 +151,7 @@ RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool preregister){ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){ Node resultNode = node; if(RewriteRule<NotXor>::applies(node)) { @@ -166,7 +166,7 @@ RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool preregister){ return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) { Node resultNode = node; if (RewriteRule<ExtractConcat>::applies(node)) { @@ -206,7 +206,7 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) { } -RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<ConcatFlatten>, @@ -220,63 +220,70 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) { Node resultNode = node; - resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, - RewriteRule<AndSimplify>, - RewriteRule<BitwiseSlicing> + RewriteRule<AndSimplify> >::apply(node); - if (resultNode.getKind() != node.getKind()) { - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + if (!prerewrite) { + resultNode = LinearRewriteStrategy + < RewriteRule<BitwiseSlicing> + >::apply(resultNode); + + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } } return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){ Node resultNode = node; - resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, - RewriteRule<OrSimplify>, - RewriteRule<BitwiseSlicing> - >::apply(node); + RewriteRule<OrSimplify> + >::apply(node); - if (resultNode.getKind() != node.getKind()) { - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + if (!prerewrite) { + resultNode = LinearRewriteStrategy + < RewriteRule<BitwiseSlicing> + >::apply(resultNode); + + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } } return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) { Node resultNode = node; - resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, // flatten the expression RewriteRule<XorSimplify>, // simplify duplicates and constants RewriteRule<XorZero>, // checks if the constant part is zero and eliminates it RewriteRule<BitwiseSlicing> - >::apply(node); - - // this simplification introduces new terms and might require further - // rewriting - if (RewriteRule<XorOne>::applies(resultNode)) { - resultNode = RewriteRule<XorOne>::run<false> (resultNode); - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); - } + >::apply(node); - if (resultNode.getKind() != node.getKind()) { - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + if (!prerewrite) { + resultNode = LinearRewriteStrategy + < RewriteRule<XorOne>, + RewriteRule <BitwiseSlicing> + >::apply(resultNode); + + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } } return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<XnorEliminate> >::apply(node); @@ -284,7 +291,7 @@ RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<NandEliminate> >::apply(node); @@ -292,7 +299,7 @@ RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<NorEliminate> >::apply(node); @@ -300,7 +307,7 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<CompEliminate> >::apply(node); @@ -308,7 +315,7 @@ RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) { Node resultNode = node; resultNode = LinearRewriteStrategy @@ -318,7 +325,7 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { >::apply(node); // only apply if every subterm was already rewritten - if (!preregister) { + if (!prerewrite) { // distributes multiplication by constant over +, - and unary - if(RewriteRule<MultDistribConst>::applies(resultNode)) { resultNode = RewriteRule<MultDistribConst>::run<false>(resultNode); @@ -333,23 +340,28 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) { - if (preregister) { - return RewriteResponse(REWRITE_DONE, node); +RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) { + Node resultNode = node; + if (prerewrite) { + resultNode = LinearRewriteStrategy + < RewriteRule<FlattenAssocCommut> + >::apply(node); + return RewriteResponse(REWRITE_DONE, resultNode); } - Node resultNode = LinearRewriteStrategy - < RewriteRule<FlattenAssocCommut>, + + resultNode = LinearRewriteStrategy + < RewriteRule<FlattenAssocCommut>, RewriteRule<PlusCombineLikeTerms> - // RewriteRule<PlusLiftConcat> >::apply(node); - if (resultNode == node) { - return RewriteResponse(REWRITE_DONE, resultNode); - } else { - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + + if (node != resultNode) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + + return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){ // return RewriteResponse(REWRITE_DONE, node); Node resultNode = LinearRewriteStrategy < RewriteRule<SubEliminate> @@ -358,7 +370,7 @@ RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool preregister){ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) { Node resultNode = node; resultNode = LinearRewriteStrategy @@ -372,7 +384,7 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } - if(!preregister) { + if(!prerewrite) { if (RewriteRule<NegMult>::applies(node)) { resultNode = RewriteRule<NegMult>::run<false>(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -382,8 +394,27 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } +RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool prerewrite){ + Node resultNode = node; + + if(node[1].isConst() && node[1].getConst<BitVector>().getValue() != 0) { + return RewriteUdivTotal(node, prerewrite); + } -RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister){ + return RewriteResponse(REWRITE_DONE, resultNode); +} + +RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite){ + Node resultNode = node; + + if(node[1].isConst() && node[1].getConst<BitVector>().getValue() != 0) { + return RewriteUremTotal(node, prerewrite); + } + + return RewriteResponse(REWRITE_DONE, resultNode); +} + +RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){ Node resultNode = node; if(RewriteRule<UdivPow2>::applies(node)) { @@ -400,7 +431,7 @@ RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister) return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite) { Node resultNode = node; if(RewriteRule<UremPow2>::applies(node)) { @@ -416,7 +447,7 @@ RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister) return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<SmodEliminate> >::apply(node); @@ -424,7 +455,7 @@ RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<SdivEliminate> >::apply(node); @@ -432,14 +463,14 @@ RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<SremEliminate> >::apply(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool prerewrite) { Node resultNode = node; if(RewriteRule<ShlByConst>::applies(node)) { resultNode = RewriteRule<ShlByConst>::run <false> (node); @@ -454,7 +485,7 @@ RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool prerewrite) { Node resultNode = node; if(RewriteRule<LshrByConst>::applies(node)) { resultNode = RewriteRule<LshrByConst>::run <false> (node); @@ -469,7 +500,7 @@ RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool prerewrite) { Node resultNode = node; if(RewriteRule<AshrByConst>::applies(node)) { resultNode = RewriteRule<AshrByConst>::run <false> (node); @@ -485,7 +516,7 @@ RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool preregister) { } -RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<RepeatEliminate > >::apply(node); @@ -493,7 +524,7 @@ RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<ZeroExtendEliminate > >::apply(node); @@ -501,7 +532,7 @@ RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool preregister return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<EvalSignExtend> >::apply(node); @@ -511,7 +542,7 @@ RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool preregister } -RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<RotateRightEliminate > >::apply(node); @@ -519,16 +550,32 @@ RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool preregiste return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<RotateLeftEliminate > - >::apply(node); + >::apply(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) { - if (preregister) { +RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { + Node resultNode = LinearRewriteStrategy + < RewriteRule<BVToNatEliminate> + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + +RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) { + Node resultNode = LinearRewriteStrategy + < RewriteRule<IntToBVEliminate> + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + +RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) { + if (prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<FailEq>, RewriteRule<SimplifyEq>, @@ -593,8 +640,8 @@ void TheoryBVRewriter::initializeRewrites() { 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_UDIV ] = RewriteUdiv; + d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem; d_rewriteTable [ kind::BITVECTOR_UDIV_TOTAL ] = RewriteUdivTotal; d_rewriteTable [ kind::BITVECTOR_UREM_TOTAL ] = RewriteUremTotal; d_rewriteTable [ kind::BITVECTOR_SMOD ] = RewriteSmod; @@ -609,6 +656,9 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend; d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight; d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft; + + d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat; + d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV; } Node TheoryBVRewriter::eliminateBVSDiv(TNode node) { diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 183b5e8d5..def8e24fe 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -78,6 +78,9 @@ class TheoryBVRewriter { static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false); static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false); + static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false); + static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false); + public: static RewriteResponse postRewrite(TNode node); diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 00284e7ae..67dae0cfa 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -29,6 +29,11 @@ class BitVectorConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { + if (check) { + if (n.getConst<BitVector>().getSize() == 0) { + throw TypeCheckingExceptionPrivate(n, "constant of size 0"); + } + } return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize()); } }; @@ -190,6 +195,29 @@ public: } }; +class BitVectorConversionTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if(n.getKind() == kind::BITVECTOR_TO_NAT) { + if(check && !n[0].getType(check).isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + return nodeManager->integerType(); + } + + if(n.getKind() == kind::INT_TO_BITVECTOR) { + size_t bvSize = n.getOperator().getConst<IntToBitVector>(); + if(check && !n[0].getType(check).isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting integer term"); + } + return nodeManager->mkBitVectorType(bvSize); + } + + InternalError("bv-conversion typerule invoked for non-bv-conversion kind"); + } +}; + class CardinalityComputer { public: inline static Cardinality computeCardinality(TypeNode type) { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 5847bac3e..ab6a615a2 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -357,7 +357,7 @@ inline Node flattenAnd(std::vector<TNode>& queue) { } -// neeed a better name, this is not technically a ground term +// need a better name, this is not technically a ground term inline bool isBVGroundTerm(TNode node) { if (node.getNumChildren() == 0) { return node.isConst(); |