From: Mathias Preiner Date: Wed, 4 Aug 2021 19:38:24 +0000 (-0700) Subject: syqi: Add debug information for dumping instantiations. (#6978) X-Git-Tag: cvc5-1.0.0~1406 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ad59051f029507a6c49411b71b9c67467a53660d;p=cvc5.git syqi: Add debug information for dumping instantiations. (#6978) Adds the datatype values as debug information for dumping instantiations produced by --sygus-inst. --- 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 terms, eval_unfold_lemmas; + std::vector 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 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); } }