This is required for proofs. The internal calculus no longer uses witness forms for reasoning, and hence we cannot return witness terms in ppRewrite. This is required to fix a debug failure, as well as making life easier on external proof conversions.
As a result of this PR, for example, given (P a) as input to ppRewrite, previous we returned:
(P (witness ((x T)) (A x)))
now we return:
(P k), with skolem lemma ( (A k), k )
Followup PRs will remove the use of WITNESS in ppRewrite (e.g. in sets and strings); this PR modifies arithmetic to not return WITNESS in response to ppRewrite.
const std::string& prefix,
const std::string& comment,
int flags,
- ProofGenerator* pg,
- bool retWitness)
+ ProofGenerator* pg)
{
// We do not currently insist that pred does not contain witness terms
Assert(v.getKind() == BOUND_VARIABLE);
k.setAttribute(wfa, w);
Trace("sk-manager-skolem")
<< "skolem: " << k << " witness " << w << std::endl;
- // if we want to return the witness term, make it
- if (retWitness)
- {
- return nm->mkNode(WITNESS, bvl, pred);
- }
return k;
}
* @param pg The proof generator for this skolem. If non-null, this proof
* generator must respond to a call to getProofFor(exists v. pred) during
* the lifetime of the current node manager.
- * @param retWitness Whether we wish to return the witness term for the
- * given Skolem, which notice is of the form (witness v. pred), where pred
- * is in Skolem form. A typical use case of setting this flag to true
- * is preprocessing passes that eliminate terms. Using a witness term
- * instead of its corresponding Skolem indicates that the body of the witness
- * term needs to be added as an assertion, e.g. by the term formula remover.
* @return The skolem whose witness form is registered by this class.
*/
Node mkSkolem(Node v,
const std::string& prefix,
const std::string& comment = "",
int flags = NodeManager::SKOLEM_DEFAULT,
- ProofGenerator* pg = nullptr,
- bool retWitness = false);
+ ProofGenerator* pg = nullptr);
/**
* Make skolemized form of existentially quantified formula q, and store its
* Skolems into the argument skolems.
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
// we mark that we should send a lemma
- Node k = sm->mkSkolem(
- v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this, true);
- // TODO: (project #37) add to lems
+ 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)
+ {
+ TrustNode tlem =
+ mkTrustNode(lem, PfRule::THEORY_PREPROCESS_LEMMA, {}, {lem});
+ lems.push_back(SkolemLemma(tlem, k));
+ }
+ else
+ {
+ lems.push_back(SkolemLemma(TrustNode::mkTrustLemma(lem), k));
+ }
return k;
}
void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
-TrustNode TheoryArith::ppRewrite(TNode atom)
+TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
{
CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
{
return ppRewriteEq(atom);
}
- // TODO (project #37): this will be passed to ppRewrite
- std::vector<SkolemLemma> lems;
Assert(Theory::theoryOf(atom) == THEORY_ARITH);
// Eliminate operators. Notice we must do this here since other
// theories may generate lemmas that involve non-standard operators. For
* This calls the operator elimination utility to eliminate extended
* symbols.
*/
- TrustNode ppRewrite(TNode atom) override;
+ TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
std::string identify() const override { return std::string("TheoryArith"); }
return term;
}
-TrustNode TheoryArrays::ppRewrite(TNode term)
+TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
{
// first, see if we need to expand definitions
TrustNode texp = expandDefinition(term);
public:
PPAssertStatus ppAssert(TrustNode tin,
TrustSubstitutionMap& outSubstitutions) override;
- TrustNode ppRewrite(TNode atom) override;
+ TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
/////////////////////////////////////////////////////////////////////////////
// T-PROPAGATION / REGISTRATION
return d_internal->ppAssert(tin, outSubstitutions);
}
-TrustNode TheoryBV::ppRewrite(TNode t)
+TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
{
// first, see if we need to expand definitions
TrustNode texp = expandDefinition(t);
PPAssertStatus ppAssert(TrustNode in,
TrustSubstitutionMap& outSubstitutions) override;
- TrustNode ppRewrite(TNode t) override;
+ TrustNode ppRewrite(TNode t, std::vector<SkolemLemma>& lems) override;
void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
return TrustNode::null();
}
-TrustNode TheoryDatatypes::ppRewrite(TNode in)
+TrustNode TheoryDatatypes::ppRewrite(TNode in, std::vector<SkolemLemma>& lems)
{
Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
// first, see if we need to expand definitions
//--------------------------------- end standard check
void preRegisterTerm(TNode n) override;
TrustNode expandDefinition(Node n) override;
- TrustNode ppRewrite(TNode n) override;
+ TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems) override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
std::string identify() const override
{
return TrustNode::null();
}
-TrustNode TheoryFp::ppRewrite(TNode node)
+TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
{
Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
// first, see if we need to expand definitions
void preRegisterTerm(TNode node) override;
- TrustNode ppRewrite(TNode node) override;
+ TrustNode ppRewrite(TNode node, std::vector<SkolemLemma>& lems) override;
//--------------------------------- standard check
/** Do we need a check call at last call effort? */
return d_internal->expandDefinition(n);
}
-TrustNode TheorySets::ppRewrite(TNode n)
+TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
{
Kind nk = n.getKind();
if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
throw LogicException(ss.str());
}
}
- return d_internal->ppRewrite(n);
+ return d_internal->ppRewrite(n, lems);
}
Theory::PPAssertStatus TheorySets::ppAssert(
* we throw an exception. Additionally, we expand operators like choose
* and is_singleton.
*/
- TrustNode ppRewrite(TNode n) override;
+ TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems) override;
PPAssertStatus ppAssert(TrustNode tin,
TrustSubstitutionMap& outSubstitutions) override;
void presolve() override;
return TrustNode::null();
}
-TrustNode TheorySetsPrivate::ppRewrite(Node node)
+TrustNode TheorySetsPrivate::ppRewrite(Node node,
+ std::vector<SkolemLemma>& lems)
{
Debug("sets-proc") << "ppRewrite : " << node << std::endl;
/** ppRewrite, which expands choose. */
TrustNode expandDefinition(Node n);
/** ppRewrite, which expands choose and is_singleton. */
- TrustNode ppRewrite(Node n);
+ TrustNode ppRewrite(Node n, std::vector<SkolemLemma>& lems);
void presolve();
}
}
-TrustNode TheoryStrings::ppRewrite(TNode atom)
+TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
{
Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
if (atom.getKind() == STRING_FROM_CODE)
Node k = nm->mkBoundVar(nm->stringType());
Node bvl = nm->mkNode(BOUND_VAR_LIST, k);
Node emp = Word::mkEmptyWord(atom.getType());
+ // TODO: use skolem manager
Node ret = nm->mkNode(
WITNESS,
bvl,
/** called when a new equivalence class is created */
void eqNotifyNewClass(TNode t);
/** preprocess rewrite */
- TrustNode ppRewrite(TNode atom) override;
+ TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
/** Collect model values in m based on the relevant terms given by termSet */
bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet) override;
#include "theory/assertion.h"
#include "theory/care_graph.h"
#include "theory/logic_info.h"
+#include "theory/skolem_lemma.h"
#include "theory/theory_id.h"
#include "theory/trust_node.h"
#include "theory/valuation.h"
* preprocessing pass, where n is an equality from the input formula,
* and in theory preprocessing, where n is a (non-equality) term occurring
* in the input or generated in a lemma.
+ *
+ * @param n the node to preprocess-rewrite.
+ * @param lems a set of lemmas that should be added as a consequence of
+ * preprocessing n. These are in the form of "skolem lemmas". For example,
+ * calling this method on (div x n), we return a trust node proving:
+ * (= (div x n) k_div)
+ * for fresh skolem k, and add the skolem lemma for k that indicates that
+ * it is the division of x and n.
+ *
+ * Note that ppRewrite should not return WITNESS terms, since the internal
+ * calculus works in "original forms" and not "witness forms".
*/
- virtual TrustNode ppRewrite(TNode n) { return TrustNode::null(); }
+ virtual TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
+ {
+ return TrustNode::null();
+ }
/**
* Notify preprocessed assertions. Called on new assertions after
theory::TrustNode TheoryEngine::ppRewriteEquality(TNode eq)
{
Assert(eq.getKind() == kind::EQUAL);
- return theoryOf(eq)->ppRewrite(eq);
+ std::vector<SkolemLemma> lems;
+ TrustNode trn = theoryOf(eq)->ppRewrite(eq, lems);
+ // should never introduce a skolem to eliminate an equality
+ Assert(lems.empty());
+ return trn;
}
void TheoryEngine::notifyPreprocessedAssertions(
{
// In this method, all rewriting steps of node are stored in d_tpg.
- Trace("tpp-debug") << "TheoryPreprocessor::preprocess: start " << node
- << std::endl;
+ Trace("tpp") << "TheoryPreprocessor::preprocess: start " << node << std::endl;
// We must rewrite before preprocessing, because some terms when rewritten
// may introduce new terms that are not top-level and require preprocessing.
}
Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
}
+
+ if (procLemmas)
+ {
+ // Also must preprocess the new lemmas. This is especially important for
+ // formulas containing witness terms whose bodies are not in preprocessed
+ // form, as term formula removal introduces new lemmas for these that
+ // require theory-preprocessing.
+ size_t i = 0;
+ while (i < newLemmas.size())
+ {
+ TrustNode cur = newLemmas[i];
+ newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, false);
+ Trace("tpp") << "Final lemma : " << newLemmas[i].getProven() << std::endl;
+ i++;
+ }
+ }
+
if (node == ppNode)
{
Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
<< tret.getNode() << std::endl;
- if (procLemmas)
- {
- // Also must preprocess the new lemmas. This is especially important for
- // formulas containing witness terms whose bodies are not in preprocessed
- // form, as term formula removal introduces new lemmas for these that
- // require theory-preprocessing.
- size_t i = 0;
- while (i < newLemmas.size())
- {
- TrustNode cur = newLemmas[i];
- newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, false);
- i++;
- }
- }
+ Trace("tpp") << "TheoryPreprocessor::preprocess: return " << tret.getNode()
+ << ", procLemmas=" << procLemmas
+ << ", # lemmas = " << newLemmas.size() << std::endl;
return tret;
}
// If this is an atom, we preprocess its terms with the theory ppRewriter
if (tid != THEORY_BOOL)
{
- Node ppRewritten = ppTheoryRewrite(current);
+ std::vector<SkolemLemma> lems;
+ Node ppRewritten = ppTheoryRewrite(current, lems);
+ for (const SkolemLemma& lem : lems)
+ {
+ newLemmas.push_back(lem.d_lemma);
+ newSkolems.push_back(lem.d_skolem);
+ }
Assert(Rewriter::rewrite(ppRewritten) == ppRewritten);
if (isProofEnabled() && ppRewritten != current)
{
}
// Recursively traverse a term and call the theory rewriter on its sub-terms
-Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
+Node TheoryPreprocessor::ppTheoryRewrite(TNode term,
+ std::vector<SkolemLemma>& lems)
{
NodeMap::iterator find = d_ppCache.find(term);
if (find != d_ppCache.end())
}
if (term.getNumChildren() == 0)
{
- return preprocessWithProof(term);
+ return preprocessWithProof(term, lems);
}
// should be in rewritten form here
Assert(term == Rewriter::rewrite(term));
}
for (const Node& nt : term)
{
- newNode << ppTheoryRewrite(nt);
+ newNode << ppTheoryRewrite(nt, lems);
}
newTerm = Node(newNode);
newTerm = rewriteWithProof(newTerm, d_tpg.get(), false);
}
- newTerm = preprocessWithProof(newTerm);
+ newTerm = preprocessWithProof(newTerm, lems);
d_ppCache[term] = newTerm;
Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl;
return newTerm;
return termr;
}
-Node TheoryPreprocessor::preprocessWithProof(Node term)
+Node TheoryPreprocessor::preprocessWithProof(Node term,
+ std::vector<SkolemLemma>& lems)
{
// Important that it is in rewritten form, to ensure that the rewrite steps
// recorded in d_tpg are functional. In other words, there should not
// be steps from the same term to multiple rewritten forms, which would be
// the case if we registered a preprocessing step for a non-rewritten term.
Assert(term == Rewriter::rewrite(term));
+ Trace("tpp-debug2") << "preprocessWithProof " << term
+ << ", #lems = " << lems.size() << std::endl;
// We never call ppRewrite on equalities here, since equalities have a
// special status. In particular, notice that theory preprocessing can be
// called on all formulas asserted to theory engine, including those generated
return term;
}
// call ppRewrite for the given theory
- TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term);
+ TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term, lems);
+ Trace("tpp-debug2") << "preprocessWithProof returned " << trn
+ << ", #lems = " << lems.size() << std::endl;
if (trn.isNull())
{
- // no change, return original term
+ // no change, return
return term;
}
Node termr = trn.getNode();
}
// Rewrite again here, which notice is a *pre* rewrite.
termr = rewriteWithProof(termr, d_tpg.get(), true);
- return ppTheoryRewrite(termr);
+ return ppTheoryRewrite(termr, lems);
}
bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }
#include "expr/tconv_seq_proof_generator.h"
#include "expr/term_conversion_proof_generator.h"
#include "smt/term_formula_removal.h"
+#include "theory/skolem_lemma.h"
#include "theory/trust_node.h"
namespace CVC4 {
* applies ppRewrite and rewriting until fixed point on term using
* the method preprocessWithProof helper below.
*/
- Node ppTheoryRewrite(TNode term);
+ Node ppTheoryRewrite(TNode term, std::vector<SkolemLemma>& lems);
/**
* Rewrite with proof, which stores a REWRITE step in pg if necessary
* and returns the rewritten form of term.
* the preprocessed and rewritten form of term. It should be the case that
* term is already in rewritten form.
*/
- Node preprocessWithProof(Node term);
+ Node preprocessWithProof(Node term, std::vector<SkolemLemma>& lems);
/**
* Register rewrite trn based on trust node into term conversion generator
* pg, which uses THEORY_PREPROCESS as a step if no proof generator is
}
//--------------------------------- end standard check
-TrustNode TheoryUF::ppRewrite(TNode node)
+TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
{
Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node
<< std::endl;
bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet) override;
- TrustNode ppRewrite(TNode node) override;
+ TrustNode ppRewrite(TNode node, std::vector<SkolemLemma>& lems) override;
void preRegisterTerm(TNode term) override;
TrustNode explain(TNode n) override;
projects / cvc5.git / commitdiff