1 /********************* */
2 /*! \file sygus_inst.cpp
4 ** Top contributors (to current version):
5 ** Mathias Preiner, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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 SyGuS instantiator class.
15 #include "theory/quantifiers/sygus_inst.h"
18 #include <unordered_set>
20 #include "expr/node_algorithm.h"
21 #include "theory/bv/theory_bv_utils.h"
22 #include "theory/datatypes/sygus_datatype_utils.h"
23 #include "theory/quantifiers/sygus/sygus_enumerator.h"
24 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
25 #include "theory/quantifiers/sygus/synth_engine.h"
26 #include "theory/quantifiers_engine.h"
27 #include "theory/theory_engine.h"
31 namespace quantifiers
{
36 * Collect maximal ground terms with type tn in node n.
38 * @param n: Node to traverse.
39 * @param tn: Collects only terms with type tn.
40 * @param terms: Collected terms.
41 * @param cache: Caches visited nodes.
42 * @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
44 void getMaxGroundTerms(TNode n
,
46 std::unordered_set
<Node
, NodeHashFunction
>& terms
,
47 std::unordered_set
<TNode
, TNodeHashFunction
>& cache
,
48 bool skip_quant
= false)
50 if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MAX
51 && options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH
)
56 Trace("sygus-inst-term") << "Find maximal terms with type " << tn
57 << " in: " << n
<< std::endl
;
60 std::vector
<TNode
> visit
;
68 if (cache
.find(cur
) != cache
.end())
74 if (expr::hasBoundVar(cur
) || cur
.getType() != tn
)
76 if (!skip_quant
|| cur
.getKind() != kind::FORALL
)
78 visit
.insert(visit
.end(), cur
.begin(), cur
.end());
84 Trace("sygus-inst-term") << " found: " << cur
<< std::endl
;
86 } while (!visit
.empty());
90 * Collect minimal ground terms with type tn in node n.
92 * @param n: Node to traverse.
93 * @param tn: Collects only terms with type tn.
94 * @param terms: Collected terms.
95 * @param cache: Caches visited nodes and flags indicating whether a minimal
96 * term was already found in a subterm.
97 * @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
99 void getMinGroundTerms(
102 std::unordered_set
<Node
, NodeHashFunction
>& terms
,
103 std::unordered_map
<TNode
, std::pair
<bool, bool>, TNodeHashFunction
>& cache
,
104 bool skip_quant
= false)
106 if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MIN
107 && options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH
)
112 Trace("sygus-inst-term") << "Find minimal terms with type " << tn
113 << " in: " << n
<< std::endl
;
116 std::vector
<TNode
> visit
;
124 auto it
= cache
.find(cur
);
125 if (it
== cache
.end())
127 cache
.emplace(cur
, std::make_pair(false, false));
128 if (!skip_quant
|| cur
.getKind() != kind::FORALL
)
130 visit
.push_back(cur
);
131 visit
.insert(visit
.end(), cur
.begin(), cur
.end());
135 else if (!it
->second
.first
)
137 bool found_min_term
= false;
139 /* Check if we found a minimal term in one of the children. */
140 for (const Node
& c
: cur
)
142 found_min_term
|= cache
[c
].second
;
143 if (found_min_term
) break;
146 /* If we haven't found a minimal term yet, add this term if it has the
148 if (cur
.getType() == tn
&& !expr::hasBoundVar(cur
) && !found_min_term
)
151 found_min_term
= true;
152 Trace("sygus-inst-term") << " found: " << cur
<< std::endl
;
155 it
->second
.first
= true;
156 it
->second
.second
= found_min_term
;
158 } while (!visit
.empty());
162 * Add special values for a given type.
164 * @param tn: The type node.
165 * @param extra_cons: A map of TypeNode to constants, which are added in
166 * addition to the default grammar.
168 void addSpecialValues(
170 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>>& extra_cons
)
172 if (tn
.isBitVector())
174 uint32_t size
= tn
.getBitVectorSize();
175 extra_cons
[tn
].insert(bv::utils::mkOnes(size
));
176 extra_cons
[tn
].insert(bv::utils::mkMinSigned(size
));
177 extra_cons
[tn
].insert(bv::utils::mkMaxSigned(size
));
183 SygusInst::SygusInst(QuantifiersEngine
* qe
)
184 : QuantifiersModule(qe
),
185 d_lemma_cache(qe
->getUserContext()),
186 d_ce_lemma_added(qe
->getUserContext()),
187 d_global_terms(qe
->getUserContext()),
188 d_notified_assertions(qe
->getUserContext())
192 bool SygusInst::needsCheck(Theory::Effort e
)
194 return e
>= Theory::EFFORT_LAST_CALL
;
197 QuantifiersModule::QEffort
SygusInst::needsModel(Theory::Effort e
)
199 return QEFFORT_STANDARD
;
202 void SygusInst::reset_round(Theory::Effort e
)
204 d_active_quant
.clear();
205 d_inactive_quant
.clear();
207 FirstOrderModel
* model
= d_quantEngine
->getModel();
208 uint32_t nasserted
= model
->getNumAssertedQuantifiers();
210 for (uint32_t i
= 0; i
< nasserted
; ++i
)
212 Node q
= model
->getAssertedQuantifier(i
);
214 if (model
->isQuantifierActive(q
))
216 d_active_quant
.insert(q
);
217 Node lit
= getCeLiteral(q
);
220 if (d_quantEngine
->getValuation().hasSatValue(lit
, value
))
224 if (!d_quantEngine
->getValuation().isDecision(lit
))
226 model
->setQuantifierActive(q
, false);
227 d_active_quant
.erase(q
);
228 d_inactive_quant
.insert(q
);
229 Trace("sygus-inst") << "Set inactive: " << q
<< std::endl
;
237 void SygusInst::check(Theory::Effort e
, QEffort quant_e
)
239 Trace("sygus-inst") << "Check " << e
<< ", " << quant_e
<< std::endl
;
241 if (quant_e
!= QEFFORT_STANDARD
) return;
243 FirstOrderModel
* model
= d_quantEngine
->getModel();
244 Instantiate
* inst
= d_quantEngine
->getInstantiate();
245 TermDbSygus
* db
= d_quantEngine
->getTermDatabaseSygus();
246 SygusExplain
syexplain(db
);
247 NodeManager
* nm
= NodeManager::currentNM();
249 for (const Node
& q
: d_active_quant
)
251 std::vector
<Node
> terms
;
252 for (const Node
& var
: q
[0])
254 Node dt_var
= d_inst_constants
[var
];
255 Node dt_eval
= d_var_eval
[var
];
256 Node value
= model
->getValue(dt_var
);
257 Node t
= datatypes::utils::sygusToBuiltin(value
);
260 std::vector
<Node
> exp
;
261 syexplain
.getExplanationForEquality(dt_var
, value
, exp
);
265 lem
= dt_eval
.eqNode(t
);
269 lem
= nm
->mkNode(kind::IMPLIES
,
270 exp
.size() == 1 ? exp
[0] : nm
->mkNode(kind::AND
, exp
),
274 if (d_lemma_cache
.find(lem
) == d_lemma_cache
.end())
276 Trace("sygus-inst") << "Evaluation unfolding: " << lem
<< std::endl
;
277 d_quantEngine
->addLemma(lem
, false);
278 d_lemma_cache
.insert(lem
);
282 if (inst
->addInstantiation(q
, terms
))
284 Trace("sygus-inst") << "Instantiate " << q
<< std::endl
;
289 bool SygusInst::checkCompleteFor(Node q
)
291 return d_inactive_quant
.find(q
) != d_inactive_quant
.end();
294 void SygusInst::registerQuantifier(Node q
)
296 Assert(d_ce_lemmas
.find(q
) == d_ce_lemmas
.end());
298 Trace("sygus-inst") << "Register " << q
<< std::endl
;
300 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>> extra_cons
;
301 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>> exclude_cons
;
302 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>> include_cons
;
303 std::unordered_set
<Node
, NodeHashFunction
> term_irrelevant
;
305 /* Collect relevant local ground terms for each variable type. */
306 if (options::sygusInstScope() == options::SygusInstScope::IN
307 || options::sygusInstScope() == options::SygusInstScope::BOTH
)
309 std::unordered_map
<TypeNode
,
310 std::unordered_set
<Node
, NodeHashFunction
>,
311 TypeNodeHashFunction
>
313 for (const Node
& var
: q
[0])
315 TypeNode tn
= var
.getType();
317 /* Collect relevant ground terms for type tn. */
318 if (relevant_terms
.find(tn
) == relevant_terms
.end())
320 std::unordered_set
<Node
, NodeHashFunction
> terms
;
321 std::unordered_set
<TNode
, TNodeHashFunction
> cache_max
;
322 std::unordered_map
<TNode
, std::pair
<bool, bool>, TNodeHashFunction
>
325 getMinGroundTerms(q
, tn
, terms
, cache_min
);
326 getMaxGroundTerms(q
, tn
, terms
, cache_max
);
327 relevant_terms
.emplace(tn
, terms
);
330 /* Add relevant ground terms to grammar. */
331 auto& terms
= relevant_terms
[tn
];
332 for (const auto& t
: terms
)
334 TypeNode ttn
= t
.getType();
335 extra_cons
[ttn
].insert(t
);
336 Trace("sygus-inst") << "Adding (local) extra cons: " << t
<< std::endl
;
341 /* Collect relevant global ground terms for each variable type. */
342 if (options::sygusInstScope() == options::SygusInstScope::OUT
343 || options::sygusInstScope() == options::SygusInstScope::BOTH
)
345 for (const Node
& var
: q
[0])
347 TypeNode tn
= var
.getType();
349 /* Collect relevant ground terms for type tn. */
350 if (d_global_terms
.find(tn
) == d_global_terms
.end())
352 std::unordered_set
<Node
, NodeHashFunction
> terms
;
353 std::unordered_set
<TNode
, TNodeHashFunction
> cache_max
;
354 std::unordered_map
<TNode
, std::pair
<bool, bool>, TNodeHashFunction
>
357 for (const Node
& a
: d_notified_assertions
)
359 getMinGroundTerms(a
, tn
, terms
, cache_min
, true);
360 getMaxGroundTerms(a
, tn
, terms
, cache_max
, true);
362 d_global_terms
.insert(tn
, terms
);
365 /* Add relevant ground terms to grammar. */
366 auto it
= d_global_terms
.find(tn
);
367 if (it
!= d_global_terms
.end())
369 for (const auto& t
: (*it
).second
)
371 TypeNode ttn
= t
.getType();
372 extra_cons
[ttn
].insert(t
);
374 << "Adding (global) extra cons: " << t
<< std::endl
;
380 /* Construct grammar for each bound variable of 'q'. */
381 Trace("sygus-inst") << "Process variables of " << q
<< std::endl
;
382 std::vector
<TypeNode
> types
;
383 for (const Node
& var
: q
[0])
385 addSpecialValues(var
.getType(), extra_cons
);
386 TypeNode tn
= CegGrammarConstructor::mkSygusDefaultType(var
.getType(),
395 Trace("sygus-inst") << "Construct (default) datatype for " << var
400 registerCeLemma(q
, types
);
403 /* Construct grammars for all bound variables of quantifier 'q'. Currently,
404 * we use the default grammar of the variable's type.
406 void SygusInst::preRegisterQuantifier(Node q
)
408 Trace("sygus-inst") << "preRegister " << q
<< std::endl
;
412 void SygusInst::ppNotifyAssertions(const std::vector
<Node
>& assertions
)
414 for (const Node
& a
: assertions
)
416 d_notified_assertions
.insert(a
);
420 /*****************************************************************************/
421 /* private methods */
422 /*****************************************************************************/
424 Node
SygusInst::getCeLiteral(Node q
)
426 auto it
= d_ce_lits
.find(q
);
427 if (it
!= d_ce_lits
.end())
432 NodeManager
* nm
= NodeManager::currentNM();
433 Node sk
= nm
->mkSkolem("CeLiteral", nm
->booleanType());
434 Node lit
= d_quantEngine
->getValuation().ensureLiteral(sk
);
439 void SygusInst::registerCeLemma(Node q
, std::vector
<TypeNode
>& types
)
441 Assert(q
[0].getNumChildren() == types
.size());
442 Assert(d_ce_lemmas
.find(q
) == d_ce_lemmas
.end());
444 /* Generate counterexample lemma for 'q'. */
445 NodeManager
* nm
= NodeManager::currentNM();
446 TermDbSygus
* db
= d_quantEngine
->getTermDatabaseSygus();
448 /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
449 * instantiation constant ic_i with type types[i] and wrap each ic_i in
450 * DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */
451 std::vector
<Node
> vars
;
452 std::vector
<Node
> evals
;
453 for (size_t i
= 0, size
= types
.size(); i
< size
; ++i
)
455 TypeNode tn
= types
[i
];
458 /* Create the instantiation constant and set attribute accordingly. */
459 Node ic
= nm
->mkInstConstant(tn
);
460 InstConstantAttribute ica
;
461 ic
.setAttribute(ica
, q
);
463 db
->registerEnumerator(ic
, ic
, nullptr, ROLE_ENUM_MULTI_SOLUTION
);
465 std::vector
<Node
> args
= {ic
};
466 Node svl
= tn
.getDType().getSygusVarList();
469 args
.insert(args
.end(), svl
.begin(), svl
.end());
471 Node eval
= nm
->mkNode(kind::DT_SYGUS_EVAL
, args
);
473 d_inst_constants
.emplace(std::make_pair(var
, ic
));
474 d_var_eval
.emplace(std::make_pair(var
, eval
));
477 evals
.push_back(eval
);
480 Node lit
= getCeLiteral(q
);
481 d_quantEngine
->addRequirePhase(lit
, true);
483 /* The decision strategy for quantified formula 'q' ensures that its
484 * counterexample literal is decided on first. It is user-context dependent.
486 Assert(d_dstrat
.find(q
) == d_dstrat
.end());
487 DecisionStrategy
* ds
=
488 new DecisionStrategySingleton("CeLiteral",
490 d_quantEngine
->getSatContext(),
491 d_quantEngine
->getValuation());
493 d_dstrat
[q
].reset(ds
);
494 d_quantEngine
->getDecisionManager()->registerStrategy(
495 DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE
, ds
);
497 /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
499 q
[1].substitute(vars
.begin(), vars
.end(), evals
.begin(), evals
.end());
500 Node lem
= nm
->mkNode(kind::OR
, lit
.negate(), body
.negate());
501 lem
= Rewriter::rewrite(lem
);
503 d_ce_lemmas
.emplace(std::make_pair(q
, lem
));
504 Trace("sygus-inst") << "Register CE Lemma: " << lem
<< std::endl
;
507 void SygusInst::addCeLemma(Node q
)
509 Assert(d_ce_lemmas
.find(q
) != d_ce_lemmas
.end());
511 /* Already added in previous contexts. */
512 if (d_ce_lemma_added
.find(q
) != d_ce_lemma_added
.end()) return;
514 Node lem
= d_ce_lemmas
[q
];
515 d_quantEngine
->addLemma(lem
, false);
516 d_ce_lemma_added
.insert(q
);
517 Trace("sygus-inst") << "Add CE Lemma: " << lem
<< std::endl
;
520 } // namespace quantifiers
521 } // namespace theory