1 /********************* */
2 /*! \file sygus_invariance.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-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 techniques for sygus invariance tests.
13 **/
14
15 #include "theory/quantifiers/sygus/sygus_invariance.h"
16
17 #include "theory/quantifiers/sygus/sygus_pbe.h"
18 #include "theory/quantifiers/sygus/synth_conjecture.h"
19 #include "theory/quantifiers/sygus/term_database_sygus.h"
20
21 using namespace CVC4::kind;
22 using namespace std;
23
24 namespace CVC4 {
25 namespace theory {
26 namespace quantifiers {
27
init(Node conj,Node var,Node res)28 void EvalSygusInvarianceTest::init(Node conj, Node var, Node res)
29 {
30 d_terms.clear();
31 // simple miniscope
32 if ((conj.getKind() == AND || conj.getKind() == OR) && res.isConst())
33 {
34 for (const Node& c : conj)
35 {
36 d_terms.push_back(c);
37 }
38 d_kind = conj.getKind();
39 d_is_conjunctive = res.getConst<bool>() == (d_kind == AND);
40 }
41 else
42 {
43 d_terms.push_back(conj);
44 d_is_conjunctive = true;
45 }
46 d_var = var;
47 d_result = res;
48 }
49
doEvaluateWithUnfolding(TermDbSygus * tds,Node n)50 Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n)
51 {
52 return tds->evaluateWithUnfolding(n, d_visited);
53 }
54
invariant(TermDbSygus * tds,Node nvn,Node x)55 bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
56 {
57 TNode tnvn = nvn;
58 std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
59 for (const Node& c : d_terms)
60 {
61 Node conj_subs = c.substitute(d_var, tnvn, cache);
62 Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs);
63 Trace("sygus-cref-eval2-debug")
64 << " ...check unfolding : " << conj_subs_unfold << std::endl;
65 Trace("sygus-cref-eval2-debug")
66 << " ......from : " << conj_subs << std::endl;
67 if (conj_subs_unfold != d_result)
68 {
69 if (d_is_conjunctive)
70 {
71 // ti /--> true implies and( t1, ..., tn ) /--> true, where "/-->" is
72 // "does not evaluate to".
73 return false;
74 }
75 }
76 else if (!d_is_conjunctive)
77 {
78 // ti --> true implies or( t1, ..., tn ) --> true
79 return true;
80 }
81 Trace("sygus-cref-eval2") << "Evaluation min explain : " << conj_subs
82 << " still evaluates to " << d_result
83 << " regardless of ";
84 Trace("sygus-cref-eval2") << x << std::endl;
85 }
86 return d_is_conjunctive;
87 }
88
init(TermDbSygus * tds,TypeNode tn,SynthConjecture * aconj,Node e,Node bvr)89 void EquivSygusInvarianceTest::init(
90 TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr)
91 {
92 // compute the current examples
93 d_bvr = bvr;
94 if (aconj->getPbe()->hasExamples(e))
95 {
96 d_conj = aconj;
97 d_enum = e;
98 unsigned nex = aconj->getPbe()->getNumExamples(e);
99 for (unsigned i = 0; i < nex; i++)
100 {
101 d_exo.push_back(d_conj->getPbe()->evaluateBuiltin(tn, bvr, e, i));
102 }
103 }
104 }
105
invariant(TermDbSygus * tds,Node nvn,Node x)106 bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
107 {
108 TypeNode tn = nvn.getType();
109 Node nbv = tds->sygusToBuiltin(nvn, tn);
110 Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv);
111 Trace("sygus-sb-mexp-debug") << " min-exp check : " << nbv << " -> " << nbvr
112 << std::endl;
113 bool exc_arg = false;
114 // equivalent / singular up to normalization
115 if (nbvr == d_bvr)
116 {
117 // gives the same result : then the explanation for the child is irrelevant
118 exc_arg = true;
119 Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
120 << " is rewritten to " << nbvr;
121 Trace("sygus-sb-mexp") << " regardless of the content of "
122 << tds->sygusToBuiltin(x) << std::endl;
123 }
124 else
125 {
126 if (nbvr.isVar())
127 {
128 TypeNode xtn = x.getType();
129 if (xtn == tn)
130 {
131 Node bx = tds->sygusToBuiltin(x, xtn);
132 Assert(bx.getType() == nbvr.getType());
133 if (nbvr == bx)
134 {
135 Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
136 << " always rewrites to argument " << nbvr
137 << std::endl;
138 // rewrites to the variable : then the explanation of this is
139 // irrelevant as well
140 exc_arg = true;
141 d_bvr = nbvr;
142 }
143 }
144 }
145 }
146 // equivalent under examples
147 if (!exc_arg)
148 {
149 if (!d_enum.isNull())
150 {
151 bool ex_equiv = true;
152 for (unsigned j = 0; j < d_exo.size(); j++)
153 {
154 Node nbvr_ex = d_conj->getPbe()->evaluateBuiltin(tn, nbvr, d_enum, j);
155 if (nbvr_ex != d_exo[j])
156 {
157 ex_equiv = false;
158 break;
159 }
160 }
161 if (ex_equiv)
162 {
163 Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn);
164 Trace("sygus-sb-mexp")
165 << " is the same w.r.t. examples regardless of the content of "
166 << tds->sygusToBuiltin(x) << std::endl;
167 exc_arg = true;
168 }
169 }
170 }
171 return exc_arg;
172 }
173
invariant(TermDbSygus * tds,Node nvn,Node x)174 bool DivByZeroSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
175 {
176 TypeNode tn = nvn.getType();
177 Node nbv = tds->sygusToBuiltin(nvn, tn);
178 Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv);
179 if (tds->involvesDivByZero(nbvr))
180 {
181 Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
182 << " involves div-by-zero regardless of "
183 << tds->sygusToBuiltin(x) << std::endl;
184 return true;
185 }
186 return false;
187 }
188
init(Node e,std::vector<std::vector<Node>> & ex,std::vector<Node> & exo,std::vector<unsigned> & ncind)189 void NegContainsSygusInvarianceTest::init(Node e,
190 std::vector<std::vector<Node> >& ex,
191 std::vector<Node>& exo,
192 std::vector<unsigned>& ncind)
193 {
194 Assert(ex.size() == exo.size());
195 d_enum = e;
196 d_ex.insert(d_ex.end(), ex.begin(), ex.end());
197 d_exo.insert(d_exo.end(), exo.begin(), exo.end());
198 d_neg_con_indices.insert(d_neg_con_indices.end(), ncind.begin(), ncind.end());
199 }
200
invariant(TermDbSygus * tds,Node nvn,Node x)201 bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
202 Node nvn,
203 Node x)
204 {
205 if (!d_enum.isNull())
206 {
207 TypeNode tn = nvn.getType();
208 Node nbv = tds->sygusToBuiltin(nvn, tn);
209 Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv);
210 // if for any of the examples, it is not contained, then we can exclude
211 for (unsigned i = 0; i < d_neg_con_indices.size(); i++)
212 {
213 unsigned ii = d_neg_con_indices[i];
214 Assert(ii < d_exo.size());
215 Node nbvre = tds->evaluateBuiltin(tn, nbvr, d_ex[ii]);
216 Node out = d_exo[ii];
217 Node cont =
218 NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, out, nbvre);
219 Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl;
220 Node contr = Rewriter::rewrite(cont);
221 if (!contr.isConst())
222 {
223 if (d_isUniversal)
224 {
225 return false;
226 }
227 }
228 else if (contr.getConst<bool>() == d_isUniversal)
229 {
230 if (Trace.isOn("sygus-pbe-cterm"))
231 {
232 Trace("sygus-pbe-cterm")
233 << "PBE-cterm : enumerator : do not consider ";
234 Trace("sygus-pbe-cterm")
235 << nbv << " for any " << tds->sygusToBuiltin(x) << " since "
236 << std::endl;
237 Trace("sygus-pbe-cterm") << " PBE-cterm : for input example : ";
238 for (unsigned j = 0, size = d_ex[ii].size(); j < size; j++)
239 {
240 Trace("sygus-pbe-cterm") << d_ex[ii][j] << " ";
241 }
242 Trace("sygus-pbe-cterm") << std::endl;
243 Trace("sygus-pbe-cterm")
244 << " PBE-cterm : this rewrites to : " << nbvre << std::endl;
245 Trace("sygus-pbe-cterm")
246 << " PBE-cterm : and is not in output : " << out << std::endl;
247 }
248 return !d_isUniversal;
249 }
250 Trace("sygus-pbe-cterm-debug2")
251 << "...check failed, rewrites to : " << contr << std::endl;
252 }
253 }
254 return d_isUniversal;
255 }
256
257 } /* CVC4::theory::quantifiers namespace */
258 } /* CVC4::theory namespace */
259 } /* CVC4 namespace */
260