diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-18 18:42:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-18 18:42:46 -0500 |
commit | 912ada0fb5368f3420b455b8bc76e88db164c37c (patch) | |
tree | 0452820fe6d4df223681bcc28817b7d928261e81 /src/expr/skolem_manager.h | |
parent | 738676c39badd9a03db0feaa00bb4bd467f0600a (diff) |
(proof-new) Witness axiom reconstruction for purification skolems (#5289)
This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify.
This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager.
Diffstat (limited to 'src/expr/skolem_manager.h')
-rw-r--r-- | src/expr/skolem_manager.h | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index ec5189d6d..537c0b1e9 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -159,13 +159,7 @@ class SkolemManager * Get proof generator for existentially quantified formula q. This returns * the proof generator that was provided in a call to mkSkolem above. */ - ProofGenerator* getProofGenerator(Node q); - /** - * Make existential. Given t and p[t] where p is a formula, this returns - * (exists ((x T)) p[x]) - * where T is the type of t, and x is a variable unique to t,p. - */ - Node mkExistential(Node t, Node p); + ProofGenerator* getProofGenerator(Node q) const; /** * Convert to witness form, where notice this recursively replaces *all* * skolems in n by their corresponding witness term. This is intended to be @@ -197,7 +191,7 @@ class SkolemManager * Map to canonical bound variables. This is used for example by the method * mkExistential. */ - std::map<std::pair<Node, Node>, Node> d_witnessBoundVar; + std::map<Node, Node> d_witnessBoundVar; /** Convert to witness or skolem form */ static Node convertInternal(Node n, bool toWitness); /** Get or make skolem attribute for witness term w */ @@ -224,10 +218,11 @@ class SkolemManager const std::string& comment = "", int flags = NodeManager::SKOLEM_DEFAULT); /** - * Get or make bound variable unique to (s,t), for d_witnessBoundVar, where - * t and s are terms. + * Get or make bound variable unique to t whose type is the same as t. This + * is used to construct canonical bound variables e.g. for constructing + * bound variables for witness terms in the skolemize method above. */ - Node getOrMakeBoundVariable(Node t, Node s); + Node getOrMakeBoundVariable(Node t); }; } // namespace CVC4 |