diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-04-24 17:30:15 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-04-24 17:30:15 -0500 |
| commit | 698f5a09b1c0177abfd2eaa2b110de100fd108ef (patch) | |
| tree | e7d7584e67621f48a45b33ed4fc2eea5a5a70f33 /src/theory/strings/theory_strings.h | |
| parent | 9a4df62fbb05a09c95877b53053ff2e231ae254c (diff) | |
minor change: add a heuristic for preventing constant splitting.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 9f99012df..33283d1cf 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -272,8 +272,8 @@ protected: void sendInfer( Node eq_exp, Node eq, const char * c ); void sendSplit( Node a, Node b, const char * c, bool preq = true ); /** mkConcat **/ - Node mkConcat( Node n1, Node n2 ); - Node mkConcat( std::vector< Node >& c ); + inline Node mkConcat( Node n1, Node n2 ); + inline Node mkConcat( std::vector< Node >& c ); /** mkExplain **/ Node mkExplain( std::vector< Node >& a ); Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); @@ -323,6 +323,7 @@ private: bool splitRegExp( Node x, Node r, Node ant ); bool addMembershipLength(Node atom); void addMembership(Node assertion); + Node instantiateSymRegExp(Node r); // Finite Model Finding |