From 61258d16bb812c5b5c8fb8dade1d2b497c69570b Mon Sep 17 00:00:00 2001 From: lianah Date: Thu, 19 Jun 2014 18:19:25 -0400 Subject: [PATCH] added model generation to eager bit-blasting and turned abc off by default --- src/smt/smt_engine.cpp | 5 +- src/theory/bv/bitblaster_template.h | 26 ++++++---- src/theory/bv/bv_eager_solver.cpp | 10 +++- src/theory/bv/bv_eager_solver.h | 6 ++- src/theory/bv/eager_bitblaster.h | 73 +++++++++++++++++++++++++++-- src/theory/bv/lazy_bitblaster.h | 2 +- src/theory/bv/options | 4 +- src/theory/bv/options_handlers.h | 18 +------ src/theory/bv/theory_bv.cpp | 6 ++- src/theory/bv/theory_bv.h | 1 + src/theory/theory_model.cpp | 4 +- test/unit/Makefile.am | 1 + test/unit/theory/theory_bv_white.h | 3 +- 13 files changed, 120 insertions(+), 39 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f82fc86ed..ffe239e2f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3180,8 +3180,11 @@ void SmtEnginePrivate::processAssertions() { // everything gets bit-blasted to internal SAT solver if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) { - Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, d_assertionsToCheck[i]); + TNode atom = d_assertionsToCheck[i]; + Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, atom); d_assertionsToCheck[i] = eager_atom; + TheoryModel* m = d_smt.d_theoryEngine->getModel(); + m->addSubstitution(eager_atom, atom); } } diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 8971d289f..4b0465498 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -57,6 +57,8 @@ namespace bv { class BitblastingRegistrar; typedef __gnu_cxx::hash_set NodeSet; +typedef __gnu_cxx::hash_set TNodeSet; + class AbstractionModule; /** @@ -70,7 +72,7 @@ class TBitblaster { protected: typedef std::vector Bits; typedef __gnu_cxx::hash_map TermDefMap; - typedef __gnu_cxx::hash_set AtomSet; + typedef __gnu_cxx::hash_set TNodeSet; typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster*); typedef T (*AtomBBStrategy) (TNode, TBitblaster*); @@ -104,8 +106,6 @@ class TheoryBV; class TLazyBitblaster : public TBitblaster { typedef std::vector Bits; - typedef __gnu_cxx::hash_set VarSet; - typedef __gnu_cxx::hash_set AtomSet; typedef context::CDList AssertionList; typedef context::CDHashMap , prop::SatLiteralHashFunction> ExplanationMap; @@ -138,8 +138,8 @@ class TLazyBitblaster : public TBitblaster { currently asserted by the DPLL SAT solver. */ ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals. Only used when bvEagerPropagate option enabled. */ - VarSet d_variables; - AtomSet d_bbAtoms; + TNodeSet d_variables; + TNodeSet d_bbAtoms; AbstractionModule* d_abstraction; bool d_emptyNotify; @@ -188,7 +188,7 @@ public: */ void collectModelInfo(TheoryModel* m, bool fullModel); - typedef VarSet::const_iterator vars_iterator; + typedef TNodeSet::const_iterator vars_iterator; vars_iterator beginVars() { return d_variables.begin(); } vars_iterator endVars() { return d_variables.end(); } @@ -239,7 +239,14 @@ class EagerBitblaster : public TBitblaster { BitblastingRegistrar* d_bitblastingRegistrar; context::Context* d_nullContext; prop::CnfStream* d_cnfStream; - TNodeSet d_bbAtoms; + + theory::bv::TheoryBV* d_bv; + TNodeSet d_bbAtoms; + TNodeSet d_variables; + + Node getVarValue(TNode a, bool fullModel); + bool isSharedTerm(TNode node); + public: void addAtom(TNode atom); void makeVariable(TNode node, Bits& bits); @@ -249,10 +256,11 @@ public: bool hasBBAtom(TNode atom) const; void bbFormula(TNode formula); void storeBBAtom(TNode atom, Node atom_bb); - EagerBitblaster(); + EagerBitblaster(theory::bv::TheoryBV* theory_bv); ~EagerBitblaster(); bool assertToSat(TNode node, bool propagate = true); - bool solve(); + bool solve(); + void collectModelInfo(TheoryModel* m, bool fullModel); }; class AigBitblaster : public TBitblaster { diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index af35c0499..166d43e35 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -24,11 +24,12 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; -EagerBitblastSolver::EagerBitblastSolver() +EagerBitblastSolver::EagerBitblastSolver(TheoryBV* bv) : d_assertionSet() , d_bitblaster(NULL) , d_aigBitblaster(NULL) , d_useAig(options::bitvectorAig()) + , d_bv(bv) {} EagerBitblastSolver::~EagerBitblastSolver() { @@ -53,7 +54,7 @@ void EagerBitblastSolver::initialize() { if (d_useAig) { d_aigBitblaster = new AigBitblaster(); } else { - d_bitblaster = new EagerBitblaster(); + d_bitblaster = new EagerBitblaster(d_bv); } } @@ -106,3 +107,8 @@ bool EagerBitblastSolver::hasAssertions(const std::vector &formulas) { } return true; } + +void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) { + AlwaysAssert(!d_useAig && d_bitblaster); + d_bitblaster->collectModelInfo(m, fullModel); +} diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 1fb65c9c8..65fddd819 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -16,6 +16,8 @@ #include "cvc4_private.h" #include "expr/node.h" +#include "theory/theory_model.h" +#include "theory/bv/theory_bv.h" #include #pragma once @@ -37,8 +39,9 @@ class EagerBitblastSolver { EagerBitblaster* d_bitblaster; AigBitblaster* d_aigBitblaster; bool d_useAig; + TheoryBV* d_bv; public: - EagerBitblastSolver(); + EagerBitblastSolver(theory::bv::TheoryBV* bv); ~EagerBitblastSolver(); bool checkSat(); void assertFormula(TNode formula); @@ -48,6 +51,7 @@ public: void turnOffAig(); bool isInitialized(); void initialize(); + void collectModelInfo(theory::TheoryModel* m, bool fullModel); }; } diff --git a/src/theory/bv/eager_bitblaster.h b/src/theory/bv/eager_bitblaster.h index da73c7f09..91ef866bd 100644 --- a/src/theory/bv/eager_bitblaster.h +++ b/src/theory/bv/eager_bitblaster.h @@ -20,11 +20,13 @@ #define __CVC4__EAGER__BITBLASTER_H -#include "bitblaster_template.h" #include "theory/theory_registrar.h" +#include "theory/bv/bitblaster_template.h" +#include "theory/bv/options.h" +#include "theory/theory_model.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" -#include "theory/bv/options.h" + namespace CVC4 { namespace theory { @@ -43,9 +45,11 @@ public: };/* class Registrar */ -EagerBitblaster::EagerBitblaster() +EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) : TBitblaster() + , d_bv(theory_bv) , d_bbAtoms() + , d_variables() { d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); @@ -126,6 +130,7 @@ void EagerBitblaster::makeVariable(TNode var, Bits& bits) { for (unsigned i = 0; i < utils::getSize(var); ++i) { bits.push_back(utils::mkBitOf(var, i)); } + d_variables.insert(var); } Node EagerBitblaster::getBBAtom(TNode node) const { @@ -154,6 +159,68 @@ bool EagerBitblaster::solve() { } +/** + * Returns the value a is currently assigned to in the SAT solver + * 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 EagerBitblaster::getVarValue(TNode a, bool fullModel) { + if (!hasBBTerm(a)) { + Assert(isSharedTerm(a)); + return Node(); + } + Bits bits; + getBBTerm(a, bits); + Integer value(0); + for (int i = bits.size() -1; i >= 0; --i) { + prop::SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { + prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); + bit_value = d_satSolver->value(bit); + Assert (bit_value != prop::SAT_VALUE_UNKNOWN); + } else { + // the bit is unconstrainted so we can give it an arbitrary value + bit_value = prop::SAT_VALUE_FALSE; + } + Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); + value = value * 2 + bit_int; + } + return utils::mkConst(BitVector(bits.size(), value)); +} + + +void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { + TNodeSet::const_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, fullModel); + if(const_value == Node()) { + 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") << "TLazyBitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; + m->assertEquality(var, const_value, true); + } + } + } +} + +bool EagerBitblaster::isSharedTerm(TNode node) { + return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); +} + + } /*bv namespace */ } /* theory namespace */ } /* CVC4 namespace*/ diff --git a/src/theory/bv/lazy_bitblaster.h b/src/theory/bv/lazy_bitblaster.h index 570549866..e11254dbb 100644 --- a/src/theory/bv/lazy_bitblaster.h +++ b/src/theory/bv/lazy_bitblaster.h @@ -453,7 +453,7 @@ Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) { } void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { - __gnu_cxx::hash_set::iterator it = d_variables.begin(); + TNodeSet::iterator it = d_variables.begin(); for (; it!= d_variables.end(); ++it) { TNode var = *it; if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { diff --git a/src/theory/bv/options b/src/theory/bv/options index b5a4fea93..81d88421b 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -5,14 +5,14 @@ module BV "theory/bv/options.h" Bitvector theory -# Option to set the bit-blasting mode (lazy, eager, eager-aig) +# Option to set the bit-blasting mode (lazy, eager) option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler CVC4::theory::bv::stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "theory/bv/bitblast_mode.h" :handler-include "theory/bv/options_handlers.h" choose bitblasting mode, see --bitblast=help # Options for eager bit-blasting -option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager +option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager :link --bv-aig-simp="balance;drw" bitblast by first converting to AIG (only if --bitblast=eager) expert-option bitvectorAigSimplifications --bv-aig-simp=FILE std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h index 5d85a1be0..7cdd4aac5 100644 --- a/src/theory/bv/options_handlers.h +++ b/src/theory/bv/options_handlers.h @@ -56,9 +56,6 @@ lazy (default)\n\ \n\ eager\n\ + Bitblast eagerly to bv SAT solver\n\ -\n\ -aig\n\ -+ Bitblast eagerly to bv SAT solver by converting to AIG\n\ "; inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { @@ -70,7 +67,8 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, options::bitvectorEqualitySolver.set(true); } if (!options::bitvectorEqualitySlicer.wasSetByUser()) { - if (options::incrementalSolving()) { + if (options::incrementalSolving() || + options::produceModels()) { options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_OFF); } else { options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_AUTO); @@ -85,10 +83,6 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, } return BITBLAST_MODE_LAZY; } else if(optarg == "eager") { - if (options::produceModels()) { - throw OptionException(std::string("Eager bit-blasting does not currently support model generation. \n\ - Try --bitblast=lazy")); - } if (options::incrementalSolving() && options::incrementalSolving.wasSetByUser()) { @@ -96,14 +90,6 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, Try --bitblast=lazy")); } - if (!options::bitvectorAig.wasSetByUser()) { - options::bitvectorAig.set(true); - abcEnabledBuild("--bitblast-aig", true, NULL); - } - if (!options::bitvectorAigSimplifications.wasSetByUser()) { - // due to a known bug in abc switching to using drw instead of rw - options::bitvectorAigSimplifications.set("balance;drw"); - } if (!options::bitvectorToBool.wasSetByUser()) { options::bitvectorToBool.set(true); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d3da10a90..4b5333e46 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -61,7 +61,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_eagerSolver = new EagerBitblastSolver(); + d_eagerSolver = new EagerBitblastSolver(this); return; } @@ -434,7 +434,9 @@ void TheoryBV::check(Effort e) void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(!inConflict()); - + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + d_eagerSolver->collectModelInfo(m, fullModel); + } for (unsigned i = 0; i < d_subtheories.size(); ++i) { if (d_subtheories[i]->isComplete()) { d_subtheories[i]->collectModelInfo(m, fullModel); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 683f002cf..e96df8df2 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -209,6 +209,7 @@ private: friend class LazyBitblaster; friend class TLazyBitblaster; + friend class EagerBitblaster; friend class BitblastSolver; friend class EqualitySolver; friend class CoreSolver; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 6c0018c05..46eb5606b 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -152,7 +152,9 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const Unreachable(); } - if (n.getNumChildren() > 0) { + if (n.getNumChildren() > 0 && + n.getKind() != kind::BITVECTOR_ACKERMANIZE_UDIV && + n.getKind() != kind::BITVECTOR_ACKERMANIZE_UREM) { std::vector children; if (n.getKind() == APPLY_UF) { Node op = getModelValue(n.getOperator(), hasBoundVars); diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 4d437d2f0..be64e3ea1 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -11,6 +11,7 @@ UNIT_TESTS += \ theory/theory_black \ theory/theory_white \ theory/theory_arith_white \ + theory/theory_bv_white \ theory/type_enumerator_white \ expr/node_white \ expr/node_black \ diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index 4999ec3d4..dd65fc8e4 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -21,6 +21,7 @@ #include "theory/theory.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "theory/bv/theory_bv.h" #include "theory/bv/eager_bitblaster.h" #include "expr/node.h" #include "expr/node_manager.h" @@ -59,7 +60,7 @@ public: d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); d_smt->setOption("bitblast", SExpr("eager")); - d_bb = new EagerBitblaster(); + d_bb = new EagerBitblaster(NULL); } void tearDown() { -- 2.30.2