diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-05-21 13:01:14 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-21 13:01:14 -0500 |
| commit | 2c78f3bf696e7eb4b04f687e15b9569b9e1b8f23 (patch) | |
| tree | ff490ec9c28be25ca7de7b201349b93935371027 /test/unit/api | |
| parent | 3dc56426a37bf85f82ed6dc8cf15e4eb81498110 (diff) | |
Make Grammar reusable. (#4506)
This PR modifies the Grammar implementation to make it reusable (i.e., can be copied or passed multiple times to synthFun/synthInv) with the catch that it becomes read-only after the first use.
Diffstat (limited to 'test/unit/api')
| -rw-r--r-- | test/unit/api/grammar_black.h | 28 |
1 files changed, 23 insertions, 5 deletions
diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h index abf37f210..03525f12f 100644 --- a/test/unit/api/grammar_black.h +++ b/test/unit/api/grammar_black.h @@ -58,6 +58,11 @@ void GrammarBlack::testAddRule() TS_ASSERT_THROWS(g.addRule(nts, d_solver->mkBoolean(false)), CVC4ApiException&); TS_ASSERT_THROWS(g.addRule(start, d_solver->mkReal(0)), CVC4ApiException&); + + d_solver->synthFun("f", {}, boolean, g); + + TS_ASSERT_THROWS(g.addRule(start, d_solver->mkBoolean(false)), + CVC4ApiException&); } void GrammarBlack::testAddRules() @@ -75,10 +80,15 @@ void GrammarBlack::testAddRules() TS_ASSERT_THROWS(g.addRules(nullTerm, {d_solver->mkBoolean(false)}), CVC4ApiException&); - TS_ASSERT_THROWS(g.addRule(start, {nullTerm}), CVC4ApiException&); - TS_ASSERT_THROWS(g.addRule(nts, {d_solver->mkBoolean(false)}), + TS_ASSERT_THROWS(g.addRules(start, {nullTerm}), CVC4ApiException&); + TS_ASSERT_THROWS(g.addRules(nts, {d_solver->mkBoolean(false)}), + CVC4ApiException&); + TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkReal(0)}), CVC4ApiException&); + + d_solver->synthFun("f", {}, boolean, g); + + TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkBoolean(false)}), CVC4ApiException&); - TS_ASSERT_THROWS(g.addRule(start, {d_solver->mkReal(0)}), CVC4ApiException&); } void GrammarBlack::testAddAnyConstant() @@ -96,6 +106,10 @@ void GrammarBlack::testAddAnyConstant() TS_ASSERT_THROWS(g.addAnyConstant(nullTerm), CVC4ApiException&); TS_ASSERT_THROWS(g.addAnyConstant(nts), CVC4ApiException&); + + d_solver->synthFun("f", {}, boolean, g); + + TS_ASSERT_THROWS(g.addAnyConstant(start), CVC4ApiException&); } void GrammarBlack::testAddAnyVariable() @@ -114,6 +128,10 @@ void GrammarBlack::testAddAnyVariable() TS_ASSERT_THROWS_NOTHING(g1.addAnyVariable(start)); TS_ASSERT_THROWS_NOTHING(g2.addAnyVariable(start)); - TS_ASSERT_THROWS(g1.addAnyConstant(nullTerm), CVC4ApiException&); - TS_ASSERT_THROWS(g1.addAnyConstant(nts), CVC4ApiException&); + TS_ASSERT_THROWS(g1.addAnyVariable(nullTerm), CVC4ApiException&); + TS_ASSERT_THROWS(g1.addAnyVariable(nts), CVC4ApiException&); + + d_solver->synthFun("f", {}, boolean, g1); + + TS_ASSERT_THROWS(g1.addAnyVariable(start), CVC4ApiException&); } |