diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-07 11:49:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-07 16:49:41 +0000 |
| commit | e9cffe98e1ef34cde01e7778fc2be55839044007 (patch) | |
| tree | 81589c71b3c6d717ed06259a499ea601db6ec2a2 /src/prop/prop_engine.h | |
| parent | bd41ade5f0eee5afe8bc7f6c7c3ca76f1fa296b4 (diff) | |
Use skolem lemma in prop layer interfaces (#7320)
Diffstat (limited to 'src/prop/prop_engine.h')
| -rw-r--r-- | src/prop/prop_engine.h | 26 |
1 files changed, 11 insertions, 15 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 3556108d1..2f569ba72 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -25,6 +25,7 @@ #include "proof/trust_node.h" #include "prop/skolem_def_manager.h" #include "theory/output_channel.h" +#include "theory/skolem_lemma.h" #include "util/result.h" namespace cvc5 { @@ -85,14 +86,12 @@ class PropEngine * ppSkolems respectively. * * @param node The assertion to preprocess, - * @param ppLemmas The lemmas to add to the set of assertions, - * @param ppSkolems The skolems that newLemmas correspond to, + * @param ppLemmas The lemmas to add to the set of assertions, which tracks + * their corresponding skolems, * @return The (REWRITE) trust node corresponding to rewritten node via * preprocessing. */ - TrustNode preprocess(TNode node, - std::vector<TrustNode>& ppLemmas, - std::vector<Node>& ppSkolems); + TrustNode preprocess(TNode node, std::vector<theory::SkolemLemma>& ppLemmas); /** * Remove term ITEs (and more generally, term formulas) from the given node. * Return the REWRITE trust node corresponding to rewriting node. New lemmas @@ -101,14 +100,12 @@ class PropEngine * preprocessing and rewriting. * * @param node The assertion to preprocess, - * @param ppLemmas The lemmas to add to the set of assertions, - * @param ppSkolems The skolems that newLemmas correspond to, + * @param ppLemmas The lemmas to add to the set of assertions, which tracks + * their corresponding skolems. * @return The (REWRITE) trust node corresponding to rewritten node via * preprocessing. */ - TrustNode removeItes(TNode node, - std::vector<TrustNode>& ppLemmas, - std::vector<Node>& ppSkolems); + TrustNode removeItes(TNode node, std::vector<theory::SkolemLemma>& ppLemmas); /** * Converts the given formulas to CNF and assert the CNF to the SAT solver. @@ -334,13 +331,12 @@ class PropEngine ProofGenerator* pg = nullptr); /** * Assert lemmas internal, where trn is a trust node corresponding to a - * formula to assert to the CNF stream, ppLemmas and ppSkolems are the - * skolem definitions and skolems obtained from preprocessing it, and - * removable is whether the lemma is removable. + * formula to assert to the CNF stream, ppLemmas are the skolem definitions + * obtained from preprocessing it, and removable is whether the lemma is + * removable. */ void assertLemmasInternal(TrustNode trn, - const std::vector<TrustNode>& ppLemmas, - const std::vector<Node>& ppSkolems, + const std::vector<theory::SkolemLemma>& ppLemmas, bool removable); /** |