diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-09-03 16:33:33 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-03 23:33:33 +0000 |
| commit | 1eb3c6c8eb3da95cababcc0b1705c0299eee099c (patch) | |
| tree | 72233917af15c553dfbbf59f1125952cab83c89b /src/theory/quantifiers | |
| parent | 5cef06bd2beff38a911c74ec082d9789eed83421 (diff) | |
EnvObj: Add options(), context(), userContext(). (#7137)
This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 2b6719b27..bcd826799 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -189,7 +189,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, // check whether it is not in the current logic, e.g. non-linear arithmetic. // if so, undo replacements until it is in the current logic. - const LogicInfo& logic = getLogicInfo(); + const LogicInfo& logic = logicInfo(); if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear()) { fo_body = fitToLogic(sygusBody, diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 2ad475f01..67c40eaac 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -34,7 +34,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_QUANTIFIERS, env, out, valuation), - d_qstate(env, valuation, getLogicInfo()), + d_qstate(env, valuation, logicInfo()), d_qreg(), d_treg(d_qstate, d_qreg), d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm), |