From 71e843a8e9e88fc739aaa5a4a5d608004648fafa Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 11 Mar 2021 03:21:06 -0600 Subject: [PATCH] (proof-new) Clean up uses of witness with skolem lemmas (#6109) This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy. It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted. --- src/CMakeLists.txt | 1 + src/theory/arith/operator_elim.cpp | 6 ++-- src/theory/sets/theory_sets.cpp | 3 +- src/theory/sets/theory_sets_private.cpp | 34 ++++++------------- src/theory/sets/theory_sets_private.h | 5 ++- src/theory/skolem_lemma.cpp | 43 +++++++++++++++++++++++++ src/theory/skolem_lemma.h | 20 +++++++++--- src/theory/strings/theory_strings.cpp | 14 ++++---- src/theory/theory_preprocessor.cpp | 5 +-- 9 files changed, 84 insertions(+), 47 deletions(-) create mode 100644 src/theory/skolem_lemma.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3fc12c585..a086d4224 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -900,6 +900,7 @@ libcvc4_add_sources( theory/shared_solver_distributed.h theory/shared_terms_database.cpp theory/shared_terms_database.h + theory/skolem_lemma.cpp theory/skolem_lemma.h theory/smt_engine_subsolver.cpp theory/smt_engine_subsolver.h diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 100116fd7..ab01960dd 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -481,18 +481,16 @@ Node OperatorElim::mkWitnessTerm(Node v, // we mark that we should send a lemma Node k = sm->mkSkolem(v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this); - TNode tv = v; - TNode tk = k; - Node lem = pred.substitute(tv, tk); if (d_pnm != nullptr) { + Node lem = SkolemLemma::getSkolemLemmaFor(k); TrustNode tlem = mkTrustNode(lem, PfRule::THEORY_PREPROCESS_LEMMA, {}, {lem}); lems.push_back(SkolemLemma(tlem, k)); } else { - lems.push_back(SkolemLemma(TrustNode::mkTrustLemma(lem), k)); + lems.push_back(SkolemLemma(k, nullptr)); } return k; } diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index ee23aae49..f3ad57535 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -132,7 +132,8 @@ void TheorySets::preRegisterTerm(TNode node) TrustNode TheorySets::expandDefinition(Node n) { - return d_internal->expandDefinition(n); + // we currently do not expand any set operators + return TrustNode::null(); } TrustNode TheorySets::ppRewrite(TNode n, std::vector& lems) diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index c15ea6f65..da2958c5c 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -20,6 +20,7 @@ #include "expr/emptyset.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/sets_options.h" #include "smt/smt_statistics_registry.h" #include "theory/sets/normal_form.h" @@ -1265,17 +1266,6 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) } } -TrustNode TheorySetsPrivate::expandDefinition(Node node) -{ - Debug("sets-proc") << "expandDefinition : " << node << std::endl; - - if (node.getKind()==kind::CHOOSE) - { - return expandChooseOperator(node); - } - return TrustNode::null(); -} - TrustNode TheorySetsPrivate::ppRewrite(Node node, std::vector& lems) { @@ -1283,24 +1273,17 @@ TrustNode TheorySetsPrivate::ppRewrite(Node node, switch (node.getKind()) { - case kind::CHOOSE: return expandChooseOperator(node); + case kind::CHOOSE: return expandChooseOperator(node, lems); case kind::IS_SINGLETON: return expandIsSingletonOperator(node); default: return TrustNode::null(); } } -TrustNode TheorySetsPrivate::expandChooseOperator(const Node& node) +TrustNode TheorySetsPrivate::expandChooseOperator( + const Node& node, std::vector& lems) { Assert(node.getKind() == CHOOSE); - // we call the rewriter here to handle the pattern (choose (singleton x)) - // because the rewriter is called after expansion - Node rewritten = Rewriter::rewrite(node); - if (rewritten.getKind() != CHOOSE) - { - return TrustNode::mkTrustRewrite(node, rewritten, nullptr); - } - // (choose A) is expanded as // (witness ((x elementType)) // (ite @@ -1309,7 +1292,7 @@ TrustNode TheorySetsPrivate::expandChooseOperator(const Node& node) // (and (member x A) (= x chooseUf(A))) NodeManager* nm = NodeManager::currentNM(); - Node set = rewritten[0]; + Node set = node[0]; TypeNode setType = set.getType(); Node chooseSkolem = getChooseFunction(setType); Node apply = NodeManager::currentNM()->mkNode(APPLY_UF, chooseSkolem, set); @@ -1322,9 +1305,10 @@ TrustNode TheorySetsPrivate::expandChooseOperator(const Node& node) Node member = nm->mkNode(MEMBER, witnessVariable, set); Node memberAndEqual = member.andNode(equal); Node ite = nm->mkNode(ITE, isEmpty, equal, memberAndEqual); - Node witnessVariables = nm->mkNode(BOUND_VAR_LIST, witnessVariable); - Node witness = nm->mkNode(WITNESS, witnessVariables, ite); - return TrustNode::mkTrustRewrite(node, witness, nullptr); + SkolemManager* sm = nm->getSkolemManager(); + Node ret = sm->mkSkolem(witnessVariable, ite, "kSetChoose"); + lems.push_back(SkolemLemma(ret, nullptr)); + return TrustNode::mkTrustRewrite(node, ret, nullptr); } TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node) diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 262a4c572..329fbfc17 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -167,8 +167,6 @@ class TheorySetsPrivate { void preRegisterTerm(TNode node); - /** ppRewrite, which expands choose. */ - TrustNode expandDefinition(Node n); /** ppRewrite, which expands choose and is_singleton. */ TrustNode ppRewrite(Node n, std::vector& lems); @@ -204,7 +202,8 @@ class TheorySetsPrivate { */ Node getChooseFunction(const TypeNode& setType); /** expand the definition of the choose operator */ - TrustNode expandChooseOperator(const Node& node); + TrustNode expandChooseOperator(const Node& node, + std::vector& lems); /** expand the definition of is_singleton operator */ TrustNode expandIsSingletonOperator(const Node& node); /** subtheory solver for the theory of relations */ diff --git a/src/theory/skolem_lemma.cpp b/src/theory/skolem_lemma.cpp new file mode 100644 index 000000000..7c8f00dd7 --- /dev/null +++ b/src/theory/skolem_lemma.cpp @@ -0,0 +1,43 @@ +/********************* */ +/*! \file skolem_lemma.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The skolem lemma utility + **/ + +#include "theory/skolem_lemma.h" + +#include "expr/skolem_manager.h" + +namespace CVC4 { +namespace theory { + +SkolemLemma::SkolemLemma(TrustNode lem, Node k) : d_lemma(lem), d_skolem(k) +{ + Assert(lem.getKind() == TrustNodeKind::LEMMA); +} + +SkolemLemma::SkolemLemma(Node k, ProofGenerator* pg) : d_lemma(), d_skolem(k) +{ + Node lem = getSkolemLemmaFor(k); + d_lemma = TrustNode::mkTrustLemma(lem, pg); +} + +Node SkolemLemma::getSkolemLemmaFor(Node k) +{ + Node w = SkolemManager::getWitnessForm(k); + Assert(w.getKind() == kind::WITNESS); + TNode tx = w[0][0]; + TNode tk = k; + return w[1].substitute(tx, tk); +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h index a44d5a30d..c669b527d 100644 --- a/src/theory/skolem_lemma.h +++ b/src/theory/skolem_lemma.h @@ -36,14 +36,26 @@ namespace theory { class SkolemLemma { public: - SkolemLemma(TrustNode lem, Node k) : d_lemma(lem), d_skolem(k) - { - Assert(lem.getKind() == TrustNodeKind::LEMMA); - } + /** + * Make skolem from trust node lem of kind LEMMA and skolem k. + */ + SkolemLemma(TrustNode lem, Node k); + /** + * Make skolem lemma from witness form of skolem k. If non-null, pg is + * proof generator that can generator a proof for getSkolemLemmaFor(k). + */ + SkolemLemma(Node k, ProofGenerator* pg); + /** The lemma, a trust node of kind LEMMA */ TrustNode d_lemma; /** The skolem associated with that lemma */ Node d_skolem; + + /** + * Get the lemma for skolem k based on its witness form. If k has witness + * form (witness ((x T)) (P x)), this is the formula (P k). + */ + static Node getSkolemLemmaFor(Node k); }; } // namespace theory diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7f838e411..fbede89f0 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -998,15 +998,13 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector& lems) Node card = nm->mkConst(Rational(utils::getAlphabetCardinality())); Node cond = nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card)); - Node k = nm->mkBoundVar(nm->stringType()); - Node bvl = nm->mkNode(BOUND_VAR_LIST, k); + Node v = nm->mkBoundVar(nm->stringType()); Node emp = Word::mkEmptyWord(atom.getType()); - // TODO: use skolem manager - Node ret = nm->mkNode( - WITNESS, - bvl, - nm->mkNode( - ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); + Node pred = nm->mkNode( + ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, v)), v.eqNode(emp)); + SkolemManager* sm = nm->getSkolemManager(); + Node ret = sm->mkSkolem(v, pred, "kFromCode"); + lems.push_back(SkolemLemma(ret, nullptr)); return TrustNode::mkTrustRewrite(atom, ret, nullptr); } TrustNode ret; diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index ea4b0f82f..a9e16f48f 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -204,13 +204,14 @@ TrustNode TheoryPreprocessor::preprocessLemmaInternal( { Assert(d_lp != nullptr); // add the original proof to the lazy proof - d_lp->addLazyStep(node.getProven(), node.getGenerator()); + d_lp->addLazyStep( + node.getProven(), node.getGenerator(), PfRule::THEORY_PREPROCESS_LEMMA); // only need to do anything if lemmap changed in a non-trivial way if (!CDProof::isSame(lemmap, lemma)) { d_lp->addLazyStep(tplemma.getProven(), tplemma.getGenerator(), - PfRule::PREPROCESS_LEMMA, + PfRule::THEORY_PREPROCESS, true, "TheoryEngine::lemma_pp"); // ---------- from node -------------- from theory preprocess -- 2.30.2