1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
/********************* */
/*! \file sygus_unif.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Implementation of sygus_unif
**/
#include "theory/quantifiers/sygus/sygus_unif.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "util/random.h"
using namespace std;
using namespace CVC4::kind;
namespace CVC4 {
namespace theory {
namespace quantifiers {
SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {}
SygusUnif::~SygusUnif() {}
void SygusUnif::initializeCandidate(
QuantifiersEngine* qe,
Node f,
std::vector<Node>& enums,
std::map<Node, std::vector<Node>>& strategy_lemmas)
{
d_qe = qe;
d_tds = qe->getTermDatabaseSygus();
d_candidates.push_back(f);
// initialize the strategy
d_strategy[f].initialize(qe, f, enums);
}
Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved)
{
Assert(!solved.empty());
return solved[0];
}
Node SygusUnif::constructBestStringSolvedTerm(const std::vector<Node>& solved)
{
Assert(!solved.empty());
return solved[0];
}
Node SygusUnif::constructBestSolvedConditional(const std::vector<Node>& solved)
{
Assert(!solved.empty());
return solved[0];
}
Node SygusUnif::constructBestConditional(const std::vector<Node>& conds)
{
Assert(!conds.empty());
double r = Random::getRandom().pickDouble(0.0, 1.0);
unsigned cindex = r * conds.size();
if (cindex > conds.size())
{
cindex = conds.size() - 1;
}
return conds[cindex];
}
Node SygusUnif::constructBestStringToConcat(
const std::vector<Node>& strs,
const std::map<Node, unsigned>& total_inc,
const std::map<Node, std::vector<unsigned>>& incr)
{
Assert(!strs.empty());
std::vector<Node> strs_tmp = strs;
std::shuffle(strs_tmp.begin(), strs_tmp.end(), Random::getRandom());
// prefer one that has incremented by more than 0
for (const Node& ns : strs_tmp)
{
const std::map<Node, unsigned>::const_iterator iti = total_inc.find(ns);
if (iti != total_inc.end() && iti->second > 0)
{
return ns;
}
}
return strs_tmp[0];
}
void SygusUnif::indent(const char* c, int ind)
{
if (Trace.isOn(c))
{
for (int i = 0; i < ind; i++)
{
Trace(c) << " ";
}
}
}
void SygusUnif::print_val(const char* c, std::vector<Node>& vals, bool pol)
{
if (Trace.isOn(c))
{
for (unsigned i = 0; i < vals.size(); i++)
{
Trace(c) << ((pol ? vals[i].getConst<bool>() : !vals[i].getConst<bool>())
? "1"
: "0");
}
}
}
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
|
