Home
last modified time | relevance | path

Searched refs:TheoryEngineModelBuilder (Results 1 – 8 of 8) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dtheory_model_builder.cpp29 TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te) in TheoryEngineModelBuilder() function in CVC4::theory::TheoryEngineModelBuilder
33 bool TheoryEngineModelBuilder::isAssignable(TNode n) in isAssignable()
79 void TheoryEngineModelBuilder::addAssignableSubterms(TNode n, in addAssignableSubterms()
102 void TheoryEngineModelBuilder::assignConstantRep(TheoryModel* tm, in assignConstantRep()
112 bool TheoryEngineModelBuilder::isExcludedCdtValue( in isExcludedCdtValue()
144 bool TheoryEngineModelBuilder::isCdtValueMatch(Node v, in isCdtValueMatch()
184 bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) in involvesUSort()
210 bool TheoryEngineModelBuilder::isExcludedUSortValue( in isExcludedUSortValue()
242 void TheoryEngineModelBuilder::addToTypeList( in addToTypeList()
284 bool TheoryEngineModelBuilder::buildModel(Model* m) in buildModel()
[all …]
H A Dtheory_model_builder.h41 class TheoryEngineModelBuilder : public ModelBuilder
47 TheoryEngineModelBuilder(TheoryEngine* te);
48 virtual ~TheoryEngineModelBuilder() {} in ~TheoryEngineModelBuilder()
H A Dtheory_engine.h87 class TheoryEngineModelBuilder; variable
215 theory::TheoryEngineModelBuilder* d_curr_model_builder;
782 theory::TheoryEngineModelBuilder* getModelBuilder() { return d_curr_model_builder; } in getModelBuilder()
H A Dtheory_model.h80 friend class TheoryEngineModelBuilder; variable
H A Dtheory_engine.cpp243 d_curr_model_builder = new theory::TheoryEngineModelBuilder(this); in finishInit()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/
H A Dmodel_builder.h29 class QModelBuilder : public TheoryEngineModelBuilder
H A Dmodel_builder.cpp39 : TheoryEngineModelBuilder(qe->getTheoryEngine()), in QModelBuilder()
H A Dfull_model_check.cpp513 return TheoryEngineModelBuilder::processBuildModel( m ); in processBuildModel()