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/datatypes/sygus_datatype_utils.h"
22 #include "theory/quantifiers/sygus/sygus_enumerator.h"
23 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
24 #include "theory/quantifiers/sygus/synth_engine.h"
25 #include "theory/quantifiers_engine.h"
26 #include "theory/theory_engine.h"
30 namespace quantifiers
{
32 SygusInst::SygusInst(QuantifiersEngine
* qe
)
33 : QuantifiersModule(qe
),
34 d_lemma_cache(qe
->getUserContext()),
35 d_ce_lemma_added(qe
->getUserContext())
39 bool SygusInst::needsCheck(Theory::Effort e
)
41 return e
>= Theory::EFFORT_LAST_CALL
;
44 QuantifiersModule::QEffort
SygusInst::needsModel(Theory::Effort e
)
46 return QEFFORT_STANDARD
;
49 void SygusInst::reset_round(Theory::Effort e
)
51 d_active_quant
.clear();
52 d_inactive_quant
.clear();
54 FirstOrderModel
* model
= d_quantEngine
->getModel();
55 uint32_t nasserted
= model
->getNumAssertedQuantifiers();
57 for (uint32_t i
= 0; i
< nasserted
; ++i
)
59 Node q
= model
->getAssertedQuantifier(i
);
61 if (model
->isQuantifierActive(q
))
63 d_active_quant
.insert(q
);
64 Node lit
= getCeLiteral(q
);
67 if (d_quantEngine
->getValuation().hasSatValue(lit
, value
))
71 if (!d_quantEngine
->getValuation().isDecision(lit
))
73 model
->setQuantifierActive(q
, false);
74 d_active_quant
.erase(q
);
75 d_inactive_quant
.insert(q
);
76 Trace("sygus-inst") << "Set inactive: " << q
<< std::endl
;
84 void SygusInst::check(Theory::Effort e
, QEffort quant_e
)
86 Trace("sygus-inst") << "Check " << e
<< ", " << quant_e
<< std::endl
;
88 if (quant_e
!= QEFFORT_STANDARD
) return;
90 FirstOrderModel
* model
= d_quantEngine
->getModel();
91 Instantiate
* inst
= d_quantEngine
->getInstantiate();
92 TermDbSygus
* db
= d_quantEngine
->getTermDatabaseSygus();
93 SygusExplain
syexplain(db
);
94 NodeManager
* nm
= NodeManager::currentNM();
96 for (const Node
& q
: d_active_quant
)
98 std::vector
<Node
> terms
;
99 for (const Node
& var
: q
[0])
101 Node dt_var
= d_inst_constants
[var
];
102 Node dt_eval
= d_var_eval
[var
];
103 Node value
= model
->getValue(dt_var
);
104 Node t
= datatypes::utils::sygusToBuiltin(value
);
107 std::vector
<Node
> exp
;
108 syexplain
.getExplanationForEquality(dt_var
, value
, exp
);
112 lem
= dt_eval
.eqNode(t
);
116 lem
= nm
->mkNode(kind::IMPLIES
,
117 exp
.size() == 1 ? exp
[0] : nm
->mkNode(kind::AND
, exp
),
121 if (d_lemma_cache
.find(lem
) == d_lemma_cache
.end())
123 Trace("sygus-inst") << "Evaluation unfolding: " << lem
<< std::endl
;
124 d_quantEngine
->addLemma(lem
, false);
125 d_lemma_cache
.insert(lem
);
129 if (inst
->addInstantiation(q
, terms
))
131 Trace("sygus-inst") << "Instantiate " << q
<< std::endl
;
136 bool SygusInst::checkCompleteFor(Node q
)
138 return d_inactive_quant
.find(q
) != d_inactive_quant
.end();
141 void SygusInst::registerQuantifier(Node q
)
143 Assert(d_ce_lemmas
.find(q
) == d_ce_lemmas
.end());
145 Trace("sygus-inst") << "Register " << q
<< std::endl
;
147 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>> extra_cons
;
148 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>> exclude_cons
;
149 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>> include_cons
;
150 std::unordered_set
<Node
, NodeHashFunction
> term_irrelevant
;
152 /* Collect extra symbols in 'q' to be used in the grammar. */
153 std::unordered_set
<Node
, NodeHashFunction
> syms
;
154 expr::getSymbols(q
, syms
);
155 for (const TNode
& var
: syms
)
157 TypeNode tn
= var
.getType();
158 extra_cons
[tn
].insert(var
);
159 Trace("sygus-inst") << "Found symbol: " << var
<< std::endl
;
162 /* Construct grammar for each bound variable of 'q'. */
163 Trace("sygus-inst") << "Process variables of " << q
<< std::endl
;
164 std::vector
<TypeNode
> types
;
165 for (const Node
& var
: q
[0])
167 TypeNode tn
= CegGrammarConstructor::mkSygusDefaultType(var
.getType(),
176 Trace("sygus-inst") << "Construct (default) datatype for " << var
181 registerCeLemma(q
, types
);
184 /* Construct grammars for all bound variables of quantifier 'q'. Currently,
185 * we use the default grammar of the variable's type.
187 void SygusInst::preRegisterQuantifier(Node q
)
189 Trace("sygus-inst") << "preRegister " << q
<< std::endl
;
193 /*****************************************************************************/
194 /* private methods */
195 /*****************************************************************************/
197 Node
SygusInst::getCeLiteral(Node q
)
199 auto it
= d_ce_lits
.find(q
);
200 if (it
!= d_ce_lits
.end())
205 NodeManager
* nm
= NodeManager::currentNM();
206 Node sk
= nm
->mkSkolem("CeLiteral", nm
->booleanType());
207 Node lit
= d_quantEngine
->getValuation().ensureLiteral(sk
);
212 void SygusInst::registerCeLemma(Node q
, std::vector
<TypeNode
>& types
)
214 Assert(q
[0].getNumChildren() == types
.size());
215 Assert(d_ce_lemmas
.find(q
) == d_ce_lemmas
.end());
217 /* Generate counterexample lemma for 'q'. */
218 NodeManager
* nm
= NodeManager::currentNM();
219 TermDbSygus
* db
= d_quantEngine
->getTermDatabaseSygus();
221 /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
222 * instantiation constant ic_i with type types[i] and wrap each ic_i in
223 * DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */
224 std::vector
<Node
> vars
;
225 std::vector
<Node
> evals
;
226 for (size_t i
= 0, size
= types
.size(); i
< size
; ++i
)
228 TypeNode tn
= types
[i
];
231 /* Create the instantiation constant and set attribute accordingly. */
232 Node ic
= nm
->mkInstConstant(tn
);
233 InstConstantAttribute ica
;
234 ic
.setAttribute(ica
, q
);
236 db
->registerEnumerator(ic
, ic
, nullptr, ROLE_ENUM_MULTI_SOLUTION
);
238 std::vector
<Node
> args
= {ic
};
239 Node svl
= tn
.getDType().getSygusVarList();
242 args
.insert(args
.end(), svl
.begin(), svl
.end());
244 Node eval
= nm
->mkNode(kind::DT_SYGUS_EVAL
, args
);
246 d_inst_constants
.emplace(std::make_pair(var
, ic
));
247 d_var_eval
.emplace(std::make_pair(var
, eval
));
250 evals
.push_back(eval
);
253 Node lit
= getCeLiteral(q
);
254 d_quantEngine
->addRequirePhase(lit
, true);
256 /* The decision strategy for quantified formula 'q' ensures that its
257 * counterexample literal is decided on first. It is user-context dependent.
259 Assert(d_dstrat
.find(q
) == d_dstrat
.end());
260 DecisionStrategy
* ds
=
261 new DecisionStrategySingleton("CeLiteral",
263 d_quantEngine
->getSatContext(),
264 d_quantEngine
->getValuation());
266 d_dstrat
[q
].reset(ds
);
267 d_quantEngine
->getDecisionManager()->registerStrategy(
268 DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE
, ds
);
270 /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
272 q
[1].substitute(vars
.begin(), vars
.end(), evals
.begin(), evals
.end());
273 Node lem
= nm
->mkNode(kind::OR
, lit
.negate(), body
.negate());
274 lem
= Rewriter::rewrite(lem
);
276 d_ce_lemmas
.emplace(std::make_pair(q
, lem
));
277 Trace("sygus-inst") << "Register CE Lemma: " << lem
<< std::endl
;
280 void SygusInst::addCeLemma(Node q
)
282 Assert(d_ce_lemmas
.find(q
) != d_ce_lemmas
.end());
284 /* Already added in previous contexts. */
285 if (d_ce_lemma_added
.find(q
) != d_ce_lemma_added
.end()) return;
287 Node lem
= d_ce_lemmas
[q
];
288 d_quantEngine
->addLemma(lem
, false);
289 d_ce_lemma_added
.insert(q
);
290 Trace("sygus-inst") << "Add CE Lemma: " << lem
<< std::endl
;
293 } // namespace quantifiers
294 } // namespace theory