GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/candidate_rewrite_database.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file candidate_rewrite_database.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 candidate_rewrite_database
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
18
#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
19
20
#include <vector>
21
22
#include "theory/quantifiers/candidate_rewrite_filter.h"
23
#include "theory/quantifiers/expr_miner.h"
24
#include "theory/quantifiers/sygus_sampler.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace quantifiers {
29
30
/** CandidateRewriteDatabase
31
 *
32
 * This maintains the necessary data structures for generating a database
33
 * of candidate rewrite rules (see Noetzli et al "Syntax-Guided Rewrite Rule
34
 * Enumeration for SMT Solvers" SAT 2019). The primary responsibilities
35
 * of this class are to perform the "equivalence checking" and "congruence
36
 * and matching filtering" in Figure 1. The equivalence checking is done
37
 * through a combination of the sygus sampler object owned by this class
38
 * and the calls made to copies of the SmtEngine in ::addTerm. The rewrite
39
 * rule filtering (based on congruence, matching, variable ordering) is also
40
 * managed by the sygus sampler object.
41
 */
42
class CandidateRewriteDatabase : public ExprMiner
43
{
44
 public:
45
  /**
46
   * Constructor
47
   * @param doCheck Whether to check rewrite rules using subsolvers.
48
   * @param rewAccel Whether to construct symmetry breaking lemmas based on
49
   * discovered rewrites (see option sygusRewSynthAccel()).
50
   * @param silent Whether to silence the output of rewrites discovered by this
51
   * class.
52
   * @param filterPairs Whether to filter rewrite pairs using filtering
53
   * techniques from the SAT 2019 paper above.
54
   */
55
  CandidateRewriteDatabase(bool doCheck,
56
                           bool rewAccel = false,
57
                           bool silent = false,
58
                           bool filterPairs = true);
59
12
  ~CandidateRewriteDatabase() {}
60
  /**  Initialize this class */
61
  void initialize(const std::vector<Node>& var,
62
                  SygusSampler* ss = nullptr) override;
63
  /**  Initialize this class
64
   *
65
   * Serves the same purpose as the above function, but we will be using
66
   * sygus to enumerate terms and generate samples.
67
   *
68
   * qe : pointer to quantifiers engine. We use the sygus term database of this
69
   * quantifiers engine, and the extended rewriter of the corresponding term
70
   * database when computing candidate rewrites,
71
   * f : a term of some SyGuS datatype type whose values we will be
72
   * testing under the free variables in the grammar of f. This is the
73
   * "candidate variable" CegConjecture::d_candidates.
74
   */
75
  void initializeSygus(const std::vector<Node>& vars,
76
                       QuantifiersEngine* qe,
77
                       Node f,
78
                       SygusSampler* ss = nullptr);
79
  /** add term
80
   *
81
   * Notifies this class that the solution sol was enumerated. This may
82
   * cause a candidate-rewrite to be printed on the output stream out.
83
   *
84
   * @param sol The term to add to this class.
85
   * @param rec If true, then we also recursively add all subterms of sol
86
   * to this class as well.
87
   * @param out The stream to output rewrite rules on.
88
   * @param rew_print Set to true if this class printed a rewrite involving sol.
89
   * @return A previous term eq_sol added to this class, such that sol is
90
   * equivalent to eq_sol based on the criteria used by this class.
91
   */
92
  Node addTerm(Node sol, bool rec, std::ostream& out, bool& rew_print);
93
  Node addTerm(Node sol, bool rec, std::ostream& out);
94
  /**
95
   * Same as above, returns true if the return value of addTerm was equal to
96
   * sol, in other words, sol was a new unique term. This assumes false for
97
   * the argument rec.
98
   */
99
  bool addTerm(Node sol, std::ostream& out) override;
100
  /** sets whether this class should output candidate rewrites it finds */
101
  void setSilent(bool flag);
102
  /** set the (extended) rewriter used by this class */
103
  void setExtendedRewriter(ExtendedRewriter* er);
104
105
 private:
106
  /** reference to quantifier engine */
107
  QuantifiersEngine* d_qe;
108
  /** (required) pointer to the sygus term database of d_qe */
109
  TermDbSygus* d_tds;
110
  /** an extended rewriter object */
111
  ExtendedRewriter* d_ext_rewrite;
112
  /** the function-to-synthesize we are testing (if sygus) */
113
  Node d_candidate;
114
  /** whether we are checking equivalence using subsolver */
115
  bool d_doCheck;
116
  /**
117
   * If true, we use acceleration for symmetry breaking rewrites (see option
118
   * sygusRewSynthAccel()).
119
   */
120
  bool d_rewAccel;
121
  /** if true, we silence the output of candidate rewrites */
122
  bool d_silent;
123
  /** if true, we filter pairs of terms to check equivalence */
124
  bool d_filterPairs;
125
  /** whether we are using sygus */
126
  bool d_using_sygus;
127
  /** candidate rewrite filter */
128
  CandidateRewriteFilter d_crewrite_filter;
129
  /** the cache for results of addTerm */
130
  std::unordered_map<Node, Node, NodeHashFunction> d_add_term_cache;
131
};
132
133
} /* CVC4::theory::quantifiers namespace */
134
} /* CVC4::theory namespace */
135
} /* CVC4 namespace */
136
137
#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */