diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-11 03:21:06 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-11 09:21:06 +0000 |
commit | 71e843a8e9e88fc739aaa5a4a5d608004648fafa (patch) | |
tree | 6f18912dfcb230139bbb6bdb68b38400d23d7eff /src/theory/sets | |
parent | 223155cfb300458f534f4be6b88e5fdc17b0ff14 (diff) |
(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.
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 3 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 34 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 5 |
3 files changed, 13 insertions, 29 deletions
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<SkolemLemma>& 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<SkolemLemma>& 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<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 @@ -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<SkolemLemma>& 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<SkolemLemma>& lems); /** expand the definition of is_singleton operator */ TrustNode expandIsSingletonOperator(const Node& node); /** subtheory solver for the theory of relations */ |