Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/prop/
H A Dtheory_proxy.cpp46 : d_propEngine(propEngine), in TheoryProxy()
164 d_propEngine->spendResource(options::restartStep()); in notifyRestart()
184 d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID); in notifyRestart()
H A Dtheory_proxy.h108 PropEngine* d_propEngine;
/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dtheory_engine.h117 prop::PropEngine* d_propEngine; variable
320 d_engine->d_propEngine->requirePhase(n, phase); in requirePhase()
502 Assert(d_propEngine == NULL); in setPropEngine()
503 d_propEngine = propEngine; in setPropEngine()
518 return d_propEngine; in getPropEngine()
H A Dtheory_engine.cpp286 : d_propEngine(nullptr), in TheoryEngine()
726 d_propEngine->requirePhase(e, true); in combineTheories()
759 if(d_propEngine->hasValue(atom, value)) { in propagate()
840 return d_propEngine->hasValue(expl, value) && value; in properExplanation()
863 d_propEngine->getBooleanVariables(boolVars); in collectModelInfo()
868 hasValue = d_propEngine->hasValue(var, value); in collectModelInfo()
1263 if (d_propEngine->hasValue(assertion, value)) { in assertToTheory()
1435 if (d_propEngine->isSatLiteral(literal)) { in propagate()
1462 Assert(d_propEngine->isSatLiteral(literal)); in propagate()
1501 d_propEngine->ensureLiteral(preprocessed); in ensureLiteral()
[all …]
/dports/math/cvc4/CVC4-1.7/src/preprocessing/
H A Dpreprocessing_pass_context.h49 prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; } in getPropEngine()
/dports/math/cvc4/CVC4-1.7/src/smt/
H A Dsmt_engine.cpp870 d_propEngine(NULL), in SmtEngine()
963 d_theoryEngine->setPropEngine(d_propEngine); in finishInit()
1041 if(d_propEngine != NULL) { in shutdown()
1042 d_propEngine->shutdown(); in shutdown()
1104 delete d_propEngine; in ~SmtEngine()
1105 d_propEngine = NULL; in ~SmtEngine()
3052 Result result = d_propEngine->checkSat(); in check()
5124 d_propEngine->push(); in internalPush()
5145 d_propEngine->resetTrail(); in doPendingPops()
5149 d_propEngine->pop(); in doPendingPops()
[all …]
H A Dsmt_engine.h145 prop::PropEngine* d_propEngine; variable