Home
last modified time | relevance | path

Searched refs:d_satContext (Results 1 – 7 of 7) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/decision/
H A Ddecision_engine.cpp37 d_satContext(sc), in DecisionEngine()
59 new decision::JustificationHeuristic(this, d_userContext, d_satContext); in init()
H A Ddecision_engine.h53 context::Context* d_satContext; variable
/dports/math/cvc4/CVC4-1.7/src/theory/arrays/
H A Dtheory_arrays.h393 context::Context* d_satContext; variable
398 if (d_contextToPop->getLevel() > d_satContext->getLevel()) in contextNotifyPop()
405 :context::ContextNotifyObj(context), d_satContext(context), in ContextPopper()
/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dtheory.h100 context::Context* d_satContext; variable
366 return d_satContext; in getSatContext()
454 << d_satContext->getLevel() << "](" << assertion << ", " in assertFact()
H A Dtheory.cpp64 d_satContext(satContext), in Theory()
/dports/math/cvc4/CVC4-1.7/src/theory/arith/
H A Dconstraint.h1073 const context::Context * const d_satContext; variable
H A Dconstraint.cpp801 , d_satContext(satContext) in ConstraintDatabase()