Add Result.java to the java API (#6385)

This PR adds Result.java ResultTest.java and cvc5_Result.cpp to the java api.

1 files changed, 126 insertions, 0 deletions

diff --git a/test/unit/api/java/cvc5/ResultTest.java b/test/unit/api/java/cvc5/ResultTest.java
new file mode 100644
index 000000000..8ba50c00a
--- /dev/null
+++ b/test/unit/api/java/cvc5/ResultTest.java
@@ -0,0 +1,126 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, 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 Result class
+ */
+
+package cvc5;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+class ResultTest
+{
+  private Solver d_solver;
+
+  @BeforeEach void setUp()
+  {
+    d_solver = new Solver();
+  }
+
+  @Test void isNull()
+  {
+    Result res_null = d_solver.getNullResult();
+    assertTrue(res_null.isNull());
+    assertFalse(res_null.isSat());
+    assertFalse(res_null.isUnsat());
+    assertFalse(res_null.isSatUnknown());
+    assertFalse(res_null.isEntailed());
+    assertFalse(res_null.isNotEntailed());
+    assertFalse(res_null.isEntailmentUnknown());
+    Sort u_sort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkVar(u_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    Result res = d_solver.checkSat();
+    assertFalse(res.isNull());
+  }
+
+  @Test void eq()
+  {
+    Sort u_sort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkVar(u_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    Result res;
+    Result res2 = d_solver.checkSat();
+    Result res3 = d_solver.checkSat();
+    res = res2;
+    assertEquals(res, res2);
+    assertEquals(res3, res2);
+  }
+
+  @Test void isSat()
+  {
+    Sort u_sort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkVar(u_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    Result res = d_solver.checkSat();
+    assertTrue(res.isSat());
+    assertFalse(res.isSatUnknown());
+  }
+
+  @Test void isUnsat()
+  {
+    Sort u_sort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkVar(u_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x).notTerm());
+    Result res = d_solver.checkSat();
+    assertTrue(res.isUnsat());
+    assertFalse(res.isSatUnknown());
+  }
+
+  @Test void isSatUnknown() throws CVC5ApiException
+  {
+    d_solver.setLogic("QF_NIA");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("solve-int-as-bv", "32");
+    Sort int_sort = d_solver.getIntegerSort();
+    Term x = d_solver.mkVar(int_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x).notTerm());
+    Result res = d_solver.checkSat();
+    assertFalse(res.isSat());
+    assertTrue(res.isSatUnknown());
+  }
+
+  @Test void isEntailed()
+  {
+    d_solver.setOption("incremental", "true");
+    Sort u_sort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkConst(u_sort, "x");
+    Term y = d_solver.mkConst(u_sort, "y");
+    Term a = x.eqTerm(y).notTerm();
+    Term b = x.eqTerm(y);
+    d_solver.assertFormula(a);
+    Result entailed = d_solver.checkEntailed(a);
+    assertTrue(entailed.isEntailed());
+    assertFalse(entailed.isEntailmentUnknown());
+    Result not_entailed = d_solver.checkEntailed(b);
+    assertTrue(not_entailed.isNotEntailed());
+    assertFalse(not_entailed.isEntailmentUnknown());
+  }
+
+  @Test void isEntailmentUnknown() throws CVC5ApiException
+  {
+    d_solver.setLogic("QF_NIA");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("solve-int-as-bv", "32");
+    Sort int_sort = d_solver.getIntegerSort();
+    Term x = d_solver.mkVar(int_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x).notTerm());
+    Result res = d_solver.checkEntailed(x.eqTerm(x));
+    assertFalse(res.isEntailed());
+    assertTrue(res.isEntailmentUnknown());
+    assertEquals(res.getUnknownExplanation(), Result.UnknownExplanation.UNKNOWN_REASON);
+  }
+}