diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-04 09:31:22 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-04 09:31:22 -0600 |
commit | d0f7a3922e38483908d4b86829241a48d8d8db57 (patch) | |
tree | 962228c839eaffbc8f4dbd949eb5dd666b6ca7b9 /src/theory/strings/theory_strings.h | |
parent | d90b26309b0f3a4ca9d57349f6cedf7b8bbbe6a8 (diff) |
Split base solver from the theory of strings (#3680)
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r-- | src/theory/strings/theory_strings.h | 66 |
1 files changed, 6 insertions, 60 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index ce92ada86..3b53fcded 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -24,6 +24,7 @@ #include "expr/attribute.h" #include "expr/node_trie.h" #include "theory/decision_manager.h" +#include "theory/strings/base_solver.h" #include "theory/strings/infer_info.h" #include "theory/strings/inference_manager.h" #include "theory/strings/normal_form.h" @@ -244,30 +245,6 @@ class TheoryStrings : public Theory { NodeSet d_extf_infer_cache; std::vector< Node > d_empty_vec; private: - NodeSet d_congruent; - /** - * The following three vectors are used for tracking constants that each - * equivalence class is entailed to be equal to. - * - The map d_eqc_to_const maps (representatives) r of equivalence classes to - * the constant that that equivalence class is entailed to be equal to, - * - The term d_eqc_to_const_base[r] is the term in the equivalence class r - * that is entailed to be equal to the constant d_eqc_to_const[r], - * - The term d_eqc_to_const_exp[r] is the explanation of why - * d_eqc_to_const_base[r] is equal to d_eqc_to_const[r]. - * - * For example, consider the equivalence class { r, x++"a"++y, x++z }, and - * assume x = "" and y = "bb" in the current context. We have that - * d_eqc_to_const[r] = "abb", - * d_eqc_to_const_base[r] = x++"a"++y - * d_eqc_to_const_exp[r] = ( x = "" AND y = "bb" ) - * - * This information is computed during checkInit and is used during various - * inference schemas for deriving inferences. - */ - std::map< Node, Node > d_eqc_to_const; - std::map< Node, Node > d_eqc_to_const_base; - std::map< Node, Node > d_eqc_to_const_exp; - Node getConstantEqc( Node eqc ); /** * Get the current substitution for term n. * @@ -285,19 +262,6 @@ private: std::map< Node, Node > d_eqc_to_len_term; std::vector< Node > d_strings_eqc; - Node d_emptyString_r; - class TermIndex { - public: - Node d_data; - std::map< TNode, TermIndex > d_children; - Node add(TNode n, - unsigned index, - const SolverState& s, - Node er, - std::vector<Node>& c); - void clear(){ d_children.clear(); } - }; - std::map< Kind, TermIndex > d_term_index; //list of non-congruent concat terms in each eqc std::map< Node, std::vector< Node > > d_eqc; std::map< Node, std::vector< Node > > d_flat_form; @@ -360,7 +324,6 @@ private: /** cache of all skolems */ SkolemCache d_sk_cache; - void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ); /** Get proxy variable * * If this method returns the proxy variable for (string) term n if one @@ -619,6 +582,11 @@ private: // Symbolic Regular Expression private: + /** + * The base solver, responsible for reasoning about congruent terms and + * inferring constants for equivalence classes. + */ + BaseSolver d_bsolver; /** regular expression solver module */ RegExpSolver d_regexp_solver; /** regular expression elimination module */ @@ -688,28 +656,6 @@ private: private: //-----------------------inference steps - /** check initial - * - * This function initializes term indices for each strings function symbol. - * One key aspect of this construction is that concat terms are indexed by - * their list of non-empty components. For example, if x = "" is an equality - * asserted in this SAT context, then y ++ x ++ z may be indexed by (y,z). - * This method may infer various facts while building these term indices, for - * instance, based on congruence. An example would be inferring: - * y ++ x ++ z = y ++ z - * if both terms are registered in this SAT context. - * - * This function should be called as a first step of any strategy. - */ - void checkInit(); - /** check constant equivalence classes - * - * This function infers whether CONCAT terms can be simplified to constants. - * For example, if x = "a" and y = "b" are equalities in the current SAT - * context, then we may infer x ++ "c" ++ y is equivalent to "acb". In this - * case, we infer the fact x ++ "c" ++ y = "acb". - */ - void checkConstantEquivalenceClasses(); /** check extended functions evaluation * * This applies "context-dependent simplification" for all active extended |