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.
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <vector>
+
+#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<std::pair<InferStep, int> >::iterator stepBegin(Theory::Effort e);
+ std::vector<std::pair<InferStep, int> >::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<std::pair<InferStep, int> > d_infer_steps;
+ /** the range (begin, end) of steps to run at given efforts */
+ std::map<Theory::Effort, std::pair<unsigned, unsigned> > d_strat_steps;
+}; /* class Strategy */
+
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__STRATEGY_H */
** 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 <cmath>
-
#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"
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,
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();
}
+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();
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())
}
d_im->doPendingFacts();
- Assert(d_strategy_init);
- std::map<Effort, std::pair<unsigned, unsigned> >::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;
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();
<< 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<Effort, unsigned> step_begin;
- std::map<Effort, unsigned> 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<const Effort, unsigned>& it_begin : step_begin)
- {
- Effort e = it_begin.first;
- std::map<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);
- }
- }
-}
+ std::vector<std::pair<InferStep, int> >::iterator it = d_strat.stepBegin(e);
+ std::vector<std::pair<InferStep, int> >::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())
}
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;
}
#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"
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<Node> NodeList;
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
- typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> 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<Node>& vars,
std::vector<Node>& subs,
std::map<Node, std::vector<Node> >& 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) {}
/** 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<InferenceManager> 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;
/**
* 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
* 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<BaseSolver> d_bsolver;
- /**
- * The core solver, responsible for reasoning about string concatenation
- * with length constraints.
- */
- std::unique_ptr<CoreSolver> d_csolver;
- /**
- * Extended function solver, responsible for reductions and simplifications
- * involving extended string functions.
- */
- std::unique_ptr<ExtfSolver> d_esolver;
- /** regular expression solver module */
- std::unique_ptr<RegExpSolver> 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
*
*/
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<InferStep> d_infer_steps;
- /** the effort levels */
- std::vector<int> d_infer_step_effort;
- /** the range (begin, end) of steps to run at given efforts */
- std::map<Effort, std::pair<unsigned, unsigned> > 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<InferenceManager> 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<BaseSolver> 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<CoreSolver> d_csolver;
+ /**
+ * Extended function solver, responsible for reductions and simplifications
+ * involving extended string functions.
+ */
+ std::unique_ptr<ExtfSolver> d_esolver;
+ /** regular expression solver module */
+ std::unique_ptr<RegExpSolver> 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 */
projects / cvc5.git / commitdiff