Add Grammar.java to the java API (#6388)

This commit adds Grammar.java GrammarTest.java and cvc5_Grammar.cpp to the java api.

diff --git a/src/api/java/cvc5/Grammar.java b/src/api/java/cvc5/Grammar.java
new file mode 100644 (file)
index 0000000..f8c6b05
--- /dev/null
+++ b/src/api/java/cvc5/Grammar.java
@@ -0,0 +1,87 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, 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.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ */
+
+package cvc5;
+
+public class Grammar extends AbstractPointer {
+  // region construction and destruction
+  Grammar(Solver solver, long pointer) {
+    super(solver, pointer);
+  }
+
+  protected static native void deletePointer(long pointer);
+
+  public long getPointer() {
+    return pointer;
+  }
+
+  @Override
+  public void finalize() {
+    deletePointer(pointer);
+  }
+
+  // endregion
+
+  /**
+   * Add \p rule to the set of rules corresponding to \p ntSymbol.
+   * @param ntSymbol the non-terminal to which the rule is added
+   * @param rule the rule to add
+   */
+  public void addRule(Term ntSymbol, Term rule) {
+    addRule(pointer, ntSymbol.getPointer(), rule.getPointer());
+  }
+
+  private native void addRule(
+      long pointer, long ntSymbolPointer, long rulePointer);
+
+  /**
+   * Add \p rules to the set of rules corresponding to \p ntSymbol.
+   * @param ntSymbol the non-terminal to which the rules are added
+   * @param rules the rules to add
+   */
+  public void addRules(Term ntSymbol, Term[] rules) {
+    long[] pointers = Utils.getPointers(rules);
+    addRules(pointer, ntSymbol.getPointer(), pointers);
+  }
+
+  public native void addRules(
+      long pointer, long ntSymbolPointer, long[] rulePointers);
+
+  /**
+   * Allow \p ntSymbol to be an arbitrary constant.
+   * @param ntSymbol the non-terminal allowed to be any constant
+   */
+  void addAnyConstant(Term ntSymbol) {
+    addAnyConstant(pointer, ntSymbol.getPointer());
+  }
+
+  private native void addAnyConstant(long pointer, long ntSymbolPointer);
+
+  /**
+   * Allow \p ntSymbol to be any input variable to corresponding
+   * synth-fun/synth-inv with the same sort as \p ntSymbol.
+   * @param ntSymbol the non-terminal allowed to be any input constant
+   */
+  void addAnyVariable(Term ntSymbol) {
+    addAnyVariable(pointer, ntSymbol.getPointer());
+  }
+
+  private native void addAnyVariable(long pointer, long ntSymbolPointer);
+
+  /**
+   * @return a string representation of this grammar.
+   */
+  protected native String toString(long pointer);
+}

diff --git a/src/api/java/jni/cvc5_Grammar.cpp b/src/api/java/jni/cvc5_Grammar.cpp
new file mode 100644 (file)
index 0000000..95af210
--- /dev/null
+++ b/src/api/java/jni/cvc5_Grammar.cpp
@@ -0,0 +1,120 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   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.
+ * ****************************************************************************
+ *
+ * The cvc5 Java API.
+ */
+
+#include "cvc5_Grammar.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Grammar_deletePointer(JNIEnv*,
+                                                       jclass,
+                                                       jlong pointer)
+{
+  delete reinterpret_cast<Grammar*>(pointer);
+}
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    addRule
+ * Signature: (JJJ)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Grammar_addRule(JNIEnv* env,
+                                                 jobject,
+                                                 jlong pointer,
+                                                 jlong ntSymbolPointer,
+                                                 jlong rulePointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Grammar* current = reinterpret_cast<Grammar*>(pointer);
+  Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer);
+  Term* rule = reinterpret_cast<Term*>(rulePointer);
+  current->addRule(*ntSymbol, *rule);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    addRules
+ * Signature: (JJ[J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Grammar_addRules(JNIEnv* env,
+                                                  jobject,
+                                                  jlong pointer,
+                                                  jlong ntSymbolPointer,
+                                                  jlongArray rulePointers)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Grammar* current = reinterpret_cast<Grammar*>(pointer);
+  Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer);
+  std::vector<Term> rules = getObjectsFromPointers<Term>(env, rulePointers);
+  current->addRules(*ntSymbol, rules);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    addAnyConstant
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyConstant(JNIEnv* env,
+                                                        jobject,
+                                                        jlong pointer,
+                                                        jlong ntSymbolPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Grammar* current = reinterpret_cast<Grammar*>(pointer);
+  Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer);
+  current->addAnyConstant(*ntSymbol);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    addAnyVariable
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyVariable(JNIEnv* env,
+                                                        jobject,
+                                                        jlong pointer,
+                                                        jlong ntSymbolPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Grammar* current = reinterpret_cast<Grammar*>(pointer);
+  Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer);
+  current->addAnyVariable(*ntSymbol);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Grammar_toString(JNIEnv* env,
+                                                     jobject,
+                                                     jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Grammar* current = reinterpret_cast<Grammar*>(pointer);
+  return env->NewStringUTF(current->toString().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}

diff --git a/test/unit/api/java/cvc5/GrammarTest.java b/test/unit/api/java/cvc5/GrammarTest.java
new file mode 100644 (file)
index 0000000..76a80f5
--- /dev/null
+++ b/test/unit/api/java/cvc5/GrammarTest.java
@@ -0,0 +1,137 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Abdalrhman Mohamed, 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the guards of the Java API functions.
+ */
+
+package cvc5;
+
+import static cvc5.Kind.*;
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.Arrays;
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+class GrammarTest {
+  private Solver d_solver;
+
+  @BeforeEach
+  void setUp() {
+    d_solver = new Solver();
+  }
+
+  @Test
+  void addRule() {
+    Sort bool = d_solver.getBooleanSort();
+    Sort integer = d_solver.getIntegerSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term start = d_solver.mkVar(bool);
+    Term nts = d_solver.mkVar(bool);
+
+    Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+
+    assertDoesNotThrow(() -> g.addRule(start, d_solver.mkBoolean(false)));
+
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRule(nullTerm, d_solver.mkBoolean(false)));
+    assertThrows(CVC5ApiException.class, () -> g.addRule(start, nullTerm));
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRule(nts, d_solver.mkBoolean(false)));
+    assertThrows(
+        CVC5ApiException.class, () -> g.addRule(start, d_solver.mkInteger(0)));
+    assertThrows(CVC5ApiException.class, () -> g.addRule(start, nts));
+
+    d_solver.synthFun("f", new Term[] {}, bool, g);
+
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRule(start, d_solver.mkBoolean(false)));
+  }
+
+  @Test
+  void addRules() {
+    Sort bool = d_solver.getBooleanSort();
+    Sort integer = d_solver.getIntegerSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term start = d_solver.mkVar(bool);
+    Term nts = d_solver.mkVar(bool);
+
+    Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+
+    assertDoesNotThrow(
+        () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)}));
+
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRules(nullTerm, new Term[] {d_solver.mkBoolean(false)}));
+    assertThrows(
+        CVC5ApiException.class, () -> g.addRules(start, new Term[] {nullTerm}));
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRules(nts, new Term[] {d_solver.mkBoolean(false)}));
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRules(start, new Term[] {d_solver.mkInteger(0)}));
+    assertThrows(
+        CVC5ApiException.class, () -> g.addRules(start, new Term[] {nts}));
+
+    d_solver.synthFun("f", new Term[] {}, bool, g);
+
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)}));
+  }
+
+  @Test
+  void addAnyConstant() {
+    Sort bool = d_solver.getBooleanSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term start = d_solver.mkVar(bool);
+    Term nts = d_solver.mkVar(bool);
+
+    Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+
+    assertDoesNotThrow(() -> g.addAnyConstant(start));
+    assertDoesNotThrow(() -> g.addAnyConstant(start));
+
+    assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(nullTerm));
+    assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(nts));
+
+    d_solver.synthFun("f", new Term[] {}, bool, g);
+
+    assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(start));
+  }
+
+  @Test
+  void addAnyVariable() {
+    Sort bool = d_solver.getBooleanSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term x = d_solver.mkVar(bool);
+    Term start = d_solver.mkVar(bool);
+    Term nts = d_solver.mkVar(bool);
+
+    Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start});
+    Grammar g2 = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+
+    assertDoesNotThrow(() -> g1.addAnyVariable(start));
+    assertDoesNotThrow(() -> g1.addAnyVariable(start));
+    assertDoesNotThrow(() -> g2.addAnyVariable(start));
+
+    assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(nullTerm));
+    assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(nts));
+
+    d_solver.synthFun("f", new Term[] {}, bool, g1);
+
+    assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(start));
+  }
+}