diff options
Diffstat (limited to 'src/theory/strings/regexp_solver.h')
| -rw-r--r-- | src/theory/strings/regexp_solver.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index 13b66557a..ec74d98cd 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -23,6 +23,7 @@ #include "context/cdlist.h" #include "context/context.h" #include "expr/node.h" +#include "theory/strings/inference_manager.h" #include "theory/strings/regexp_operation.h" #include "util/regexp.h" @@ -42,7 +43,10 @@ class RegExpSolver typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: - RegExpSolver(TheoryStrings& p, context::Context* c, context::UserContext* u); + RegExpSolver(TheoryStrings& p, + InferenceManager& im, + context::Context* c, + context::UserContext* u); ~RegExpSolver() {} /** add membership @@ -69,6 +73,8 @@ class RegExpSolver Node d_false; /** the parent of this object */ TheoryStrings& d_parent; + /** the output channel of the parent of this object */ + InferenceManager& d_im; // check membership constraints Node mkAnd(Node c1, Node c2); bool checkPDerivative( |