diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:46:24 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:46:24 -0700 |
commit | 4dac1ec234ee0d0885f058b4b35a7eeba2ca5007 (patch) | |
tree | aae1792c05c0a67c521160226deb451ca861822c /src/theory/bv/theory_bv.h | |
parent | de0dd1dc966b05467f1a5443ff33094262f5076a (diff) |
Merge from proof branch
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 7f0494dc1..ba2a4fc2a 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -56,7 +56,8 @@ class TheoryBV : public Theory { public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo); + Valuation valuation, const LogicInfo& logicInfo, + std::string name = ""); ~TheoryBV(); @@ -88,8 +89,8 @@ public: void presolve(); - bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); - + bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + void setProofLog( BitVectorProof * bvp ); private: @@ -100,10 +101,10 @@ private: IntStat d_solveSubstitutions; TimerStat d_solveTimer; IntStat d_numCallsToCheckFullEffort; - IntStat d_numCallsToCheckStandardEffort; + IntStat d_numCallsToCheckStandardEffort; TimerStat d_weightComputationTimer; IntStat d_numMultSlice; - Statistics(); + Statistics(const std::string &name); ~Statistics(); }; @@ -121,12 +122,12 @@ private: */ Node getBVDivByZero(Kind k, unsigned width); - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; void collectFunctionSymbols(TNode term, TNodeSet& seen); void storeFunction(TNode func, TNode term); typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; NodeSet d_staticLearnCache; - + /** * Maps from bit-vector width to division-by-zero uninterpreted * function symbols. @@ -142,7 +143,7 @@ private: CVC4::theory::SubstitutionMap d_funcToSkolem; context::CDO<bool> d_lemmasAdded; - + // Are we in conflict? context::CDO<bool> d_conflict; @@ -165,17 +166,17 @@ private: typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap; PropagatedMap d_propagatedBy; - EagerBitblastSolver* d_eagerSolver; + EagerBitblastSolver* d_eagerSolver; AbstractionModule* d_abstractionModule; bool d_isCoreTheory; bool d_calledPreregister; - + bool wasPropagatedBySubtheory(TNode literal) const { - return d_propagatedBy.find(literal) != d_propagatedBy.end(); + return d_propagatedBy.find(literal) != d_propagatedBy.end(); } - + SubTheory getPropagatingSubtheory(TNode literal) const { - Assert(wasPropagatedBySubtheory(literal)); + Assert(wasPropagatedBySubtheory(literal)); PropagatedMap::const_iterator find = d_propagatedBy.find(literal); return (*find).second; } @@ -191,7 +192,7 @@ private: void addSharedTerm(TNode t); bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } - + EqualityStatus getEqualityStatus(TNode a, TNode b); Node getModelValue(TNode var); @@ -212,7 +213,7 @@ private: void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; } - void checkForLemma(TNode node); + void checkForLemma(TNode node); friend class LazyBitblaster; friend class TLazyBitblaster; |