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_ce_lemma_added(qe
->getUserContext()),
186 d_global_terms(qe
->getUserContext()),
187 d_notified_assertions(qe
->getUserContext())
191 bool SygusInst::needsCheck(Theory::Effort e
)
193 return e
>= Theory::EFFORT_LAST_CALL
;
196 QuantifiersModule::QEffort
SygusInst::needsModel(Theory::Effort e
)
198 return QEFFORT_STANDARD
;
201 void SygusInst::reset_round(Theory::Effort e
)
203 d_active_quant
.clear();
204 d_inactive_quant
.clear();
206 FirstOrderModel
* model
= d_quantEngine
->getModel();
207 uint32_t nasserted
= model
->getNumAssertedQuantifiers();
209 for (uint32_t i
= 0; i
< nasserted
; ++i
)
211 Node q
= model
->getAssertedQuantifier(i
);
213 if (model
->isQuantifierActive(q
))
215 d_active_quant
.insert(q
);
216 Node lit
= getCeLiteral(q
);
219 if (d_quantEngine
->getValuation().hasSatValue(lit
, value
))
223 if (!d_quantEngine
->getValuation().isDecision(lit
))
225 model
->setQuantifierActive(q
, false);
226 d_active_quant
.erase(q
);
227 d_inactive_quant
.insert(q
);
228 Trace("sygus-inst") << "Set inactive: " << q
<< std::endl
;
236 void SygusInst::check(Theory::Effort e
, QEffort quant_e
)
238 Trace("sygus-inst") << "Check " << e
<< ", " << quant_e
<< std::endl
;
240 if (quant_e
!= QEFFORT_STANDARD
) return;
242 FirstOrderModel
* model
= d_quantEngine
->getModel();
243 Instantiate
* inst
= d_quantEngine
->getInstantiate();
244 TermDbSygus
* db
= d_quantEngine
->getTermDatabaseSygus();
245 SygusExplain
syexplain(db
);
246 NodeManager
* nm
= NodeManager::currentNM();
247 options::SygusInstMode mode
= options::sygusInstMode();
249 for (const Node
& q
: d_active_quant
)
251 const std::vector
<Node
>& inst_constants
= d_inst_constants
.at(q
);
252 const std::vector
<Node
>& dt_evals
= d_var_eval
.at(q
);
253 Assert(inst_constants
.size() == dt_evals
.size());
254 Assert(inst_constants
.size() == q
[0].getNumChildren());
256 std::vector
<Node
> terms
, eval_unfold_lemmas
;
257 for (size_t i
= 0, size
= q
[0].getNumChildren(); i
< size
; ++i
)
259 Node dt_var
= inst_constants
[i
];
260 Node dt_eval
= dt_evals
[i
];
261 Node value
= model
->getValue(dt_var
);
262 Node t
= datatypes::utils::sygusToBuiltin(value
);
265 std::vector
<Node
> exp
;
266 syexplain
.getExplanationForEquality(dt_var
, value
, exp
);
270 lem
= dt_eval
.eqNode(t
);
274 lem
= nm
->mkNode(kind::IMPLIES
,
275 exp
.size() == 1 ? exp
[0] : nm
->mkNode(kind::AND
, exp
),
278 eval_unfold_lemmas
.push_back(lem
);
281 if (mode
== options::SygusInstMode::PRIORITY_INST
)
283 if (!inst
->addInstantiation(q
, terms
))
285 sendEvalUnfoldLemmas(eval_unfold_lemmas
);
288 else if (mode
== options::SygusInstMode::PRIORITY_EVAL
)
290 if (!sendEvalUnfoldLemmas(eval_unfold_lemmas
))
292 inst
->addInstantiation(q
, terms
);
297 Assert(mode
== options::SygusInstMode::INTERLEAVE
);
298 inst
->addInstantiation(q
, terms
);
299 sendEvalUnfoldLemmas(eval_unfold_lemmas
);
304 bool SygusInst::sendEvalUnfoldLemmas(const std::vector
<Node
>& lemmas
)
306 bool added_lemma
= false;
307 for (const Node
& lem
: lemmas
)
309 Trace("sygus-inst") << "Evaluation unfolding: " << lem
<< std::endl
;
310 added_lemma
|= d_quantEngine
->addLemma(lem
);
315 bool SygusInst::checkCompleteFor(Node q
)
317 return d_inactive_quant
.find(q
) != d_inactive_quant
.end();
320 void SygusInst::registerQuantifier(Node q
)
322 Assert(d_ce_lemmas
.find(q
) == d_ce_lemmas
.end());
324 Trace("sygus-inst") << "Register " << q
<< std::endl
;
326 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>> extra_cons
;
327 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>> exclude_cons
;
328 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>> include_cons
;
329 std::unordered_set
<Node
, NodeHashFunction
> term_irrelevant
;
331 /* Collect relevant local ground terms for each variable type. */
332 if (options::sygusInstScope() == options::SygusInstScope::IN
333 || options::sygusInstScope() == options::SygusInstScope::BOTH
)
335 std::unordered_map
<TypeNode
,
336 std::unordered_set
<Node
, NodeHashFunction
>,
337 TypeNodeHashFunction
>
339 for (const Node
& var
: q
[0])
341 TypeNode tn
= var
.getType();
343 /* Collect relevant ground terms for type tn. */
344 if (relevant_terms
.find(tn
) == relevant_terms
.end())
346 std::unordered_set
<Node
, NodeHashFunction
> terms
;
347 std::unordered_set
<TNode
, TNodeHashFunction
> cache_max
;
348 std::unordered_map
<TNode
, std::pair
<bool, bool>, TNodeHashFunction
>
351 getMinGroundTerms(q
, tn
, terms
, cache_min
);
352 getMaxGroundTerms(q
, tn
, terms
, cache_max
);
353 relevant_terms
.emplace(tn
, terms
);
356 /* Add relevant ground terms to grammar. */
357 auto& terms
= relevant_terms
[tn
];
358 for (const auto& t
: terms
)
360 TypeNode ttn
= t
.getType();
361 extra_cons
[ttn
].insert(t
);
362 Trace("sygus-inst") << "Adding (local) extra cons: " << t
<< std::endl
;
367 /* Collect relevant global ground terms for each variable type. */
368 if (options::sygusInstScope() == options::SygusInstScope::OUT
369 || options::sygusInstScope() == options::SygusInstScope::BOTH
)
371 for (const Node
& var
: q
[0])
373 TypeNode tn
= var
.getType();
375 /* Collect relevant ground terms for type tn. */
376 if (d_global_terms
.find(tn
) == d_global_terms
.end())
378 std::unordered_set
<Node
, NodeHashFunction
> terms
;
379 std::unordered_set
<TNode
, TNodeHashFunction
> cache_max
;
380 std::unordered_map
<TNode
, std::pair
<bool, bool>, TNodeHashFunction
>
383 for (const Node
& a
: d_notified_assertions
)
385 getMinGroundTerms(a
, tn
, terms
, cache_min
, true);
386 getMaxGroundTerms(a
, tn
, terms
, cache_max
, true);
388 d_global_terms
.insert(tn
, terms
);
391 /* Add relevant ground terms to grammar. */
392 auto it
= d_global_terms
.find(tn
);
393 if (it
!= d_global_terms
.end())
395 for (const auto& t
: (*it
).second
)
397 TypeNode ttn
= t
.getType();
398 extra_cons
[ttn
].insert(t
);
400 << "Adding (global) extra cons: " << t
<< std::endl
;
406 /* Construct grammar for each bound variable of 'q'. */
407 Trace("sygus-inst") << "Process variables of " << q
<< std::endl
;
408 std::vector
<TypeNode
> types
;
409 for (const Node
& var
: q
[0])
411 addSpecialValues(var
.getType(), extra_cons
);
412 TypeNode tn
= CegGrammarConstructor::mkSygusDefaultType(var
.getType(),
421 Trace("sygus-inst") << "Construct (default) datatype for " << var
426 registerCeLemma(q
, types
);
429 /* Construct grammars for all bound variables of quantifier 'q'. Currently,
430 * we use the default grammar of the variable's type.
432 void SygusInst::preRegisterQuantifier(Node q
)
434 Trace("sygus-inst") << "preRegister " << q
<< std::endl
;
438 void SygusInst::ppNotifyAssertions(const std::vector
<Node
>& assertions
)
440 for (const Node
& a
: assertions
)
442 d_notified_assertions
.insert(a
);
446 /*****************************************************************************/
447 /* private methods */
448 /*****************************************************************************/
450 Node
SygusInst::getCeLiteral(Node q
)
452 auto it
= d_ce_lits
.find(q
);
453 if (it
!= d_ce_lits
.end())
458 NodeManager
* nm
= NodeManager::currentNM();
459 Node sk
= nm
->mkSkolem("CeLiteral", nm
->booleanType());
460 Node lit
= d_quantEngine
->getValuation().ensureLiteral(sk
);
465 void SygusInst::registerCeLemma(Node q
, std::vector
<TypeNode
>& types
)
467 Assert(q
[0].getNumChildren() == types
.size());
468 Assert(d_ce_lemmas
.find(q
) == d_ce_lemmas
.end());
469 Assert(d_inst_constants
.find(q
) == d_inst_constants
.end());
470 Assert(d_var_eval
.find(q
) == d_var_eval
.end());
472 Trace("sygus-inst") << "Register CE Lemma for " << q
<< std::endl
;
474 /* Generate counterexample lemma for 'q'. */
475 NodeManager
* nm
= NodeManager::currentNM();
476 TermDbSygus
* db
= d_quantEngine
->getTermDatabaseSygus();
478 /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
479 * instantiation constant ic_i with type types[i] and wrap each ic_i in
480 * DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */
481 std::vector
<Node
> evals
;
482 std::vector
<Node
> inst_constants
;
483 for (size_t i
= 0, size
= types
.size(); i
< size
; ++i
)
485 TypeNode tn
= types
[i
];
488 /* Create the instantiation constant and set attribute accordingly. */
489 Node ic
= nm
->mkInstConstant(tn
);
490 InstConstantAttribute ica
;
491 ic
.setAttribute(ica
, q
);
492 Trace("sygus-inst") << "Create " << ic
<< " for " << var
<< std::endl
;
494 db
->registerEnumerator(ic
, ic
, nullptr, ROLE_ENUM_MULTI_SOLUTION
);
496 std::vector
<Node
> args
= {ic
};
497 Node svl
= tn
.getDType().getSygusVarList();
500 args
.insert(args
.end(), svl
.begin(), svl
.end());
502 Node eval
= nm
->mkNode(kind::DT_SYGUS_EVAL
, args
);
504 inst_constants
.push_back(ic
);
505 evals
.push_back(eval
);
508 d_inst_constants
.emplace(q
, inst_constants
);
509 d_var_eval
.emplace(q
, evals
);
511 Node lit
= getCeLiteral(q
);
512 d_quantEngine
->addRequirePhase(lit
, true);
514 /* The decision strategy for quantified formula 'q' ensures that its
515 * counterexample literal is decided on first. It is user-context dependent.
517 Assert(d_dstrat
.find(q
) == d_dstrat
.end());
518 DecisionStrategy
* ds
=
519 new DecisionStrategySingleton("CeLiteral",
521 d_quantEngine
->getSatContext(),
522 d_quantEngine
->getValuation());
524 d_dstrat
[q
].reset(ds
);
525 d_quantEngine
->getDecisionManager()->registerStrategy(
526 DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE
, ds
);
528 /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
530 q
[1].substitute(q
[0].begin(), q
[0].end(), evals
.begin(), evals
.end());
531 Node lem
= nm
->mkNode(kind::OR
, lit
.negate(), body
.negate());
532 lem
= Rewriter::rewrite(lem
);
534 d_ce_lemmas
.emplace(std::make_pair(q
, lem
));
535 Trace("sygus-inst") << "Register CE Lemma: " << lem
<< std::endl
;
538 void SygusInst::addCeLemma(Node q
)
540 Assert(d_ce_lemmas
.find(q
) != d_ce_lemmas
.end());
542 /* Already added in previous contexts. */
543 if (d_ce_lemma_added
.find(q
) != d_ce_lemma_added
.end()) return;
545 Node lem
= d_ce_lemmas
[q
];
546 d_quantEngine
->addLemma(lem
, false);
547 d_ce_lemma_added
.insert(q
);
548 Trace("sygus-inst") << "Add CE Lemma: " << lem
<< std::endl
;
551 } // namespace quantifiers
552 } // namespace theory