diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-11 16:54:22 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-11 16:54:22 -0500 |
commit | c388e89e5253aa6fbde7685fc53126872f578f0b (patch) | |
tree | 0ace860103f2ad2da266e1f639d170baac73b4da /src/theory/strings/theory_strings.h | |
parent | 7c190dcead07d797d475a07522c595f97c7ef2db (diff) |
Adds regular expression support, it is actually CFL because of variables.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r-- | src/theory/strings/theory_strings.h | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c906d7f91..48bc28b05 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -37,6 +37,7 @@ class TheoryStrings : public Theory { typedef context::CDChunkList<Node> NodeList; typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; + typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; public: TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); @@ -124,6 +125,8 @@ class TheoryStrings : public Theory { Node d_true; Node d_false; Node d_zero; + // RegExp depth + int d_regexp_unroll_depth; //list of pairs of nodes to merge std::map< Node, Node > d_pending_exp; std::vector< Node > d_pending; @@ -142,18 +145,10 @@ class TheoryStrings : public Theory { bool isNormalFormPair( Node n1, Node n2 ); bool isNormalFormPair2( Node n1, Node n2 ); - //inductive equations - NodeListMap d_ind_map1; - NodeListMap d_ind_map2; - NodeListMap d_ind_map_exp; - NodeListMap d_ind_map_lemma; //regular expression memberships NodeList d_reg_exp_mem; - bool addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ); - - //for unrolling inductive equations - NodeBoolMap d_lit_to_unroll; - + std::map< Node, bool > d_reg_exp_unroll; + std::map< Node, int > d_reg_exp_unroll_depth; ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION @@ -200,6 +195,7 @@ class TheoryStrings : public Theory { std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src); bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); bool normalizeDisequality( Node n1, Node n2 ); + bool unrollStar( Node atom ); bool checkLengths(); bool checkNormalForms(); |