diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-09-04 11:35:50 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-04 11:35:50 -0700 |
| commit | 32530dad5747665df4086abd2c4fabff15bb7d12 (patch) | |
| tree | d662902d9c61a418b17bb1058899c90f75bf30d4 /src/theory/booleans | |
| parent | 4c9c917c41af40d1cbb00e33551756450a43c025 (diff) | |
Transfer ownership of learned literals from SMT engine to circuit propagator. (#2421)
Diffstat (limited to 'src/theory/booleans')
| -rw-r--r-- | src/theory/booleans/circuit_propagator.h | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index adb1eb42f..077a019fd 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -63,15 +63,13 @@ class CircuitPropagator /** * Construct a new CircuitPropagator. */ - CircuitPropagator(std::vector<Node>& outLearnedLiterals, - bool enableForward = true, - bool enableBackward = true) + CircuitPropagator(bool enableForward = true, bool enableBackward = true) : d_context(), d_propagationQueue(), d_propagationQueueClearer(&d_context, d_propagationQueue), d_conflict(&d_context, false), - d_learnedLiterals(outLearnedLiterals), - d_learnedLiteralClearer(&d_context, outLearnedLiterals), + d_learnedLiterals(), + d_learnedLiteralClearer(&d_context, d_learnedLiterals), d_backEdges(), d_backEdgesClearer(&d_context, d_backEdges), d_seen(&d_context), @@ -97,6 +95,8 @@ class CircuitPropagator bool getNeedsFinish() { return d_needsFinish; } + std::vector<Node>& getLearnedLiterals() { return d_learnedLiterals; } + void finish() { d_context.pop(); } /** Assert for propagation */ @@ -275,12 +275,12 @@ class CircuitPropagator context::CDO<bool> d_conflict; /** Map of substitutions */ - std::vector<Node>& d_learnedLiterals; + std::vector<Node> d_learnedLiterals; /** * Similar data clearer for learned literals. */ - DataClearer<std::vector<Node> > d_learnedLiteralClearer; + DataClearer<std::vector<Node>> d_learnedLiteralClearer; /** * Back edges from nodes to where they are used. |