1 /*********************                                                        */
2 /*! \file model_builder.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Andrew Reynolds, Morgan Deters, Mathias Preiner
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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.\endverbatim
11  **
12  ** \brief Model Builder class
13  **/
14 
15 #include "cvc4_private.h"
16 
17 #ifndef __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
18 #define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
19 
20 #include "theory/quantifiers_engine.h"
21 #include "theory/theory_model_builder.h"
22 #include "theory/uf/theory_uf_model.h"
23 
24 namespace CVC4 {
25 namespace theory {
26 namespace quantifiers {
27 
28 
29 class QModelBuilder : public TheoryEngineModelBuilder
30 {
31 protected:
32   //quantifiers engine
33   QuantifiersEngine* d_qe;
34   // must call preProcessBuildModelStd
35   bool preProcessBuildModel(TheoryModel* m) override;
36   bool preProcessBuildModelStd(TheoryModel* m);
37   /** number of lemmas generated while building model */
38   unsigned d_addedLemmas;
39   unsigned d_triedLemmas;
40 public:
41   QModelBuilder( context::Context* c, QuantifiersEngine* qe );
42 
43   //do exhaustive instantiation
44   // 0 :  failed, but resorting to true exhaustive instantiation may work
45   // >0 : success
46   // <0 : failed
doExhaustiveInstantiation(FirstOrderModel * fm,Node f,int effort)47   virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
48   //whether to construct model
49   virtual bool optUseModel();
50   /** exist instantiation ? */
51   virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
52   //debug model
53   void debugModel(TheoryModel* m) override;
54   //statistics
getNumAddedLemmas()55   unsigned getNumAddedLemmas() { return d_addedLemmas; }
getNumTriedLemmas()56   unsigned getNumTriedLemmas() { return d_triedLemmas; }
57 };
58 
59 }/* CVC4::theory::quantifiers namespace */
60 }/* CVC4::theory namespace */
61 }/* CVC4 namespace */
62 
63 #endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */
64