diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-27 22:01:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-27 22:01:03 +0000 |
commit | 485c03a323911142e460bd0a7c428759496dc631 (patch) | |
tree | 8c512712734dd2862c89acd8681357d0a2e0dabe /src/theory/quantifiers/model_builder.h | |
parent | 33fd76601b42599d9883889a03d59d0d85729661 (diff) |
Minor cleanup after today's commits:
* change some uses of "std::cout" to "Message()"
* change some files to use Unix newlines instead of DOS newlines
* fix compiler warning
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 182 |
1 files changed, 91 insertions, 91 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 13d500d8e..05eb8f55f 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -1,91 +1,91 @@ -/********************* */
-/*! \file model_builder.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Model Builder class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H
-#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/model.h"
-#include "theory/uf/theory_uf_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-//the model builder
-class ModelEngineBuilder : public TheoryEngineModelBuilder
-{
-protected:
- //quantifiers engine
- QuantifiersEngine* d_qe;
- //map from operators to model preference data
- std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
- //built model uf
- std::map< Node, bool > d_uf_model_constructed;
- /** process build model */
- void processBuildModel( TheoryModel* m );
- /** choose representative for unconstrained equivalence class */
- Node chooseRepresentative( TheoryModel* m, Node eqc );
- /** bad representative */
- bool isBadRepresentative( Node n );
-protected:
- //analyze model
- void analyzeModel( FirstOrderModel* fm );
- //analyze quantifiers
- void analyzeQuantifiers( FirstOrderModel* fm );
- //build model
- void finishBuildModel( FirstOrderModel* fm );
- //theory-specific build models
- void finishBuildModelUf( FirstOrderModel* fm, Node op );
- //do InstGen techniques for quantifier, return number of lemmas produced
- int doInstGen( FirstOrderModel* fm, Node f );
-public:
- ModelEngineBuilder( QuantifiersEngine* qe );
- virtual ~ModelEngineBuilder(){}
- /** finish model */
- void finishProcessBuildModel( TheoryModel* m );
-public:
- /** number of lemmas generated while building model */
- int d_addedLemmas;
- //map from quantifiers to if are constant SAT
- std::map< Node, bool > d_quant_sat;
- //map from quantifiers to the instantiation literals that their model is dependent upon
- std::map< Node, std::vector< Node > > d_quant_selection_lits;
-public:
- //map from quantifiers to model basis match
- std::map< Node, InstMatch > d_quant_basis_match;
- //options
- bool optUseModel();
- bool optInstGen();
- bool optOneQuantPerRoundInstGen();
- /** statistics class */
- class Statistics {
- public:
- IntStat d_pre_sat_quant;
- IntStat d_pre_nsat_quant;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
-};
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file model_builder.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Model Builder class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H +#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H + +#include "theory/quantifiers_engine.h" +#include "theory/model.h" +#include "theory/uf/theory_uf_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +//the model builder +class ModelEngineBuilder : public TheoryEngineModelBuilder +{ +protected: + //quantifiers engine + QuantifiersEngine* d_qe; + //map from operators to model preference data + std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; + //built model uf + std::map< Node, bool > d_uf_model_constructed; + /** process build model */ + void processBuildModel( TheoryModel* m ); + /** choose representative for unconstrained equivalence class */ + Node chooseRepresentative( TheoryModel* m, Node eqc ); + /** bad representative */ + bool isBadRepresentative( Node n ); +protected: + //analyze model + void analyzeModel( FirstOrderModel* fm ); + //analyze quantifiers + void analyzeQuantifiers( FirstOrderModel* fm ); + //build model + void finishBuildModel( FirstOrderModel* fm ); + //theory-specific build models + void finishBuildModelUf( FirstOrderModel* fm, Node op ); + //do InstGen techniques for quantifier, return number of lemmas produced + int doInstGen( FirstOrderModel* fm, Node f ); +public: + ModelEngineBuilder( QuantifiersEngine* qe ); + virtual ~ModelEngineBuilder(){} + /** finish model */ + void finishProcessBuildModel( TheoryModel* m ); +public: + /** number of lemmas generated while building model */ + int d_addedLemmas; + //map from quantifiers to if are constant SAT + std::map< Node, bool > d_quant_sat; + //map from quantifiers to the instantiation literals that their model is dependent upon + std::map< Node, std::vector< Node > > d_quant_selection_lits; +public: + //map from quantifiers to model basis match + std::map< Node, InstMatch > d_quant_basis_match; + //options + bool optUseModel(); + bool optInstGen(); + bool optOneQuantPerRoundInstGen(); + /** statistics class */ + class Statistics { + public: + IntStat d_pre_sat_quant; + IntStat d_pre_nsat_quant; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; +}; + +} +} +} + +#endif |