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, Paul Meng, Morgan Deters
   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 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 "expr/attribute.h"
  21 #include "theory/theory_model.h"
  22 #include "theory/uf/theory_uf_model.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 namespace fmcheck {
  46   class FirstOrderModelFmc;
  47 }/* CVC4::theory::quantifiers::fmcheck namespace */
  48
  49 struct IsStarAttributeId {};
  50 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
  51
  52 /** Quantifiers representative bound
  53  *
  54  * This class is used for computing (finite)
  55  * bounds for the domain of a quantifier
  56  * in the context of a RepSetIterator
  57  * (see theory/rep_set.h).
  58  */
  59 class QRepBoundExt : public RepBoundExt
  60 {
  61  public:
  62   QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
  63   virtual ~QRepBoundExt() {}
  64   /** set bound */
  65   RepSetIterator::RsiEnumType setBound(Node owner,
  66                                        unsigned i,
  67                                        std::vector<Node>& elements) override;
  68   /** reset index */
  69   bool resetIndex(RepSetIterator* rsi,
  70                   Node owner,
  71                   unsigned i,
  72                   bool initial,
  73                   std::vector<Node>& elements) override;
  74   /** initialize representative set for type */
  75   bool initializeRepresentativesForType(TypeNode tn) override;
  76   /** get variable order */
  77   bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
  78
  79  private:
  80   /** quantifiers engine associated with this bound */
  81   QuantifiersEngine* d_qe;
  82   /** indices that are bound integer enumeration */
  83   std::map<unsigned, bool> d_bound_int;
  84 };
  85
  86 // TODO (#1301) : document and refactor this class
  87 class FirstOrderModel : public TheoryModel
  88 {
  89  public:
  90   FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
  91
  92   virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
  93   /** assert quantifier */
  94   void assertQuantifier( Node n );
  95   /** get number of asserted quantifiers */
  96   unsigned getNumAssertedQuantifiers();
  97   /** get asserted quantifier */
  98   Node getAssertedQuantifier( unsigned i, bool ordered = false );
  99   /** initialize model for term */
 100   void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
 101   // initialize the model
 102   void initialize();
 103   /** get variable id */
 104   int getVariableId(TNode q, TNode n) {
 105     return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
 106   }
 107   /** do we need to do any work? */
 108   bool checkNeeded();
 109   /** reset round */
 110   void reset_round();
 111   /** mark quantified formula relevant */
 112   void markRelevant( Node q );
 113   /** set quantified formula active/inactive
 114    *
 115    * This indicates that quantified formula is "inactive", that is, it need
 116    * not be considered during this instantiation round.
 117    *
 118    * A quantified formula may be set inactive if for instance:
 119    *   - It is entailed by other quantified formulas, or
 120    *   - All of its instances are known to be true in the current model.
 121    *
 122    * This method should be called after a call to FirstOrderModel::reset_round,
 123    * and before calls to QuantifiersModule check calls. A common place to call
 124    * this method is during QuantifiersModule reset_round calls.
 125    */
 126   void setQuantifierActive( TNode q, bool active );
 127   /** is quantified formula active?
 128    *
 129    * Returns false if there has been a call to setQuantifierActive( q, false )
 130    * during this instantiation round.
 131    */
 132   bool isQuantifierActive(TNode q) const;
 133   /** is quantified formula asserted */
 134   bool isQuantifierAsserted(TNode q) const;
 135   /** get model basis term */
 136   Node getModelBasisTerm(TypeNode tn);
 137   /** is model basis term */
 138   bool isModelBasisTerm(Node n);
 139   /** get model basis term for op */
 140   Node getModelBasisOpTerm(Node op);
 141   /** get model basis */
 142   Node getModelBasis(Node q, Node n);
 143   /** get model basis arg */
 144   unsigned getModelBasisArg(Node n);
 145   /** get some domain element */
 146   Node getSomeDomainElement(TypeNode tn);
 147   /** initialize representative set for type
 148    *
 149    * This ensures that TheoryModel::d_rep_set
 150    * is initialized for type tn. In particular:
 151    * (1) If tn is an uninitialized (unconstrained)
 152    * uninterpreted sort, then we interpret it
 153    * as a set of size one,
 154    * (2) If tn is a "small" enumerable finite type,
 155    * then we ensure that all its values are in
 156    * TheoryModel::d_rep_set.
 157    *
 158    * Returns true if the initialization was complete,
 159    * in that the set for tn in TheoryModel::d_rep_set
 160    * has all representatives of type tn.
 161    */
 162   bool initializeRepresentativesForType(TypeNode tn);
 163
 164  protected:
 165   /** quant engine */
 166   QuantifiersEngine* d_qe;
 167   /** list of quantifiers asserted in the current context */
 168   context::CDList<Node> d_forall_asserts;
 169   /** quantified formulas marked as relevant */
 170   std::vector<Node> d_forall_rlv_vec;
 171   Node d_last_forall_rlv;
 172   std::vector<Node> d_forall_rlv_assert;
 173   /** get variable id */
 174   std::map<Node, std::map<Node, int> > d_quant_var_id;
 175   /** process initialize model for term */
 176   virtual void processInitializeModelForTerm(Node n) {}
 177   /** process initialize quantifier */
 178   virtual void processInitializeQuantifier(Node q) {}
 179   /** process initialize */
 180   virtual void processInitialize(bool ispre) {}
 181
 182  private:
 183   // list of inactive quantified formulas
 184   std::map<TNode, bool> d_quant_active;
 185   /** map from types to model basis terms */
 186   std::map<TypeNode, Node> d_model_basis_term;
 187   /** map from ops to model basis terms */
 188   std::map<Node, Node> d_model_basis_op_term;
 189   /** map from instantiation terms to their model basis equivalent */
 190   std::map<Node, Node> d_model_basis_body;
 191   /** map from universal quantifiers to model basis terms */
 192   std::map<Node, std::vector<Node> > d_model_basis_terms;
 193   /** compute model basis arg */
 194   void computeModelBasisArgAttribute(Node n);
 195 };/* class FirstOrderModel */
 196
 197 namespace fmcheck {
 198
 199 class Def;
 200
 201 class FirstOrderModelFmc : public FirstOrderModel
 202 {
 203   friend class FullModelChecker;
 204
 205  private:
 206   /** models for UF */
 207   std::map<Node, Def * > d_models;
 208   std::map<TypeNode, Node > d_type_star;
 209   /** get current model value */
 210   void processInitializeModelForTerm(Node n) override;
 211
 212  public:
 213   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
 214   ~FirstOrderModelFmc() override;
 215   FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
 216   // initialize the model
 217   void processInitialize(bool ispre) override;
 218   Node getFunctionValue(Node op, const char* argPrefix );
 219
 220   bool isStar(Node n);
 221   Node getStar(TypeNode tn);
 222 };/* class FirstOrderModelFmc */
 223
 224 }/* CVC4::theory::quantifiers::fmcheck namespace */
 225
 226 }/* CVC4::theory::quantifiers namespace */
 227 }/* CVC4::theory namespace */
 228 }/* CVC4 namespace */
 229
 230 #endif /* CVC4__FIRST_ORDER_MODEL_H */