Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dtheory_engine.h132 theory::Theory* d_theoryTable[theory::THEORY_LAST]; variable
494 Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); in addTheory()
496 d_theoryTable[theoryId] = in addTheory()
791 return d_theoryTable[theory::Theory::theoryOf(node)]; in theoryOf()
800 return d_theoryTable[theoryId]; in theoryOf()
H A Dtheory_engine.cpp228 if (d_theoryTable[theoryId]) { in finishInit()
248 if (d_theoryTable[theoryId]) { in finishInit()
252 d_theoryTable[theoryId]->finishInit(); in finishInit()
331 d_theoryTable[theoryId] = NULL; in TheoryEngine()
350 if(d_theoryTable[theoryId] != NULL) { in ~TheoryEngine()
351 delete d_theoryTable[theoryId]; in ~TheoryEngine()
439 Theory* theory = d_theoryTable[theoryId]; in printAssertions()
469 Theory* theory = d_theoryTable[theoryId]; in dumpAssertions()
1019 if(d_theoryTable[theoryId]) { in shutdown()
1198 if (d_theoryTable[theoryId]) { in notifyPreprocessedAssertions()
[all …]
/dports/math/cvc4/CVC4-1.7/test/unit/theory/
H A Dtheory_white.h174 delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN]; in setUp()
176 d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL; in setUp()
H A Dtheory_engine_white.h261 delete d_theoryEngine->d_theoryTable[id]; in setUp()
263 d_theoryEngine->d_theoryTable[id] = NULL; in setUp()
H A Dtheory_bv_white.h79 d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]), in testBitblasterCore()
H A Dtheory_arith_white.h118 delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]; in setUp()
120 d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL; in setUp()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dterm_database.cpp932 Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId]; in reset()