summaryrefslogtreecommitdiff
path: root/src/theory/combination_care_graph.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-08-28 15:40:16 -0500
committerGitHub <noreply@github.com>2020-08-28 15:40:16 -0500
commitf51d3e353fe8e50e5e73c37c17229e603a56ecdd (patch)
treed3a00e94d2850aaac623d81df04a0bfc7f762087 /src/theory/combination_care_graph.h
parentc137366e668aff70b1739a1f2c5cf8e6e2e28a72 (diff)
(proof-new) Make CombinationEngine proof producing (#4955)
Makes combination engine proof producing (for Boolean splits). Followup PRs will start to add proof production in TheoryEngine.
Diffstat (limited to 'src/theory/combination_care_graph.h')
-rw-r--r--src/theory/combination_care_graph.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/combination_care_graph.h b/src/theory/combination_care_graph.h
index 0fbefb16a..78f892f5e 100644
--- a/src/theory/combination_care_graph.h
+++ b/src/theory/combination_care_graph.h
@@ -35,7 +35,8 @@ class CombinationCareGraph : public CombinationEngine
{
public:
CombinationCareGraph(TheoryEngine& te,
- const std::vector<Theory*>& paraTheories);
+ const std::vector<Theory*>& paraTheories,
+ ProofNodeManager* pnm);
~CombinationCareGraph();
bool buildModel() override;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback