From: Andrew Reynolds Date: Mon, 22 Jul 2013 19:29:28 +0000 (-0500) Subject: Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastructure... X-Git-Tag: cvc5-1.0.0~7287^2~53 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bdb5789713c03cf16f0ce6178b2fdc66f96ddc9e;p=cvc5.git Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastructure to BV collectModelInfo in preparation for bug fix. --- diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 7960b0320..47aac4370 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() ? "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,35 +64,35 @@ 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 normalized = Rewriter::rewrite(node); @@ -126,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) { @@ -142,21 +142,21 @@ Node Bitblaster::bbOptimize(TNode node) { if (node.getKind() == kind::BITVECTOR_PLUS) { if (RewriteRule::applies(node)) { Node res = RewriteRule::run(node); - return res; + return res; } // if (RewriteRule::applies(node)) { // Node res = RewriteRule::run(node); - // return res; - // } + // return res; + // } } else if (node.getKind() == kind::BITVECTOR_MULT) { if (RewriteRule::applies(node)) { Node res = RewriteRule::run(node); - return res; + return res; } } - - return node; + + return node; } /// Public methods @@ -173,31 +173,31 @@ void Bitblaster::explain(TNode atom, std::vector& explanation) { std::vector 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); @@ -205,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); @@ -217,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 "; @@ -232,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& 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); } } @@ -259,9 +259,9 @@ void Bitblaster::getConflict(std::vector& 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; @@ -272,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() { @@ -281,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; @@ -298,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; @@ -316,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; } @@ -340,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); @@ -377,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) { @@ -420,70 +420,75 @@ 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 + * + * @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::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..83efc05b0 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -55,14 +55,14 @@ namespace bv { typedef std::vector 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 TermDefMap; typedef __gnu_cxx::hash_set AtomSet; - typedef __gnu_cxx::hash_set VarSet; - - typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*); - typedef Node (*AtomBBStrategy) (TNode, Bitblaster*); + typedef __gnu_cxx::hash_set 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 d_assertedAtoms; /**< context dependent list storing the atoms currently asserted by the DPLL SAT solver. */ @@ -111,79 +111,79 @@ 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& conflict); + void getConflict(std::vector& conflict); void explain(TNode atom, std::vector& 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 */ - 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 + * @param bits */ 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 1c6920236..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,10 +55,10 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { } -// forward declaration -class TheoryBV; +// forward declaration +class TheoryBV; -typedef context::CDQueue AssertionQueue; +typedef context::CDQueue AssertionQueue; /** * Abstract base class for bit-vector subtheory solvers * @@ -75,7 +75,7 @@ protected: AssertionQueue d_assertionQueue; context::CDO d_assertionIndex; public: - + SubtheorySolver(context::Context* c, TheoryBV* bv) : d_context(c), d_bv(bv), @@ -83,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& 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 244d87233..5a0c17134 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -84,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); @@ -144,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) @@ -189,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 315254c8e..71e80238d 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -33,21 +33,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 d_bitblastQueue; - Statistics d_statistics; + Statistics d_statistics; typedef std::hash_map NodeMap; NodeMap d_modelCache; context::CDO d_validModelCache; Node getModelValueRec(TNode node); - bool d_useSatPropagation; + bool d_useSatPropagation; public: BitblastSolver(context::Context* c, TheoryBV* bv); ~BitblastSolver(); @@ -56,7 +56,7 @@ public: bool check(Theory::Effort e); void explain(TNode literal, std::vector& 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 f7209d326..45946b8c8 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -72,7 +72,7 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv) } CoreSolver::~CoreSolver() { - delete d_slicer; + delete d_slicer; } void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); @@ -104,51 +104,51 @@ Node CoreSolver::getBaseDecomposition(TNode a) { std::vector 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); @@ -156,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 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()) { @@ -181,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) { @@ -213,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. @@ -254,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 equalities; + std::vector equalities; for (unsigned i = 0; i < representatives.size(); ++i) { for (unsigned j = i + 1; j < representatives.size(); ++j) { TNode a = representatives[i]; @@ -274,18 +274,18 @@ 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 + // 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; @@ -310,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) { @@ -356,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::const_iterator it = d_assertionQueue.begin(); @@ -372,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); } } } @@ -385,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 ModelValue; - typedef __gnu_cxx::hash_set TNodeSet; + typedef __gnu_cxx::hash_set 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 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& 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 6c95bd308..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 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,39 +89,39 @@ bool InequalitySolver::check(Theory::Effort e) { std::vector 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; } } @@ -129,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 && @@ -149,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& 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 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 d_assertionSet; + context::CDHashSet d_assertionSet; InequalityGraph d_inequalityGraph; - context::CDHashMap d_explanations; + context::CDHashMap d_explanations; context::CDO d_isComplete; - __gnu_cxx::hash_map d_ineqTermCache; - bool isInequalityOnly(TNode node); - Statistics d_statistics; + __gnu_cxx::hash_map 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& 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/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 38d3a2f5e..d7a7f358a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -50,24 +50,24 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_propagatedBy(c) { if (options::bvEquality()) { - SubtheorySolver* core_solver = new CoreSolver(c, this); + 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]; } } @@ -113,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); } } @@ -134,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); } @@ -165,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()) { @@ -177,28 +177,28 @@ 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; } } } @@ -208,8 +208,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; } } } @@ -218,10 +218,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) { @@ -239,7 +239,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); @@ -289,14 +289,14 @@ Node TheoryBV::ppRewrite(TNode t) if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { std::vector 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) @@ -321,7 +321,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) // Safe to ignore this one, subtheory should produce a conflict return true; } - + d_propagatedBy[literal] = subtheory; } @@ -382,11 +382,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/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 42d5bbd3a..4c168acfc 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -193,6 +193,7 @@ bool EntryTrie::isComplete(FirstOrderModelFmc * m, Node c, int index) { bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) { if (d_et.hasGeneralization(m, c)) { + Trace("fmc-debug") << "Already has generalization, skip." << std::endl; return false; } int newIndex = (int)d_cond.size(); @@ -382,18 +383,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Node op = it->first; TypeNode tno = op.getType(); for( unsigned i=0; id_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){ - Node mbn; - if (!fm->d_rep_set.hasType(tn)) { - mbn = fm->getSomeDomainElement(tn); - }else{ - mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); - } - Node mbnr = fm->getUsedRepresentative( mbn ); - fm->d_model_basis_rep[tn] = mbnr; - Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl; - } + initializeType( fm, tno[i] ); } } //now, make models @@ -561,6 +551,21 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } } +void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){ + if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){ + Trace("fmc") << "Initialize type " << tn << std::endl; + Node mbn; + if (!fm->d_rep_set.hasType(tn)) { + mbn = fm->getSomeDomainElement(tn); + }else{ + mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); + } + Node mbnr = fm->getUsedRepresentative( mbn ); + fm->d_model_basis_rep[tn] = mbnr; + Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl; + } +} + void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) { Trace(tr) << "("; for( unsigned j=0; jmkSkolem( "fmc_$$", typ, "op created for full-model checking" ); d_quant_cond[f] = op; } + //make sure all types are set + for( unsigned i=0; igetUsedRepresentative( r ); } + Trace("fmc-debug") << "Add constant entry..." << std::endl; d.addEntry(fm, mkCondDefault(fm, f), r); } else{ @@ -906,6 +917,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n } } Trace("fmc-debug") << "Simplify the definition..." << std::endl; + d.debugPrint("fmc-debug", Node::null(), this); d.simplify(this, fm); Trace("fmc-debug") << "Done simplifying" << std::endl; } diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 8ebef640c..fb810c355 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -90,6 +90,7 @@ protected: std::map< Node, Node > d_array_term_cond; std::map > d_quant_var_id; std::map > d_star_insts; + void initializeType( FirstOrderModelFmc * fm, TypeNode tn ); Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); protected: diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 3e0f13e4b..628f8b14a 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -92,7 +92,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ NodeBuilder<> nb(kind::OR); nb << f << ceLit; Node lem = nb; - Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; + Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; d_quantEngine->getOutputChannel().lemma( lem ); addedLemma = true; } @@ -213,7 +213,9 @@ void InstantiationEngine::check( Theory::Effort e ){ d_quant_active[n] = active; if( active ){ Debug("quantifiers") << " Active : " << n; - quantActive = true; + if( !TermDb::hasInstConstAttr(n) ){ + quantActive = true; + } }else{ Debug("quantifiers") << " NOT active : " << n; if( d_quantEngine->getValuation().isDecision( cel ) ){ @@ -232,7 +234,9 @@ void InstantiationEngine::check( Theory::Effort e ){ //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine }else{ d_quant_active[n] = true; - quantActive = true; + if( !TermDb::hasInstConstAttr(n) ){ + quantActive = true; + } Debug("quantifiers") << " Active : " << n << ", no ce assigned." << std::endl; } Debug("quantifiers-relevance") << "Quantifier : " << n << std::endl; diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index c68623baa..52c9e34f3 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -163,7 +163,7 @@ void TheoryQuantifiers::assertExistential( Node n ){ NodeBuilder<> nb(kind::OR); nb << n[0] << body.notNode(); Node lem = nb; - Debug("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl; + Trace("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl; d_out->lemma( lem ); d_skolemized[n] = true; }