diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-07-31 23:50:40 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-31 23:50:40 -0700 |
commit | 0c78ef9adbddbc7ed875c3c3a41f60e48abdd17f (patch) | |
tree | 14bb779d85d59a8c49b8187b07840cdfcf94ea32 /test | |
parent | 0f040cbc2b068d3f22f6d46ec35aff3ab720ec28 (diff) |
Add SyGuS Python API (#4812)
This commit extends the Python API with support for SyGuS functionality.
This required the addition of a nullary constructor for `Grammar` in the C++ API.
A unit test is also included, and is a translation of the corresponding C++ API unit test.
Examples are not added yet, but are ready and planned for a next PR (in order to keep this one shorter).
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/api/python/test_grammar.py | 117 |
1 files changed, 117 insertions, 0 deletions
diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py new file mode 100644 index 000000000..3a703017f --- /dev/null +++ b/test/unit/api/python/test_grammar.py @@ -0,0 +1,117 @@ +# translated from test/unit/api/grammar_black.h + +import pytest + +import pycvc4 +from pycvc4 import kinds + +def test_add_rule(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + nullTerm = pycvc4.Term() + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + # expecting no error + g = solver.mkSygusGrammar([], [start]) + + g.addRule(start, solver.mkBoolean(False)) + + # expecting errors + with pytest.raises(Exception): + g.addRule(nullTerm, solver.mkBoolean(false)) + with pytest.raises(Exception): + g.addRule(start, nullTerm) + with pytest.raises(Exception): + g.addRule(nts, solver.mkBoolean(false)) + with pytest.raises(Exception): + g.addRule(start, solver.mkReal(0)) + + # expecting no errors + solver.synthFun("f", {}, boolean, g) + + # expecting an error + with pytest.raises(Exception): + g.addRule(start, solver.mkBoolean(false)) + +def test_add_rules(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + nullTerm = pycvc4.Term() + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g = solver.mkSygusGrammar([], [start]) + + g.addRules(start, {solver.mkBoolean(False)}) + + #Expecting errors + with pytest.raises(Exception): + g.addRules(nullTerm, solver.mkBoolean(False)) + with pytest.raises(Exception): + g.addRules(start, {nullTerm}) + with pytest.raises(Exception): + g.addRules(nts, {solver.mkBoolean(False)}) + with pytest.raises(Exception): + g.addRules(start, {solver.mkReal(0)}) + #Expecting no errors + solver.synthFun("f", {}, boolean, g) + + #Expecting an error + with pytest.raises(Exception): + g.addRules(start, solver.mkBoolean(False)) + +def testAddAnyConstant(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + + nullTerm = pycvc4.Term() + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g = solver.mkSygusGrammar({}, {start}) + + g.addAnyConstant(start) + g.addAnyConstant(start) + + with pytest.raises(Exception): + g.addAnyConstant(nullTerm) + with pytest.raises(Exception): + g.addAnyConstant(nts) + + solver.synthFun("f", {}, boolean, g) + + with pytest.raises(Exception): + g.addAnyConstant(start) + + +def testAddAnyVariable(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + + nullTerm = pycvc4.Term() + x = solver.mkVar(boolean) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g1 = solver.mkSygusGrammar({x}, {start}) + g2 = solver.mkSygusGrammar({}, {start}) + + g1.addAnyVariable(start) + g1.addAnyVariable(start) + g2.addAnyVariable(start) + + with pytest.raises(Exception): + g1.addAnyVariable(nullTerm) + with pytest.raises(Exception): + g1.addAnyVariable(nts) + + solver.synthFun("f", {}, boolean, g1) + + with pytest.raises(Exception): + g1.addAnyVariable(start) + |