From 2bb47a96e61babeedfd717104a9ec80b559017a9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Jul 2021 09:24:20 -0500 Subject: [PATCH] Minor fix for term database + central equality engine (#6928) Previously we provided a bogus (self) explanation in a rare case of setting up the term database for higher order. This is incompatible with cases where central equality engine = master equality engine. --- src/theory/quantifiers/term_database.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index bedab16f1..523b84e65 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -480,9 +480,8 @@ void TermDb::addTermHo(Node n) Node psk; if (itp == d_ho_fun_op_purify.end()) { - psk = sm->mkDummySkolem("pfun", - curr.getType(), - "purify for function operator term indexing"); + psk = sm->mkPurifySkolem( + curr, "pfun", "purify for function operator term indexing"); d_ho_fun_op_purify[curr] = psk; // we do not add it to d_ops since it is an internal operator } @@ -1034,7 +1033,10 @@ bool TermDb::reset( Theory::Effort effort ){ eq = itpe->second; } Trace("quant-ho") << "- assert purify equality : " << eq << std::endl; - ee->assertEquality(eq, true, eq); + // Note that ee may be the central equality engine, in which case this + // equality is explained trivially with "true", since both sides of + // eq are HOL and FOL encodings of the same thing. + ee->assertEquality(eq, true, d_true); if (!ee->consistent()) { // In some rare cases, purification functions (in the domain of -- 2.30.2