diff options
Diffstat (limited to 'src/theory/quantifiers/model_engine.h')
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 67 |
1 files changed, 6 insertions, 61 deletions
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index b01139826..1139332fe 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -11,81 +11,25 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Model Engine classes + ** \brief Model Engine class **/ #include "cvc4_private.h" -#ifndef __CVC4__MODEL_ENGINE_H -#define __CVC4__MODEL_ENGINE_H +#ifndef __CVC4__QUANTIFIERS_MODEL_ENGINE_H +#define __CVC4__QUANTIFIERS_MODEL_ENGINE_H #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers/model_builder.h" #include "theory/model.h" -#include "theory/uf/theory_uf_model.h" #include "theory/quantifiers/relevant_domain.h" namespace CVC4 { namespace theory { - -namespace uf{ - class StrongSolverTheoryUf; -} - 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; - /** choose representative */ - Node chooseRepresentative( TheoryModel* tm, Node eqc ); - /** use constants for representatives */ - void processBuildModel( TheoryModel* m ); - //analyze quantifiers - void analyzeQuantifiers( FirstOrderModel* fm ); - //build model - void finishBuildModel( FirstOrderModel* fm ); - //theory-specific build models - void finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model ); - //do InstGen techniques for quantifier, return number of lemmas produced - int doInstGen( FirstOrderModel* fm, Node f ); -public: - ModelEngineBuilder( QuantifiersEngine* qe ); - virtual ~ModelEngineBuilder(){} -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; -}; - class ModelEngine : public QuantifiersModule { - friend class uf::UfModel; friend class RepSetIterator; private: /** builder class */ @@ -128,8 +72,9 @@ public: public: IntStat d_inst_rounds; IntStat d_eval_formulas; - IntStat d_eval_eqs; IntStat d_eval_uf_terms; + IntStat d_eval_lits; + IntStat d_eval_lits_unknown; IntStat d_num_quants_init; IntStat d_num_quants_init_fail; Statistics(); |