1 files changed, 128 insertions, 0 deletions
diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py
new file mode 100644
index 000000000..5a0d5101f
--- /dev/null
+++ b/test/api/python/test_grammar.py
@@ -0,0 +1,128 @@
+#####################
+## test_grammar.py
+## Top contributors (to current version):
+##   Yoni Zohar, Makai Mann
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 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 pycvc4
+from pycvc4 import kinds
+
+def test_add_rule():
+  solver = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+  integer = solver.getIntegerSort()
+
+  nullTerm = pycvc4.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 = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+  integer = solver.getIntegerSort()
+
+  nullTerm = pycvc4.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 = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+
+  nullTerm = pycvc4.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 = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+
+  nullTerm = pycvc4.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)
+