Fixes for SyGuS + regular expressions (#3313)

This commit fixes numerous issues involving the combination of SyGuS and regular expressions.

Combining SyGuS and regular expressions may involve constructing regular expressions that are neither variables nor builtin regular expression operators. The code was not robust for this case, either throwing spurious assertion failures or having incorrect behavior.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index 0b84ebc79..a43ea516a 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -108,6 +108,16 @@ class RegExpSolver
   InferenceManager& d_im;
   // check membership constraints
   Node mkAnd(Node c1, Node c2);
+  /**
+   * Check partial derivative
+   *
+   * Returns false if a lemma pertaining to checking the partial derivative
+   * of x in r was added. In this case, addedLemma is updated to true.
+   *
+   * The argument atom is the assertion that explains x in r, which is the
+   * normalized form of atom that may be modified using a substitution whose
+   * explanation is nf_exp.
+   */
   bool checkPDerivative(
       Node x, Node r, Node atom, bool& addedLemma, std::vector<Node>& nf_exp);
   Node getMembership(Node n, bool isPos, unsigned i);