diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-06-21 13:36:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-21 18:36:47 +0000 |
commit | 62cf9381eac3609e4af0509ffce3abf58ba71238 (patch) | |
tree | 355c9b77036d914b4b1657cc9100e9759ee6955a /test | |
parent | 38bf0edcc479a20dceeb5bcf7710862c7e60a0b8 (diff) |
Add Grammar.java to the java API (#6388)
This commit adds Grammar.java GrammarTest.java and cvc5_Grammar.cpp to the java api.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/api/java/cvc5/GrammarTest.java | 137 |
1 files changed, 137 insertions, 0 deletions
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)); + } +} |