/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Mudathir Mohamed, 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 TermManager class of the Java API.
 */

package tests;

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

import io.github.cvc5.*;
import java.math.BigInteger;
import java.util.*;
import java.util.concurrent.atomic.AtomicReference;
import org.junit.jupiter.api.*;
import org.junit.jupiter.api.function.Executable;

class TermManagerTest
{
  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 getBooleanSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.getBooleanSort());
  }

  @Test
  void getIntegerSort()
  {
    assertDoesNotThrow(() -> d_tm.getIntegerSort());
  }

  @Test
  void getRealSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.getRealSort());
  }

  @Test
  void getRegExpSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.getRegExpSort());
  }

  @Test
  void getStringSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.getStringSort());
  }

  @Test
  void getRoundingModeSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.getRoundingModeSort());
  }

  @Test
  void mkArraySort() throws CVC5ApiException
  {
    Sort boolSort = d_tm.getBooleanSort();
    Sort intSort = d_tm.getIntegerSort();
    Sort realSort = d_tm.getRealSort();
    Sort bvSort = d_tm.mkBitVectorSort(32);
    assertDoesNotThrow(() -> d_tm.mkArraySort(boolSort, boolSort));
    assertDoesNotThrow(() -> d_tm.mkArraySort(intSort, intSort));
    assertDoesNotThrow(() -> d_tm.mkArraySort(realSort, realSort));
    assertDoesNotThrow(() -> d_tm.mkArraySort(bvSort, bvSort));
    assertDoesNotThrow(() -> d_tm.mkArraySort(boolSort, intSort));
    assertDoesNotThrow(() -> d_tm.mkArraySort(realSort, bvSort));

    Sort fpSort = d_tm.mkFloatingPointSort(3, 5);
    assertDoesNotThrow(() -> d_tm.mkArraySort(fpSort, fpSort));
    assertDoesNotThrow(() -> d_tm.mkArraySort(bvSort, fpSort));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkArraySort(boolSort, boolSort));
  }

  @Test
  void mkBitVectorSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkBitVectorSort(32));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVectorSort(0));
  }

  @Test
  void mkFloatingPointSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkFloatingPointSort(4, 8));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkFloatingPointSort(0, 8));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkFloatingPointSort(4, 0));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkFloatingPointSort(1, 8));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkFloatingPointSort(4, 1));
  }

  @Test
  void mkDatatypeSort() throws CVC5ApiException
  {
    DatatypeDecl dtypeSpec = d_tm.mkDatatypeDecl("list");
    DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
    cons.addSelector("head", d_tm.getIntegerSort());
    dtypeSpec.addConstructor(cons);
    DatatypeConstructorDecl nil = d_tm.mkDatatypeConstructorDecl("nil");
    dtypeSpec.addConstructor(nil);
    assertDoesNotThrow(() -> d_tm.mkDatatypeSort(dtypeSpec));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkDatatypeSort(dtypeSpec));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkDatatypeSort(dtypeSpec));

    DatatypeDecl throwsDtypeSpec = d_tm.mkDatatypeDecl("list");
    assertThrows(CVC5ApiException.class, () -> d_tm.mkDatatypeSort(throwsDtypeSpec));
  }

  @Test
  void mkDatatypeSorts() throws CVC5ApiException
  {
    DatatypeDecl dtypeSpec1 = d_tm.mkDatatypeDecl("list1");
    DatatypeConstructorDecl cons1 = d_tm.mkDatatypeConstructorDecl("cons1");
    cons1.addSelector("head1", d_tm.getIntegerSort());
    dtypeSpec1.addConstructor(cons1);
    DatatypeConstructorDecl nil1 = d_tm.mkDatatypeConstructorDecl("nil1");
    dtypeSpec1.addConstructor(nil1);
    DatatypeDecl dtypeSpec2 = d_tm.mkDatatypeDecl("list2");
    DatatypeConstructorDecl cons2 = d_tm.mkDatatypeConstructorDecl("cons2");
    cons2.addSelector("head2", d_tm.getIntegerSort());
    dtypeSpec2.addConstructor(cons2);
    DatatypeConstructorDecl nil2 = d_tm.mkDatatypeConstructorDecl("nil2");
    dtypeSpec2.addConstructor(nil2);
    DatatypeDecl[] decls = {dtypeSpec1, dtypeSpec2};
    assertDoesNotThrow(() -> d_tm.mkDatatypeSorts(decls));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkDatatypeSorts(decls));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(decls));

    DatatypeDecl throwsDtypeSpec = d_tm.mkDatatypeDecl("list");
    DatatypeDecl[] throwsDecls = new DatatypeDecl[] {throwsDtypeSpec};
    assertThrows(CVC5ApiException.class, () -> d_tm.mkDatatypeSorts(throwsDecls));

    /* with unresolved sorts */
    Sort unresList = d_tm.mkUnresolvedDatatypeSort("ulist", 1);
    DatatypeDecl ulist = d_tm.mkDatatypeDecl("ulist");
    DatatypeConstructorDecl ucons = d_tm.mkDatatypeConstructorDecl("ucons");
    ucons.addSelector("car", unresList);
    ucons.addSelector("cdr", unresList);
    ulist.addConstructor(ucons);
    DatatypeConstructorDecl unil = d_tm.mkDatatypeConstructorDecl("unil");
    ulist.addConstructor(unil);
    DatatypeDecl[] udecls = new DatatypeDecl[] {ulist};
    assertDoesNotThrow(() -> d_tm.mkDatatypeSorts(udecls));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkDatatypeSorts(udecls));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(udecls));

    /* mutually recursive with unresolved parameterized sorts */
    Sort p0 = d_tm.mkParamSort("p0");
    Sort p1 = d_tm.mkParamSort("p1");
    Sort u0 = d_tm.mkUnresolvedDatatypeSort("dt0", 1);
    Sort u1 = d_tm.mkUnresolvedDatatypeSort("dt1", 1);
    DatatypeDecl dtdecl0 = d_tm.mkDatatypeDecl("dt0", new Sort[] {p0});
    DatatypeDecl dtdecl1 = d_tm.mkDatatypeDecl("dt1", new Sort[] {p1});
    DatatypeConstructorDecl ctordecl0 = d_tm.mkDatatypeConstructorDecl("c0");
    ctordecl0.addSelector("s0", u1.instantiate(new Sort[] {p0}));
    DatatypeConstructorDecl ctordecl1 = d_tm.mkDatatypeConstructorDecl("c1");
    ctordecl1.addSelector("s1", u0.instantiate(new Sort[] {p1}));
    dtdecl0.addConstructor(ctordecl0);
    dtdecl1.addConstructor(ctordecl1);
    dtdecl1.addConstructor(d_tm.mkDatatypeConstructorDecl("nil"));
    Sort[] dt_sorts = d_tm.mkDatatypeSorts(new DatatypeDecl[] {dtdecl0, dtdecl1});
    Sort isort1 = dt_sorts[1].instantiate(new Sort[] {d_tm.getBooleanSort()});
    Term t1 = d_tm.mkConst(isort1, "t");
    Term t0 = d_tm.mkTerm(APPLY_SELECTOR,
        t1.getSort().getDatatype().getConstructor("c1").getSelector("s1").getTerm(),
        t1);
    assertEquals(dt_sorts[0].instantiate(new Sort[] {d_tm.getBooleanSort()}), t0.getSort());

    /* Note: More tests are in datatype_api_black. */
  }

  @Test
  void mkFunctionSort() throws CVC5ApiException
  {
    assertDoesNotThrow(
        () -> d_tm.mkFunctionSort(d_tm.mkUninterpretedSort("u"), d_tm.getIntegerSort()));
    Sort funSort = d_tm.mkFunctionSort(d_tm.mkUninterpretedSort("u"), d_tm.getIntegerSort());
    // function arguments are allowed
    assertDoesNotThrow(() -> d_tm.mkFunctionSort(funSort, d_tm.getIntegerSort()));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkFunctionSort(d_tm.getIntegerSort(), funSort));

    assertDoesNotThrow(()
                           -> d_tm.mkFunctionSort(
                               new Sort[] {d_tm.mkUninterpretedSort("u"), d_tm.getIntegerSort()},
                               d_tm.getIntegerSort()));
    Sort funSort2 = d_tm.mkFunctionSort(d_tm.mkUninterpretedSort("u"), d_tm.getIntegerSort());
    // function arguments are allowed
    assertDoesNotThrow(
        ()
            -> d_tm.mkFunctionSort(
                new Sort[] {funSort2, d_tm.mkUninterpretedSort("u")}, d_tm.getIntegerSort()));
    assertThrows(CVC5ApiException.class,
        ()
            -> d_tm.mkFunctionSort(
                new Sort[] {d_tm.getIntegerSort(), d_tm.mkUninterpretedSort("u")}, funSort2));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class,
        () -> slv.mkFunctionSort(d_tm.mkUninterpretedSort("u"), d_tm.getIntegerSort()));

    assertThrows(CVC5ApiException.class,
        () -> slv.mkFunctionSort(slv.mkUninterpretedSort("u"), d_tm.getIntegerSort()));

    Sort[] sorts1 = new Sort[] {d_tm.getBooleanSort(), slv.getIntegerSort(), d_tm.getIntegerSort()};
    Sort[] sorts2 = new Sort[] {slv.getBooleanSort(), slv.getIntegerSort()};
    assertThrows(
        CVC5ApiException.class, () -> slv.mkFunctionSort(sorts2, d_solver.getIntegerSort()));
    assertThrows(
        CVC5ApiException.class, () -> slv.mkFunctionSort(sorts1, d_solver.getIntegerSort()));
    assertThrows(CVC5ApiException.class, () -> slv.mkFunctionSort(sorts2, d_tm.getIntegerSort()));
  }

  @Test
  void mkParamSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkParamSort("T"));
    assertDoesNotThrow(() -> d_tm.mkParamSort(""));
  }

  @Test
  void mkPredicateSort()
  {
    assertDoesNotThrow(() -> d_tm.mkPredicateSort(new Sort[] {d_tm.getIntegerSort()}));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkPredicateSort(new Sort[] {}));
    Sort funSort = d_tm.mkFunctionSort(d_tm.mkUninterpretedSort("u"), d_tm.getIntegerSort());
    // functions as arguments are allowed
    assertDoesNotThrow(() -> d_tm.mkPredicateSort(new Sort[] {d_tm.getIntegerSort(), funSort}));

    Solver slv = new Solver();
    assertThrows(
        CVC5ApiException.class, () -> slv.mkPredicateSort(new Sort[] {d_tm.getIntegerSort()}));
  }

  @Test
  void mkRecordSort() throws CVC5ApiException
  {
    Pair<String, Sort>[] fields = new Pair[] {new Pair<>("b", d_tm.getBooleanSort()),
        new Pair<>("bv", d_tm.mkBitVectorSort(8)),
        new Pair<>("i", d_tm.getIntegerSort())};
    Pair<String, Sort>[] empty = new Pair[0];
    assertDoesNotThrow(() -> d_tm.mkRecordSort(fields));
    assertDoesNotThrow(() -> d_tm.mkRecordSort(empty));
    Sort recSort = d_tm.mkRecordSort(fields);
    assertDoesNotThrow(() -> recSort.getDatatype());

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkRecordSort(fields));
  }

  @Test
  void mkSetSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkSetSort(d_tm.getBooleanSort()));
    assertDoesNotThrow(() -> d_tm.mkSetSort(d_tm.getIntegerSort()));
    assertDoesNotThrow(() -> d_tm.mkSetSort(d_tm.mkBitVectorSort(4)));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkSetSort(d_tm.mkBitVectorSort(4)));
  }

  @Test
  void mkBagSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkBagSort(d_tm.getBooleanSort()));
    assertDoesNotThrow(() -> d_tm.mkBagSort(d_tm.getIntegerSort()));
    assertDoesNotThrow(() -> d_tm.mkBagSort(d_tm.mkBitVectorSort(4)));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkBagSort(d_tm.mkBitVectorSort(4)));
  }

  @Test
  void mkSequenceSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkSequenceSort(d_tm.getBooleanSort()));
    assertDoesNotThrow(() -> d_tm.mkSequenceSort(d_tm.mkSequenceSort(d_tm.getIntegerSort())));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkSequenceSort(d_tm.getIntegerSort()));
  }

  @Test
  void mkAbstractSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkAbstractSort(ARRAY_SORT));
    assertDoesNotThrow(() -> d_tm.mkAbstractSort(BITVECTOR_SORT));
    assertDoesNotThrow(() -> d_tm.mkAbstractSort(TUPLE_SORT));
    assertDoesNotThrow(() -> d_tm.mkAbstractSort(SET_SORT));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkAbstractSort(BOOLEAN_SORT));
  }

  @Test
  void mkUninterpretedSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkUninterpretedSort("u"));
    assertDoesNotThrow(() -> d_tm.mkUninterpretedSort(""));
  }

  @Test
  void mkUnresolvedDatatypeSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkUnresolvedDatatypeSort("u"));
    assertDoesNotThrow(() -> d_tm.mkUnresolvedDatatypeSort("u", 1));
    assertDoesNotThrow(() -> d_tm.mkUnresolvedDatatypeSort(""));
    assertDoesNotThrow(() -> d_tm.mkUnresolvedDatatypeSort("", 1));
  }

  @Test
  void mkUninterpretedSortConstructorSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkUninterpretedSortConstructorSort(2, "s"));
    assertDoesNotThrow(() -> d_tm.mkUninterpretedSortConstructorSort(2));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkUninterpretedSortConstructorSort(0));
  }

  @Test
  void mkTupleSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkTupleSort(new Sort[] {d_tm.getIntegerSort()}));
    Sort funSort = d_tm.mkFunctionSort(d_tm.mkUninterpretedSort("u"), d_tm.getIntegerSort());
    assertDoesNotThrow(() -> d_tm.mkTupleSort(new Sort[] {d_tm.getIntegerSort(), funSort}));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkTupleSort(new Sort[] {d_tm.getIntegerSort()}));
  }

  @Test
  void mkNullableSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkNullableSort(d_tm.getIntegerSort()));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkNullableSort(d_tm.getIntegerSort()));
  }

  @Test
  void mkBitVector() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkBitVector(8, 2));
    assertDoesNotThrow(() -> d_tm.mkBitVector(32, 2));
    assertDoesNotThrow(() -> d_tm.mkBitVector(8, "-1111111", 2));
    assertDoesNotThrow(() -> d_tm.mkBitVector(8, "0101", 2));
    assertDoesNotThrow(() -> d_tm.mkBitVector(8, "00000101", 2));
    assertDoesNotThrow(() -> d_tm.mkBitVector(8, "-127", 10));
    assertDoesNotThrow(() -> d_tm.mkBitVector(8, "255", 10));
    assertDoesNotThrow(() -> d_tm.mkBitVector(8, "-7f", 16));
    assertDoesNotThrow(() -> d_tm.mkBitVector(8, "a0", 16));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(0, 2));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(0, "-127", 10));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(0, "a0", 16));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "", 2));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "101", 5));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "128", 11));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "a0", 21));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "-11111111", 2));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "101010101", 2));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "-256", 10));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "257", 10));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "-a0", 16));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "fffff", 16));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "10201010", 2));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "-25x", 10));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "2x7", 10));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkBitVector(8, "fzff", 16));

    assertEquals(d_tm.mkBitVector(8, "0101", 2), d_tm.mkBitVector(8, "00000101", 2));
    assertEquals(d_tm.mkBitVector(4, "-1", 2), d_tm.mkBitVector(4, "1111", 2));
    assertEquals(d_tm.mkBitVector(4, "-1", 16), d_tm.mkBitVector(4, "1111", 2));
    assertEquals(d_tm.mkBitVector(4, "-1", 10), d_tm.mkBitVector(4, "1111", 2));
    assertEquals(d_tm.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
    assertEquals(d_tm.mkBitVector(8, "F", 16).toString(), "#b00001111");
    assertEquals(d_tm.mkBitVector(8, "-1", 10), d_tm.mkBitVector(8, "FF", 16));
  }

  @Test
  void mkVar() throws CVC5ApiException
  {
    Sort boolSort = d_tm.getBooleanSort();
    Sort intSort = d_tm.getIntegerSort();
    Sort funSort = d_tm.mkFunctionSort(intSort, boolSort);
    assertDoesNotThrow(() -> d_tm.mkVar(boolSort));
    assertDoesNotThrow(() -> d_tm.mkVar(funSort));
    assertDoesNotThrow(() -> d_tm.mkVar(boolSort, ("b")));
    assertDoesNotThrow(() -> d_tm.mkVar(funSort, ""));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkVar(new Sort()));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkVar(new Sort(), "a"));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkVar(boolSort, "x"));
  }

  @Test
  void mkBoolean() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkBoolean(true));
    assertDoesNotThrow(() -> d_tm.mkBoolean(false));
  }

  @Test
  void mkRoundingMode() throws CVC5ApiException
  {
    assertEquals(d_tm.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).toString(),
        "roundNearestTiesToEven");
    assertEquals(
        d_tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE).toString(), "roundTowardPositive");
    assertEquals(
        d_tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE).toString(), "roundTowardNegative");
    assertEquals(d_tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO).toString(), "roundTowardZero");
    assertEquals(d_tm.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY).toString(),
        "roundNearestTiesToAway");
  }

  @Test
  void mkFloatingPoint() throws CVC5ApiException
  {
    Term t1 = d_tm.mkBitVector(8);
    Term t2 = d_tm.mkBitVector(4);
    Term t3 = d_tm.mkInteger(2);
    assertDoesNotThrow(() -> d_tm.mkFloatingPoint(3, 5, t1));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkFloatingPoint(0, 5, new Term()));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkFloatingPoint(0, 5, t1));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkFloatingPoint(3, 0, t1));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkFloatingPoint(3, 5, t2));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkFloatingPoint(3, 5, t2));

    assertEquals(
        d_tm.mkFloatingPoint(d_tm.mkBitVector(1), d_tm.mkBitVector(5), d_tm.mkBitVector(10)),
        d_tm.mkFloatingPoint(5, 11, d_tm.mkBitVector(16)));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkFloatingPoint(3, 5, t1));
  }

  @Test
  void mkCardinalityConstraint() throws CVC5ApiException
  {
    Sort su = d_tm.mkUninterpretedSort("u");
    Sort si = d_tm.getIntegerSort();
    assertDoesNotThrow(() -> d_tm.mkCardinalityConstraint(su, 3));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkCardinalityConstraint(si, 3));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkCardinalityConstraint(su, 0));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkCardinalityConstraint(su, 3));
  }

  @Test
  void mkEmptySet() throws CVC5ApiException
  {
    Sort s = d_tm.mkSetSort(d_tm.getBooleanSort());
    assertThrows(CVC5ApiException.class, () -> d_tm.mkEmptySet(new Sort()));
    assertDoesNotThrow(() -> d_tm.mkEmptySet(s));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkEmptySet(d_tm.getBooleanSort()));
    assertDoesNotThrow(() -> d_solver.mkEmptySet(s));
  }

  @Test
  void mkEmptyBag() throws CVC5ApiException
  {
    Sort s = d_tm.mkBagSort(d_tm.getBooleanSort());
    assertThrows(CVC5ApiException.class, () -> d_tm.mkEmptyBag(new Sort()));
    assertDoesNotThrow(() -> d_tm.mkEmptyBag(s));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkEmptyBag(d_tm.getBooleanSort()));

    assertDoesNotThrow(() -> d_solver.mkEmptyBag(s));
  }

  @Test
  void mkEmptySequence() throws CVC5ApiException
  {
    Sort s = d_tm.mkSequenceSort(d_tm.getBooleanSort());
    assertDoesNotThrow(() -> d_tm.mkEmptySequence(s));
    assertDoesNotThrow(() -> d_tm.mkEmptySequence(d_tm.getBooleanSort()));
    assertDoesNotThrow(() -> d_solver.mkEmptySequence(s));
  }

  @Test
  void mkFalse() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkFalse());
    assertDoesNotThrow(() -> d_tm.mkFalse());
  }

  @Test
  void mkFloatingPointNaN() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkFloatingPointNaN(3, 5));
  }

  @Test
  void mkFloatingPointNegZero() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_tm.mkFloatingPointNegZero(3, 5));
  }

  @Test
  void mkFloatingPointNegInf()
  {
    assertDoesNotThrow(() -> d_tm.mkFloatingPointNegInf(3, 5));
  }

  @Test
  void mkFloatingPointPosInf()
  {
    assertDoesNotThrow(() -> d_tm.mkFloatingPointPosInf(3, 5));
  }

  @Test
  void mkFloatingPointPosZero()
  {
    assertDoesNotThrow(() -> d_tm.mkFloatingPointPosZero(3, 5));
  }

  @Test
  void mkOp()
  {
    // Unlike c++,  mkOp(Kind kind, Kind k) is a type error in java
    // assertThrows(CVC5ApiException.class, () -> d_tm.mkOp(BITVECTOR_EXTRACT, EQUAL));

    // mkOp(Kind kind, const std::string& arg)
    assertDoesNotThrow(() -> d_tm.mkOp(DIVISIBLE, "2147483648"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkOp(BITVECTOR_EXTRACT, "asdf"));

    // mkOp(Kind kind, int arg)
    assertDoesNotThrow(() -> d_tm.mkOp(DIVISIBLE, 1));
    assertDoesNotThrow(() -> d_tm.mkOp(BITVECTOR_ROTATE_LEFT, 1));
    assertDoesNotThrow(() -> d_tm.mkOp(BITVECTOR_ROTATE_RIGHT, 1));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkOp(BITVECTOR_EXTRACT, 1));

    // mkOp(Kind kind, int arg1, int arg2)
    assertDoesNotThrow(() -> d_tm.mkOp(BITVECTOR_EXTRACT, 1, 1));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkOp(DIVISIBLE, 1, 2));

    // mkOp(Kind kind, int[] args)
    int[] args = new int[] {1, 2, 2};
    assertDoesNotThrow(() -> d_tm.mkOp(TUPLE_PROJECT, args));
  }

  @Test
  void mkPi()
  {
    assertDoesNotThrow(() -> d_tm.mkPi());
  }

  @Test
  void mkInteger()
  {
    assertDoesNotThrow(() -> d_tm.mkInteger("123"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("1.23"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("1/23"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("12/3"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(".2"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("2."));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(""));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("asdf"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("1.2/3"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("."));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("/"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("2/"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("/2"));

    assertDoesNotThrow(() -> d_tm.mkReal(("123")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(("1.23")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(("1/23")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(("12/3")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger((".2")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(("2.")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(("")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(("asdf")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(("1.2/3")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger((".")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(("/")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(("2/")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(("/2")));

    int val1 = 1;
    long val2 = -1;
    int val3 = 1;
    long val4 = -1;
    assertDoesNotThrow(() -> d_tm.mkInteger(val1));
    assertDoesNotThrow(() -> d_tm.mkInteger(val2));
    assertDoesNotThrow(() -> d_tm.mkInteger(val3));
    assertDoesNotThrow(() -> d_tm.mkInteger(val4));
    assertDoesNotThrow(() -> d_tm.mkInteger(val4));
  }

  @Test
  void mkReal()
  {
    assertDoesNotThrow(() -> d_tm.mkReal("123"));
    assertDoesNotThrow(() -> d_tm.mkReal("1.23"));
    assertDoesNotThrow(() -> d_tm.mkReal("1/23"));
    assertDoesNotThrow(() -> d_tm.mkReal("12/3"));
    assertDoesNotThrow(() -> d_tm.mkReal(".2"));
    assertDoesNotThrow(() -> d_tm.mkReal("2."));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal(""));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal("asdf"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal("1.2/3"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal("."));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal("/"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal("2/"));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal("/2"));

    assertDoesNotThrow(() -> d_tm.mkReal(("123")));
    assertDoesNotThrow(() -> d_tm.mkReal(("1.23")));
    assertDoesNotThrow(() -> d_tm.mkReal(("1/23")));
    assertDoesNotThrow(() -> d_tm.mkReal(("12/3")));
    assertDoesNotThrow(() -> d_tm.mkReal((".2")));
    assertDoesNotThrow(() -> d_tm.mkReal(("2.")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal(("")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal(("asdf")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal(("1.2/3")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal((".")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal(("/")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal(("2/")));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkReal(("/2")));

    int val1 = 1;
    long val2 = -1;
    int val3 = 1;
    long val4 = -1;
    assertDoesNotThrow(() -> d_tm.mkReal(val1));
    assertDoesNotThrow(() -> d_tm.mkReal(val2));
    assertDoesNotThrow(() -> d_tm.mkReal(val3));
    assertDoesNotThrow(() -> d_tm.mkReal(val4));
    assertDoesNotThrow(() -> d_tm.mkReal(val4));
    assertDoesNotThrow(() -> d_tm.mkReal(val1, val1));
    assertDoesNotThrow(() -> d_tm.mkReal(val2, val2));
    assertDoesNotThrow(() -> d_tm.mkReal(val3, val3));
    assertDoesNotThrow(() -> d_tm.mkReal(val4, val4));
  }

  @Test
  void mkRegexpNone()
  {
    Sort strSort = d_tm.getStringSort();
    Term s = d_tm.mkConst(strSort, "s");
    assertDoesNotThrow(() -> d_tm.mkTerm(STRING_IN_REGEXP, s, d_tm.mkRegexpNone()));
  }

  @Test
  void mkRegexpAll()
  {
    Sort strSort = d_tm.getStringSort();
    Term s = d_tm.mkConst(strSort, "s");
    assertDoesNotThrow(() -> d_tm.mkTerm(STRING_IN_REGEXP, s, d_tm.mkRegexpAll()));
  }

  @Test
  void mkRegexpAllchar()
  {
    Sort strSort = d_tm.getStringSort();
    Term s = d_tm.mkConst(strSort, "s");
    assertDoesNotThrow(() -> d_tm.mkTerm(STRING_IN_REGEXP, s, d_tm.mkRegexpAllchar()));
  }

  @Test
  void mkSepEmp()
  {
    assertDoesNotThrow(() -> d_tm.mkSepEmp());
  }

  @Test
  void mkSepNil()
  {
    assertDoesNotThrow(() -> d_tm.mkSepNil(d_tm.getBooleanSort()));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkSepNil(new Sort()));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkSepNil(d_tm.getIntegerSort()));
  }

  @Test
  void mkString()
  {
    assertDoesNotThrow(() -> d_tm.mkString(""));
    assertDoesNotThrow(() -> d_tm.mkString("asdfasdf"));
    assertEquals(d_tm.mkString("asdf\\nasdf").toString(), "\"asdf\\u{5c}nasdf\"");
    assertEquals(d_tm.mkString("asdf\\u{005c}nasdf", true).toString(), "\"asdf\\u{5c}nasdf\"");
  }

  @Test
  void mkTerm() throws CVC5ApiException
  {
    Sort bv32 = d_tm.mkBitVectorSort(32);
    Term a = d_tm.mkConst(bv32, "a");
    Term b = d_tm.mkConst(bv32, "b");
    Term[] v1 = new Term[] {a, b};
    Term[] v2 = new Term[] {a, new Term()};
    Term[] v3 = new Term[] {a, d_tm.mkTrue()};
    Term[] v4 = new Term[] {d_tm.mkInteger(1), d_tm.mkInteger(2)};
    Term[] v5 = new Term[] {d_tm.mkInteger(1), new Term()};
    Term[] v6 = new Term[] {};

    // mkTerm(Kind kind) const
    assertDoesNotThrow(() -> d_tm.mkTerm(PI));
    assertDoesNotThrow(() -> d_tm.mkTerm(REGEXP_NONE));
    assertDoesNotThrow(() -> d_tm.mkTerm(REGEXP_ALLCHAR));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(CONST_BITVECTOR));

    // mkTerm(Kind kind, Term child) const
    assertDoesNotThrow(() -> d_tm.mkTerm(NOT, d_tm.mkTrue()));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(NOT, new Term()));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(NOT, a));
    assertDoesNotThrow(() -> d_solver.mkTerm(NOT, d_tm.mkTrue()));

    // mkTerm(Kind kind, Term child1, Term child2) const
    assertDoesNotThrow(() -> d_tm.mkTerm(EQUAL, a, b));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(EQUAL, new Term(), b));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(EQUAL, a, new Term()));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(EQUAL, a, d_tm.mkTrue()));
    assertDoesNotThrow(() -> d_solver.mkTerm(EQUAL, a, b));

    // mkTerm(Kind kind, Term child1, Term child2, Term child3) const
    assertDoesNotThrow(() -> d_tm.mkTerm(ITE, d_tm.mkTrue(), d_tm.mkTrue(), d_tm.mkTrue()));
    assertThrows(
        CVC5ApiException.class, () -> d_tm.mkTerm(ITE, new Term(), d_tm.mkTrue(), d_tm.mkTrue()));

    assertThrows(
        CVC5ApiException.class, () -> d_tm.mkTerm(ITE, d_tm.mkTrue(), new Term(), d_tm.mkTrue()));

    assertThrows(
        CVC5ApiException.class, () -> d_tm.mkTerm(ITE, d_tm.mkTrue(), d_tm.mkTrue(), new Term()));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(ITE, d_tm.mkTrue(), d_tm.mkTrue(), b));

    assertDoesNotThrow(() -> d_solver.mkTerm(ITE, d_tm.mkTrue(), d_tm.mkTrue(), d_tm.mkTrue()));

    // mkTerm(Kind kind, const Term[]& children) const
    assertDoesNotThrow(() -> d_tm.mkTerm(EQUAL, v1));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(EQUAL, v2));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(EQUAL, v3));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(DISTINCT, v6));
  }

  @Test
  void mkTermFromOp() throws CVC5ApiException
  {
    Sort bv32 = d_tm.mkBitVectorSort(32);
    Term a = d_tm.mkConst(bv32, "a");
    Term b = d_tm.mkConst(bv32, "b");
    Term[] v1 = new Term[] {d_tm.mkInteger(1), d_tm.mkInteger(2)};
    Term[] v2 = new Term[] {d_tm.mkInteger(1), new Term()};
    Term[] v3 = new Term[] {};
    Term[] v4 = new Term[] {d_tm.mkInteger(5)};

    // simple operator terms
    Op opterm1 = d_tm.mkOp(BITVECTOR_EXTRACT, 2, 1);
    Op opterm2 = d_tm.mkOp(DIVISIBLE, 1);

    // list datatype
    Sort sort = d_tm.mkParamSort("T");
    DatatypeDecl listDecl = d_tm.mkDatatypeDecl("paramlist", new Sort[] {sort});
    DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
    DatatypeConstructorDecl nil = d_tm.mkDatatypeConstructorDecl("nil");
    cons.addSelector("head", sort);
    cons.addSelectorSelf("tail");
    listDecl.addConstructor(cons);
    listDecl.addConstructor(nil);
    Sort listSort = d_tm.mkDatatypeSort(listDecl);
    Sort intListSort = listSort.instantiate(new Sort[] {d_tm.getIntegerSort()});
    Term c = d_tm.mkConst(intListSort, "c");
    Datatype list = listSort.getDatatype();

    // list datatype constructor and selector operator terms
    Term consTerm = list.getConstructor("cons").getTerm();
    Term nilTerm = list.getConstructor("nil").getTerm();
    Term headTerm = list.getConstructor("cons").getSelector("head").getTerm();
    Term tailTerm = list.getConstructor("cons").getSelector("tail").getTerm();

    // mkTerm(Op op, Term term) const
    assertDoesNotThrow(() -> d_tm.mkTerm(APPLY_CONSTRUCTOR, nilTerm));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(APPLY_SELECTOR, nilTerm));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(APPLY_SELECTOR, consTerm));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(APPLY_CONSTRUCTOR, consTerm));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm1));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(APPLY_SELECTOR, headTerm));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm1));
    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm));

    // mkTerm(Op op, Term child) const
    assertDoesNotThrow(() -> d_tm.mkTerm(opterm1, a));
    assertDoesNotThrow(() -> d_tm.mkTerm(opterm2, d_tm.mkInteger(1)));
    assertDoesNotThrow(() -> d_tm.mkTerm(APPLY_SELECTOR, headTerm, c));
    assertDoesNotThrow(() -> d_tm.mkTerm(APPLY_SELECTOR, tailTerm, c));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm2, a));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm1, new Term()));
    assertThrows(
        CVC5ApiException.class, () -> d_tm.mkTerm(APPLY_CONSTRUCTOR, consTerm, d_tm.mkInteger(0)));

    assertDoesNotThrow(() -> d_solver.mkTerm(opterm1, a));

    // mkTerm(Op op, Term child1, Term child2) const
    assertDoesNotThrow(()
                           -> d_tm.mkTerm(APPLY_CONSTRUCTOR,
                               consTerm,
                               d_tm.mkInteger(0),
                               d_tm.mkTerm(APPLY_CONSTRUCTOR, nilTerm)));
    assertThrows(
        CVC5ApiException.class, () -> d_tm.mkTerm(opterm2, d_tm.mkInteger(1), d_tm.mkInteger(2)));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm1, a, b));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm2, d_tm.mkInteger(1), new Term()));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm2, new Term(), d_tm.mkInteger(1)));

    assertDoesNotThrow(()
                           -> d_solver.mkTerm(APPLY_CONSTRUCTOR,
                               consTerm,
                               d_tm.mkInteger(0),
                               d_tm.mkTerm(APPLY_CONSTRUCTOR, nilTerm)));

    // mkTerm(Op op, Term child1, Term child2, Term child3) const
    Sort ssort = d_tm.getStringSort();
    Sort isort = d_tm.getIntegerSort();
    Sort xsort = d_tm.mkTupleSort(new Sort[] {ssort, ssort, isort});
    Sort ysort = d_tm.mkTupleSort(new Sort[] {ssort, isort});
    Term f = d_solver.defineFun("f",
        new Term[] {d_tm.mkVar(xsort, "x"), d_tm.mkVar(ysort, "y")},
        ysort,
        d_tm.mkTuple(new Term[] {
            d_tm.mkString("a"), d_tm.mkTerm(ADD, d_tm.mkInteger(1), d_tm.mkInteger(2))}));
    Term tup =
        d_tm.mkTuple(new Term[] {d_tm.mkString("foo"), d_tm.mkString("bar"), d_tm.mkInteger(1)});
    assertDoesNotThrow(()
                           -> d_tm.mkTerm(d_tm.mkOp(RELATION_AGGREGATE, 0),
                               f,
                               d_tm.mkTuple(new Term[] {d_tm.mkString(""), d_tm.mkInteger(0)}),
                               d_tm.mkTerm(SET_SINGLETON, tup)));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm1, a, b, a));
    assertThrows(CVC5ApiException.class,
        () -> d_tm.mkTerm(opterm2, d_tm.mkInteger(1), d_tm.mkInteger(1), new Term()));

    // mkTerm(Op op, Term[] children)
    assertDoesNotThrow(() -> d_tm.mkTerm(opterm2, v4));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm2, v1));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm2, v2));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkTerm(opterm2, v3));
    assertDoesNotThrow(() -> d_solver.mkTerm(opterm2, v4));
  }

  @Test
  void mkTrue()
  {
    assertDoesNotThrow(() -> d_tm.mkTrue());
    assertDoesNotThrow(() -> d_tm.mkTrue());
  }

  @Test
  void mkTuple()
  {
    assertDoesNotThrow(() -> d_tm.mkTuple(new Term[] {d_tm.mkBitVector(3, "101", 2)}));
    assertDoesNotThrow(() -> d_tm.mkTuple(new Term[] {d_tm.mkInteger("5")}));

    assertDoesNotThrow(() -> d_tm.mkTuple(new Term[] {d_tm.mkReal("5.3")}));

    Solver slv = new Solver();
    assertThrows(
        CVC5ApiException.class, () -> slv.mkTuple(new Term[] {d_solver.mkBitVector(3, "101", 2)}));

    assertThrows(
        CVC5ApiException.class, () -> slv.mkTuple(new Term[] {d_tm.mkBitVector(3, "101", 2)}));
  }

  @Test
  void mkNullableSome()
  {
    assertDoesNotThrow(() -> d_tm.mkNullableSome(d_tm.mkBitVector(3, "101", 2)));
    assertDoesNotThrow(() -> d_tm.mkNullableSome(d_tm.mkInteger("5")));
    assertDoesNotThrow(() -> d_tm.mkNullableSome(d_tm.mkReal("5.3")));

    Solver slv = new Solver();
    assertThrows(
        CVC5ApiException.class, () -> slv.mkNullableSome(d_solver.mkBitVector(3, "101", 2)));

    assertThrows(CVC5ApiException.class, () -> slv.mkNullableSome(d_tm.mkBitVector(3, "101", 2)));
  }

  @Test
  void mkNullableVal()
  {
    Term some = d_tm.mkNullableSome(d_tm.mkInteger(5));
    Term value = d_tm.mkNullableVal(some);
    value = d_solver.simplify(value);
    assertEquals(5, value.getIntegerValue().intValue());
  }

  @Test
  void mkNullableIsNull()
  {
    Term some = d_tm.mkNullableSome(d_tm.mkInteger(5));
    Term value = d_tm.mkNullableIsNull(some);
    value = d_solver.simplify(value);
    assertEquals(false, value.getBooleanValue());
  }

  @Test
  void mkNullableIsSome()
  {
    Term some = d_tm.mkNullableSome(d_tm.mkInteger(5));
    Term value = d_tm.mkNullableIsSome(some);
    value = d_solver.simplify(value);
    assertEquals(true, value.getBooleanValue());
  }

  @Test
  void mkNullableNull()
  {
    Sort nullableSort = d_tm.mkNullableSort(d_tm.getBooleanSort());
    Term nullableNull = d_tm.mkNullableNull(nullableSort);
    Term value = d_tm.mkNullableIsNull(nullableNull);
    value = d_solver.simplify(value);
    assertEquals(true, value.getBooleanValue());
  }

  @Test
  void mkNullableLift()
  {
    Term some1 = d_tm.mkNullableSome(d_tm.mkInteger(1));
    Term some2 = d_tm.mkNullableSome(d_tm.mkInteger(2));
    Term some3 = d_tm.mkNullableLift(Kind.ADD, new Term[] {some1, some2});
    Term three = d_solver.simplify(d_tm.mkNullableVal(some3));
    assertEquals(3, three.getIntegerValue().intValue());
  }

  @Test
  void mkUniverseSet()
  {
    assertDoesNotThrow(() -> d_tm.mkUniverseSet(d_tm.getBooleanSort()));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkUniverseSet(new Sort()));
    assertDoesNotThrow(() -> d_solver.mkUniverseSet(d_tm.getBooleanSort()));
  }

  @Test
  void mkConst()
  {
    Sort boolSort = d_tm.getBooleanSort();
    Sort intSort = d_tm.getIntegerSort();
    Sort funSort = d_tm.mkFunctionSort(intSort, boolSort);
    assertDoesNotThrow(() -> d_tm.mkConst(boolSort));
    assertDoesNotThrow(() -> d_tm.mkConst(funSort));
    assertDoesNotThrow(() -> d_tm.mkConst(boolSort, ("b")));
    assertDoesNotThrow(() -> d_tm.mkConst(intSort, ("i")));
    assertDoesNotThrow(() -> d_tm.mkConst(funSort, "f"));
    assertDoesNotThrow(() -> d_tm.mkConst(funSort, ""));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkConst(new Sort()));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkConst(new Sort(), "a"));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkConst(boolSort));
  }

  @Test
  void mkConstArray()
  {
    Sort intSort = d_tm.getIntegerSort();
    Sort arrSort = d_tm.mkArraySort(intSort, intSort);
    Term zero = d_tm.mkInteger(0);
    Term constArr = d_tm.mkConstArray(arrSort, zero);

    assertDoesNotThrow(() -> d_tm.mkConstArray(arrSort, zero));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkConstArray(new Sort(), zero));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkConstArray(arrSort, new Term()));
    assertThrows(CVC5ApiException.class, () -> d_tm.mkConstArray(arrSort, d_tm.mkBitVector(1, 1)));

    assertThrows(CVC5ApiException.class, () -> d_tm.mkConstArray(intSort, zero));
    Solver slv = new Solver();
    Term zero2 = slv.mkInteger(0);
    Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
    assertThrows(CVC5ApiException.class, () -> slv.mkConstArray(arrSort2, zero));
    assertThrows(CVC5ApiException.class, () -> slv.mkConstArray(arrSort, zero2));
  }

  @Test
  void uFIteration()
  {
    Sort intSort = d_tm.getIntegerSort();
    Sort funSort = d_tm.mkFunctionSort(new Sort[] {intSort, intSort}, intSort);
    Term x = d_tm.mkConst(intSort, "x");
    Term y = d_tm.mkConst(intSort, "y");
    Term f = d_tm.mkConst(funSort, "f");
    Term fxy = d_tm.mkTerm(APPLY_UF, f, x, y);

    // Expecting the uninterpreted function to be one of the children
    Term expected_children[] = new Term[] {f, x, y};
    int idx = 0;
    for (Term c : fxy)
    {
      assertEquals(c, expected_children[idx]);
      idx++;
    }
  }

  @Test
  void getStatistics()
  {
    // do some array reasoning to make sure we have a double statistics
    {
      Sort s1 = d_tm.getIntegerSort();
      Sort s2 = d_tm.mkArraySort(s1, s1);
      Term t1 = d_tm.mkConst(s1, "i");
      Term t2 = d_tm.mkVar(s2, "a");
      Term t3 = d_tm.mkTerm(Kind.SELECT, t2, t1);
      d_solver.checkSat();
    }
    Statistics stats = d_tm.getStatistics();
    stats.toString();
    for (Map.Entry<String, Stat> s : stats)
    {
      assertFalse(s.getKey().isEmpty());
    }
    for (Statistics.ConstIterator it = stats.iterator(true, true); it.hasNext();)
    {
      Map.Entry<String, Stat> elem = it.next();
      if (elem.getKey().equals("cvc5::CONSTANT"))
      {
        assertFalse(elem.getValue().isInternal());
        assertFalse(elem.getValue().isDefault());
        assertTrue(elem.getValue().isHistogram());
        Map<String, Long> hist = elem.getValue().getHistogram();
        assertFalse(hist.isEmpty());
        assertEquals(elem.getValue().toString(), "{ integer type: 1 }");
      }
    }
  }
}