summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes/ite_simp.cpp
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-09-03 16:33:33 -0700
committerGitHub <noreply@github.com>2021-09-03 23:33:33 +0000
commit1eb3c6c8eb3da95cababcc0b1705c0299eee099c (patch)
tree72233917af15c553dfbbf59f1125952cab83c89b /src/preprocessing/passes/ite_simp.cpp
parent5cef06bd2beff38a911c74ec082d9789eed83421 (diff)
EnvObj: Add options(), context(), userContext(). (#7137)
This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.
Diffstat (limited to 'src/preprocessing/passes/ite_simp.cpp')
-rw-r--r--src/preprocessing/passes/ite_simp.cpp9
1 files changed, 5 insertions, 4 deletions
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 54e2b657e..434256d28 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -144,16 +144,17 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
}
// Do theory specific preprocessing passes
- if (d_env.getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH)
+ if (logicInfo().isTheoryEnabled(theory::THEORY_ARITH)
&& !options::incrementalSolving())
{
if (!simpDidALotOfWork)
{
util::ContainsTermITEVisitor& contains =
*(d_iteUtilities.getContainsVisitor());
- arith::ArithIteUtils aiteu(contains,
- d_preprocContext->getUserContext(),
- d_preprocContext->getTopLevelSubstitutions().get());
+ arith::ArithIteUtils aiteu(
+ contains,
+ userContext(),
+ d_preprocContext->getTopLevelSubstitutions().get());
bool anyItes = false;
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback