diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-08-04 12:38:24 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-04 19:38:24 +0000 |
| commit | ad59051f029507a6c49411b71b9c67467a53660d (patch) | |
| tree | e132ac89f4a68fadd32326d1c86aa1ba89b3c767 | |
| parent | e29a86f380354371dee1e5032034a2fe5edfee16 (diff) | |
syqi: Add debug information for dumping instantiations. (#6978)
Adds the datatype values as debug information for dumping instantiations produced by --sygus-inst.
| -rw-r--r-- | src/theory/quantifiers/sygus_inst.cpp | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 286d5f42b..21852f25a 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -258,7 +258,7 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) Assert(inst_constants.size() == dt_evals.size()); Assert(inst_constants.size() == q[0].getNumChildren()); - std::vector<Node> terms, eval_unfold_lemmas; + std::vector<Node> terms, values, eval_unfold_lemmas; for (size_t i = 0, size = q[0].getNumChildren(); i < size; ++i) { Node dt_var = inst_constants[i]; @@ -266,6 +266,7 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) Node value = model->getValue(dt_var); Node t = datatypes::utils::sygusToBuiltin(value); terms.push_back(t); + values.push_back(value); std::vector<Node> exp; syexplain.getExplanationForEquality(dt_var, value, exp); @@ -285,7 +286,10 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) if (mode == options::SygusInstMode::PRIORITY_INST) { - if (!inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI)) + if (!inst->addInstantiation(q, + terms, + InferenceId::QUANTIFIERS_INST_SYQI, + nm->mkNode(kind::SEXPR, values))) { sendEvalUnfoldLemmas(eval_unfold_lemmas); } @@ -294,13 +298,19 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) { if (!sendEvalUnfoldLemmas(eval_unfold_lemmas)) { - inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI); + inst->addInstantiation(q, + terms, + InferenceId::QUANTIFIERS_INST_SYQI, + nm->mkNode(kind::SEXPR, values)); } } else { Assert(mode == options::SygusInstMode::INTERLEAVE); - inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI); + inst->addInstantiation(q, + terms, + InferenceId::QUANTIFIERS_INST_SYQI, + nm->mkNode(kind::SEXPR, values)); sendEvalUnfoldLemmas(eval_unfold_lemmas); } } |