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.
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
// 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;
}
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<SkolemLemma>& lems)
#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"
}
}
-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<SkolemLemma>& lems)
{
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<SkolemLemma>& 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
// (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);
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)
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<SkolemLemma>& lems);
*/
Node getChooseFunction(const TypeNode& setType);
/** expand the definition of the choose operator */
- TrustNode expandChooseOperator(const Node& node);
+ TrustNode expandChooseOperator(const Node& node,
+ std::vector<SkolemLemma>& lems);
/** expand the definition of is_singleton operator */
TrustNode expandIsSingletonOperator(const Node& node);
/** subtheory solver for the theory of relations */
--- /dev/null
+/********************* */
+/*! \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
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
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;
{
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
projects / cvc5.git / commitdiff