Home
last modified time | relevance | path

Searched refs:getModelBuilder (Results 1 – 5 of 5) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dquantifiers_engine.cpp309 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const in getModelBuilder() function in QuantifiersEngine
477 if (!d_te->getModelBuilder()->buildModel(d_model.get())) in check()
641 Assert(!getModelBuilder() in check()
642 || getModelBuilder() == d_te->getModelBuilder()); in check()
644 if (!d_te->getModelBuilder()->buildModel(d_model.get())) in check()
H A Dquantifiers_engine.h121 quantifiers::QModelBuilder* getModelBuilder() const;
H A Dtheory_engine.h782 theory::TheoryEngineModelBuilder* getModelBuilder() { return d_curr_model_builder; } in getModelBuilder() function
H A Dtheory_engine.cpp234 d_curr_model_builder = d_quantEngine->getModelBuilder(); in finishInit()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/
H A Dmodel_engine.cpp256 quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); in exhaustiveInstantiate()