| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_engine.cpp | 218 void TheoryEngine::finishInit() { in finishInit()
281 TheoryEngine::TheoryEngine(context::Context* context, in TheoryEngine() function in CVC4::TheoryEngine
346 TheoryEngine::~TheoryEngine() { in ~TheoryEngine()
669 void TheoryEngine::combineTheories() { in combineTheories()
893 TheoryModel* TheoryEngine::getModel() { in getModel()
897 TheoryModel* TheoryEngine::getBuiltModel() in getBuiltModel()
922 bool TheoryEngine::presolve() { in presolve()
948 void TheoryEngine::postsolve() { in postsolve()
977 void TheoryEngine::notifyRestart() { in notifyRestart()
1011 void TheoryEngine::shutdown() { in shutdown()
[all …]
|
| H A D | valuation.h | 29 class TheoryEngine; variable
66 TheoryEngine* d_engine;
68 Valuation(TheoryEngine* engine) : in Valuation()
|
| H A D | term_registration_visitor.h | 27 class TheoryEngine; variable
43 TheoryEngine* d_engine;
67 PreRegisterVisitor(TheoryEngine* engine, context::Context* context) in PreRegisterVisitor()
|
| H A D | theory_registrar.h | 34 TheoryEngine* d_theoryEngine;
38 TheoryRegistrar(TheoryEngine* te) : d_theoryEngine(te) { } in TheoryRegistrar()
|
| H A D | theory_engine.h | 110 class TheoryEngine {
155 TheoryEngine& d_te;
157 NotifyClass(TheoryEngine& te): d_te(te) {} in NotifyClass()
267 friend class TheoryEngine; variable
272 TheoryEngine* d_engine;
283 EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory) in EngineOutputChannel()
476 TheoryEngine(context::Context* context, context::UserContext* userContext,
481 ~TheoryEngine();
|
| H A D | shared_terms_database.h | 30 class TheoryEngine; variable
130 TheoryEngine* d_theoryEngine;
160 SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
|
| H A D | theory_model_builder.h | 47 TheoryEngineModelBuilder(TheoryEngine* te);
82 TheoryEngine* d_te;
|
| H A D | quantifiers_engine.h | 37 class TheoryEngine; variable
93 QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
97 TheoryEngine* getTheoryEngine() const { return d_te; } in getTheoryEngine()
319 TheoryEngine* d_te;
|
| H A D | theory_traits_template.h | 42 static void addTheory(TheoryEngine* engine, TheoryId id) { in addTheory()
|
| H A D | theory.h | 50 class TheoryEngine; variable
84 friend class ::CVC4::TheoryEngine;
|
| H A D | shared_terms_database.cpp | 26 SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, in SharedTermsDatabase()
|
| H A D | theory_model_builder.cpp | 29 TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te) in TheoryEngineModelBuilder()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/ |
| H A D | theory_proxy.h | 42 class TheoryEngine; variable
55 TheoryEngine* theoryEngine,
117 TheoryEngine* d_theoryEngine;
|
| H A D | prop_engine.h | 39 class TheoryEngine; variable
65 TheoryEngine *d_theoryEngine;
101 PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext,
|
| H A D | theory_proxy.cpp | 39 TheoryEngine* theoryEngine, in TheoryProxy()
|
| H A D | prop_engine.cpp | 78 PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, in PropEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
| H A D | theory_preprocess.cpp | 34 TheoryEngine* te = d_preprocContext->getTheoryEngine(); in applyInternal()
|
| H A D | bv_abstraction.cpp | 47 TheoryEngine* te = d_preprocContext->getTheoryEngine(); in applyInternal()
|
| H A D | ite_simp.cpp | 154 TheoryEngine* theory_engine = d_preprocContext->getTheoryEngine(); in doneSimpITE()
|
| H A D | miplib_trick.cpp | 184 TheoryEngine* te = d_preprocContext->getTheoryEngine(); in applyInternal()
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/ |
| H A D | preprocessing_pass_context.h | 47 TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; } in getTheoryEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/smt/ |
| H A D | smt_engine.h | 60 class TheoryEngine; variable
143 TheoryEngine* d_theoryEngine;
|
| H A D | smt_engine.cpp | 310 UseTheoryListListener(TheoryEngine* theoryEngine) in UseTheoryListListener()
338 TheoryEngine* d_theoryEngine;
830 void addUseTheoryListListener(TheoryEngine* theoryEngine){ in addUseTheoryListListener()
927 d_theoryEngine = new TheoryEngine(d_context, in finishInit()
|
| /dports/math/cvc4/CVC4-1.7/test/unit/prop/ |
| H A D | cnf_stream_white.h | 113 TheoryEngine* d_theoryEngine;
|
| /dports/math/cvc4/CVC4-1.7/test/unit/theory/ |
| H A D | theory_engine_white.h | 239 TheoryEngine* d_theoryEngine;
|