From: Andrew Reynolds Date: Thu, 2 Jul 2020 13:33:49 +0000 (-0500) Subject: (proof-new) Updates to skolem manager interface (#4664) X-Git-Tag: cvc5-1.0.0~3151 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5401565e7622f9ee6b07abb68e1a9378cb9876a8;p=cvc5.git (proof-new) Updates to skolem manager interface (#4664) Adds a fix for mkPurifySkolem and introduces new interfaces in preparation for arithmetic operator elimination and term formula removal proofs. --- diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index c3435f445..098ff8eea 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -550,8 +550,10 @@ public: SKOLEM_DEFAULT = 0, /**< default behavior */ SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */ SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */ - SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */ - }; + SKOLEM_IS_GLOBAL = 4, /**< global vars appear in models even after a pop */ + SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */ + }; /* enum SkolemFlags */ + /** * Create a skolem constant with the given name, type, and comment. * diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 99f252530..e22bd26cf 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -15,6 +15,7 @@ #include "expr/skolem_manager.h" #include "expr/attribute.h" +#include "expr/node_algorithm.h" using namespace CVC4::kind; @@ -42,7 +43,8 @@ Node SkolemManager::mkSkolem(Node v, const std::string& prefix, const std::string& comment, int flags, - ProofGenerator* pg) + ProofGenerator* pg, + bool retWitness) { Assert(v.getKind() == BOUND_VARIABLE); // make the witness term @@ -55,12 +57,20 @@ Node SkolemManager::mkSkolem(Node v, // store the mapping to proof generator if it exists if (pg != nullptr) { - Node q = nm->mkNode(EXISTS, w[0], w[1]); + // We cache based on the original (Skolem) form, since the user of this + // method operates on Skolem forms. + Node q = nm->mkNode(EXISTS, bvl, pred); // Notice this may overwrite an existing proof generator. This does not // matter since either should be able to prove q. d_gens[q] = pg; } - return getOrMakeSkolem(w, prefix, comment, flags); + Node k = getOrMakeSkolem(w, prefix, comment, flags); + // if we want to return the witness term, make it + if (retWitness) + { + return nm->mkNode(WITNESS, bvl, pred); + } + return k; } Node SkolemManager::mkSkolemize(Node q, @@ -159,7 +169,7 @@ Node SkolemManager::mkPurifySkolem(Node t, // directly. if (t.getKind() == WITNESS) { - return getOrMakeSkolem(t, prefix, comment, flags); + return getOrMakeSkolem(getWitnessForm(t), prefix, comment, flags); } Node v = NodeManager::currentNM()->mkBoundVar(t.getType()); Node k = mkSkolem(v, v.eqNode(t), prefix, comment, flags); @@ -167,6 +177,11 @@ Node SkolemManager::mkPurifySkolem(Node t, return k; } +Node SkolemManager::mkBooleanTermVariable(Node t) +{ + return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR); +} + Node SkolemManager::mkExistential(Node t, Node p) { Assert(p.getType().isBoolean()); @@ -275,7 +290,9 @@ Node SkolemManager::convertInternal(Node n, bool toWitness) // called on them. Regardless, witness terms with free variables // should never be themselves assigned skolems (otherwise we would have // assertions with free variables), and thus they can be treated like - // ordinary terms here. + // ordinary terms here. We use an assertion to check that this is + // indeed the case. + Assert(cur.getKind() != WITNESS || expr::hasFreeVar(cur)); cur.setAttribute(sfa, ret); } visited[cur] = ret; @@ -316,7 +333,16 @@ Node SkolemManager::getOrMakeSkolem(Node w, } NodeManager* nm = NodeManager::currentNM(); // make the new skolem - Node k = nm->mkSkolem(prefix, w.getType(), comment, flags); + Node k; + if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR) + { + Assert (w.getType().isBoolean()); + k = nm->mkBooleanTermVariable(); + } + else + { + k = nm->mkSkolem(prefix, w.getType(), comment, flags); + } // set witness form attribute for k WitnessFormAttribute wfa; k.setAttribute(wfa, w); diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 8dd3a3ef9..1e02d94f4 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -86,6 +86,12 @@ class SkolemManager * @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, @@ -93,7 +99,8 @@ class SkolemManager const std::string& prefix, const std::string& comment = "", int flags = NodeManager::SKOLEM_DEFAULT, - ProofGenerator* pg = nullptr); + ProofGenerator* pg = nullptr, + bool retWitness = false); /** * Make skolemized form of existentially quantified formula q, and store its * Skolems into the argument skolems. @@ -142,6 +149,12 @@ class SkolemManager const std::string& prefix, const std::string& comment = "", int flags = NodeManager::SKOLEM_DEFAULT); + /** + * Make Boolean term variable for term t. This is a special case of + * mkPurifySkolem above, where the returned term has kind + * BOOLEAN_TERM_VARIABLE. + */ + Node mkBooleanTermVariable(Node t); /** * Get proof generator for existentially quantified formula q. This returns * the proof generator that was provided in a call to mkSkolem above. @@ -153,13 +166,18 @@ class SkolemManager * where T is the type of t, and x is a variable unique to t,p. */ Node mkExistential(Node t, Node p); - /** convert to witness form + /** + * Convert to witness form, where notice this recursively replaces *all* + * skolems in n by their corresponding witness term. This is intended to be + * used by the proof checker only. * * @param n The term or formula to convert to witness form described above * @return n in witness form. */ static Node getWitnessForm(Node n); - /** convert to Skolem form + /** + * Convert to Skolem form, which recursively replaces all witness terms in n + * by their corresponding Skolems. * * @param n The term or formula to convert to Skolem form described above * @return n in Skolem form.