diff options
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 297 |
1 files changed, 102 insertions, 195 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 7c99b6968..368c13a2d 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tianyi Liang, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -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<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) {} @@ -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<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; /** @@ -277,17 +192,25 @@ 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 - * tn in the current context, which are stored in repSet. + * tn in the current context, which are stored in repSet. Furthermore, + * col is a partition of repSet where equivalence classes are grouped into + * sets having equal length, where these lengths are stored in lts. * * Returns false if a conflict is discovered while doing this assignment. */ bool collectModelInfoType( TypeNode tn, const std::unordered_set<Node, NodeHashFunction>& repSet, + std::vector<std::vector<Node> >& col, + std::vector<Node>& lts, TheoryModel* m); /** assert pending fact @@ -299,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<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 * @@ -356,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<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 */ |