diff options
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 10 | ||||
| -rw-r--r-- | src/theory/strings/solver_state.cpp | 3 | ||||
| -rw-r--r-- | src/theory/strings/solver_state.h | 3 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 13 |
4 files changed, 18 insertions, 11 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index b13b64f98..e4fe2cf17 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -374,7 +374,7 @@ bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems) bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems) { // do not compute intersections if the re intersection mode is none - if (options::stringRegExpInterMode() == RE_INTER_NONE) + if (options::stringRegExpInterMode() == options::RegExpInterMode::NONE) { return true; } @@ -397,19 +397,21 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems) } RegExpConstType rct = d_regexp_opr.getRegExpConstType(m[1]); if (rct == RE_C_VARIABLE - || (options::stringRegExpInterMode() == RE_INTER_CONSTANT + || (options::stringRegExpInterMode() + == options::RegExpInterMode::CONSTANT && rct != RE_C_CONRETE_CONSTANT)) { // cannot do intersection on RE with variables, or with re.allchar based // on option. continue; } - if (options::stringRegExpInterMode() == RE_INTER_ONE_CONSTANT) + if (options::stringRegExpInterMode() + == options::RegExpInterMode::ONE_CONSTANT) { if (!mi.isNull() && rcti >= RE_C_CONSTANT && rct >= RE_C_CONSTANT) { // if both have re.allchar, do not do intersection if the - // RE_INTER_ONE_CONSTANT option is set. + // options::RegExpInterMode::ONE_CONSTANT option is set. continue; } } diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index b69c99e8c..66ae8d6bc 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -284,7 +284,8 @@ void SolverState::setPendingConflictWhen(Node conf) Node SolverState::getPendingConflict() const { return d_pendingConflict; } -std::pair<bool, Node> SolverState::entailmentCheck(TheoryOfMode mode, TNode lit) +std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode, + TNode lit) { return d_valuation.entailmentCheck(mode, lit); } diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index a2001bb3b..46d198d36 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -22,6 +22,7 @@ #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" +#include "options/theory_options.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" @@ -171,7 +172,7 @@ class SolverState * * This calls entailmentCheck on the Valuation object of theory of strings. */ - std::pair<bool, Node> entailmentCheck(TheoryOfMode mode, TNode lit); + std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit); /** Separate by length * * Separate the string representatives in argument n into a partition cols diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index df2364790..7b00ed2e2 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -20,6 +20,7 @@ #include "expr/kind.h" #include "options/strings_options.h" +#include "options/theory_options.h" #include "smt/command.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" @@ -3369,7 +3370,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, Node lt2 = e==0 ? length_term_j : length_term_i; Node ent_lit = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, lt1, lt2 ) ); std::pair<bool, Node> et = d_state.entailmentCheck( - THEORY_OF_TYPE_BASED, ent_lit); + options::TheoryOfMode::THEORY_OF_TYPE_BASED, ent_lit); if( et.first ){ Trace("strings-entail") << "Strings entailment : " << ent_lit << " is entailed in the current context." << std::endl; Trace("strings-entail") << " explanation was : " << et.second << std::endl; @@ -3482,11 +3483,11 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi, int index, InferInfo& info) { - if (options::stringProcessLoopMode() == ProcessLoopMode::ABORT) + if (options::stringProcessLoopMode() == options::ProcessLoopMode::ABORT) { throw LogicException("Looping word equation encountered."); } - else if (options::stringProcessLoopMode() == ProcessLoopMode::NONE) + else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE) { d_out->setIncomplete(); return ProcessLoopResult::SKIPPED; @@ -3629,11 +3630,13 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi, } else { - if (options::stringProcessLoopMode() == ProcessLoopMode::SIMPLE_ABORT) + if (options::stringProcessLoopMode() + == options::ProcessLoopMode::SIMPLE_ABORT) { throw LogicException("Normal looping word equation encountered."); } - else if (options::stringProcessLoopMode() == ProcessLoopMode::SIMPLE) + else if (options::stringProcessLoopMode() + == options::ProcessLoopMode::SIMPLE) { d_out->setIncomplete(); return ProcessLoopResult::SKIPPED; |