diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-25 21:09:22 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-25 23:09:22 -0500 |
| commit | b70ccff4de0a23bdf11c70002d10a2cc0795a91c (patch) | |
| tree | 9898234cdf62e2e58941ba1dd9bed2dca5de8e50 /src/preprocessing/preprocessing_pass_context.h | |
| parent | c66033a67511b10b5ee22b7072b9ceab45552a79 (diff) | |
Refactor unconstrained simplification pass (#2374)
Diffstat (limited to 'src/preprocessing/preprocessing_pass_context.h')
| -rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index a289752fa..96e554680 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -43,6 +43,7 @@ class PreprocessingPassContext DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; } prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; } context::Context* getUserContext() { return d_smt->d_userContext; } + context::Context* getDecisionContext() { return d_smt->d_context; } RemoveTermFormulas* getIteRemover() { return d_iteRemover; } void spendResource(unsigned amount) @@ -50,6 +51,8 @@ class PreprocessingPassContext d_resourceManager->spendResource(amount); } + const LogicInfo& getLogicInfo() { return d_smt->d_logic; } + /* Widen the logic to include the given theory. */ void widenLogic(theory::TheoryId id); |