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-2021 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 "context/cdlist.h"
  21 #include "expr/attribute.h"
  22 #include "theory/theory_model.h"
  23 #include "theory/uf/theory_uf_model.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 class QuantifiersEngine;
  29
  30 struct ModelBasisAttributeId
  31 {
  32 };
  33 typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
  34 // for APPLY_UF terms, 1 : term has direct child with model basis attribute,
  35 //                     0 : term has no direct child with model basis attribute.
  36 struct ModelBasisArgAttributeId
  37 {
  38 };
  39 typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t>
  40     ModelBasisArgAttribute;
  41
  42 namespace quantifiers {
  43
  44 class TermDb;
  45 class QuantifiersState;
  46 class QuantifiersRegistry;
  47
  48 namespace fmcheck {
  49   class FirstOrderModelFmc;
  50 }/* CVC4::theory::quantifiers::fmcheck namespace */
  51
  52 struct IsStarAttributeId {};
  53 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
  54
  55 // TODO (#1301) : document and refactor this class
  56 class FirstOrderModel : public TheoryModel
  57 {
  58  public:
  59   FirstOrderModel(QuantifiersEngine* qe,
  60                   QuantifiersState& qs,
  61                   QuantifiersRegistry& qr,
  62                   std::string name);
  63
  64   virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
  65   /** assert quantifier */
  66   void assertQuantifier( Node n );
  67   /** get number of asserted quantifiers */
  68   size_t getNumAssertedQuantifiers() const;
  69   /** get asserted quantifier */
  70   Node getAssertedQuantifier( unsigned i, bool ordered = false );
  71   /** initialize model for term */
  72   void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
  73   // initialize the model
  74   void initialize();
  75   /** get variable id */
  76   int getVariableId(TNode q, TNode n) {
  77     return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
  78   }
  79   /** do we need to do any work? */
  80   bool checkNeeded();
  81   /** reset round */
  82   void reset_round();
  83   /** mark quantified formula relevant */
  84   void markRelevant( Node q );
  85   /** set quantified formula active/inactive
  86    *
  87    * This indicates that quantified formula is "inactive", that is, it need
  88    * not be considered during this instantiation round.
  89    *
  90    * A quantified formula may be set inactive if for instance:
  91    *   - It is entailed by other quantified formulas, or
  92    *   - All of its instances are known to be true in the current model.
  93    *
  94    * This method should be called after a call to FirstOrderModel::reset_round,
  95    * and before calls to QuantifiersModule check calls. A common place to call
  96    * this method is during QuantifiersModule reset_round calls.
  97    */
  98   void setQuantifierActive( TNode q, bool active );
  99   /** is quantified formula active?
 100    *
 101    * Returns false if there has been a call to setQuantifierActive( q, false )
 102    * during this instantiation round.
 103    */
 104   bool isQuantifierActive(TNode q) const;
 105   /** is quantified formula asserted */
 106   bool isQuantifierAsserted(TNode q) const;
 107   /** get model basis term */
 108   Node getModelBasisTerm(TypeNode tn);
 109   /** is model basis term */
 110   bool isModelBasisTerm(Node n);
 111   /** get model basis term for op */
 112   Node getModelBasisOpTerm(Node op);
 113   /** get model basis */
 114   Node getModelBasis(Node q, Node n);
 115   /** get model basis arg */
 116   unsigned getModelBasisArg(Node n);
 117   /** get some domain element */
 118   Node getSomeDomainElement(TypeNode tn);
 119   /** initialize representative set for type
 120    *
 121    * This ensures that TheoryModel::d_rep_set
 122    * is initialized for type tn. In particular:
 123    * (1) If tn is an uninitialized (unconstrained)
 124    * uninterpreted sort, then we interpret it
 125    * as a set of size one,
 126    * (2) If tn is a "small" enumerable finite type,
 127    * then we ensure that all its values are in
 128    * TheoryModel::d_rep_set.
 129    *
 130    * Returns true if the initialization was complete,
 131    * in that the set for tn in TheoryModel::d_rep_set
 132    * has all representatives of type tn.
 133    */
 134   bool initializeRepresentativesForType(TypeNode tn);
 135
 136  protected:
 137   /** quant engine */
 138   QuantifiersEngine* d_qe;
 139   /** The quantifiers registry */
 140   QuantifiersRegistry& d_qreg;
 141   /** list of quantifiers asserted in the current context */
 142   context::CDList<Node> d_forall_asserts;
 143   /**
 144    * The (ordered) list of quantified formulas marked as relevant using
 145    * markRelevant, where the quantified formula q in the most recent
 146    * call to markRelevant comes last in the list.
 147    */
 148   std::vector<Node> d_forall_rlv_vec;
 149   /** The last quantified formula marked as relevant, if one exists. */
 150   Node d_last_forall_rlv;
 151   /**
 152    * The list of asserted quantified formulas, ordered by relevance.
 153    * Relevance is a dynamic partial ordering where q1 < q2 if there has been
 154    * a call to markRelevant( q1 ) after the last call to markRelevant( q2 )
 155    * (or no call to markRelevant( q2 ) has been made).
 156    *
 157    * This list is used primarily as an optimization for conflict-based
 158    * instantiation so that quantifed formulas that have been instantiated
 159    * most recently are processed first, since these are (statistically) more
 160    * likely to have conflicting instantiations.
 161    */
 162   std::vector<Node> d_forall_rlv_assert;
 163   /**
 164    * Whether the above list has been computed. This flag is updated during
 165    * reset_round and is valid within a full effort check.
 166    */
 167   bool d_forallRlvComputed;
 168   /** get variable id */
 169   std::map<Node, std::map<Node, int> > d_quant_var_id;
 170   /** process initialize model for term */
 171   virtual void processInitializeModelForTerm(Node n) {}
 172   /** process initialize quantifier */
 173   virtual void processInitializeQuantifier(Node q) {}
 174   /** process initialize */
 175   virtual void processInitialize(bool ispre) {}
 176
 177  private:
 178   // list of inactive quantified formulas
 179   std::map<TNode, bool> d_quant_active;
 180   /** map from types to model basis terms */
 181   std::map<TypeNode, Node> d_model_basis_term;
 182   /** map from ops to model basis terms */
 183   std::map<Node, Node> d_model_basis_op_term;
 184   /** map from instantiation terms to their model basis equivalent */
 185   std::map<Node, Node> d_model_basis_body;
 186   /** map from universal quantifiers to model basis terms */
 187   std::map<Node, std::vector<Node> > d_model_basis_terms;
 188   /** compute model basis arg */
 189   void computeModelBasisArgAttribute(Node n);
 190 };/* class FirstOrderModel */
 191
 192 }/* CVC4::theory::quantifiers namespace */
 193 }/* CVC4::theory namespace */
 194 }/* CVC4 namespace */
 195
 196 #endif /* CVC4__FIRST_ORDER_MODEL_H */