1 /********************* */
2 /*! \file cegis_unif.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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
12 ** \brief implementation of class for cegis with unification techniques
15 #include "theory/quantifiers/sygus/cegis_unif.h"
17 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
18 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
19 #include "theory/quantifiers/sygus/term_database_sygus.h"
21 using namespace CVC4::kind
;
25 namespace quantifiers
{
27 CegisUnif::CegisUnif(QuantifiersEngine
* qe
, CegConjecture
* p
)
30 d_tds
= d_qe
->getTermDatabaseSygus();
33 CegisUnif::~CegisUnif() {}
34 bool CegisUnif::initialize(Node n
,
35 const std::vector
<Node
>& candidates
,
36 std::vector
<Node
>& lemmas
)
38 Trace("cegis-unif") << "Initialize CegisUnif : " << n
<< std::endl
;
39 Assert(candidates
.size() > 0);
40 if (candidates
.size() > 1)
44 d_candidate
= candidates
[0];
45 Trace("cegis-unif") << "Initialize unif utility for " << d_candidate
47 d_sygus_unif
.initialize(d_qe
, candidates
, d_enums
, lemmas
);
48 Assert(!d_enums
.empty());
49 Trace("cegis-unif") << "Initialize " << d_enums
.size() << " enumerators for "
50 << d_candidate
<< "...\n";
51 /* initialize the enumerators */
52 for (const Node
& e
: d_enums
)
54 d_tds
->registerEnumerator(e
, d_candidate
, d_parent
, true);
55 Node g
= d_tds
->getActiveGuardForEnumerator(e
);
56 d_enum_to_active_guard
[e
] = g
;
61 void CegisUnif::getTermList(const std::vector
<Node
>& candidates
,
62 std::vector
<Node
>& terms
)
64 Assert(candidates
.size() == 1);
65 Valuation
& valuation
= d_qe
->getValuation();
66 for (const Node
& e
: d_enums
)
68 Assert(d_enum_to_active_guard
.find(e
) != d_enum_to_active_guard
.end());
69 Node g
= d_enum_to_active_guard
[e
];
70 /* Get whether the active guard for this enumerator is if so, then there may
71 exist more values for it, and hence we add it to terms. */
72 Node gstatus
= valuation
.getSatValue(g
);
73 if (!gstatus
.isNull() && gstatus
.getConst
<bool>())
80 bool CegisUnif::constructCandidates(const std::vector
<Node
>& enums
,
81 const std::vector
<Node
>& enum_values
,
82 const std::vector
<Node
>& candidates
,
83 std::vector
<Node
>& candidate_values
,
84 std::vector
<Node
>& lems
)
86 Assert(enums
.size() == enum_values
.size());
91 unsigned min_term_size
= 0;
92 std::vector
<unsigned> enum_consider
;
93 Trace("cegis-unif-enum") << "Register new enumerated values :\n";
94 for (unsigned i
= 0, size
= enums
.size(); i
< size
; ++i
)
96 Trace("cegis-unif-enum") << " " << enums
[i
] << " -> " << enum_values
[i
]
98 unsigned sz
= d_tds
->getSygusTermSize(enum_values
[i
]);
99 if (i
== 0 || sz
< min_term_size
)
101 enum_consider
.clear();
103 enum_consider
.push_back(i
);
105 else if (sz
== min_term_size
)
107 enum_consider
.push_back(i
);
110 /* only consider the enumerators that are at minimum size (for fairness) */
111 Trace("cegis-unif-enum") << "...register " << enum_consider
.size() << " / "
112 << enums
.size() << std::endl
;
113 NodeManager
* nm
= NodeManager::currentNM();
114 for (unsigned i
= 0, ecsize
= enum_consider
.size(); i
< ecsize
; ++i
)
116 unsigned j
= enum_consider
[i
];
118 Node v
= enum_values
[j
];
119 std::vector
<Node
> enum_lems
;
120 d_sygus_unif
.notifyEnumeration(e
, v
, enum_lems
);
121 /* the lemmas must be guarded by the active guard of the enumerator */
122 Assert(d_enum_to_active_guard
.find(e
) != d_enum_to_active_guard
.end());
123 Node g
= d_enum_to_active_guard
[e
];
124 for (unsigned j
= 0, size
= enum_lems
.size(); j
< size
; ++j
)
126 enum_lems
[j
] = nm
->mkNode(OR
, g
.negate(), enum_lems
[j
]);
128 lems
.insert(lems
.end(), enum_lems
.begin(), enum_lems
.end());
130 /* build candidate solution */
131 Assert(candidates
.size() == 1);
132 if (d_sygus_unif
.constructSolution(candidate_values
))
134 Node vc
= candidate_values
[0];
135 Trace("cegis-unif-enum") << "... candidate solution :" << vc
<< "\n";
141 Node
CegisUnif::purifyLemma(Node n
,
143 std::vector
<Node
>& model_guards
,
144 BoolNodePairMap
& cache
)
146 Trace("cegis-unif-purify") << "PurifyLemma : " << n
<< "\n";
147 BoolNodePairMap::const_iterator it
= cache
.find(BoolNodePair(ensureConst
, n
));
148 if (it
!= cache
.end())
150 Trace("cegis-unif-purify") << "... already visited " << n
<< "\n";
154 unsigned size
= n
.getNumChildren();
155 Kind k
= n
.getKind();
156 bool fapp
= k
== APPLY_UF
&& size
> 0 && n
[0] == d_candidate
;
157 bool childChanged
= false;
158 std::vector
<Node
> children
;
159 for (unsigned i
= 0; i
< size
; ++i
)
163 children
.push_back(n
[0]);
166 Node child
= purifyLemma(n
[i
], ensureConst
|| fapp
, model_guards
, cache
);
167 children
.push_back(child
);
168 childChanged
= childChanged
|| child
!= n
[i
];
175 children
.insert(children
.begin(), n
.getOperator());
177 nb
= NodeManager::currentNM()->mkNode(k
, children
);
178 Trace("cegis-unif-purify") << "PurifyLemma : transformed " << n
<< " into "
185 /* get model value of non-top level applications of d_candidate */
186 if (ensureConst
&& fapp
)
188 Node nv
= d_parent
->getModelValue(nb
);
189 Trace("cegis-unif-purify") << "PurifyLemma : model value for " << nb
190 << " is " << nv
<< "\n";
191 /* test if different, then update model_guards */
194 Trace("cegis-unif-purify") << "PurifyLemma : adding model eq\n";
195 model_guards
.push_back(
196 NodeManager::currentNM()->mkNode(EQUAL
, nv
, nb
).negate());
200 nb
= Rewriter::rewrite(nb
);
201 /* every non-top level application of function-to-synthesize must be reduced
202 to a concrete constant */
203 Assert(!ensureConst
|| nb
.isConst());
204 Trace("cegis-unif-purify") << "... caching [" << n
<< "] = " << nb
<< "\n";
205 cache
[BoolNodePair(ensureConst
, n
)] = nb
;
209 void CegisUnif::registerRefinementLemma(const std::vector
<Node
>& vars
,
211 std::vector
<Node
>& lems
)
214 std::vector
<Node
> model_guards
;
215 BoolNodePairMap cache
;
216 Trace("cegis-unif") << "Registering lemma at CegisUnif : " << lem
<< "\n";
217 /* Make the purified lemma which will guide the unification utility. */
218 plem
= purifyLemma(lem
, false, model_guards
, cache
);
219 if (!model_guards
.empty())
221 model_guards
.push_back(plem
);
222 plem
= NodeManager::currentNM()->mkNode(OR
, model_guards
);
224 plem
= Rewriter::rewrite(plem
);
225 Trace("cegis-unif") << "Purified lemma : " << plem
<< "\n";
226 d_refinement_lemmas
.push_back(plem
);
227 /* Notify lemma to unification utility */
228 d_sygus_unif
.addRefLemma(plem
);
229 /* Make the refinement lemma and add it to lems. This lemma is guarded by the
230 parent's guard, which has the semantics "this conjecture has a solution",
231 hence this lemma states: if the parent conjecture has a solution, it
232 satisfies the specification for the given concrete point. */
233 /* Store lemma for external modules */
235 NodeManager::currentNM()->mkNode(OR
, d_parent
->getGuard().negate(), lem
));
238 } // namespace quantifiers
239 } // namespace theory