diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-22 12:30:21 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-22 12:30:21 -0500 |
| commit | 64abc6827ec78183605db53e5dd8e2a7a0db59ed (patch) | |
| tree | 42b38f99bf9ad70cc2991fb015848a4913bdbb57 /src/prop/theory_proxy.h | |
| parent | 30034769128894884a94b1b99feb95737f163bab (diff) | |
Add skolem definition manager (#6187)
This creates a central utility for managing "skolem definitions", e.g. mapping between skolems and the lemmas that define their behavior.
This utility is taken from the satRlv branch. It will also be used for the new implementation of the justification decision heuristic.
Note that this PR takes some helper functions out of term formula removal (e.g. hasSkolems) Prior to this PR, these helper functions were incorrect since term formula removal does not account for all introduced skolems. For instance, Theory::ppRewrite may introduce skolems directly. This PR consolidates these cases into the new class, which is called from PropEngine when lemmas and assertions are added. At the moment, the only use of this method is for CEGQI, which needs to do its own tracking of skolems in certain literals.
It also makes some minor reorganization to prop engine.
Diffstat (limited to 'src/prop/theory_proxy.h')
| -rw-r--r-- | src/prop/theory_proxy.h | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 83c64d726..01d98f1b9 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -29,6 +29,7 @@ #include "expr/node.h" #include "prop/registrar.h" #include "prop/sat_solver_types.h" +#include "prop/skolem_def_manager.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" #include "theory/trust_node.h" @@ -62,6 +63,12 @@ class TheoryProxy : public Registrar /** Finish initialize */ void finishInit(CnfStream* cnfStream); + /** Notify (preprocessed) assertions. */ + void notifyPreprocessedAssertions(const std::vector<Node>& assertions); + + /** Notify a lemma, possibly corresponding to a skolem definition */ + void notifyAssertion(Node lem, TNode skolem = TNode::null()); + void theoryCheck(theory::Theory::Effort effort); void explainPropagation(SatLiteral l, SatClause& explanation); @@ -124,7 +131,7 @@ class TheoryProxy : public Registrar * fixed point is reached. */ void getSkolems(TNode node, - std::vector<theory::TrustNode>& skAsserts, + std::vector<Node>& skAsserts, std::vector<Node>& sks); /** Preregister term */ void preRegister(Node n) override; @@ -153,6 +160,9 @@ class TheoryProxy : public Registrar /** The theory preprocessor */ theory::TheoryPreprocessor d_tpp; + + /** The skolem definition manager */ + std::unique_ptr<SkolemDefManager> d_skdm; }; /* class TheoryProxy */ }/* CVC4::prop namespace */ |