Home
last modified time | relevance | path

Searched refs:getDecisionManager (Results 1 – 11 of 11) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dtheory.h412 DecisionManager* getDecisionManager() { return d_decManager; } in getDecisionManager() function
H A Dtheory_engine.h544 theory::DecisionManager* getDecisionManager() const in getDecisionManager() function
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/
H A Dsynth_conjecture.cpp210 d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( in assign()
246 d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( in assign()
H A Dcegis_unif.cpp547 d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( in initialize()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/
H A Dinst_strategy_cegqi.cpp200 d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy( in registerCbqiLemma()
/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dtheory_uf_strong_solver.cpp505 d_thss->getTheory()->getDecisionManager()->registerStrategy( in initialize()
1768 d_th->getDecisionManager()->registerStrategy( in initializeCombinedCardinality()
/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/
H A Ddatatypes_sygus.cpp1307 d_td->getDecisionManager()->registerStrategy( in registerSizeTerm()
1389 d_td->getDecisionManager()->registerStrategy( in registerMeasureTerm()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/
H A Dbounded_integers.cpp498 ->getDecisionManager() in checkOwnership()
/dports/math/cvc4/CVC4-1.7/src/theory/arrays/
H A Dtheory_arrays.cpp1256 getDecisionManager()->registerStrategy(DecisionManager::STRAT_ARRAYS, in presolve()
/dports/math/cvc4/CVC4-1.7/src/theory/sep/
H A Dtheory_sep.cpp462 getDecisionManager()->registerStrategy( in check()
/dports/math/cvc4/CVC4-1.7/src/theory/strings/
H A Dtheory_strings.cpp573 getDecisionManager()->registerStrategy( in presolve()