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