diff options
Diffstat (limited to 'src/theory/bv/bitblaster.h')
-rw-r--r-- | src/theory/bv/bitblaster.h | 197 |
1 files changed, 0 insertions, 197 deletions
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h deleted file mode 100644 index 34345086b..000000000 --- a/src/theory/bv/bitblaster.h +++ /dev/null @@ -1,197 +0,0 @@ -/********************* */ -/*! \file bitblaster.h - ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): Kshitij Bansal, 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_H -#define __CVC4__BITBLASTER_H - - -#include "expr/node.h" -#include <vector> -#include <list> -#include <iostream> -#include <math.h> -#include <ext/hash_map> - -#include "context/cdo.h" -#include "context/cdhashset.h" -#include "context/cdlist.h" - -#include "theory/theory.h" -#include "theory_bv_utils.h" -#include "util/statistics_registry.h" -#include "bitblast_strategies.h" - -#include "prop/sat_solver.h" -#include "prop/registrar.h" - -namespace CVC4 { - -// forward declarations -namespace prop { -class CnfStream; -class BVSatSolverInterface; -} - -namespace theory { - -class OutputChannel; -class TheoryModel; - -namespace bv { - -typedef std::vector<Node> Bits; - -std::string toString (Bits& bits); - -class TheoryBV; - -/** - * The Bitblaster that manages the mapping between Nodes - * and their bitwise definition - * - */ -class Bitblaster { - - /** This class gets callbacks from minisat on propagations */ - class MinisatNotify : public prop::BVSatSolverInterface::Notify { - prop::CnfStream* d_cnf; - TheoryBV *d_bv; - public: - MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv) - : d_cnf(cnf) - , d_bv(bv) - {} - bool notify(prop::SatLiteral lit); - 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*); - - TheoryBV *d_bv; - - // sat solver used for bitblasting and associated CnfStream - theory::OutputChannel* d_bvOutput; - MinisatNotify* d_notify; - prop::BVSatSolverInterface* d_satSolver; - prop::CnfStream* d_cnfStream; - prop::NullRegistrar* d_nullRegistrar; - context::Context* d_nullContext; - - // caches and mappings - TermDefMap d_termCache; - AtomSet d_bitblastedAtoms; - VarSet d_variables; - context::CDList<prop::SatLiteral> d_assertedAtoms; /**< context dependent list storing the atoms - currently asserted by the DPLL SAT solver. */ - - /// helper methods - public: - bool hasBBAtom(TNode node) const; - private: - bool hasBBTerm(TNode node) const; - void getBBTerm(TNode node, Bits& bits) const; - - /// function tables for the various bitblasting strategies indexed by node kind - TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; - AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; - - // helper methods to initialize function tables - void initAtomBBStrategies(); - void initTermBBStrategies(); - - // returns a node that might be easier to bitblast - 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); -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(); - bool assertToSat(TNode node, bool propagate = true); - bool propagate(); - bool solve(bool quick_solve = false); - 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 - */ - 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); - /** - * Stores the variable (or non-bv term) and its corresponding bits. - * - * @param var - */ - void storeVariable(TNode 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; - TimerStat d_bitblastTimer; - Statistics(); - ~Statistics(); - }; - - Statistics d_statistics; -}; - - - -} /* bv namespace */ - -} /* theory namespace */ - -} /* CVC4 namespace */ - -#endif /* __CVC4__BITBLASTER_H */ |