From f5e2348c7350ce21716f595eb8703635782c6285 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 19 Jun 2020 14:40:27 -0500 Subject: [PATCH] Clean the header file of TheoryStrings (#4272) Now conforms to coding guidelines. For the sake of ensuring that the aspects related to the strategy were maintained in one place, I split this to its own file, strategy.h/cpp. --- src/CMakeLists.txt | 2 + src/theory/strings/strategy.cpp | 161 ++++++++++++++ src/theory/strings/strategy.h | 116 +++++++++++ src/theory/strings/theory_strings.cpp | 163 ++------------- src/theory/strings/theory_strings.h | 289 +++++++++----------------- 5 files changed, 397 insertions(+), 334 deletions(-) create mode 100644 src/theory/strings/strategy.cpp create mode 100644 src/theory/strings/strategy.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c50578c46..d16164562 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -716,6 +716,8 @@ libcvc4_add_sources( theory/strings/skolem_cache.h theory/strings/solver_state.cpp theory/strings/solver_state.h + theory/strings/strategy.cpp + theory/strings/strategy.h theory/strings/strings_entail.cpp theory/strings/strings_entail.h theory/strings/strings_fmf.cpp 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 >::iterator Strategy::stepBegin( + Theory::Effort e) +{ + std::map >::const_iterator it = + d_strat_steps.find(e); + Assert(it != d_strat_steps.end()); + return d_infer_steps.begin() + it->second.first; +} + +std::vector >::iterator Strategy::stepEnd( + Theory::Effort e) +{ + std::map >::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(s, effort)); + if (addBreak) + { + d_infer_steps.push_back(std::pair(BREAK, 0)); + } +} + +void Strategy::initializeStrategy() +{ + // initialize the strategy if not already done so + if (!d_strategy_init) + { + std::map step_begin; + std::map 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& it_begin : step_begin) + { + Theory::Effort e = it_begin.first; + std::map::iterator it_end = step_end.find(e); + Assert(it_end != step_end.end()); + d_strat_steps[e] = + std::pair(it_begin.second, it_end->second); + } + } +} + +} // namespace strings +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/strings/strategy.h b/src/theory/strings/strategy.h new file mode 100644 index 000000000..9afb6a92f --- /dev/null +++ b/src/theory/strings/strategy.h @@ -0,0 +1,116 @@ +/********************* */ +/*! \file strategy.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Strategy of the theory of strings + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__STRINGS__STRATEGY_H +#define CVC4__THEORY__STRINGS__STRATEGY_H + +#include +#include + +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +/** inference steps + * + * Corresponds to a step in the overall strategy of the strings solver. For + * details on the individual steps, see documentation on the inference schemas + * within Strategy. + */ +enum InferStep +{ + // indicates that the strategy should break if lemmas or facts are added + BREAK, + // check initial + CHECK_INIT, + // check constant equivalence classes + CHECK_CONST_EQC, + // check extended function evaluation + CHECK_EXTF_EVAL, + // check cycles + CHECK_CYCLES, + // check flat forms + CHECK_FLAT_FORMS, + // check register terms pre-normal forms + CHECK_REGISTER_TERMS_PRE_NF, + // check normal forms equalities + CHECK_NORMAL_FORMS_EQ, + // check normal forms disequalities + CHECK_NORMAL_FORMS_DEQ, + // check codes + CHECK_CODES, + // check lengths for equivalence classes + CHECK_LENGTH_EQC, + // check register terms for normal forms + CHECK_REGISTER_TERMS_NF, + // check extended function reductions + CHECK_EXTF_REDUCTION, + // check regular expression memberships + CHECK_MEMBERSHIP, + // check cardinality + CHECK_CARDINALITY, +}; +std::ostream& operator<<(std::ostream& out, InferStep i); + +/** + * The strategy of theory of strings. + * + * This stores a sequence of the above enum that indicates the calls to + * runInferStep to make on the theory of strings, given by parent. + */ +class Strategy +{ + public: + Strategy(); + ~Strategy(); + /** is this strategy initialized? */ + bool isStrategyInit() const; + /** do we have a strategy for effort e? */ + bool hasStrategyEffort(Theory::Effort e) const; + /** begin and end iterators for effort e */ + std::vector >::iterator stepBegin(Theory::Effort e); + std::vector >::iterator stepEnd(Theory::Effort e); + /** initialize the strategy + * + * This initializes the above information based on the options. This makes + * a series of calls to addStrategyStep above. + */ + void initializeStrategy(); + + private: + /** add strategy step + * + * This adds (s,effort) as a strategy step to the vectors d_infer_steps and + * d_infer_step_effort. This indicates that a call to runInferStep should + * be run as the next step in the strategy. If addBreak is true, we add + * a BREAK to the strategy following this step. + */ + void addStrategyStep(InferStep s, int effort = 0, bool addBreak = true); + /** is strategy initialized */ + bool d_strategy_init; + /** the strategy */ + std::vector > d_infer_steps; + /** the range (begin, end) of steps to run at given efforts */ + std::map > d_strat_steps; +}; /* class Strategy */ + +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__STRATEGY_H */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8b9eb7124..562d8eab8 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -10,20 +10,14 @@ ** directory for licensing information.\endverbatim ** ** \brief Implementation of the theory of strings. - ** - ** Implementation of the theory of strings. **/ #include "theory/strings/theory_strings.h" -#include - #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" #include "theory/ext_theory.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" @@ -40,28 +34,6 @@ 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; -} - TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, @@ -79,8 +51,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_csolver(nullptr), d_esolver(nullptr), d_rsolver(nullptr), - d_stringsFmf(c, u, valuation, d_termReg), - d_strategy_init(false) + d_stringsFmf(c, u, valuation, d_termReg) { setupExtTheory(); ExtTheory* extt = getExtTheory(); @@ -139,6 +110,15 @@ TheoryStrings::~TheoryStrings() { } +TheoryRewriter* TheoryStrings::getTheoryRewriter() { return &d_rewriter; } +std::string TheoryStrings::identify() const +{ + return std::string("TheoryStrings"); +} +eq::EqualityEngine* TheoryStrings::getEqualityEngine() +{ + return &d_equalityEngine; +} void TheoryStrings::finishInit() { TheoryModel* tm = d_valuation.getModel(); @@ -235,14 +215,9 @@ bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& var return true; } -///////////////////////////////////////////////////////////////////////////// -// NOTIFICATIONS -///////////////////////////////////////////////////////////////////////////// - - void TheoryStrings::presolve() { Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl; - initializeStrategy(); + d_strat.initializeStrategy(); // if strings fmf is enabled, register the strategy if (options::stringFMF()) @@ -639,11 +614,9 @@ void TheoryStrings::check(Effort e) { } d_im->doPendingFacts(); - Assert(d_strategy_init); - std::map >::iterator itsr = - d_strat_steps.find(e); + Assert(d_strat.isStrategyInit()); if (!d_state.isInConflict() && !d_valuation.needCheck() - && itsr != d_strat_steps.end()) + && d_strat.hasStrategyEffort(e)) { Trace("strings-check-debug") << "Theory of strings " << e << " effort check " << std::endl; @@ -684,15 +657,13 @@ void TheoryStrings::check(Effort e) { Trace("strings-eqc") << std::endl; } ++(d_statistics.d_checkRuns); - unsigned sbegin = itsr->second.first; - unsigned send = itsr->second.second; bool addedLemma = false; bool addedFact; Trace("strings-check") << "Full effort check..." << std::endl; do{ ++(d_statistics.d_strategyRuns); Trace("strings-check") << " * Run strategy..." << std::endl; - runStrategy(sbegin, send); + runStrategy(e); // flush the facts addedFact = d_im->hasPendingFact(); addedLemma = d_im->hasPendingLemma(); @@ -1045,107 +1016,16 @@ void TheoryStrings::runInferStep(InferStep s, int effort) << std::endl; } -bool TheoryStrings::hasStrategyEffort(Effort e) const -{ - return d_strat_steps.find(e) != d_strat_steps.end(); -} - -void TheoryStrings::addStrategyStep(InferStep s, int effort, bool addBreak) -{ - // must run check init first - Assert((s == CHECK_INIT) == d_infer_steps.empty()); - // must use check cycles when using flat forms - Assert(s != CHECK_FLAT_FORMS - || std::find(d_infer_steps.begin(), d_infer_steps.end(), CHECK_CYCLES) - != d_infer_steps.end()); - d_infer_steps.push_back(s); - d_infer_step_effort.push_back(effort); - if (addBreak) - { - d_infer_steps.push_back(BREAK); - d_infer_step_effort.push_back(0); - } -} - -void TheoryStrings::initializeStrategy() +void TheoryStrings::runStrategy(Theory::Effort e) { - // initialize the strategy if not already done so - if (!d_strategy_init) - { - std::map step_begin; - std::map step_end; - d_strategy_init = true; - // beginning indices - step_begin[EFFORT_FULL] = 0; - if (options::stringEager()) - { - step_begin[EFFORT_STANDARD] = 0; - } - // add the inference steps - addStrategyStep(CHECK_INIT); - addStrategyStep(CHECK_CONST_EQC); - addStrategyStep(CHECK_EXTF_EVAL, 0); - 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[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[EFFORT_FULL] = d_infer_steps.size() - 1; - if (options::stringExp() && options::stringGuessModel()) - { - step_begin[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[EFFORT_LAST_CALL] = d_infer_steps.size() - 1; - } - // set the beginning/ending ranges - for (const std::pair& it_begin : step_begin) - { - Effort e = it_begin.first; - std::map::iterator it_end = step_end.find(e); - Assert(it_end != step_end.end()); - d_strat_steps[e] = - std::pair(it_begin.second, it_end->second); - } - } -} + std::vector >::iterator it = d_strat.stepBegin(e); + std::vector >::iterator stepEnd = + d_strat.stepEnd(e); -void TheoryStrings::runStrategy(unsigned sbegin, unsigned send) -{ Trace("strings-process") << "----check, next round---" << std::endl; - for (unsigned i = sbegin; i <= send; i++) + while (it != stepEnd) { - InferStep curr = d_infer_steps[i]; + InferStep curr = it->first; if (curr == BREAK) { if (d_im->hasProcessed()) @@ -1155,12 +1035,13 @@ void TheoryStrings::runStrategy(unsigned sbegin, unsigned send) } else { - runInferStep(curr, d_infer_step_effort[i]); + runInferStep(curr, it->second); if (d_state.isInConflict()) { break; } } + ++it; } Trace("strings-process") << "----finished round---" << std::endl; } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 90a97fe3c..368c13a2d 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -35,8 +35,8 @@ #include "theory/strings/regexp_operation.h" #include "theory/strings/regexp_solver.h" #include "theory/strings/sequences_stats.h" -#include "theory/strings/skolem_cache.h" #include "theory/strings/solver_state.h" +#include "theory/strings/strategy.h" #include "theory/strings/strings_fmf.h" #include "theory/strings/strings_rewriter.h" #include "theory/strings/term_registry.h" @@ -48,91 +48,72 @@ namespace theory { namespace strings { /** - * Decision procedure for strings. - * + * A theory solver for strings. At a high level, the solver implements + * techniques described in: + * - Liang et al, CAV 2014, + * - Reynolds et al, CAV 2017, + * - Reynolds et al, IJCAR 2020. + * Its rewriter is described in: + * - Reynolds et al, CAV 2019. */ - -/** inference steps - * - * Corresponds to a step in the overall strategy of the strings solver. For - * details on the individual steps, see documentation on the inference schemas - * within TheoryStrings. - */ -enum InferStep -{ - // indicates that the strategy should break if lemmas or facts are added - BREAK, - // check initial - CHECK_INIT, - // check constant equivalence classes - CHECK_CONST_EQC, - // check extended function evaluation - CHECK_EXTF_EVAL, - // check cycles - CHECK_CYCLES, - // check flat forms - CHECK_FLAT_FORMS, - // check register terms pre-normal forms - CHECK_REGISTER_TERMS_PRE_NF, - // check normal forms equalities - CHECK_NORMAL_FORMS_EQ, - // check normal forms disequalities - CHECK_NORMAL_FORMS_DEQ, - // check codes - CHECK_CODES, - // check lengths for equivalence classes - CHECK_LENGTH_EQC, - // check register terms for normal forms - CHECK_REGISTER_TERMS_NF, - // check extended function reductions - CHECK_EXTF_REDUCTION, - // check regular expression memberships - CHECK_MEMBERSHIP, - // check cardinality - CHECK_CARDINALITY, -}; -std::ostream& operator<<(std::ostream& out, Inference i); - class TheoryStrings : public Theory { friend class InferenceManager; - typedef context::CDList NodeList; - typedef context::CDHashMap NodeBoolMap; - typedef context::CDHashMap NodeIntMap; - typedef context::CDHashMap NodeNodeMap; typedef context::CDHashSet NodeSet; typedef context::CDHashSet TypeNodeSet; - public: TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryStrings(); - /** finish initialization */ void finishInit() override; - - TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } - + /** Get the theory rewriter of this class */ + TheoryRewriter* getTheoryRewriter() override; + /** Set the master equality engine */ void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - - std::string identify() const override { return std::string("TheoryStrings"); } - - public: + /** Identify this theory */ + std::string identify() const override; + /** Propagate */ void propagate(Effort e) override; - bool propagate(TNode literal); + /** Explain */ Node explain(TNode literal) override; - eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } + /** Get the equality engine */ + eq::EqualityEngine* getEqualityEngine() override; + /** Get current substitution */ bool getCurrentSubstitution(int effort, std::vector& vars, std::vector& subs, std::map >& exp) override; + /** presolve */ + void presolve() override; + /** shutdown */ + void shutdown() override {} + /** add shared term */ + void addSharedTerm(TNode n) override; + /** get equality status */ + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + /** preregister term */ + void preRegisterTerm(TNode n) override; + /** Expand definition */ + Node expandDefinition(Node n) override; + /** Check at effort e */ + void check(Effort e) override; + /** needs check last effort */ + bool needsCheckLastEffort() override; + /** Conflict when merging two constants */ + void conflict(TNode a, TNode b); + /** called when a new equivalence class is created */ + void eqNotifyNewClass(TNode t); + /** preprocess rewrite */ + Node ppRewrite(TNode atom) override; /** * Get all relevant information in this theory regarding the current * model. Return false if a contradiction is discovered. */ bool collectModelInfo(TheoryModel* m) override; - // NotifyClass for equality engine + private: + /** NotifyClass for equality engine */ class NotifyClass : public eq::EqualityEngineNotify { public: NotifyClass(TheoryStrings& ts) : d_str(ts), d_state(ts.d_state) {} @@ -202,74 +183,8 @@ class TheoryStrings : public Theory { /** The solver state of the theory of strings */ SolverState& d_state; };/* class TheoryStrings::NotifyClass */ - - private: - // Constants - Node d_emptyString; - Node d_true; - Node d_false; - Node d_zero; - Node d_one; - Node d_neg_one; - /** the cardinality of the alphabet */ - uint32_t d_cardSize; - /** The notify class */ - NotifyClass d_notify; - - /** - * Statistics for the theory of strings/sequences. All statistics for these - * theories is collected in this object. - */ - SequencesStatistics d_statistics; - - /** Equaltity engine */ - eq::EqualityEngine d_equalityEngine; - /** The solver state object */ - SolverState d_state; - /** The term registry for this theory */ - TermRegistry d_termReg; - /** The (custom) output channel of the theory of strings */ - std::unique_ptr d_im; - - private: - std::map< Node, Node > d_eqc_to_len_term; - - - ///////////////////////////////////////////////////////////////////////////// - // NOTIFICATIONS - ///////////////////////////////////////////////////////////////////////////// - public: - void presolve() override; - void shutdown() override {} - - ///////////////////////////////////////////////////////////////////////////// - // MAIN SOLVER - ///////////////////////////////////////////////////////////////////////////// - private: - void addSharedTerm(TNode n) override; - EqualityStatus getEqualityStatus(TNode a, TNode b) override; - - private: - void addCarePairs(TNodeTrie* t1, - TNodeTrie* t2, - unsigned arity, - unsigned depth); - - public: - /** preregister term */ - void preRegisterTerm(TNode n) override; - /** Expand definition */ - Node expandDefinition(Node n) override; - /** Check at effort e */ - void check(Effort e) override; - /** needs check last effort */ - bool needsCheckLastEffort() override; - /** Conflict when merging two constants */ - void conflict(TNode a, TNode b); - /** called when a new equivalence class is created */ - void eqNotifyNewClass(TNode t); - - protected: + /** propagate method */ + bool propagate(TNode literal); /** compute care graph */ void computeCareGraph() override; /** @@ -277,7 +192,11 @@ class TheoryStrings : public Theory { * the care graph in the above function. */ bool areCareDisequal(TNode x, TNode y); - + /** Add care pairs */ + void addCarePairs(TNodeTrie* t1, + TNodeTrie* t2, + unsigned arity, + unsigned depth); /** Collect model info for type tn * * Assigns model values (in m) to all relevant terms of the string-like type @@ -303,38 +222,6 @@ class TheoryStrings : public Theory { * of atom, including calls to registerTerm. */ void assertPendingFact(Node atom, bool polarity, Node exp); - - // Symbolic Regular Expression - private: - /** The theory rewriter for this theory. */ - StringsRewriter d_rewriter; - /** - * The base solver, responsible for reasoning about congruent terms and - * inferring constants for equivalence classes. - */ - std::unique_ptr d_bsolver; - /** - * The core solver, responsible for reasoning about string concatenation - * with length constraints. - */ - std::unique_ptr d_csolver; - /** - * Extended function solver, responsible for reductions and simplifications - * involving extended string functions. - */ - std::unique_ptr d_esolver; - /** regular expression solver module */ - std::unique_ptr d_rsolver; - /** regular expression elimination module */ - RegExpElimination d_regexp_elim; - /** Strings finite model finding decision strategy */ - StringsFmf d_stringsFmf; - - public: - // ppRewrite - Node ppRewrite(TNode atom) override; - - private: //-----------------------inference steps /** check register terms pre-normal forms * @@ -360,42 +247,58 @@ class TheoryStrings : public Theory { */ void checkRegisterTermsNormalForms(); //-----------------------end inference steps - - //-----------------------representation of the strategy - /** is strategy initialized */ - bool d_strategy_init; /** run the given inference step */ void runInferStep(InferStep s, int effort); - /** the strategy */ - std::vector d_infer_steps; - /** the effort levels */ - std::vector d_infer_step_effort; - /** the range (begin, end) of steps to run at given efforts */ - std::map > d_strat_steps; - /** do we have a strategy for effort e? */ - bool hasStrategyEffort(Effort e) const; - /** initialize the strategy - * - * This adds (s,effort) as a strategy step to the vectors d_infer_steps and - * d_infer_step_effort. This indicates that a call to runInferStep should - * be run as the next step in the strategy. If addBreak is true, we add - * a BREAK to the strategy following this step. + /** run strategy for effort e */ + void runStrategy(Theory::Effort e); + /** Commonly used constants */ + Node d_true; + Node d_false; + Node d_zero; + Node d_one; + Node d_neg_one; + /** the cardinality of the alphabet */ + uint32_t d_cardSize; + /** The notify class */ + NotifyClass d_notify; + /** + * Statistics for the theory of strings/sequences. All statistics for these + * theories is collected in this object. */ - void addStrategyStep(InferStep s, int effort = 0, bool addBreak = true); - /** initialize the strategy - * - * This initializes the above information based on the options. This makes - * a series of calls to addStrategyStep above. + SequencesStatistics d_statistics; + /** Equaltity engine */ + eq::EqualityEngine d_equalityEngine; + /** The solver state object */ + SolverState d_state; + /** The term registry for this theory */ + TermRegistry d_termReg; + /** The (custom) output channel of the theory of strings */ + std::unique_ptr d_im; + /** The theory rewriter for this theory. */ + StringsRewriter d_rewriter; + /** + * The base solver, responsible for reasoning about congruent terms and + * inferring constants for equivalence classes. */ - void initializeStrategy(); - /** run strategy - * - * This executes the inference steps starting at index sbegin and ending at - * index send. We exit if any step in this sequence adds a lemma or infers a - * fact. + std::unique_ptr d_bsolver; + /** + * The core solver, responsible for reasoning about string concatenation + * with length constraints. */ - void runStrategy(unsigned sbegin, unsigned send); - //-----------------------end representation of the strategy + std::unique_ptr d_csolver; + /** + * Extended function solver, responsible for reductions and simplifications + * involving extended string functions. + */ + std::unique_ptr d_esolver; + /** regular expression solver module */ + std::unique_ptr d_rsolver; + /** regular expression elimination module */ + RegExpElimination d_regexp_elim; + /** Strings finite model finding decision strategy */ + StringsFmf d_stringsFmf; + /** The representation of the strategy */ + Strategy d_strat; };/* class TheoryStrings */ }/* CVC4::theory::strings namespace */ -- 2.30.2