diff options
Diffstat (limited to 'src/theory/strings/strategy.cpp')
| -rw-r--r-- | src/theory/strings/strategy.cpp | 161 |
1 files changed, 161 insertions, 0 deletions
diff --git a/src/theory/strings/strategy.cpp b/src/theory/strings/strategy.cpp new file mode 100644 index 000000000..549bba9d6 --- /dev/null +++ b/src/theory/strings/strategy.cpp @@ -0,0 +1,161 @@ +/********************* */ +/*! \file strategy.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tianyi Liang, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of the strategy of the theory of strings. + **/ + +#include "theory/strings/strategy.h" + +#include "options/strings_options.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +std::ostream& operator<<(std::ostream& out, InferStep s) +{ + switch (s) + { + case BREAK: out << "break"; break; + case CHECK_INIT: out << "check_init"; break; + case CHECK_CONST_EQC: out << "check_const_eqc"; break; + case CHECK_EXTF_EVAL: out << "check_extf_eval"; break; + case CHECK_CYCLES: out << "check_cycles"; break; + case CHECK_FLAT_FORMS: out << "check_flat_forms"; break; + case CHECK_NORMAL_FORMS_EQ: out << "check_normal_forms_eq"; break; + case CHECK_NORMAL_FORMS_DEQ: out << "check_normal_forms_deq"; break; + case CHECK_CODES: out << "check_codes"; break; + case CHECK_LENGTH_EQC: out << "check_length_eqc"; break; + case CHECK_EXTF_REDUCTION: out << "check_extf_reduction"; break; + case CHECK_MEMBERSHIP: out << "check_membership"; break; + case CHECK_CARDINALITY: out << "check_cardinality"; break; + default: out << "?"; break; + } + return out; +} + +Strategy::Strategy() : d_strategy_init(false) {} + +Strategy::~Strategy() {} + +bool Strategy::isStrategyInit() const { return d_strategy_init; } + +bool Strategy::hasStrategyEffort(Theory::Effort e) const +{ + return d_strat_steps.find(e) != d_strat_steps.end(); +} + +std::vector<std::pair<InferStep, int> >::iterator Strategy::stepBegin( + Theory::Effort e) +{ + std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it = + d_strat_steps.find(e); + Assert(it != d_strat_steps.end()); + return d_infer_steps.begin() + it->second.first; +} + +std::vector<std::pair<InferStep, int> >::iterator Strategy::stepEnd( + Theory::Effort e) +{ + std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it = + d_strat_steps.find(e); + Assert(it != d_strat_steps.end()); + return d_infer_steps.begin() + it->second.second; +} + +void Strategy::addStrategyStep(InferStep s, int effort, bool addBreak) +{ + // must run check init first + Assert((s == CHECK_INIT) == d_infer_steps.empty()); + d_infer_steps.push_back(std::pair<InferStep, int>(s, effort)); + if (addBreak) + { + d_infer_steps.push_back(std::pair<InferStep, int>(BREAK, 0)); + } +} + +void Strategy::initializeStrategy() +{ + // initialize the strategy if not already done so + if (!d_strategy_init) + { + std::map<Theory::Effort, unsigned> step_begin; + std::map<Theory::Effort, unsigned> step_end; + d_strategy_init = true; + // beginning indices + step_begin[Theory::EFFORT_FULL] = 0; + if (options::stringEager()) + { + step_begin[Theory::EFFORT_STANDARD] = 0; + } + // add the inference steps + addStrategyStep(CHECK_INIT); + addStrategyStep(CHECK_CONST_EQC); + addStrategyStep(CHECK_EXTF_EVAL, 0); + // we must check cycles before using flat forms + addStrategyStep(CHECK_CYCLES); + if (options::stringFlatForms()) + { + addStrategyStep(CHECK_FLAT_FORMS); + } + addStrategyStep(CHECK_EXTF_REDUCTION, 1); + if (options::stringEager()) + { + // do only the above inferences at standard effort, if applicable + step_end[Theory::EFFORT_STANDARD] = d_infer_steps.size() - 1; + } + if (!options::stringEagerLen()) + { + addStrategyStep(CHECK_REGISTER_TERMS_PRE_NF); + } + addStrategyStep(CHECK_NORMAL_FORMS_EQ); + addStrategyStep(CHECK_EXTF_EVAL, 1); + if (!options::stringEagerLen() && options::stringLenNorm()) + { + addStrategyStep(CHECK_LENGTH_EQC, 0, false); + addStrategyStep(CHECK_REGISTER_TERMS_NF); + } + addStrategyStep(CHECK_NORMAL_FORMS_DEQ); + addStrategyStep(CHECK_CODES); + if (options::stringEagerLen() && options::stringLenNorm()) + { + addStrategyStep(CHECK_LENGTH_EQC); + } + if (options::stringExp() && !options::stringGuessModel()) + { + addStrategyStep(CHECK_EXTF_REDUCTION, 2); + } + addStrategyStep(CHECK_MEMBERSHIP); + addStrategyStep(CHECK_CARDINALITY); + step_end[Theory::EFFORT_FULL] = d_infer_steps.size() - 1; + if (options::stringExp() && options::stringGuessModel()) + { + step_begin[Theory::EFFORT_LAST_CALL] = d_infer_steps.size(); + // these two steps are run in parallel + addStrategyStep(CHECK_EXTF_REDUCTION, 2, false); + addStrategyStep(CHECK_EXTF_EVAL, 3); + step_end[Theory::EFFORT_LAST_CALL] = d_infer_steps.size() - 1; + } + // set the beginning/ending ranges + for (const std::pair<const Theory::Effort, unsigned>& it_begin : step_begin) + { + Theory::Effort e = it_begin.first; + std::map<Theory::Effort, unsigned>::iterator it_end = step_end.find(e); + Assert(it_end != step_end.end()); + d_strat_steps[e] = + std::pair<unsigned, unsigned>(it_begin.second, it_end->second); + } + } +} + +} // namespace strings +} // namespace theory +} // namespace CVC4 |