GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/relevant_domain.h Lines: 12 12 100.0 %
Date: 2021-03-23 Branches: 1 2 50.0 %

Line Exec Source
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
1116
  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
5132
  class RDomain
66
  {
67
  public:
68
5132
    RDomain() : d_parent( NULL ) {}
69
    /** the set of terms in this relevant domain */
70
    std::vector< Node > d_terms;
71
    /** reset this object */
72
9899
    void reset()
73
    {
74
9899
      d_parent = NULL;
75
9899
      d_terms.clear();
76
9899
    }
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
416
    RDomainLit() : d_merge(false){
132
416
      d_rd[0] = NULL;
133
416
      d_rd[1] = NULL;
134
416
    }
135
416
    ~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 */