From: yoni206 Date: Mon, 17 May 2021 18:00:41 +0000 (-0700) Subject: Move and enhance python API grammar tests (#6538) X-Git-Tag: cvc5-1.0.0~1754 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91e41bcb666d25b19074537f3f2ee98281592616;p=cvc5.git Move and enhance python API grammar tests (#6538) The existing test for python API grammar is moved to the right location, `yapf`ed, and changed according to the new style of python API tests. Additionally, minor changes are introduced in order to be an exact translation of https://github.com/cvc5/cvc5/blob/master/test/unit/api/grammar_black.cpp --- diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt index 87ddbb5d6..7f05bf130 100644 --- a/test/api/python/CMakeLists.txt +++ b/test/api/python/CMakeLists.txt @@ -39,5 +39,4 @@ macro(cvc5_add_python_api_test name filename) endmacro() cvc5_add_python_api_test(pytest_datatype_api test_datatype_api.py) -cvc5_add_python_api_test(pytest_grammar test_grammar.py) cvc5_add_python_api_test(pytest_to_python_obj test_to_python_obj.py) diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py deleted file mode 100644 index f83bee548..000000000 --- a/test/api/python/test_grammar.py +++ /dev/null @@ -1,130 +0,0 @@ -############################################################################### -# Top contributors (to current version): -# Yoni Zohar, Makai Mann, Mudathir Mohamed -# -# This file is part of the cvc5 project. -# -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -# in the top-level source directory and their institutional affiliations. -# All rights reserved. See the file COPYING in the top-level source -# directory for licensing information. -# ############################################################################# -# -# Translated from test/unit/api/grammar_black.h -## - -import pytest - -import pycvc5 -from pycvc5 import kinds - -def test_add_rule(): - solver = pycvc5.Solver() - boolean = solver.getBooleanSort() - integer = solver.getIntegerSort() - - nullTerm = pycvc5.Term(solver) - 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.mkInteger(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 = pycvc5.Solver() - boolean = solver.getBooleanSort() - integer = solver.getIntegerSort() - - nullTerm = pycvc5.Term(solver) - 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.mkInteger(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 = pycvc5.Solver() - boolean = solver.getBooleanSort() - - nullTerm = pycvc5.Term(solver) - 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 = pycvc5.Solver() - boolean = solver.getBooleanSort() - - nullTerm = pycvc5.Term(solver) - 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) - diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt index b7de1cbb0..6091e3275 100644 --- a/test/python/CMakeLists.txt +++ b/test/python/CMakeLists.txt @@ -30,3 +30,4 @@ endmacro() cvc5_add_python_api_test(pytest_solver unit/api/test_solver.py) cvc5_add_python_api_test(pytest_sort unit/api/test_sort.py) cvc5_add_python_api_test(pytest_term unit/api/test_term.py) +cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py) diff --git a/test/python/unit/api/test_grammar.py b/test/python/unit/api/test_grammar.py new file mode 100644 index 000000000..db567a6ba --- /dev/null +++ b/test/python/unit/api/test_grammar.py @@ -0,0 +1,137 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Makai Mann, Mudathir Mohamed +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# Translated from test/unit/api/grammar_black.h +## + +import pytest + +import pycvc5 +from pycvc5 import kinds, Term + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_add_rule(solver): + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + null_term = Term(solver) + 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(RuntimeError): + g.addRule(null_term, solver.mkBoolean(False)) + with pytest.raises(RuntimeError): + g.addRule(start, null_term) + with pytest.raises(RuntimeError): + g.addRule(nts, solver.mkBoolean(False)) + with pytest.raises(RuntimeError): + g.addRule(start, solver.mkInteger(0)) + with pytest.raises(RuntimeError): + g.addRule(start, nts) + + # expecting no errors + solver.synthFun("f", {}, boolean, g) + + # expecting an error + with pytest.raises(RuntimeError): + g.addRule(start, solver.mkBoolean(False)) + + +def test_add_rules(solver): + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + null_term = Term(solver) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g = solver.mkSygusGrammar([], [start]) + + g.addRules(start, {solver.mkBoolean(False)}) + + #Expecting errors + with pytest.raises(RuntimeError): + g.addRules(null_term, [solver.mkBoolean(False)]) + with pytest.raises(RuntimeError): + g.addRules(start, [null_term]) + with pytest.raises(RuntimeError): + g.addRules(nts, [solver.mkBoolean(False)]) + with pytest.raises(RuntimeError): + g.addRules(start, [solver.mkInteger(0)]) + with pytest.raises(RuntimeError): + g.addRules(start, [nts]) + #Expecting no errors + solver.synthFun("f", {}, boolean, g) + + #Expecting an error + with pytest.raises(RuntimeError): + g.addRules(start, solver.mkBoolean(False)) + + +def test_add_any_constant(solver): + boolean = solver.getBooleanSort() + + null_term = Term(solver) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g = solver.mkSygusGrammar({}, {start}) + + g.addAnyConstant(start) + g.addAnyConstant(start) + + with pytest.raises(RuntimeError): + g.addAnyConstant(null_term) + with pytest.raises(RuntimeError): + g.addAnyConstant(nts) + + solver.synthFun("f", {}, boolean, g) + + with pytest.raises(RuntimeError): + g.addAnyConstant(start) + + +def test_add_any_variable(solver): + boolean = solver.getBooleanSort() + + null_term = Term(solver) + 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(RuntimeError): + g1.addAnyVariable(null_term) + with pytest.raises(RuntimeError): + g1.addAnyVariable(nts) + + solver.synthFun("f", {}, boolean, g1) + + with pytest.raises(RuntimeError): + g1.addAnyVariable(start)