1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Mathias Preiner, Gereon Kremer
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
13 * Model Builder class.
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H
19 #define CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H
21 #include "expr/node.h"
22 #include "theory/quantifiers/inst_match.h"
23 #include "theory/theory_model_builder.h"
27 namespace quantifiers
{
29 class FirstOrderModel
;
30 class QuantifiersState
;
31 class QuantifiersRegistry
;
32 class QuantifiersInferenceManager
;
35 class QModelBuilder
: public TheoryEngineModelBuilder
38 // must call preProcessBuildModelStd
39 bool preProcessBuildModel(TheoryModel
* m
) override
;
40 bool preProcessBuildModelStd(TheoryModel
* m
);
41 /** number of lemmas generated while building model */
42 unsigned d_addedLemmas
;
43 unsigned d_triedLemmas
;
46 QModelBuilder(QuantifiersState
& qs
,
47 QuantifiersInferenceManager
& qim
,
48 QuantifiersRegistry
& qr
,
50 /** finish init, which sets the model object */
51 virtual void finishInit();
52 //do exhaustive instantiation
53 // 0 : failed, but resorting to true exhaustive instantiation may work
56 virtual int doExhaustiveInstantiation( FirstOrderModel
* fm
, Node f
, int effort
) { return false; }
57 //whether to construct model
58 virtual bool optUseModel();
60 void debugModel(TheoryModel
* m
) override
;
62 unsigned getNumAddedLemmas() { return d_addedLemmas
; }
63 unsigned getNumTriedLemmas() { return d_triedLemmas
; }
64 /** get the model we are using */
65 FirstOrderModel
* getModel();
68 /** The quantifiers state object */
69 QuantifiersState
& d_qstate
;
70 /** The quantifiers inference manager */
71 QuantifiersInferenceManager
& d_qim
;
72 /** Reference to the quantifiers registry */
73 QuantifiersRegistry
& d_qreg
;
76 /** Pointer to the model object we are using */
77 FirstOrderModel
* d_model
;
78 /** The model object we have allocated */
79 std::unique_ptr
<FirstOrderModel
> d_modelAloc
;
82 } // namespace quantifiers
86 #endif /* CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H */