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-2019 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/datatypes/datatypes_rewriter.h"
18 #include "theory/quantifiers/sygus/term_database_sygus.h"
19 #include "theory/quantifiers/term_util.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
SygusUnif()29 SygusUnif::SygusUnif()
30 : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false)
31 {
32 }
~SygusUnif()33 SygusUnif::~SygusUnif() {}
34
initializeCandidate(QuantifiersEngine * qe,Node f,std::vector<Node> & enums,std::map<Node,std::vector<Node>> & strategy_lemmas)35 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 d_qe = qe;
42 d_tds = qe->getTermDatabaseSygus();
43 d_candidates.push_back(f);
44 // initialize the strategy
45 d_strategy[f].initialize(qe, f, enums);
46 }
47
getMinimalTerm(const std::vector<Node> & terms)48 Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms)
49 {
50 unsigned minSize = 0;
51 Node minTerm;
52 std::map<Node, unsigned>::iterator it;
53 for (const Node& n : terms)
54 {
55 it = d_termToSize.find(n);
56 unsigned ssize = 0;
57 if (it == d_termToSize.end())
58 {
59 ssize = d_tds->getSygusTermSize(n);
60 d_termToSize[n] = ssize;
61 }
62 else
63 {
64 ssize = it->second;
65 }
66 if (minTerm.isNull() || ssize < minSize)
67 {
68 minTerm = n;
69 minSize = ssize;
70 }
71 }
72 return minTerm;
73 }
74
constructBestSolvedTerm(Node e,const std::vector<Node> & solved)75 Node SygusUnif::constructBestSolvedTerm(Node e, const std::vector<Node>& solved)
76 {
77 Assert(!solved.empty());
78 if (d_enableMinimality)
79 {
80 return getMinimalTerm(solved);
81 }
82 return solved[0];
83 }
84
constructBestConditional(Node ce,const std::vector<Node> & conds)85 Node SygusUnif::constructBestConditional(Node ce,
86 const std::vector<Node>& conds)
87 {
88 Assert(!conds.empty());
89 double r = Random::getRandom().pickDouble(0.0, 1.0);
90 unsigned cindex = r * conds.size();
91 if (cindex > conds.size())
92 {
93 cindex = conds.size() - 1;
94 }
95 return conds[cindex];
96 }
97
constructBestStringToConcat(const std::vector<Node> & strs,const std::map<Node,unsigned> & total_inc,const std::map<Node,std::vector<unsigned>> & incr)98 Node SygusUnif::constructBestStringToConcat(
99 const std::vector<Node>& strs,
100 const std::map<Node, unsigned>& total_inc,
101 const std::map<Node, std::vector<unsigned>>& incr)
102 {
103 Assert(!strs.empty());
104 std::vector<Node> strs_tmp = strs;
105 std::shuffle(strs_tmp.begin(), strs_tmp.end(), Random::getRandom());
106 // prefer one that has incremented by more than 0
107 for (const Node& ns : strs_tmp)
108 {
109 const std::map<Node, unsigned>::const_iterator iti = total_inc.find(ns);
110 if (iti != total_inc.end() && iti->second > 0)
111 {
112 return ns;
113 }
114 }
115 return strs_tmp[0];
116 }
117
indent(const char * c,int ind)118 void SygusUnif::indent(const char* c, int ind)
119 {
120 if (Trace.isOn(c))
121 {
122 for (int i = 0; i < ind; i++)
123 {
124 Trace(c) << " ";
125 }
126 }
127 }
128
print_val(const char * c,std::vector<Node> & vals,bool pol)129 void SygusUnif::print_val(const char* c, std::vector<Node>& vals, bool pol)
130 {
131 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 }
141
142 } /* CVC4::theory::quantifiers namespace */
143 } /* CVC4::theory namespace */
144 } /* CVC4 namespace */
145