From: mudathirmahgoub Date: Mon, 21 Jun 2021 18:36:47 +0000 (-0500) Subject: Add Grammar.java to the java API (#6388) X-Git-Tag: cvc5-1.0.0~1581 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=62cf9381eac3609e4af0509ffce3abf58ba71238;p=cvc5.git 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 index 000000000..f8c6b05c5 --- /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 index 000000000..95af2108f --- /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(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(pointer); + Term* ntSymbol = reinterpret_cast(ntSymbolPointer); + Term* rule = reinterpret_cast(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(pointer); + Term* ntSymbol = reinterpret_cast(ntSymbolPointer); + std::vector rules = getObjectsFromPointers(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(pointer); + Term* ntSymbol = reinterpret_cast(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(pointer); + Term* ntSymbol = reinterpret_cast(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(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 index 000000000..76a80f55e --- /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)); + } +}