diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-06 06:48:45 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-06 06:48:45 -0500 |
| commit | 77e98815254c68301ffcd7fb8addeb6751c51187 (patch) | |
| tree | 068ad98b6b43692276972a1ee5111ced3178338c /test | |
| parent | d8d3c55afc94482fc05f68ba6be47f767ab3b5c6 (diff) | |
(proof-new) Refactor regular expression operation (#4596)
This refactors the regular expression operation class so that some of its key methods are static, so that they can used by both the regular expression solver and the strings proof checker.
Notice that many cases of regular expression unfolding are deleted by this PR, since they are unnecessary. This is due to the fact that all regular expression memberships are rewritten except those whose RHS are re.++ or re.*.
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/regexp_operation_black.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/test/unit/theory/regexp_operation_black.h b/test/unit/theory/regexp_operation_black.h index 6e01392ab..551d59bef 100644 --- a/test/unit/theory/regexp_operation_black.h +++ b/test/unit/theory/regexp_operation_black.h @@ -25,7 +25,9 @@ #include "expr/node_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "theory/rewriter.h" #include "theory/strings/regexp_operation.h" +#include "theory/strings/skolem_cache.h" using namespace CVC4; using namespace CVC4::kind; @@ -46,7 +48,8 @@ class RegexpOperationBlack : public CxxTest::TestSuite d_em = d_slv->getExprManager(); d_smt = d_slv->getSmtEngine(); d_scope = new SmtScope(d_smt); - d_regExpOpr = new RegExpOpr(); + d_skc = new SkolemCache(); + d_regExpOpr = new RegExpOpr(d_skc); // Ensure that the SMT engine is fully initialized (required for the // rewriter) @@ -58,6 +61,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite void tearDown() override { delete d_regExpOpr; + delete d_skc; delete d_scope; delete d_slv; } @@ -153,6 +157,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite ExprManager* d_em; SmtEngine* d_smt; SmtScope* d_scope; + SkolemCache* d_skc; RegExpOpr* d_regExpOpr; NodeManager* d_nm; |