From 2b62f6384a550ee961455e6b354e615cb134411c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 Mar 2022 14:46:56 -0600 Subject: [PATCH] Do not use sygus evaluation functions in sygus-inst (#8185) This simplification was realized while we were writing the paper. This should avoid spurious check-model failures when using sygus-inst. --- src/theory/quantifiers/sygus_inst.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index b67743f59..153d5bc37 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -490,11 +490,12 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) /* Generate counterexample lemma for 'q'. */ NodeManager* nm = NodeManager::currentNM(); + SkolemManager * sm = nm->getSkolemManager(); TermDbSygus* db = d_treg.getTermDatabaseSygus(); - /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype - * instantiation constant ic_i with type types[i] and wrap each ic_i in - * DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */ + // For each variable x_i of \forall x_i . P[x_i], create a fresh datatype + // instantiation constant ic_i with type types[i], and a Skolem eval_i whose + // type is is the same as x_i, and whose value will be used to instantiate x_i std::vector evals; std::vector inst_constants; for (size_t i = 0, size = types.size(); i < size; ++i) @@ -517,9 +518,14 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) args.insert(args.end(), svl.begin(), svl.end()); } Node eval = nm->mkNode(kind::DT_SYGUS_EVAL, args); + // we use a Skolem constant here, instead of an application of an + // evaluation function, since we are not using the builtin support + // for evaluation functions. We use the DT_SYGUS_EVAL term so that the + // skolem construction here is deterministic and reproducible. + Node k = sm->mkPurifySkolem(eval, "eval"); inst_constants.push_back(ic); - evals.push_back(eval); + evals.push_back(k); } d_inst_constants.emplace(q, inst_constants); -- 2.30.2