diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-12 03:45:29 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-12 10:45:29 +0100 |
| commit | d47a8708171f1cf488fe9ce05f56f2566db53093 (patch) | |
| tree | d9c1e5b69d5acb3d44483c42750aa4de4b01082c /src/decision/justification_heuristic.h | |
| parent | dd89a91a12afb86ae34497f2e8b2ebe95ec377a5 (diff) | |
Simplify and fix decision engine's handling of skolem definitions (#5888)
This PR changes the front end of prop engine to distinguish input formulas from skolem definitions, which is required by the decision engine. This PR breaks the dependency of PropEngine on the AssertionsPipeline, as now the determining of whether an input formula is a skolem definition is handled externally, in SmtSolver.
With this PR, we should not be required to satisfy skolem definitions that are not relevant based on the techniques already implemented in the decision engine. Currently, we are not distinguishing input formulas from skolem definitions properly, meaning we assert more literals than we need to.
This also simplifies related interfaces within decision engine.
We should test this PR with --decision=justification on SMT-LIB.
Diffstat (limited to 'src/decision/justification_heuristic.h')
| -rw-r--r-- | src/decision/justification_heuristic.h | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 81b08f1a6..f4e30417c 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -121,9 +121,16 @@ public: prop::SatLiteral getNext(bool &stopSearch) override; - void addAssertions(const std::vector<Node>& assertions, - const std::vector<Node>& ppLemmas, - const std::vector<Node>& ppSkolems) override; + /** + * Notify this class that assertion is an (input) assertion, not corresponding + * to a skolem definition. + */ + void addAssertion(TNode assertion) override; + /** + * Notify this class that lem is the skolem definition for skolem, which is + * a part of the current assertions. + */ + void addSkolemDefinition(TNode lem, TNode skolem) override; private: /* getNext with an option to specify threshold */ |