| /dports/math/cvc3/cvc3-2.4.1/src/search/ |
| H A D | search_simple.cpp | 44 d_decisionEngine->goalSatisfied(); in checkValidRec()
68 d_decisionEngine->goalSatisfied(); in checkValidRec()
80 Expr splitter = d_decisionEngine->findSplitter(rhs); in checkValidRec()
82 d_decisionEngine->pushDecision(splitter); in checkValidRec()
85 d_decisionEngine->popDecision(); in checkValidRec()
86 d_decisionEngine->pushDecision(splitter, false); in checkValidRec()
90 d_decisionEngine->popDecision(); in checkValidRec()
113 d_decisionEngine = new DecisionEngineDFS(core, this); in SearchSimple()
122 delete d_decisionEngine; in ~SearchSimple()
|
| H A D | search_fast.cpp | 104 d_decisionEngine = new DecisionEngineDFS(core, this); in SearchEngineFast()
121 delete d_decisionEngine; in ~SearchEngineFast()
199 d_decisionEngine->goalSatisfied(); in checkSAT()
303 d_decisionEngine->pushDecision(splitter); in split()
507 splitter = d_decisionEngine->findSplitter(e); in findSplitter()
952 d_decisionEngine->popTo(d_bottomScope); in fixConflict()
967 d_decisionEngine->popTo(d_bottomScope); in fixConflict()
1022 d_decisionEngine->popTo(back_dl); in fixConflict()
1848 d_decisionEngine->popTo(scope); in traceConflict()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/ |
| H A D | theory_proxy.cpp | 48 d_decisionEngine(decisionEngine), in TheoryProxy()
146 Assert(d_decisionEngine != NULL); in getNextDecisionEngineRequest()
148 SatLiteral ret = d_decisionEngine->getNext(stopSearch); in getNextDecisionEngineRequest()
247 return d_decisionEngine->isRelevant(var); in isDecisionRelevant()
251 return d_decisionEngine->isDone(); in isDecisionEngineDone()
255 return d_decisionEngine->getPolarity(var); in getDecisionPolarity()
|
| H A D | prop_engine.cpp | 83 d_decisionEngine(de), in PropEngine()
106 this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, replayLog, in PropEngine()
110 d_decisionEngine->setSatSolver(d_satSolver); in PropEngine()
111 d_decisionEngine->setCnfStream(d_cnfStream); in PropEngine()
|
| H A D | theory_proxy.h | 114 DecisionEngine* d_decisionEngine; variable
|
| H A D | prop_engine.h | 68 DecisionEngine *d_decisionEngine; variable
|
| /dports/math/cvc4/CVC4-1.7/src/decision/ |
| H A D | decision_strategy.h | 38 DecisionEngine* d_decisionEngine;
41 d_decisionEngine(de) { in DecisionStrategy()
|
| H A D | justification_heuristic.cpp | 90 SatLiteral l = d_decisionEngine->hasSatLiteral(n) ? in getNextThresh()
91 d_decisionEngine->getSatLiteral(n) : -1; in getNextThresh()
139 d_decisionEngine->setResult(SAT_VALUE_TRUE); in getNextThresh()
353 if(d_decisionEngine->hasSatLiteral(n) ) { in tryGetSatValue()
354 Debug("decision") << d_decisionEngine->getSatValue(n) << std::endl; in tryGetSatValue()
355 return d_decisionEngine->getSatValue(n); in tryGetSatValue()
432 bool litPresent = d_decisionEngine->hasSatLiteral(node); in findSplitterRec()
479 Assert(d_decisionEngine->hasSatLiteral(node)); in findSplitterRec()
483 d_decisionEngine->getSatLiteral(node).getSatVariable(); in findSplitterRec()
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | search_simple.h | 50 DecisionEngine* d_decisionEngine; variable
|
| H A D | search_fast.h | 97 DecisionEngine *d_decisionEngine; variable
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/ |
| H A D | preprocessing_pass_context.h | 48 DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; } in getDecisionEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_engine.h | 120 DecisionEngine* d_decisionEngine; variable
507 Assert(d_decisionEngine == NULL); in setDecisionEngine()
508 d_decisionEngine = decisionEngine; in setDecisionEngine()
|
| H A D | theory_engine.cpp | 287 d_decisionEngine(nullptr), in TheoryEngine()
1866 d_decisionEngine->addAssertions(additionalLemmas); in lemma()
|
| /dports/math/cvc4/CVC4-1.7/src/smt/ |
| H A D | smt_engine.cpp | 868 d_decisionEngine(NULL), in SmtEngine()
954 d_decisionEngine = new DecisionEngine(d_context, d_userContext); in finishInit()
955 d_decisionEngine->init(); // enable appropriate strategies in finishInit()
958 d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, in finishInit()
964 d_theoryEngine->setDecisionEngine(d_decisionEngine); in finishInit()
1047 if(d_decisionEngine != NULL) { in shutdown()
1048 d_decisionEngine->shutdown(); in shutdown()
1106 delete d_decisionEngine; in ~SmtEngine()
1107 d_decisionEngine = NULL; in ~SmtEngine()
3042 d_decisionEngine->clearStrategies(); in check()
[all …]
|
| H A D | smt_engine.h | 141 DecisionEngine* d_decisionEngine; variable
|