GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/expr_miner_manager.cpp Lines: 43 77 55.8 %
Date: 2021-03-22 Branches: 48 140 34.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file expr_miner_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Implementation of expression miner manager.
13
 **/
14
15
#include "theory/quantifiers/expr_miner_manager.h"
16
#include "theory/quantifiers_engine.h"
17
18
#include "options/quantifiers_options.h"
19
20
namespace CVC4 {
21
namespace theory {
22
namespace quantifiers {
23
24
12
ExpressionMinerManager::ExpressionMinerManager()
25
    : d_doRewSynth(false),
26
      d_doQueryGen(false),
27
      d_doFilterLogicalStrength(false),
28
      d_use_sygus_type(false),
29
      d_qe(nullptr),
30
      d_tds(nullptr),
31
24
      d_crd(options::sygusRewSynthCheck(), options::sygusRewSynthAccel(), false)
32
{
33
12
}
34
35
void ExpressionMinerManager::initialize(const std::vector<Node>& vars,
36
                                        TypeNode tn,
37
                                        unsigned nsamples,
38
                                        bool unique_type_ids)
39
{
40
  d_doRewSynth = false;
41
  d_doQueryGen = false;
42
  d_doFilterLogicalStrength = false;
43
  d_sygus_fun = Node::null();
44
  d_use_sygus_type = false;
45
  d_qe = nullptr;
46
  d_tds = nullptr;
47
  // initialize the sampler
48
  d_sampler.initialize(tn, vars, nsamples, unique_type_ids);
49
}
50
51
12
void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe,
52
                                             Node f,
53
                                             unsigned nsamples,
54
                                             bool useSygusType)
55
{
56
12
  d_doRewSynth = false;
57
12
  d_doQueryGen = false;
58
12
  d_doFilterLogicalStrength = false;
59
12
  d_sygus_fun = f;
60
12
  d_use_sygus_type = useSygusType;
61
12
  d_qe = qe;
62
12
  d_tds = qe->getTermDatabaseSygus();
63
  // initialize the sampler
64
12
  d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType);
65
12
}
66
67
8
void ExpressionMinerManager::enableRewriteRuleSynth()
68
{
69
8
  if (d_doRewSynth)
70
  {
71
    // already enabled
72
    return;
73
  }
74
8
  d_doRewSynth = true;
75
16
  std::vector<Node> vars;
76
8
  d_sampler.getVariables(vars);
77
  // initialize the candidate rewrite database
78
8
  if (!d_sygus_fun.isNull())
79
  {
80
8
    Assert(d_qe != nullptr);
81
8
    d_crd.initializeSygus(vars, d_qe, d_sygus_fun, &d_sampler);
82
  }
83
  else
84
  {
85
    d_crd.initialize(vars, &d_sampler);
86
  }
87
8
  d_crd.setExtendedRewriter(&d_ext_rew);
88
8
  d_crd.setSilent(false);
89
}
90
91
void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh)
92
{
93
  if (d_doQueryGen)
94
  {
95
    // already enabled
96
    return;
97
  }
98
  d_doQueryGen = true;
99
  std::vector<Node> vars;
100
  d_sampler.getVariables(vars);
101
  // must also enable rewrite rule synthesis
102
  if (!d_doRewSynth)
103
  {
104
    // initialize the candidate rewrite database, in silent mode
105
    enableRewriteRuleSynth();
106
    d_crd.setSilent(true);
107
  }
108
  // initialize the query generator
109
  d_qg.initialize(vars, &d_sampler);
110
  d_qg.setThreshold(deqThresh);
111
}
112
113
void ExpressionMinerManager::enableFilterWeakSolutions()
114
{
115
  d_doFilterLogicalStrength = true;
116
  std::vector<Node> vars;
117
  d_sampler.getVariables(vars);
118
  d_sols.initialize(vars, &d_sampler);
119
  d_sols.setLogicallyStrong(true);
120
}
121
122
4
void ExpressionMinerManager::enableFilterStrongSolutions()
123
{
124
4
  d_doFilterLogicalStrength = true;
125
8
  std::vector<Node> vars;
126
4
  d_sampler.getVariables(vars);
127
4
  d_sols.initialize(vars, &d_sampler);
128
4
  d_sols.setLogicallyStrong(false);
129
4
}
130
131
1489
bool ExpressionMinerManager::addTerm(Node sol,
132
                                     std::ostream& out,
133
                                     bool& rew_print)
134
{
135
  // set the builtin version
136
2978
  Node solb = sol;
137
1489
  if (d_use_sygus_type)
138
  {
139
1489
    solb = d_tds->sygusToBuiltin(sol);
140
  }
141
142
  // add to the candidate rewrite rule database
143
1489
  bool ret = true;
144
1489
  if (d_doRewSynth)
145
  {
146
4131
    Node rsol = d_crd.addTerm(sol, options::sygusRewSynthRec(), out, rew_print);
147
1377
    ret = (sol == rsol);
148
  }
149
150
  // a unique term, let's try the query generator
151
1489
  if (ret && d_doQueryGen)
152
  {
153
    d_qg.addTerm(solb, out);
154
  }
155
156
  // filter based on logical strength
157
1489
  if (ret && d_doFilterLogicalStrength)
158
  {
159
112
    ret = d_sols.addTerm(solb, out);
160
  }
161
2978
  return ret;
162
}
163
164
bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out)
165
{
166
  bool rew_print = false;
167
  return addTerm(sol, out, rew_print);
168
}
169
170
}  // namespace quantifiers
171
}  // namespace theory
172
28065
}  // namespace CVC4