-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
- OutputChannel& out, Valuation valuation,
- const LogicInfo& logicInfo, std::string name)
- : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
- d_context(c),
- d_alreadyPropagatedSet(c),
- d_sharedTermsSet(c),
- d_subtheories(),
- d_subtheoryMap(),
- d_statistics(),
- d_staticLearnCache(),
- d_BVDivByZero(),
- d_BVRemByZero(),
- d_lemmasAdded(c, false),
- d_conflict(c, false),
- d_invalidateModelCache(c, true),
- d_literalsToPropagate(c),
- d_literalsToPropagateIndex(c, 0),
- d_propagatedBy(c),
- d_eagerSolver(NULL),
- d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
- d_isCoreTheory(false),
- d_calledPreregister(false),
- d_needsLastCallCheck(false),
- d_extf_range_infer(u),
- d_extf_collapse_infer(u)
+TheoryBV::TheoryBV(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ std::string name)
+ : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
+ d_context(c),
+ d_alreadyPropagatedSet(c),
+ d_sharedTermsSet(c),
+ d_subtheories(),
+ d_subtheoryMap(),
+ d_statistics(),
+ d_staticLearnCache(),
+ d_BVDivByZero(),
+ d_BVRemByZero(),
+ d_lemmasAdded(c, false),
+ d_conflict(c, false),
+ d_invalidateModelCache(c, true),
+ d_literalsToPropagate(c),
+ d_literalsToPropagateIndex(c, 0),
+ d_propagatedBy(c),
+ d_eagerSolver(),
+ d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
+ d_isCoreTheory(false),
+ d_calledPreregister(false),
+ d_needsLastCallCheck(false),
+ d_extf_range_infer(u),
+ d_extf_collapse_infer(u)