Searched refs:FirstOrderModel (Results 1 – 11 of 11) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | first_order_model.cpp | 36 FirstOrderModel * d_fm;
125 FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) : in FirstOrderModel() function in CVC4::theory::quantifiers::FirstOrderModel
131 void FirstOrderModel::assertQuantifier( Node n ){ in assertQuantifier()
152 void FirstOrderModel::initialize() { in initialize()
229 bool FirstOrderModel::checkNeeded() { in checkNeeded()
233 void FirstOrderModel::reset_round() { in reset_round()
275 void FirstOrderModel::markRelevant( Node q ) { in markRelevant()
287 int FirstOrderModel::getRelevanceValue( Node q ) { in getRelevanceValue()
343 bool FirstOrderModel::isModelBasisTerm(Node n) in isModelBasisTerm()
348 Node FirstOrderModel::getModelBasisOpTerm(Node op) in getModelBasisOpTerm()
[all …]
|
| H A D | first_order_model.h | 87 class FirstOrderModel : public TheoryModel
90 FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
192 class FirstOrderModelFmc : public FirstOrderModel
|
| H A D | relevant_domain.cpp | 111 FirstOrderModel* fm = d_qe->getModel(); in compute()
|
| H A D | conjecture_generator.cpp | 524 quantifiers::FirstOrderModel* m = d_quantEngine->getModel(); in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | model_builder.cpp | 56 FirstOrderModel * fm = (FirstOrderModel*)m; in preProcessBuildModelStd()
102 FirstOrderModel* fm = (FirstOrderModel*)m; in debugModel()
|
| H A D | model_builder.h | 47 …virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; } in doExhaustiveInstantiation()
|
| H A D | model_engine.cpp | 80 FirstOrderModel* fm = d_quantEngine->getModel(); in check()
166 FirstOrderModel* fm = d_quantEngine->getModel(); in checkModel()
|
| H A D | full_model_check.h | 147 int doExhaustiveInstantiation(FirstOrderModel* fm,
|
| H A D | full_model_check.cpp | 580 int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { in doExhaustiveInstantiation()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | quantifiers_engine.h | 54 class FirstOrderModel; variable
125 quantifiers::FirstOrderModel* getModel() const;
334 std::unique_ptr<quantifiers::FirstOrderModel> d_model;
|
| H A D | quantifiers_engine.cpp | 254 new quantifiers::FirstOrderModel(this, c, "FirstOrderModel")); in QuantifiersEngine()
258 d_model.reset(new quantifiers::FirstOrderModel(this, c, "FirstOrderModel")); in QuantifiersEngine()
317 quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const in getModel()
|