diff options
Diffstat (limited to 'src/theory/bv/bitblaster_template.h')
| -rw-r--r-- | src/theory/bv/bitblaster_template.h | 399 |
1 files changed, 399 insertions, 0 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h new file mode 100644 index 000000000..25de81f2c --- /dev/null +++ b/src/theory/bv/bitblaster_template.h @@ -0,0 +1,399 @@ +/********************* */ +/*! \file bitblaster.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): lianah, Morgan Deters, Dejan Jovanovic + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Wrapper around the SAT solver used for bitblasting + ** + ** Wrapper around the SAT solver used for bitblasting. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BITBLASTER_TEMPLATE_H +#define __CVC4__BITBLASTER_TEMPLATE_H + + +#include "expr/node.h" +#include <vector> +#include <ext/hash_map> +#include "context/cdhashmap.h" +#include "bitblast_strategies_template.h" +#include "prop/sat_solver.h" +#include "theory/valuation.h" + +class Abc_Obj_t_; +typedef Abc_Obj_t_ Abc_Obj_t; + +class Abc_Ntk_t_; +typedef Abc_Ntk_t_ Abc_Ntk_t; + +class Abc_Aig_t_; +typedef Abc_Aig_t_ Abc_Aig_t; + +class Cnf_Dat_t_; +typedef Cnf_Dat_t_ Cnf_Dat_t; + + +namespace CVC4 { +namespace prop { +class CnfStream; +class BVSatSolverInterface; +class NullRegistrar; +} + +namespace theory { +class OutputChannel; +class TheoryModel; + +namespace bv { + +class BitblastingRegistrar; + +typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +class AbstractionModule; + +/** + * The Bitblaster that manages the mapping between Nodes + * and their bitwise definition + * + */ + +template <class T> +class TBitblaster { +protected: + typedef std::vector<T> Bits; + typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction> TermDefMap; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet; + + typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*); + typedef T (*AtomBBStrategy) (TNode, TBitblaster<T>*); + + // caches and mappings + TermDefMap d_termCache; + + void initAtomBBStrategies(); + void initTermBBStrategies(); +protected: + /// function tables for the various bitblasting strategies indexed by node kind + TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; + AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; +public: + TBitblaster(); + virtual ~TBitblaster() {} + virtual void bbAtom(TNode node) = 0; + virtual void bbTerm(TNode node, Bits& bits) = 0; + virtual void makeVariable(TNode node, Bits& bits) = 0; + virtual T getBBAtom(TNode atom) const = 0; + virtual bool hasBBAtom(TNode atom) const = 0; + virtual void storeBBAtom(TNode atom, T atom_bb) = 0; + + bool hasBBTerm(TNode node) const; + void getBBTerm(TNode node, Bits& bits) const; + void storeBBTerm(TNode term, const Bits& bits); +}; + + +class TheoryBV; + +class TLazyBitblaster : public TBitblaster<Node> { + typedef std::vector<Node> Bits; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> VarSet; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet; + typedef context::CDList<prop::SatLiteral> AssertionList; + typedef context::CDHashMap<prop::SatLiteral, std::vector<prop::SatLiteral> , prop::SatLiteralHashFunction> ExplanationMap; + + /** This class gets callbacks from minisat on propagations */ + class MinisatNotify : public prop::BVSatSolverInterface::Notify { + prop::CnfStream* d_cnf; + TheoryBV *d_bv; + TLazyBitblaster* d_lazyBB; + public: + MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv, TLazyBitblaster* lbv) + : d_cnf(cnf) + , d_bv(bv) + , d_lazyBB(lbv) + {} + bool notify(prop::SatLiteral lit); + void notify(prop::SatClause& clause); + void safePoint(); + }; + + TheoryBV *d_bv; + context::Context* d_ctx; + + prop::NullRegistrar* d_nullRegistrar; + context::Context* d_nullContext; + // sat solver used for bitblasting and associated CnfStream + prop::BVSatSolverInterface* d_satSolver; + prop::CnfStream* d_cnfStream; + + AssertionList d_assertedAtoms; /**< context dependent list storing the atoms + 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; + AbstractionModule* d_abstraction; + bool d_emptyNotify; + + void addAtom(TNode atom); + bool hasValue(TNode a); +public: + void bbTerm(TNode node, Bits& bits); + void bbAtom(TNode node); + Node getBBAtom(TNode atom) const; + void storeBBAtom(TNode atom, Node atom_bb); + bool hasBBAtom(TNode atom) const; + TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false); + ~TLazyBitblaster(); + /** + * Pushes the assumption literal associated with node to the SAT + * solver assumption queue. + * + * @param node assumption + * @param propagate run bcp or not + * + * @return false if a conflict detected + */ + bool assertToSat(TNode node, bool propagate = true); + bool propagate(); + bool solve(); + prop::SatValue solveWithBudget(unsigned long conflict_budget); + void getConflict(std::vector<TNode>& conflict); + void explain(TNode atom, std::vector<TNode>& explanation); + void setAbstraction(AbstractionModule* abs); + + theory::EqualityStatus getEqualityStatus(TNode a, TNode b); + /** + * Return a constant Node representing the value of a variable + * in the current model. + * @param a + * + * @return + */ + 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, bool fullModel); + + typedef VarSet::const_iterator vars_iterator; + vars_iterator beginVars() { return d_variables.begin(); } + vars_iterator endVars() { return d_variables.end(); } + + /** + * Creates the bits corresponding to the variable (or non-bv term). + * + * @param var + */ + void makeVariable(TNode var, Bits& bits); + + bool isSharedTerm(TNode node); + uint64_t computeAtomWeight(TNode node, NodeSet& seen); + /** + * Deletes SatSolver and CnfCache, but maintains bit-blasting + * terms cache. + * + */ + void clearSolver(); +private: + + class Statistics { + public: + IntStat d_numTermClauses, d_numAtomClauses; + IntStat d_numTerms, d_numAtoms; + IntStat d_numExplainedPropagations; + IntStat d_numBitblastingPropagations; + TimerStat d_bitblastTimer; + Statistics(const std::string& name); + ~Statistics(); + }; + std::string d_name; + Statistics d_statistics; +}; + +class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify { +public: + MinisatEmptyNotify() {} + bool notify(prop::SatLiteral lit) { return true; } + void notify(prop::SatClause& clause) { } + void safePoint() {} +}; + + +class EagerBitblaster : public TBitblaster<Node> { + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + // sat solver used for bitblasting and associated CnfStream + prop::BVSatSolverInterface* d_satSolver; + BitblastingRegistrar* d_bitblastingRegistrar; + context::Context* d_nullContext; + prop::CnfStream* d_cnfStream; + TNodeSet d_bbAtoms; +public: + void addAtom(TNode atom); + void makeVariable(TNode node, Bits& bits); + void bbTerm(TNode node, Bits& bits); + void bbAtom(TNode node); + Node getBBAtom(TNode node) const; + bool hasBBAtom(TNode atom) const; + void bbFormula(TNode formula); + void storeBBAtom(TNode atom, Node atom_bb); + EagerBitblaster(); + ~EagerBitblaster(); + bool assertToSat(TNode node, bool propagate = true); + bool solve(); +}; + +class AigBitblaster : public TBitblaster<Abc_Obj_t*> { + typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap; + typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap; + + static Abc_Ntk_t* abcAigNetwork; + context::Context* d_nullContext; + prop::BVSatSolverInterface* d_satSolver; + TNodeAigMap d_aigCache; + NodeAigMap d_bbAtoms; + + NodeAigMap d_nodeToAigInput; + // the thing we are checking for sat + Abc_Obj_t* d_aigOutputNode; + + void addAtom(TNode atom); + void simplifyAig(); + void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb); + Abc_Obj_t* getBBAtom(TNode atom) const; + bool hasBBAtom(TNode atom) const; + void cacheAig(TNode node, Abc_Obj_t* aig); + bool hasAig(TNode node); + Abc_Obj_t* getAig(TNode node); + Abc_Obj_t* mkInput(TNode input); + bool hasInput(TNode input); + void convertToCnfAndAssert(); + void assertToSatSolver(Cnf_Dat_t* pCnf); + +public: + AigBitblaster(); + ~AigBitblaster(); + + void makeVariable(TNode node, Bits& bits); + void bbTerm(TNode node, Bits& bits); + void bbAtom(TNode node); + Abc_Obj_t* bbFormula(TNode formula); + bool solve(TNode query); + static Abc_Aig_t* currentAigM(); + static Abc_Ntk_t* currentAigNtk(); + +private: + class Statistics { + public: + IntStat d_numClauses; + IntStat d_numVariables; + TimerStat d_simplificationTime; + TimerStat d_cnfConversionTime; + TimerStat d_solveTime; + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; + +}; + + +// Bitblaster implementation + +template <class T> void TBitblaster<T>::initAtomBBStrategies() { + for (int i = 0 ; i < kind::LAST_KIND; ++i ) { + d_atomBBStrategies[i] = UndefinedAtomBBStrategy<T>; + } + /// setting default bb strategies for atoms + d_atomBBStrategies [ kind::EQUAL ] = DefaultEqBB<T>; + d_atomBBStrategies [ kind::BITVECTOR_ULT ] = DefaultUltBB<T>; + d_atomBBStrategies [ kind::BITVECTOR_ULE ] = DefaultUleBB<T>; + d_atomBBStrategies [ kind::BITVECTOR_UGT ] = DefaultUgtBB<T>; + d_atomBBStrategies [ kind::BITVECTOR_UGE ] = DefaultUgeBB<T>; + d_atomBBStrategies [ kind::BITVECTOR_SLT ] = DefaultSltBB<T>; + d_atomBBStrategies [ kind::BITVECTOR_SLE ] = DefaultSleBB<T>; + d_atomBBStrategies [ kind::BITVECTOR_SGT ] = DefaultSgtBB<T>; + d_atomBBStrategies [ kind::BITVECTOR_SGE ] = DefaultSgeBB<T>; +} + +template <class T> void TBitblaster<T>::initTermBBStrategies() { + for (int i = 0 ; i < kind::LAST_KIND; ++i ) { + d_termBBStrategies[i] = DefaultVarBB<T>; + } + /// setting default bb strategies for terms: + d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB<T>; + d_termBBStrategies [ kind::BITVECTOR_NOT ] = DefaultNotBB<T>; + d_termBBStrategies [ kind::BITVECTOR_CONCAT ] = DefaultConcatBB<T>; + d_termBBStrategies [ kind::BITVECTOR_AND ] = DefaultAndBB<T>; + d_termBBStrategies [ kind::BITVECTOR_OR ] = DefaultOrBB<T>; + d_termBBStrategies [ kind::BITVECTOR_XOR ] = DefaultXorBB<T>; + d_termBBStrategies [ kind::BITVECTOR_XNOR ] = DefaultXnorBB<T>; + d_termBBStrategies [ kind::BITVECTOR_NAND ] = DefaultNandBB<T>; + d_termBBStrategies [ kind::BITVECTOR_NOR ] = DefaultNorBB<T>; + d_termBBStrategies [ kind::BITVECTOR_COMP ] = DefaultCompBB<T>; + d_termBBStrategies [ kind::BITVECTOR_MULT ] = DefaultMultBB<T>; + d_termBBStrategies [ kind::BITVECTOR_PLUS ] = DefaultPlusBB<T>; + d_termBBStrategies [ kind::BITVECTOR_SUB ] = DefaultSubBB<T>; + d_termBBStrategies [ kind::BITVECTOR_NEG ] = DefaultNegBB<T>; + d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy<T>; + d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy<T>; + d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ] = DefaultUdivBB<T>; + d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ] = DefaultUremBB<T>; + d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy<T>; + d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy<T>; + d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy<T>; + d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB<T>; + d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB<T>; + d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB<T>; + d_termBBStrategies [ kind::BITVECTOR_EXTRACT ] = DefaultExtractBB<T>; + d_termBBStrategies [ kind::BITVECTOR_REPEAT ] = DefaultRepeatBB<T>; + d_termBBStrategies [ kind::BITVECTOR_ZERO_EXTEND ] = DefaultZeroExtendBB<T>; + d_termBBStrategies [ kind::BITVECTOR_SIGN_EXTEND ] = DefaultSignExtendBB<T>; + d_termBBStrategies [ kind::BITVECTOR_ROTATE_RIGHT ] = DefaultRotateRightBB<T>; + d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ] = DefaultRotateLeftBB<T>; +} + +template <class T> +TBitblaster<T>::TBitblaster() + : d_termCache() +{ + initAtomBBStrategies(); + initTermBBStrategies(); +} + +template <class T> +bool TBitblaster<T>::hasBBTerm(TNode node) const { + return d_termCache.find(node) != d_termCache.end(); +} +template <class T> +void TBitblaster<T>::getBBTerm(TNode node, Bits& bits) const { + Assert (hasBBTerm(node)); + bits = d_termCache.find(node)->second; +} + +template <class T> +void TBitblaster<T>::storeBBTerm(TNode node, const Bits& bits) { + d_termCache.insert(std::make_pair(node, bits)); +} + + +} /* bv namespace */ + +} /* theory namespace */ + +} /* CVC4 namespace */ + +#endif /* __CVC4__BITBLASTER_H */ |