Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/
H A Dmodel_builder.cpp38 QModelBuilder::QModelBuilder(context::Context* c, QuantifiersEngine* qe) in QModelBuilder() function in QModelBuilder
44 bool QModelBuilder::optUseModel() { in optUseModel()
48 bool QModelBuilder::preProcessBuildModel(TheoryModel* m) { in preProcessBuildModel()
52 bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { in preProcessBuildModelStd()
99 void QModelBuilder::debugModel( TheoryModel* m ){ in debugModel()
H A Dmodel_builder.h29 class QModelBuilder : public TheoryEngineModelBuilder
41 QModelBuilder( context::Context* c, QuantifiersEngine* qe );
H A Dfull_model_check.h82 class FullModelChecker : public QModelBuilder
H A Dmodel_engine.cpp256 quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); in exhaustiveInstantiate()
H A Dfull_model_check.cpp282 QModelBuilder( c, qe ){ in FullModelChecker()
/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dquantifiers_engine.h69 class QModelBuilder; variable
121 quantifiers::QModelBuilder* getModelBuilder() const;
342 std::unique_ptr<quantifiers::QModelBuilder> d_builder;
H A Dquantifiers_engine.cpp255 d_builder.reset(new quantifiers::QModelBuilder(c, this)); in QuantifiersEngine()
309 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const in getModelBuilder()