summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r--src/theory/strings/theory_strings.h3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 6e638e445..0d4b1f282 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -457,9 +457,6 @@ private:
//--------------------------------for checkMemberships
// check membership constraints
Node mkRegExpAntec(Node atom, Node ant);
- bool applyRConsume( CVC4::String &s, Node &r );
- Node applyRSplit( Node s1, Node s2, Node r );
- bool applyRLen( std::map< Node, std::vector< Node > > &XinR_with_exps );
bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp);
//check contains
void checkPosContains( std::vector< Node >& posContains );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback