| /dports/math/cvc4/CVC4-1.7/src/preprocessing/ |
| H A D | preprocessing_pass_context.h | 64 void spendResource(unsigned amount) in spendResource() function
66 d_resourceManager->spendResource(amount); in spendResource()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/ |
| H A D | theory_proxy.cpp | 164 d_propEngine->spendResource(options::restartStep()); in notifyRestart()
241 void TheoryProxy::spendResource(unsigned amount) in spendResource() function in CVC4::prop::TheoryProxy
243 d_theoryEngine->spendResource(amount); in spendResource()
|
| H A D | bv_sat_solver_notify.h | 41 virtual void spendResource(unsigned amount) = 0;
|
| H A D | theory_proxy.h | 95 void spendResource(unsigned amount);
|
| H A D | prop_engine.h | 231 void spendResource(unsigned amount);
|
| H A D | prop_engine.cpp | 303 void PropEngine::spendResource(unsigned amount) in spendResource() function in CVC4::prop::PropEngine
305 d_resourceManager->spendResource(amount); in spendResource()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/ |
| H A D | bvminisat.h | 49 void spendResource(unsigned amount) override in spendResource() function
51 d_notify->spendResource(amount); in spendResource()
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
| H A D | ite_removal.cpp | 35 d_preprocContext->spendResource(options::preprocessStep()); in applyInternal()
|
| H A D | static_learning.cpp | 32 NodeManager::currentResourceManager()->spendResource( in applyInternal()
|
| H A D | ite_simp.cpp | 237 d_preprocContext->spendResource(options::preprocessStep()); in applyInternal()
242 d_preprocContext->spendResource(options::preprocessStep()); in applyInternal()
|
| H A D | apply_substs.cpp | 60 d_preprocContext->spendResource(options::preprocessStep()); in applyInternal()
|
| H A D | bool_to_bv.cpp | 38 NodeManager::currentResourceManager()->spendResource( in applyInternal()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_engine.h | 287 spendResource(amount); in safePoint()
328 void spendResource(unsigned amount) override { in spendResource() function
329 d_engine->spendResource(amount); in spendResource()
486 void spendResource(unsigned amount);
|
| H A D | output_channel.h | 176 virtual void spendResource(unsigned amount) {} in spendResource() function
|
| H A D | rewriter.cpp | 123 rm->spendResource(options::rewriteStep()); in rewriteTo()
|
| /dports/math/cvc4/CVC4-1.7/src/util/ |
| H A D | resource_manager.h | 156 void spendResource(unsigned amount);
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | bv_eager_solver.cpp | 73 d_bv->spendResource(1); in assertFormula()
|
| H A D | theory_bv.h | 134 void spendResource(unsigned amount);
|
| H A D | bv_subtheory_bitblast.cpp | 176 d_bv->spendResource(1); in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/ |
| H A D | bitblaster.h | 112 void spendResource(unsigned amount) override in spendResource() function
114 NodeManager::currentResourceManager()->spendResource(amount); in spendResource()
|
| H A D | lazy_bitblaster.cpp | 237 d_bv->spendResource(options::bitblastStep()); in bbTerm()
429 void TLazyBitblaster::MinisatNotify::spendResource(unsigned amount) in spendResource() function in CVC4::theory::bv::TLazyBitblaster::MinisatNotify
431 d_bv->spendResource(amount); in spendResource()
|
| H A D | lazy_bitblaster.h | 123 void spendResource(unsigned amount) override;
|
| H A D | eager_bitblaster.cpp | 155 d_bv->spendResource(options::bitblastStep()); in bbTerm()
|
| /dports/math/cvc4/CVC4-1.7/src/decision/ |
| H A D | decision_engine.h | 120 NodeManager::currentResourceManager()->spendResource(options::decisionStep()); in getNext()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | theory_arith.cpp | 86 getOutputChannel().spendResource(options::theoryCheckStep()); in check()
|