src/theory/quantifiers/first_order_model.h

   1 /*********************                                                        */
   2 /*! \file first_order_model.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King, Paul Meng
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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 extended classes
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__FIRST_ORDER_MODEL_H
  18 #define __CVC4__FIRST_ORDER_MODEL_H
  19
  20 #include "theory/theory_model.h"
  21 #include "theory/uf/theory_uf_model.h"
  22 #include "expr/attribute.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 class QuantifiersEngine;
  28
  29 struct ModelBasisAttributeId
  30 {
  31 };
  32 typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
  33 // for APPLY_UF terms, 1 : term has direct child with model basis attribute,
  34 //                     0 : term has no direct child with model basis attribute.
  35 struct ModelBasisArgAttributeId
  36 {
  37 };
  38 typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t>
  39     ModelBasisArgAttribute;
  40
  41 namespace quantifiers {
  42
  43 class TermDb;
  44
  45 class FirstOrderModelIG;
  46
  47 namespace fmcheck {
  48   class FirstOrderModelFmc;
  49 }/* CVC4::theory::quantifiers::fmcheck namespace */
  50
  51 class FirstOrderModelQInt;
  52 class FirstOrderModelAbs;
  53
  54 struct IsStarAttributeId {};
  55 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
  56
  57 /** Quantifiers representative bound
  58  *
  59  * This class is used for computing (finite)
  60  * bounds for the domain of a quantifier
  61  * in the context of a RepSetIterator
  62  * (see theory/rep_set.h).
  63  */
  64 class QRepBoundExt : public RepBoundExt
  65 {
  66  public:
  67   QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
  68   virtual ~QRepBoundExt() {}
  69   /** set bound */
  70   RepSetIterator::RsiEnumType setBound(Node owner,
  71                                        unsigned i,
  72                                        std::vector<Node>& elements) override;
  73   /** reset index */
  74   bool resetIndex(RepSetIterator* rsi,
  75                   Node owner,
  76                   unsigned i,
  77                   bool initial,
  78                   std::vector<Node>& elements) override;
  79   /** initialize representative set for type */
  80   bool initializeRepresentativesForType(TypeNode tn) override;
  81   /** get variable order */
  82   bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
  83
  84  private:
  85   /** quantifiers engine associated with this bound */
  86   QuantifiersEngine* d_qe;
  87   /** indices that are bound integer enumeration */
  88   std::map<unsigned, bool> d_bound_int;
  89 };
  90
  91 // TODO (#1301) : document and refactor this class
  92 class FirstOrderModel : public TheoryModel
  93 {
  94  public:
  95   FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
  96
  97   virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; }
  98   virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
  99   virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; }
 100   virtual FirstOrderModelAbs* asFirstOrderModelAbs() { return nullptr; }
 101   /** assert quantifier */
 102   void assertQuantifier( Node n );
 103   /** get number of asserted quantifiers */
 104   unsigned getNumAssertedQuantifiers();
 105   /** get asserted quantifier */
 106   Node getAssertedQuantifier( unsigned i, bool ordered = false );
 107   /** initialize model for term */
 108   void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
 109   // initialize the model
 110   void initialize();
 111   /** get variable id */
 112   int getVariableId(TNode q, TNode n) {
 113     return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
 114   }
 115   /** do we need to do any work? */
 116   bool checkNeeded();
 117   /** reset round */
 118   void reset_round();
 119   /** mark quantified formula relevant */
 120   void markRelevant( Node q );
 121   /** get relevance value */
 122   int getRelevanceValue( Node q );
 123   /** set quantified formula active/inactive
 124    * a quantified formula may be set inactive if for instance:
 125    *   - it is entailed by other quantified formulas
 126    */
 127   void setQuantifierActive( TNode q, bool active );
 128   /** is quantified formula active */
 129   bool isQuantifierActive( TNode q );
 130   /** is quantified formula asserted */
 131   bool isQuantifierAsserted( TNode q );
 132   /** get model basis term */
 133   Node getModelBasisTerm(TypeNode tn);
 134   /** is model basis term */
 135   bool isModelBasisTerm(Node n);
 136   /** get model basis term for op */
 137   Node getModelBasisOpTerm(Node op);
 138   /** get model basis */
 139   Node getModelBasis(Node q, Node n);
 140   /** get model basis arg */
 141   unsigned getModelBasisArg(Node n);
 142   /** get some domain element */
 143   Node getSomeDomainElement(TypeNode tn);
 144   /** initialize representative set for type
 145    *
 146    * This ensures that TheoryModel::d_rep_set
 147    * is initialized for type tn. In particular:
 148    * (1) If tn is an uninitialized (unconstrained)
 149    * uninterpreted sort, then we interpret it
 150    * as a set of size one,
 151    * (2) If tn is a "small" enumerable finite type,
 152    * then we ensure that all its values are in
 153    * TheoryModel::d_rep_set.
 154    *
 155    * Returns true if the initialization was complete,
 156    * in that the set for tn in TheoryModel::d_rep_set
 157    * has all representatives of type tn.
 158    */
 159   bool initializeRepresentativesForType(TypeNode tn);
 160
 161  protected:
 162   /** quant engine */
 163   QuantifiersEngine* d_qe;
 164   /** list of quantifiers asserted in the current context */
 165   context::CDList<Node> d_forall_asserts;
 166   /** quantified formulas marked as relevant */
 167   unsigned d_rlv_count;
 168   std::map<Node, unsigned> d_forall_rlv;
 169   std::vector<Node> d_forall_rlv_vec;
 170   Node d_last_forall_rlv;
 171   std::vector<Node> d_forall_rlv_assert;
 172   /** get variable id */
 173   std::map<Node, std::map<Node, int> > d_quant_var_id;
 174   /** process initialize model for term */
 175   virtual void processInitializeModelForTerm(Node n) = 0;
 176   /** process intialize quantifier */
 177   virtual void processInitializeQuantifier(Node q) {}
 178   /** process initialize */
 179   virtual void processInitialize(bool ispre) = 0;
 180
 181  private:
 182   // list of inactive quantified formulas
 183   std::map<TNode, bool> d_quant_active;
 184   /** map from types to model basis terms */
 185   std::map<TypeNode, Node> d_model_basis_term;
 186   /** map from ops to model basis terms */
 187   std::map<Node, Node> d_model_basis_op_term;
 188   /** map from instantiation terms to their model basis equivalent */
 189   std::map<Node, Node> d_model_basis_body;
 190   /** map from universal quantifiers to model basis terms */
 191   std::map<Node, std::vector<Node> > d_model_basis_terms;
 192   /** compute model basis arg */
 193   void computeModelBasisArgAttribute(Node n);
 194 };/* class FirstOrderModel */
 195
 196
 197 class FirstOrderModelIG : public FirstOrderModel
 198 {
 199 public: //for Theory UF:
 200   //models for each UF operator
 201   std::map< Node, uf::UfModelTree > d_uf_model_tree;
 202   //model generators
 203   std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
 204 private:
 205   //map from terms to the models used to calculate their value
 206   std::map< Node, bool > d_eval_uf_use_default;
 207   std::map< Node, uf::UfModelTree > d_eval_uf_model;
 208   void makeEvalUfModel( Node n );
 209   //index ordering to use for each term
 210   std::map< Node, std::vector< int > > d_eval_term_index_order;
 211   void makeEvalUfIndexOrder( Node n );
 212 //the following functions are for evaluating quantifier bodies
 213 public:
 214   FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
 215
 216   FirstOrderModelIG* asFirstOrderModelIG() override { return this; }
 217   // initialize the model
 218   void processInitialize(bool ispre) override;
 219   //for initialize model
 220   void processInitializeModelForTerm(Node n) override;
 221   /** reset evaluation */
 222   void resetEvaluate();
 223   /** evaluate functions */
 224   int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
 225   Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
 226 public:
 227   //statistics
 228   int d_eval_formulas;
 229   int d_eval_uf_terms;
 230   int d_eval_lits;
 231   int d_eval_lits_unknown;
 232 private:
 233   //default evaluate term function
 234   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
 235 };/* class FirstOrderModelIG */
 236
 237
 238 namespace fmcheck {
 239
 240 class Def;
 241
 242 class FirstOrderModelFmc : public FirstOrderModel
 243 {
 244   friend class FullModelChecker;
 245
 246  private:
 247   /** models for UF */
 248   std::map<Node, Def * > d_models;
 249   std::map<TypeNode, Node > d_type_star;
 250   /** get current model value */
 251   void processInitializeModelForTerm(Node n) override;
 252
 253  public:
 254   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
 255   ~FirstOrderModelFmc() override;
 256   FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
 257   // initialize the model
 258   void processInitialize(bool ispre) override;
 259   Node getFunctionValue(Node op, const char* argPrefix );
 260
 261   bool isStar(Node n);
 262   Node getStar(TypeNode tn);
 263 };/* class FirstOrderModelFmc */
 264
 265 }/* CVC4::theory::quantifiers::fmcheck namespace */
 266
 267 class AbsDef;
 268
 269 class FirstOrderModelAbs : public FirstOrderModel
 270 {
 271  public:
 272   std::map< Node, AbsDef * > d_models;
 273   std::map< Node, bool > d_models_valid;
 274   std::map< TNode, unsigned > d_rep_id;
 275   std::map< TypeNode, unsigned > d_domain;
 276   std::map< Node, std::vector< int > > d_var_order;
 277   std::map< Node, std::map< int, int > > d_var_index;
 278
 279  private:
 280   /** get current model value */
 281   void processInitializeModelForTerm(Node n) override;
 282   void processInitializeQuantifier(Node q) override;
 283   void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
 284   TNode getUsedRepresentative( TNode n );
 285
 286  public:
 287   FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
 288   ~FirstOrderModelAbs() override;
 289   FirstOrderModelAbs* asFirstOrderModelAbs() override { return this; }
 290   void processInitialize(bool ispre) override;
 291   unsigned getRepresentativeId( TNode n );
 292   bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
 293   Node getFunctionValue(Node op, const char* argPrefix );
 294   Node getVariable( Node q, unsigned i );
 295 };
 296
 297 }/* CVC4::theory::quantifiers namespace */
 298 }/* CVC4::theory namespace */
 299 }/* CVC4 namespace */
 300
 301 #endif /* __CVC4__FIRST_ORDER_MODEL_H */