src/theory/quantifiers/relevant_domain.h

   1 /*********************                                                        */
   2 /*! \file relevant_domain.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner
   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 relevant domain class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
  18 #define CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
  19
  20 #include "theory/quantifiers/first_order_model.h"
  21 #include "theory/quantifiers/quant_util.h"
  22
  23 namespace CVC4 {
  24 namespace theory {
  25 namespace quantifiers {
  26
  27 class QuantifiersRegistry;
  28
  29 /** Relevant Domain
  30  *
  31  * This class computes the relevant domain of
  32  * functions and quantified formulas based on
  33  * techniques from "Complete Instantiation for Quantified
  34  * Formulas in SMT" by Ge et al., CAV 2009.
  35  *
  36  * Calling compute() will compute a representation
  37  * of relevant domain information, which be accessed
  38  * by getRDomain(...) calls. It is intended to be called
  39  * at full effort check, after we have initialized
  40  * the term database.
  41  */
  42 class RelevantDomain : public QuantifiersUtil
  43 {
  44  public:
  45   RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr);
  46   virtual ~RelevantDomain();
  47   /** Reset. */
  48   bool reset(Theory::Effort e) override;
  49   /** Register the quantified formula q */
  50   void registerQuantifier(Node q) override;
  51   /** identify */
  52   std::string identify() const override { return "RelevantDomain"; }
  53   /** Compute the relevant domain */
  54   void compute();
  55   /** Relevant domain representation.
  56    *
  57    * This data structure is inspired by the paper
  58    * "Complete Instantiation for Quantified Formulas in SMT" by
  59    * Ge et al., CAV 2009.
  60    * Notice that relevant domains may be equated to one another,
  61    * for example, if the quantified formula forall x. P( x, x )
  62    * exists in the current context, then the relevant domain of
  63    * arguments 1 and 2 of P are equated.
  64    */
  65   class RDomain
  66   {
  67   public:
  68     RDomain() : d_parent( NULL ) {}
  69     /** the set of terms in this relevant domain */
  70     std::vector< Node > d_terms;
  71     /** reset this object */
  72     void reset()
  73     {
  74       d_parent = NULL;
  75       d_terms.clear();
  76     }
  77     /** merge this with r
  78      * This sets d_parent of this to r and
  79      * copies the terms of this to r.
  80      */
  81     void merge( RDomain * r );
  82     /** add term to the relevant domain */
  83     void addTerm( Node t );
  84     /** get the parent of this */
  85     RDomain * getParent();
  86     /** remove redundant terms for d_terms, removes
  87      * duplicates modulo equality.
  88      */
  89     void removeRedundantTerms(QuantifiersState& qs);
  90     /** is n in this relevant domain? */
  91     bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); }
  92
  93    private:
  94     /** the parent of this relevant domain */
  95     RDomain* d_parent;
  96   };
  97   /** get the relevant domain
  98    *
  99    * Gets object representing the relevant domain of the i^th argument of n.
 100    *
 101    * If getParent is true, we return the representative
 102    * of the equivalence class of relevant domain objects,
 103    * which is computed as a union find (see RDomain::d_parent).
 104    */
 105   RDomain* getRDomain(Node n, int i, bool getParent = true);
 106
 107  private:
 108   /** the relevant domains for each quantified formula and function,
 109    * for each variable # and argument #.
 110    */
 111   std::map< Node, std::map< int, RDomain * > > d_rel_doms;
 112   /** stores the function or quantified formula associated with
 113    * each relevant domain object.
 114    */
 115   std::map< RDomain *, Node > d_rn_map;
 116   /** stores the argument or variable number associated with
 117    * each relevant domain object.
 118    */
 119   std::map< RDomain *, int > d_ri_map;
 120   /** Quantifiers engine associated with this utility. */
 121   QuantifiersEngine* d_qe;
 122   /** The quantifiers registry */
 123   QuantifiersRegistry& d_qreg;
 124   /** have we computed the relevant domain on this full effort check? */
 125   bool d_is_computed;
 126   /** relevant domain literal
 127    * Caches the effect of literals on the relevant domain.
 128    */
 129   class RDomainLit {
 130   public:
 131     RDomainLit() : d_merge(false){
 132       d_rd[0] = NULL;
 133       d_rd[1] = NULL;
 134     }
 135     ~RDomainLit(){}
 136     /** whether this literal forces the merge of two relevant domains */
 137     bool d_merge;
 138     /** the relevant domains that are merged as a result
 139      * of this literal
 140      */
 141     RDomain * d_rd[2];
 142     /** the terms that are added to
 143      * the relevant domain as a result of this literal
 144      */
 145     std::vector< Node > d_val;
 146   };
 147   /** Cache of the effect of literals on the relevant domain */
 148   std::map< bool, std::map< bool, std::map< Node, RDomainLit > > > d_rel_dom_lit;
 149   /** Compute the relevant domain for a subformula n of q,
 150    * whose polarity is given by hasPol/pol.
 151    */
 152   void computeRelevantDomain(Node q, Node n, bool hasPol, bool pol);
 153   /** Compute the relevant domain when the term n
 154    * is in a position to be included in relevant domain rf.
 155    */
 156   void computeRelevantDomainOpCh(RDomain* rf, Node n);
 157   /** compute relevant domain for literal.
 158    *
 159    * Updates the relevant domains based on a literal n in quantified
 160    * formula q whose polarity is given by hasPol/pol.
 161    */
 162   void computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n );
 163 };/* class RelevantDomain */
 164
 165
 166 }/* CVC4::theory::quantifiers namespace */
 167 }/* CVC4::theory namespace */
 168 }/* CVC4 namespace */
 169
 170 #endif /* CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */