cvc5/test/unit/api/java/ResultTest.java

/******************************************************************************
 * Top contributors (to current version):
 *   Mudathir Mohamed, Aina Niemetz, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2025 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 tests;

import static io.github.cvc5.Kind.*;
import static org.junit.jupiter.api.Assertions.*;

import io.github.cvc5.*;
import org.junit.jupiter.api.AfterEach;
import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.Test;

class ResultTest
{
  private TermManager d_tm;
  private Solver d_solver;

  @BeforeEach
  void setUp()
  {
    d_tm = new TermManager();
    d_solver = new Solver(d_tm);
  }

  @AfterEach
  void tearDown()
  {
    Context.deletePointers();
  }

  @Test
  void isNull()
  {
    Result res_null = new Result();
    assertTrue(res_null.isNull());
    assertFalse(res_null.isSat());
    assertFalse(res_null.isUnsat());
    assertFalse(res_null.isUnknown());
    Sort u_sort = d_tm.mkUninterpretedSort("u");
    Term x = d_tm.mkConst(u_sort, "x");
    d_solver.assertFormula(x.eqTerm(x));
    Result res = d_solver.checkSat();
    assertFalse(res.isNull());
  }

  @Test
  void equalHash()
  {
    Sort u_sort = d_tm.mkUninterpretedSort();
    Term x = d_tm.mkConst(u_sort, "x");
    d_solver.assertFormula(x.eqTerm(x));
    Result res = null;
    Result res2 = d_solver.checkSat();
    Result res3 = d_solver.checkSat();
    res = res2;
    assertTrue(res.equals(res2));
    assertTrue(res3.equals(res2));
    assertEquals(res.toString(), "sat");
    assertEquals(res.hashCode(), res2.hashCode());
    assertEquals(res3.hashCode(), res2.hashCode());
  }

  @Test
  void isSat()
  {
    Sort u_sort = d_tm.mkUninterpretedSort("u");
    Term x = d_tm.mkConst(u_sort, "x");
    d_solver.assertFormula(x.eqTerm(x));
    Result res = d_solver.checkSat();
    assertTrue(res.isSat());
    assertFalse(res.isUnknown());
  }

  @Test
  void isUnsat()
  {
    Sort u_sort = d_tm.mkUninterpretedSort();
    Term x = d_tm.mkConst(u_sort, "x");
    d_solver.assertFormula(x.eqTerm(x).notTerm());
    Result res = d_solver.checkSat();
    assertTrue(res.isUnsat());
    assertFalse(res.isUnknown());
  }

  @Test
  void isUnknown() throws CVC5ApiException
  {
    d_solver.setLogic("QF_NIA");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("solve-real-as-int", "true");
    Sort real_sort = d_tm.getIntegerSort();
    Term x = d_tm.mkConst(real_sort, "x");
    d_solver.assertFormula(d_tm.mkTerm(LT, d_tm.mkReal("0.0"), x));
    d_solver.assertFormula(d_tm.mkTerm(LT, x, d_tm.mkReal("1.0")));
    Result res = d_solver.checkSat();
    assertFalse(res.isSat());
    assertTrue(res.isUnknown());
    UnknownExplanation ue = res.getUnknownExplanation();
    assertEquals(ue, UnknownExplanation.INCOMPLETE);
    assertEquals(ue.toString(), "INCOMPLETE");
  }
}