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 87ddbb5d62a4c6d4bb1256c657a0a049d659789e..7f05bf1307efbd89986908aef1c3efa486ddb212 100644 (file)
--- 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 (file)
index f83bee5..0000000
--- 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 b7de1cbb0e6539594f8e8bbee564ed277a8c8d37..6091e327587eb0f81b6b86c4ac27dfe9c8ae5a79 100644 (file)
--- 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 (file)
index 0000000..db567a6
--- /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)