diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/bv/theory_bv.h | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 9c27f62c5..f79b7ab71 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -49,8 +49,8 @@ class TheoryBV : public Theory { EqualitySolver d_equalitySolver; public: - TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); - ~TheoryBV(); + TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + ~TheoryBV(); void preRegisterTerm(TNode n); @@ -64,21 +64,21 @@ public: std::string identify() const { return std::string("TheoryBV"); } - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); private: - + class Statistics { public: AverageStat d_avgConflictSize; IntStat d_solveSubstitutions; - TimerStat d_solveTimer; + TimerStat d_solveTimer; Statistics(); - ~Statistics(); - }; - + ~Statistics(); + }; + Statistics d_statistics; - + // Are we in conflict? context::CDO<bool> d_conflict; @@ -133,7 +133,7 @@ private: } bool inConflict() { return d_conflict == true; } - + friend class Bitblaster; friend class BitblastSolver; friend class EqualitySolver; |