GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_unif.cpp Lines: 53 58 91.4 %
Date: 2021-03-23 Branches: 49 140 35.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_unif.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Aina Niemetz, Haniel Barbosa
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 sygus_unif
13
 **/
14
15
#include "theory/quantifiers/sygus/sygus_unif.h"
16
17
#include "theory/quantifiers/sygus/term_database_sygus.h"
18
#include "theory/quantifiers/term_util.h"
19
#include "theory/quantifiers_engine.h"
20
#include "util/random.h"
21
22
using namespace std;
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
2274
SygusUnif::SygusUnif()
30
2274
    : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false)
31
{
32
2274
}
33
2272
SygusUnif::~SygusUnif() {}
34
35
107
void SygusUnif::initializeCandidate(
36
    QuantifiersEngine* qe,
37
    Node f,
38
    std::vector<Node>& enums,
39
    std::map<Node, std::vector<Node>>& strategy_lemmas)
40
{
41
107
  d_qe = qe;
42
107
  d_tds = qe->getTermDatabaseSygus();
43
107
  d_candidates.push_back(f);
44
  // initialize the strategy
45
107
  d_strategy[f].initialize(qe, f, enums);
46
107
}
47
48
428
Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms)
49
{
50
428
  unsigned minSize = 0;
51
428
  Node minTerm;
52
428
  std::map<Node, unsigned>::iterator it;
53
1082
  for (const Node& n : terms)
54
  {
55
654
    it = d_termToSize.find(n);
56
654
    unsigned ssize = 0;
57
654
    if (it == d_termToSize.end())
58
    {
59
226
      ssize = d_tds->getSygusTermSize(n);
60
226
      d_termToSize[n] = ssize;
61
    }
62
    else
63
    {
64
428
      ssize = it->second;
65
    }
66
654
    if (minTerm.isNull() || ssize < minSize)
67
    {
68
499
      minTerm = n;
69
499
      minSize = ssize;
70
    }
71
  }
72
428
  return minTerm;
73
}
74
75
389
Node SygusUnif::constructBestSolvedTerm(Node e, const std::vector<Node>& solved)
76
{
77
389
  Assert(!solved.empty());
78
389
  if (d_enableMinimality)
79
  {
80
184
    return getMinimalTerm(solved);
81
  }
82
205
  return solved[0];
83
}
84
85
594
Node SygusUnif::constructBestConditional(Node ce,
86
                                         const std::vector<Node>& conds)
87
{
88
594
  Assert(!conds.empty());
89
594
  double r = Random::getRandom().pickDouble(0.0, 1.0);
90
594
  unsigned cindex = r * conds.size();
91
594
  if (cindex > conds.size())
92
  {
93
152
    cindex = conds.size() - 1;
94
  }
95
594
  return conds[cindex];
96
}
97
98
2082
Node SygusUnif::constructBestStringToConcat(
99
    const std::vector<Node>& strs,
100
    const std::map<Node, size_t>& total_inc,
101
    const std::map<Node, std::vector<size_t>>& incr)
102
{
103
2082
  Assert(!strs.empty());
104
4164
  std::vector<Node> strs_tmp = strs;
105
2082
  std::shuffle(strs_tmp.begin(), strs_tmp.end(), Random::getRandom());
106
  // prefer one that has incremented by more than 0
107
2256
  for (const Node& ns : strs_tmp)
108
  {
109
2196
    const std::map<Node, size_t>::const_iterator iti = total_inc.find(ns);
110
2196
    if (iti != total_inc.end() && iti->second > 0)
111
    {
112
2022
      return ns;
113
    }
114
  }
115
60
  return strs_tmp[0];
116
}
117
118
48152
void SygusUnif::indent(const char* c, int ind)
119
{
120
48152
  if (Trace.isOn(c))
121
  {
122
    for (int i = 0; i < ind; i++)
123
    {
124
      Trace(c) << "  ";
125
    }
126
  }
127
48152
}
128
129
145
void SygusUnif::print_val(const char* c, std::vector<Node>& vals, bool pol)
130
{
131
145
  if (Trace.isOn(c))
132
  {
133
    for (unsigned i = 0; i < vals.size(); i++)
134
    {
135
      Trace(c) << ((pol ? vals[i].getConst<bool>() : !vals[i].getConst<bool>())
136
                       ? "1"
137
                       : "0");
138
    }
139
  }
140
145
}
141
142
} /* CVC4::theory::quantifiers namespace */
143
} /* CVC4::theory namespace */
144
26685
} /* CVC4 namespace */