diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-23 13:40:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-23 13:40:27 -0500 |
commit | 53cade050e191c7c0dc0ebfae716a21162bd9b22 (patch) | |
tree | 99ce8fa8224660143a6afb79e65362dc5f469c9a /src/theory/strings/theory_strings.h | |
parent | d43f7760866a1a26769dfdebdffebdaf35309f9c (diff) |
Refactor normal forms in strings (#2897)
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r-- | src/theory/strings/theory_strings.h | 126 |
1 files changed, 89 insertions, 37 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index b3cb323ae..e9d82a7b2 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/normal_form.h" #include "theory/strings/regexp_elim.h" #include "theory/strings/regexp_operation.h" #include "theory/strings/regexp_solver.h" @@ -307,11 +308,10 @@ class TheoryStrings : public Theory { /** inferences: maintained to ensure ref count for internally introduced nodes */ NodeList d_infer; NodeList d_infer_exp; - /** normal forms */ - std::map< Node, Node > d_normal_forms_base; - std::map< Node, std::vector< Node > > d_normal_forms; - std::map< Node, std::vector< Node > > d_normal_forms_exp; - std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend; + /** map from terms to their normal forms */ + std::map<Node, NormalForm> d_normal_form; + /** get normal form */ + NormalForm& getNormalForm(Node n); //map of pairs of terms that have the same normal form NodeIntMap d_nf_pairs; std::map< Node, std::vector< Node > > d_nf_pairs_data; @@ -468,8 +468,14 @@ private: class InferInfo { public: - unsigned d_i; - unsigned d_j; + /** for debugging + * + * The base pair of strings d_i/d_j that led to the inference, and whether + * (d_rev) we were processing the normal forms of these strings in reverse + * direction. + */ + Node d_i; + Node d_j; bool d_rev; std::vector<Node> d_ant; std::vector<Node> d_antn; @@ -554,10 +560,77 @@ private: //--------------------------end for checkCycles //--------------------------for checkNormalFormsEq + /** normalize equivalence class + * + * This method attempts to build a "normal form" for the equivalence class + * of string term n (for more details on normal forms, see normal_form.h + * or see Liang et al CAV 2014). In particular, this method checks whether the + * current normal form for each term in this equivalence class is identical. + * If it is not, then we add an inference via sendInference and abort the + * call. + */ void normalizeEquivalenceClass( Node n ); - void getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, - std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ); - bool detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, int index, int &loop_in_i, int &loop_in_j, unsigned rproc ); + /** + * For each term in the equivalence class of eqc, this adds data regarding its + * normal form to normal_forms. The map term_to_nf_index maps terms to the + * index in normal_forms where their normal form data is located. + */ + void getNormalForms(Node eqc, + std::vector<NormalForm>& normal_forms, + std::map<Node, unsigned>& term_to_nf_index); + /** process normalize equivalence class + * + * This is called when an equivalence class contains a set of terms that + * have normal forms given by the argument normal_forms. It either + * verifies that all normal forms in this vector are identical, or otherwise + * adds a conflict, lemma, or inference via the sendInference method. + * + * To prioritize one inference versus another, it builds a set of possible + * inferences, at most two for each pair of distinct normal forms, + * corresponding to processing the normal form pair in the (forward, reverse) + * directions. Once all possible inferences are recorded, it executes the + * one with highest priority based on the enumeration type Inference. + */ + void processNEqc(std::vector<NormalForm>& normal_forms); + /** process simple normal equality + * + * This method is called when two equal terms have normal forms nfi and nfj. + * It adds (typically at most one) possible inference to the vector pinfer. + * This inference is in the form of an InferInfo object, which stores the + * necessary information regarding how to process the inference. + * + * index: The index in the normal form vectors (nfi.d_nf and nfj.d_nf) that + * we are currently checking. This method will increment this index until + * it finds an index where these vectors differ, or until it reaches the + * end of these vectors. + * isRev: Whether we are processing the normal forms in reverse direction. + * Notice in this case the normal form vectors have been reversed, hence, + * many operations are identical to the forward case, e.g. index is + * incremented not decremented, while others require special care, e.g. + * constant strings "ABC" in the normal form vectors are not reversed to + * "CBA" and hence all operations should assume a flipped semantics for + * constants when isRev is true, + * rproc: the number of string components on the suffix of the normal form of + * nfi and nfj that were already processed. This is used when using + * fowards/backwards traversals of normal forms to ensure that duplicate + * inferences are not processed. + * pinfer: the set of possible inferences we add to. + */ + void processSimpleNEq(NormalForm& nfi, + NormalForm& nfj, + unsigned& index, + bool isRev, + unsigned rproc, + std::vector<InferInfo>& pinfer); + //--------------------------end for checkNormalFormsEq + + //--------------------------for checkNormalFormsEq with loops + bool detectLoop(NormalForm& nfi, + NormalForm& nfj, + int index, + int& loop_in_i, + int& loop_in_j, + unsigned rproc); /** * Result of processLoop() below. @@ -572,36 +645,17 @@ private: SKIPPED, }; - ProcessLoopResult processLoop( - const std::vector<std::vector<Node> >& normal_forms, - const std::vector<Node>& normal_form_src, - int i, - int j, - int loop_n_index, - int other_n_index, - int loop_index, - int index, - InferInfo& info); - - void processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, - std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ); - void processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, - std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, - unsigned i, unsigned j, unsigned& index, unsigned rproc, std::vector< InferInfo >& pinfer ); - void processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, - std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, - unsigned i, unsigned j, unsigned& index, bool isRev, unsigned rproc, std::vector< InferInfo >& pinfer ); - //--------------------------end for checkNormalFormsEq + ProcessLoopResult processLoop(NormalForm& nfi, + NormalForm& nfj, + int loop_index, + int index, + InferInfo& info); + //--------------------------end for checkNormalFormsEq with loops //--------------------------for checkNormalFormsDeq void processDeq( Node n1, Node n2 ); int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ); int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ); - void getExplanationVectorForPrefix( std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, - unsigned i, int index, bool isRev, std::vector< Node >& curr_exp ); - void getExplanationVectorForPrefixEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, - std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, - unsigned i, unsigned j, int index_i, int index_j, bool isRev, std::vector< Node >& curr_exp ); //--------------------------end for checkNormalFormsDeq //--------------------------------for checkMemberships @@ -787,8 +841,6 @@ private: protected: /** mkAnd **/ Node mkAnd(std::vector<Node>& a); - /** get concat vector */ - void getConcatVec(Node n, std::vector<Node>& c); /** get equivalence classes * |