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

package cvc5;

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

import java.util.*;
import java.util.concurrent.atomic.AtomicReference;
import org.junit.jupiter.api.AfterEach;
import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.Test;

class SolverTest
{
  private Solver d_solver;

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

  @Test void recoverableException() throws CVC5ApiException
  {
    d_solver.setOption("produce-models", "true");
    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
    d_solver.assertFormula(x.eqTerm(x).notTerm());
    assertThrows(CVC5ApiRecoverableException.class, () -> d_solver.getValue(x));
  }

  @Test void supportsFloatingPoint() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
  }

  @Test void getBooleanSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_solver.getBooleanSort());
  }

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

  @Test void getNullSort() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_solver.getNullSort());
  }

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

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

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

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

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

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

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

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

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

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

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

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

  @Test void mkDatatypeSorts() throws CVC5ApiException
  {
    Solver slv = new Solver();

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

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

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

    /* with unresolved sorts */
    Sort unresList = d_solver.mkUninterpretedSort("ulist");
    Set<Sort> unresSorts = new HashSet<>();
    unresSorts.add(unresList);
    DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist");
    DatatypeConstructorDecl ucons = d_solver.mkDatatypeConstructorDecl("ucons");
    ucons.addSelector("car", unresList);
    ucons.addSelector("cdr", unresList);
    ulist.addConstructor(ucons);
    DatatypeConstructorDecl unil = d_solver.mkDatatypeConstructorDecl("unil");
    ulist.addConstructor(unil);
    DatatypeDecl[] udecls = new DatatypeDecl[] {ulist};
    assertDoesNotThrow(() -> d_solver.mkDatatypeSorts(Arrays.asList(udecls), unresSorts));

    assertThrows(
        CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls), unresSorts));

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

  @Test void mkFunctionSort() throws CVC5ApiException
  {
    assertDoesNotThrow(()
                           -> d_solver.mkFunctionSort(
                               d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()));
    Sort funSort =
        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
    // function arguments are allowed
    assertDoesNotThrow(() -> d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()));
    // non-first-class arguments are not allowed
    Sort reSort = d_solver.getRegExpSort();
    assertThrows(
        CVC5ApiException.class, () -> d_solver.mkFunctionSort(reSort, d_solver.getIntegerSort()));

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  @Test void mkRoundingMode() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO));
  }

  @Test void mkUninterpretedConst() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.mkUninterpretedConst(d_solver.getNullSort(), 1));
    Solver slv = new Solver();
    assertThrows(
        CVC5ApiException.class, () -> slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
  }

  @Test void mkAbstractValue() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_solver.mkAbstractValue(("1")));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("0")));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("-1")));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("1.2")));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("1/2"));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("asdf"));

    assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1));
    assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1));
    assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1));
    assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1));
    // java does not have specific types for unsigned integers, therefore the two lines below do not
    // make sense in java. assertDoesNotThrow(() -> d_solver.mkAbstractValue((int)-1));
    // assertDoesNotThrow(() -> d_solver.mkAbstractValue((long)-1));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(0));
  }

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

    assertThrows(
        CVC5ApiException.class, () -> d_solver.mkFloatingPoint(0, 5, d_solver.getNullTerm()));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPoint(0, 5, t1));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPoint(3, 0, t1));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPoint(3, 5, t2));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPoint(3, 5, t2));

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

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

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

    assertThrows(CVC5ApiException.class, () -> slv.mkEmptyBag(s));
  }

  @Test void mkEmptySequence() throws CVC5ApiException
  {
    Solver slv = new Solver();
    Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort());
    assertDoesNotThrow(() -> d_solver.mkEmptySequence(s));
    assertDoesNotThrow(() -> d_solver.mkEmptySequence(d_solver.getBooleanSort()));
    assertThrows(CVC5ApiException.class, () -> slv.mkEmptySequence(s));
  }

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

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

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

  @Test void mkNegInf()
  {
    assertDoesNotThrow(() -> d_solver.mkNegInf(3, 5));
  }

  @Test void mkPosInf()
  {
    assertDoesNotThrow(() -> d_solver.mkPosInf(3, 5));
  }

  @Test void mkPosZero()
  {
    assertDoesNotThrow(() -> d_solver.mkPosZero(3, 5));
  }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    // mkTerm(Kind kind) const
    assertDoesNotThrow(() -> d_solver.mkTerm(PI));
    assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_EMPTY));
    assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_SIGMA));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(CONST_BITVECTOR));

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

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

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

    assertThrows(CVC5ApiException.class,
        () -> d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.getNullTerm(), d_solver.mkTrue()));

    assertThrows(CVC5ApiException.class,
        () -> d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.getNullTerm()));

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

    assertThrows(CVC5ApiException.class,
        () -> slv.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()));

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

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

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

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

    // list datatype constructor and selector operator terms
    Term consTerm1 = list.getConstructorTerm("cons");
    Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
    Term nilTerm1 = list.getConstructorTerm("nil");
    Term nilTerm2 = list.getConstructor("nil").getConstructorTerm();
    Term headTerm1 = list.getConstructor("cons").getSelectorTerm("head");
    Term headTerm2 = list.getConstructor("cons").getSelector("head").getSelectorTerm();
    Term tailTerm1 = list.getConstructor("cons").getSelectorTerm("tail");
    Term tailTerm2 = list.getConstructor("cons").getSelector("tail").getSelectorTerm();

    // mkTerm(Op op, Term term) const
    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, nilTerm1));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, consTerm1));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, headTerm1));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1));
    assertThrows(CVC5ApiException.class, () -> slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1));

    // mkTerm(Op op, Term child) const
    assertDoesNotThrow(() -> d_solver.mkTerm(opterm1, a));
    assertDoesNotThrow(() -> d_solver.mkTerm(opterm2, d_solver.mkInteger(1)));
    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, headTerm1, c));
    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, tailTerm2, c));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, a));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, d_solver.getNullTerm()));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver.mkInteger(0)));

    assertThrows(CVC5ApiException.class, () -> slv.mkTerm(opterm1, a));

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

    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, a, b));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.mkTerm(opterm2, d_solver.mkInteger(1), d_solver.getNullTerm()));

    assertThrows(CVC5ApiException.class,
        () -> d_solver.mkTerm(opterm2, d_solver.getNullTerm(), d_solver.mkInteger(1)));

    assertThrows(CVC5ApiException.class,
        ()
            -> slv.mkTerm(APPLY_CONSTRUCTOR,
                consTerm1,
                d_solver.mkInteger(0),
                d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));

    // mkTerm(Op op, Term child1, Term child2, Term child3) const
    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, a, b, a));
    assertThrows(CVC5ApiException.class,
        ()
            -> d_solver.mkTerm(
                opterm2, d_solver.mkInteger(1), d_solver.mkInteger(1), d_solver.getNullTerm()));

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

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

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

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

    assertThrows(CVC5ApiException.class,
        ()
            -> d_solver.mkTuple(new Sort[] {d_solver.mkBitVectorSort(4)},
                new Term[] {d_solver.mkBitVector(3, "101", 2)}));

    assertThrows(CVC5ApiException.class,
        ()
            -> d_solver.mkTuple(
                new Sort[] {d_solver.getIntegerSort()}, new Term[] {d_solver.mkReal("5.3")}));

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

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

  @Test void mkUniverseSet()
  {
    assertDoesNotThrow(() -> d_solver.mkUniverseSet(d_solver.getBooleanSort()));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkUniverseSet(d_solver.getNullSort()));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.mkUniverseSet(d_solver.getBooleanSort()));
  }

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

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

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

    assertDoesNotThrow(() -> d_solver.mkConstArray(arrSort, zero));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkConstArray(d_solver.getNullSort(), zero));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.mkConstArray(arrSort, d_solver.getNullTerm()));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.mkConstArray(arrSort, d_solver.mkBitVector(1, 1)));

    assertThrows(CVC5ApiException.class, () -> d_solver.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 declareDatatype()
  {
    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
    DatatypeConstructorDecl[] ctors1 = new DatatypeConstructorDecl[] {nil};
    assertDoesNotThrow(() -> d_solver.declareDatatype(("a"), ctors1));
    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
    DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil");
    DatatypeConstructorDecl[] ctors2 = new DatatypeConstructorDecl[] {cons, nil2};
    assertDoesNotThrow(() -> d_solver.declareDatatype(("b"), ctors2));
    DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons");
    DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil");
    DatatypeConstructorDecl[] ctors3 = new DatatypeConstructorDecl[] {cons2, nil3};
    assertDoesNotThrow(() -> d_solver.declareDatatype((""), ctors3));
    DatatypeConstructorDecl[] ctors4 = new DatatypeConstructorDecl[0];
    assertThrows(CVC5ApiException.class, () -> d_solver.declareDatatype(("c"), ctors4));

    assertThrows(CVC5ApiException.class, () -> d_solver.declareDatatype((""), ctors4));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.declareDatatype(("a"), ctors1));
  }

  @Test void declareFun() throws CVC5ApiException
  {
    Sort bvSort = d_solver.mkBitVectorSort(32);
    Sort funSort =
        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
    assertDoesNotThrow(() -> d_solver.declareFun("f1", new Sort[] {}, bvSort));
    assertDoesNotThrow(
        () -> d_solver.declareFun("f3", new Sort[] {bvSort, d_solver.getIntegerSort()}, bvSort));
    assertThrows(CVC5ApiException.class, () -> d_solver.declareFun("f2", new Sort[] {}, funSort));
    // functions as arguments is allowed
    assertDoesNotThrow(() -> d_solver.declareFun("f4", new Sort[] {bvSort, funSort}, bvSort));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.declareFun("f5", new Sort[] {bvSort, bvSort}, funSort));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.declareFun("f1", new Sort[] {}, bvSort));
  }

  @Test void declareSort()
  {
    assertDoesNotThrow(() -> d_solver.declareSort("s", 0));
    assertDoesNotThrow(() -> d_solver.declareSort("s", 2));
    assertDoesNotThrow(() -> d_solver.declareSort("", 2));
  }

  @Test void defineSort()
  {
    Sort sortVar0 = d_solver.mkParamSort("T0");
    Sort sortVar1 = d_solver.mkParamSort("T1");
    Sort intSort = d_solver.getIntegerSort();
    Sort realSort = d_solver.getRealSort();
    Sort arraySort0 = d_solver.mkArraySort(sortVar0, sortVar0);
    Sort arraySort1 = d_solver.mkArraySort(sortVar0, sortVar1);
    // Now create instantiations of the defined sorts
    assertDoesNotThrow(() -> arraySort0.substitute(sortVar0, intSort));
    assertDoesNotThrow(()
                           -> arraySort1.substitute(
                               new Sort[] {sortVar0, sortVar1}, new Sort[] {intSort, realSort}));
  }

  @Test void defineFun() throws CVC5ApiException
  {
    Sort bvSort = d_solver.mkBitVectorSort(32);
    Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
    Sort funSort2 =
        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
    Term b1 = d_solver.mkVar(bvSort, "b1");
    Term b11 = d_solver.mkVar(bvSort, "b1");
    Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
    Term b3 = d_solver.mkVar(funSort2, "b3");
    Term v1 = d_solver.mkConst(bvSort, "v1");
    Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
    Term v3 = d_solver.mkConst(funSort2, "v3");
    Term f1 = d_solver.mkConst(funSort1, "f1");
    Term f2 = d_solver.mkConst(funSort2, "f2");
    Term f3 = d_solver.mkConst(bvSort, "f3");
    assertDoesNotThrow(() -> d_solver.defineFun("f", new Term[] {}, bvSort, v1));
    assertDoesNotThrow(() -> d_solver.defineFun("ff", new Term[] {b1, b2}, bvSort, v1));
    assertDoesNotThrow(() -> d_solver.defineFun(f1, new Term[] {b1, b11}, v1));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.defineFun("ff", new Term[] {v1, b2}, bvSort, v1));

    assertThrows(
        CVC5ApiException.class, () -> d_solver.defineFun("fff", new Term[] {b1}, bvSort, v3));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort2, v3));

    // b3 has function sort, which is allowed as an argument
    assertDoesNotThrow(() -> d_solver.defineFun("fffff", new Term[] {b1, b3}, bvSort, v1));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {v1, b11}, v1));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {b1}, v1));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {b1, b11}, v2));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {b1, b11}, v3));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f2, new Term[] {b1}, v2));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f3, new Term[] {b1}, v1));

    Solver slv = new Solver();
    Sort bvSort2 = slv.mkBitVectorSort(32);
    Term v12 = slv.mkConst(bvSort2, "v1");
    Term b12 = slv.mkVar(bvSort2, "b1");
    Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
    assertThrows(CVC5ApiException.class, () -> slv.defineFun("f", new Term[] {}, bvSort, v12));
    assertThrows(CVC5ApiException.class, () -> slv.defineFun("f", new Term[] {}, bvSort2, v1));
    assertThrows(
        CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b1, b22}, bvSort2, v12));
    assertThrows(
        CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b2}, bvSort2, v12));
    assertThrows(
        CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b22}, bvSort, v12));
    assertThrows(
        CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b22}, bvSort2, v1));
  }

  @Test void defineFunGlobal()
  {
    Sort bSort = d_solver.getBooleanSort();
    Sort fSort = d_solver.mkFunctionSort(bSort, bSort);

    Term bTrue = d_solver.mkBoolean(true);
    // (define-fun f () Bool true)
    Term f = d_solver.defineFun("f", new Term[] {}, bSort, bTrue, true);
    Term b = d_solver.mkVar(bSort, "b");
    Term gSym = d_solver.mkConst(fSort, "g");
    // (define-fun g (b Bool) Bool b)
    Term g = d_solver.defineFun(gSym, new Term[] {b}, b, true);

    // (assert (or (not f) (not (g true))))
    d_solver.assertFormula(
        d_solver.mkTerm(OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
    assertTrue(d_solver.checkSat().isUnsat());
    d_solver.resetAssertions();
    // (assert (or (not f) (not (g true))))
    d_solver.assertFormula(
        d_solver.mkTerm(OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
    assertTrue(d_solver.checkSat().isUnsat());
  }

  @Test void defineFunRec() throws CVC5ApiException
  {
    Sort bvSort = d_solver.mkBitVectorSort(32);
    Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
    Sort funSort2 =
        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
    Term b1 = d_solver.mkVar(bvSort, "b1");
    Term b11 = d_solver.mkVar(bvSort, "b1");
    Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
    Term b3 = d_solver.mkVar(funSort2, "b3");
    Term v1 = d_solver.mkConst(bvSort, "v1");
    Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
    Term v3 = d_solver.mkConst(funSort2, "v3");
    Term f1 = d_solver.mkConst(funSort1, "f1");
    Term f2 = d_solver.mkConst(funSort2, "f2");
    Term f3 = d_solver.mkConst(bvSort, "f3");
    assertDoesNotThrow(() -> d_solver.defineFunRec("f", new Term[] {}, bvSort, v1));
    assertDoesNotThrow(() -> d_solver.defineFunRec("ff", new Term[] {b1, b2}, bvSort, v1));
    assertDoesNotThrow(() -> d_solver.defineFunRec(f1, new Term[] {b1, b11}, v1));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.defineFunRec("fff", new Term[] {b1}, bvSort, v3));

    assertThrows(
        CVC5ApiException.class, () -> d_solver.defineFunRec("ff", new Term[] {b1, v2}, bvSort, v1));

    assertThrows(
        CVC5ApiException.class, () -> d_solver.defineFunRec("ffff", new Term[] {b1}, funSort2, v3));

    // b3 has function sort, which is allowed as an argument
    assertDoesNotThrow(() -> d_solver.defineFunRec("fffff", new Term[] {b1, b3}, bvSort, v1));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f1, new Term[] {b1}, v1));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f1, new Term[] {b1, b11}, v2));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f1, new Term[] {b1, b11}, v3));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f2, new Term[] {b1}, v2));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f3, new Term[] {b1}, v1));

    Solver slv = new Solver();
    Sort bvSort2 = slv.mkBitVectorSort(32);
    Term v12 = slv.mkConst(bvSort2, "v1");
    Term b12 = slv.mkVar(bvSort2, "b1");
    Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
    assertDoesNotThrow(() -> slv.defineFunRec("f", new Term[] {}, bvSort2, v12));
    assertDoesNotThrow(() -> slv.defineFunRec("ff", new Term[] {b12, b22}, bvSort2, v12));
    assertThrows(CVC5ApiException.class, () -> slv.defineFunRec("f", new Term[] {}, bvSort, v12));
    assertThrows(CVC5ApiException.class, () -> slv.defineFunRec("f", new Term[] {}, bvSort2, v1));
    assertThrows(
        CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b1, b22}, bvSort2, v12));

    assertThrows(
        CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b12, b2}, bvSort2, v12));

    assertThrows(
        CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b12, b22}, bvSort, v12));

    assertThrows(
        CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b12, b22}, bvSort2, v1));
  }

  @Test void defineFunRecWrongLogic() throws CVC5ApiException
  {
    d_solver.setLogic("QF_BV");
    Sort bvSort = d_solver.mkBitVectorSort(32);
    Sort funSort = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
    Term b = d_solver.mkVar(bvSort, "b");
    Term v = d_solver.mkConst(bvSort, "v");
    Term f = d_solver.mkConst(funSort, "f");
    assertThrows(
        CVC5ApiException.class, () -> d_solver.defineFunRec("f", new Term[] {}, bvSort, v));
    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f, new Term[] {b, b}, v));
  }

  @Test void defineFunRecGlobal() throws CVC5ApiException
  {
    Sort bSort = d_solver.getBooleanSort();
    Sort fSort = d_solver.mkFunctionSort(bSort, bSort);

    d_solver.push();
    Term bTrue = d_solver.mkBoolean(true);
    // (define-fun f () Bool true)
    Term f = d_solver.defineFunRec("f", new Term[] {}, bSort, bTrue, true);
    Term b = d_solver.mkVar(bSort, "b");
    Term gSym = d_solver.mkConst(fSort, "g");
    // (define-fun g (b Bool) Bool b)
    Term g = d_solver.defineFunRec(gSym, new Term[] {b}, b, true);

    // (assert (or (not f) (not (g true))))
    d_solver.assertFormula(
        d_solver.mkTerm(OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
    assertTrue(d_solver.checkSat().isUnsat());
    d_solver.pop();
    // (assert (or (not f) (not (g true))))
    d_solver.assertFormula(
        d_solver.mkTerm(OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
    assertTrue(d_solver.checkSat().isUnsat());
  }

  @Test void defineFunsRec() throws CVC5ApiException
  {
    Sort uSort = d_solver.mkUninterpretedSort("u");
    Sort bvSort = d_solver.mkBitVectorSort(32);
    Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
    Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
    Term b1 = d_solver.mkVar(bvSort, "b1");
    Term b11 = d_solver.mkVar(bvSort, "b1");
    Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
    Term b3 = d_solver.mkVar(funSort2, "b3");
    Term b4 = d_solver.mkVar(uSort, "b4");
    Term v1 = d_solver.mkConst(bvSort, "v1");
    Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
    Term v3 = d_solver.mkConst(funSort2, "v3");
    Term v4 = d_solver.mkConst(uSort, "v4");
    Term f1 = d_solver.mkConst(funSort1, "f1");
    Term f2 = d_solver.mkConst(funSort2, "f2");
    Term f3 = d_solver.mkConst(bvSort, "f3");
    assertDoesNotThrow(
        ()
            -> d_solver.defineFunsRec(
                new Term[] {f1, f2}, new Term[][] {{b1, b11}, {b4}}, new Term[] {v1, v2}));
    assertThrows(CVC5ApiException.class,
        ()
            -> d_solver.defineFunsRec(
                new Term[] {f1, f2}, new Term[][] {{v1, b11}, {b4}}, new Term[] {v1, v2}));
    assertThrows(CVC5ApiException.class,
        ()
            -> d_solver.defineFunsRec(
                new Term[] {f1, f3}, new Term[][] {{b1, b11}, {b4}}, new Term[] {v1, v2}));
    assertThrows(CVC5ApiException.class,
        ()
            -> d_solver.defineFunsRec(
                new Term[] {f1, f2}, new Term[][] {{b1}, {b4}}, new Term[] {v1, v2}));
    assertThrows(CVC5ApiException.class,
        ()
            -> d_solver.defineFunsRec(
                new Term[] {f1, f2}, new Term[][] {{b1, b2}, {b4}}, new Term[] {v1, v2}));
    assertThrows(CVC5ApiException.class,
        ()
            -> d_solver.defineFunsRec(
                new Term[] {f1, f2}, new Term[][] {{b1, b11}, {b4}}, new Term[] {v1, v4}));

    Solver slv = new Solver();
    Sort uSort2 = slv.mkUninterpretedSort("u");
    Sort bvSort2 = slv.mkBitVectorSort(32);
    Sort funSort12 = slv.mkFunctionSort(new Sort[] {bvSort2, bvSort2}, bvSort2);
    Sort funSort22 = slv.mkFunctionSort(uSort2, slv.getIntegerSort());
    Term b12 = slv.mkVar(bvSort2, "b1");
    Term b112 = slv.mkVar(bvSort2, "b1");
    Term b42 = slv.mkVar(uSort2, "b4");
    Term v12 = slv.mkConst(bvSort2, "v1");
    Term v22 = slv.mkConst(slv.getIntegerSort(), "v2");
    Term f12 = slv.mkConst(funSort12, "f1");
    Term f22 = slv.mkConst(funSort22, "f2");
    assertDoesNotThrow(
        ()
            -> slv.defineFunsRec(
                new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v22}));
    assertThrows(CVC5ApiException.class,
        ()
            -> slv.defineFunsRec(
                new Term[] {f1, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v22}));
    assertThrows(CVC5ApiException.class,
        ()
            -> slv.defineFunsRec(
                new Term[] {f12, f2}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v22}));
    assertThrows(CVC5ApiException.class,
        ()
            -> slv.defineFunsRec(
                new Term[] {f12, f22}, new Term[][] {{b1, b112}, {b42}}, new Term[] {v12, v22}));
    assertThrows(CVC5ApiException.class,
        ()
            -> slv.defineFunsRec(
                new Term[] {f12, f22}, new Term[][] {{b12, b11}, {b42}}, new Term[] {v12, v22}));
    assertThrows(CVC5ApiException.class,
        ()
            -> slv.defineFunsRec(
                new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b4}}, new Term[] {v12, v22}));
    assertThrows(CVC5ApiException.class,
        ()
            -> slv.defineFunsRec(
                new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v1, v22}));
    assertThrows(CVC5ApiException.class,
        ()
            -> slv.defineFunsRec(
                new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v2}));
  }

  @Test void defineFunsRecWrongLogic() throws CVC5ApiException
  {
    d_solver.setLogic("QF_BV");
    Sort uSort = d_solver.mkUninterpretedSort("u");
    Sort bvSort = d_solver.mkBitVectorSort(32);
    Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
    Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
    Term b = d_solver.mkVar(bvSort, "b");
    Term u = d_solver.mkVar(uSort, "u");
    Term v1 = d_solver.mkConst(bvSort, "v1");
    Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
    Term f1 = d_solver.mkConst(funSort1, "f1");
    Term f2 = d_solver.mkConst(funSort2, "f2");
    assertThrows(CVC5ApiException.class,
        ()
            -> d_solver.defineFunsRec(
                new Term[] {f1, f2}, new Term[][] {{b, b}, {u}}, new Term[] {v1, v2}));
  }

  @Test void defineFunsRecGlobal() throws CVC5ApiException
  {
    Sort bSort = d_solver.getBooleanSort();
    Sort fSort = d_solver.mkFunctionSort(bSort, bSort);

    d_solver.push();
    Term bTrue = d_solver.mkBoolean(true);
    Term b = d_solver.mkVar(bSort, "b");
    Term gSym = d_solver.mkConst(fSort, "g");
    // (define-funs-rec ((g ((b Bool)) Bool)) (b))
    d_solver.defineFunsRec(new Term[] {gSym}, new Term[][] {{b}}, new Term[] {b}, true);

    // (assert (not (g true)))
    d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, gSym, bTrue).notTerm());
    assertTrue(d_solver.checkSat().isUnsat());
    d_solver.pop();
    // (assert (not (g true)))
    d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, gSym, bTrue).notTerm());
    assertTrue(d_solver.checkSat().isUnsat());
  }

  @Test void uFIteration()
  {
    Sort intSort = d_solver.getIntegerSort();
    Sort funSort = d_solver.mkFunctionSort(new Sort[] {intSort, intSort}, intSort);
    Term x = d_solver.mkConst(intSort, "x");
    Term y = d_solver.mkConst(intSort, "y");
    Term f = d_solver.mkConst(funSort, "f");
    Term fxy = d_solver.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 getInfo()
  {
    assertDoesNotThrow(() -> d_solver.getInfo("name"));
    assertThrows(CVC5ApiException.class, () -> d_solver.getInfo("asdf"));
  }

  @Test void getInterpolant() throws CVC5ApiException
  {
    d_solver.setLogic("QF_LIA");
    d_solver.setOption("produce-interpols", "default");
    d_solver.setOption("incremental", "false");

    Sort intSort = d_solver.getIntegerSort();
    Term zero = d_solver.mkInteger(0);
    Term x = d_solver.mkConst(intSort, "x");
    Term y = d_solver.mkConst(intSort, "y");
    Term z = d_solver.mkConst(intSort, "z");

    // Assumptions for interpolation: x + y > 0 /\ x < 0
    d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero));
    d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
    // Conjecture for interpolation: y + z > 0 \/ z < 0
    Term conj = d_solver.mkTerm(
        OR, d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), d_solver.mkTerm(LT, z, zero));
    Term output = d_solver.getNullTerm();
    // Call the interpolation api, while the resulting interpolant is the output
    d_solver.getInterpolant(conj, output);

    // We expect the resulting output to be a boolean formula
    assertTrue(output.getSort().isBoolean());
  }

  @Test void getOp() throws CVC5ApiException
  {
    Sort bv32 = d_solver.mkBitVectorSort(32);
    Term a = d_solver.mkConst(bv32, "a");
    Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 2, 1);
    Term exta = d_solver.mkTerm(ext, a);

    assertFalse(a.hasOp());
    assertThrows(CVC5ApiException.class, () -> a.getOp());
    assertTrue(exta.hasOp());
    assertEquals(exta.getOp(), ext);

    // Test Datatypes -- more complicated
    DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
    cons.addSelector("head", d_solver.getIntegerSort());
    cons.addSelectorSelf("tail");
    consListSpec.addConstructor(cons);
    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
    consListSpec.addConstructor(nil);
    Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
    Datatype consList = consListSort.getDatatype();

    Term consTerm = consList.getConstructorTerm("cons");
    Term nilTerm = consList.getConstructorTerm("nil");
    Term headTerm = consList.getConstructor("cons").getSelectorTerm("head");

    Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm);
    Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil);
    Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1);

    assertTrue(listnil.hasOp());
    assertTrue(listcons1.hasOp());
    assertTrue(listhead.hasOp());
  }

  @Test void getOption()
  {
    assertDoesNotThrow(() -> d_solver.getOption("incremental"));
    assertThrows(CVC5ApiException.class, () -> d_solver.getOption("asdf"));
  }

  @Test void getUnsatAssumptions1()
  {
    d_solver.setOption("incremental", "false");
    d_solver.checkSatAssuming(d_solver.mkFalse());
    assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions());
  }

  @Test void getUnsatAssumptions2()
  {
    d_solver.setOption("incremental", "true");
    d_solver.setOption("produce-unsat-assumptions", "false");
    d_solver.checkSatAssuming(d_solver.mkFalse());
    assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions());
  }

  @Test void getUnsatAssumptions3()
  {
    d_solver.setOption("incremental", "true");
    d_solver.setOption("produce-unsat-assumptions", "true");
    d_solver.checkSatAssuming(d_solver.mkFalse());
    assertDoesNotThrow(() -> d_solver.getUnsatAssumptions());
    d_solver.checkSatAssuming(d_solver.mkTrue());
    assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions());
  }

  @Test void getUnsatCore1()
  {
    d_solver.setOption("incremental", "false");
    d_solver.assertFormula(d_solver.mkFalse());
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatCore());
  }

  @Test void getUnsatCore2()
  {
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-unsat-cores", "false");
    d_solver.assertFormula(d_solver.mkFalse());
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatCore());
  }

  @Test void getUnsatCore3()
  {
    d_solver.setOption("incremental", "true");
    d_solver.setOption("produce-unsat-cores", "true");

    Sort uSort = d_solver.mkUninterpretedSort("u");
    Sort intSort = d_solver.getIntegerSort();
    Sort boolSort = d_solver.getBooleanSort();
    Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
    Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
    Term[] unsat_core;

    Term x = d_solver.mkConst(uSort, "x");
    Term y = d_solver.mkConst(uSort, "y");
    Term f = d_solver.mkConst(uToIntSort, "f");
    Term p = d_solver.mkConst(intPredSort, "p");
    Term zero = d_solver.mkInteger(0);
    Term one = d_solver.mkInteger(1);
    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
    Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
    Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
    Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
    d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_x));
    d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_y));
    d_solver.assertFormula(d_solver.mkTerm(GT, sum, one));
    d_solver.assertFormula(p_0);
    d_solver.assertFormula(p_f_y.notTerm());
    assertTrue(d_solver.checkSat().isUnsat());

    AtomicReference<Term[]> atomic = new AtomicReference<>();
    assertDoesNotThrow(() -> atomic.set(d_solver.getUnsatCore()));
    unsat_core = atomic.get();

    d_solver.resetAssertions();
    for (Term t : unsat_core)
    {
      d_solver.assertFormula(t);
    }
    Result res = d_solver.checkSat();
    assertTrue(res.isUnsat());
  }

  @Test void getValue1()
  {
    d_solver.setOption("produce-models", "false");
    Term t = d_solver.mkTrue();
    d_solver.assertFormula(t);
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.getValue(t));
  }

  @Test void getValue2()
  {
    d_solver.setOption("produce-models", "true");
    Term t = d_solver.mkFalse();
    d_solver.assertFormula(t);
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.getValue(t));
  }

  @Test void getValue3()
  {
    d_solver.setOption("produce-models", "true");
    Sort uSort = d_solver.mkUninterpretedSort("u");
    Sort intSort = d_solver.getIntegerSort();
    Sort boolSort = d_solver.getBooleanSort();
    Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
    Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
    Term[] unsat_core;

    Term x = d_solver.mkConst(uSort, "x");
    Term y = d_solver.mkConst(uSort, "y");
    Term z = d_solver.mkConst(uSort, "z");
    Term f = d_solver.mkConst(uToIntSort, "f");
    Term p = d_solver.mkConst(intPredSort, "p");
    Term zero = d_solver.mkInteger(0);
    Term one = d_solver.mkInteger(1);
    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
    Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
    Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
    Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);

    d_solver.assertFormula(d_solver.mkTerm(LEQ, zero, f_x));
    d_solver.assertFormula(d_solver.mkTerm(LEQ, zero, f_y));
    d_solver.assertFormula(d_solver.mkTerm(LEQ, sum, one));
    d_solver.assertFormula(p_0.notTerm());
    d_solver.assertFormula(p_f_y);
    assertTrue(d_solver.checkSat().isSat());
    assertDoesNotThrow(() -> d_solver.getValue(x));
    assertDoesNotThrow(() -> d_solver.getValue(y));
    assertDoesNotThrow(() -> d_solver.getValue(z));
    assertDoesNotThrow(() -> d_solver.getValue(sum));
    assertDoesNotThrow(() -> d_solver.getValue(p_f_y));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.getValue(x));
  }

  @Test void getQuantifierElimination()
  {
    Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
    Term forall = d_solver.mkTerm(FORALL,
        d_solver.mkTerm(BOUND_VAR_LIST, x),
        d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.getQuantifierElimination(d_solver.getNullTerm()));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.getQuantifierElimination(new Solver().mkBoolean(false)));

    assertDoesNotThrow(() -> d_solver.getQuantifierElimination(forall));
  }

  @Test void getQuantifierEliminationDisjunct()
  {
    Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
    Term forall = d_solver.mkTerm(FORALL,
        d_solver.mkTerm(BOUND_VAR_LIST, x),
        d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.getQuantifierEliminationDisjunct(d_solver.getNullTerm()));

    assertThrows(CVC5ApiException.class,
        () -> d_solver.getQuantifierEliminationDisjunct(new Solver().mkBoolean(false)));

    assertDoesNotThrow(() -> d_solver.getQuantifierEliminationDisjunct(forall));
  }

  @Test void declareSeparationHeap() throws CVC5ApiException
  {
    d_solver.setLogic("ALL");
    Sort integer = d_solver.getIntegerSort();
    assertDoesNotThrow(() -> d_solver.declareSeparationHeap(integer, integer));
    // cannot declare separation logic heap more than once
    assertThrows(CVC5ApiException.class, () -> d_solver.declareSeparationHeap(integer, integer));
  }

  /**
   * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
   * some simple separation logic constraints.
   */

  void checkSimpleSeparationConstraints(Solver solver)
  {
    Sort integer = solver.getIntegerSort();
    // declare the separation heap
    solver.declareSeparationHeap(integer, integer);
    Term x = solver.mkConst(integer, "x");
    Term p = solver.mkConst(integer, "p");
    Term heap = solver.mkTerm(SEP_PTO, p, x);
    solver.assertFormula(heap);
    Term nil = solver.mkSepNil(integer);
    solver.assertFormula(nil.eqTerm(solver.mkReal(5)));
    solver.checkSat();
  }

  @Test void getSeparationHeapTerm1() throws CVC5ApiException
  {
    d_solver.setLogic("QF_BV");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-models", "true");
    Term t = d_solver.mkTrue();
    d_solver.assertFormula(t);
    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
  }

  @Test void getSeparationHeapTerm2() throws CVC5ApiException
  {
    d_solver.setLogic("ALL");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-models", "false");
    checkSimpleSeparationConstraints(d_solver);
    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
  }

  @Test void getSeparationHeapTerm3() throws CVC5ApiException
  {
    d_solver.setLogic("ALL");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-models", "true");
    Term t = d_solver.mkFalse();
    d_solver.assertFormula(t);
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
  }

  @Test void getSeparationHeapTerm4() throws CVC5ApiException
  {
    d_solver.setLogic("ALL");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-models", "true");
    Term t = d_solver.mkTrue();
    d_solver.assertFormula(t);
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
  }

  @Test void getSeparationHeapTerm5() throws CVC5ApiException
  {
    d_solver.setLogic("ALL");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-models", "true");
    checkSimpleSeparationConstraints(d_solver);
    assertDoesNotThrow(() -> d_solver.getSeparationHeap());
  }

  @Test void getSeparationNilTerm1() throws CVC5ApiException
  {
    d_solver.setLogic("QF_BV");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-models", "true");
    Term t = d_solver.mkTrue();
    d_solver.assertFormula(t);
    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
  }

  @Test void getSeparationNilTerm2() throws CVC5ApiException
  {
    d_solver.setLogic("ALL");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-models", "false");
    checkSimpleSeparationConstraints(d_solver);
    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
  }

  @Test void getSeparationNilTerm3() throws CVC5ApiException
  {
    d_solver.setLogic("ALL");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-models", "true");
    Term t = d_solver.mkFalse();
    d_solver.assertFormula(t);
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
  }

  @Test void getSeparationNilTerm4() throws CVC5ApiException
  {
    d_solver.setLogic("ALL");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-models", "true");
    Term t = d_solver.mkTrue();
    d_solver.assertFormula(t);
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
  }

  @Test void getSeparationNilTerm5() throws CVC5ApiException
  {
    d_solver.setLogic("ALL");
    d_solver.setOption("incremental", "false");
    d_solver.setOption("produce-models", "true");
    checkSimpleSeparationConstraints(d_solver);
    assertDoesNotThrow(() -> d_solver.getSeparationNilTerm());
  }

  @Test void push1()
  {
    d_solver.setOption("incremental", "true");
    assertDoesNotThrow(() -> d_solver.push(1));
    assertThrows(CVC5ApiException.class, () -> d_solver.setOption("incremental", "false"));
    assertThrows(CVC5ApiException.class, () -> d_solver.setOption("incremental", "true"));
  }

  @Test void push2()
  {
    d_solver.setOption("incremental", "false");
    assertThrows(CVC5ApiException.class, () -> d_solver.push(1));
  }

  @Test void pop1()
  {
    d_solver.setOption("incremental", "false");
    assertThrows(CVC5ApiException.class, () -> d_solver.pop(1));
  }

  @Test void pop2()
  {
    d_solver.setOption("incremental", "true");
    assertThrows(CVC5ApiException.class, () -> d_solver.pop(1));
  }

  @Test void pop3()
  {
    d_solver.setOption("incremental", "true");
    assertDoesNotThrow(() -> d_solver.push(1));
    assertDoesNotThrow(() -> d_solver.pop(1));
    assertThrows(CVC5ApiException.class, () -> d_solver.pop(1));
  }

  @Test void blockModel1()
  {
    d_solver.setOption("produce-models", "true");
    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
    d_solver.assertFormula(x.eqTerm(x));
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.blockModel());
  }

  @Test void blockModel2() throws CVC5ApiException
  {
    d_solver.setOption("block-models", "literals");
    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
    d_solver.assertFormula(x.eqTerm(x));
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.blockModel());
  }

  @Test void blockModel3() throws CVC5ApiException
  {
    d_solver.setOption("produce-models", "true");
    d_solver.setOption("block-models", "literals");
    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
    d_solver.assertFormula(x.eqTerm(x));
    assertThrows(CVC5ApiException.class, () -> d_solver.blockModel());
  }

  @Test void blockModel4() throws CVC5ApiException
  {
    d_solver.setOption("produce-models", "true");
    d_solver.setOption("block-models", "literals");
    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
    d_solver.assertFormula(x.eqTerm(x));
    d_solver.checkSat();
    assertDoesNotThrow(() -> d_solver.blockModel());
  }

  @Test void blockModelValues1() throws CVC5ApiException
  {
    d_solver.setOption("produce-models", "true");
    d_solver.setOption("block-models", "literals");
    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
    d_solver.assertFormula(x.eqTerm(x));
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {}));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.blockModelValues(new Term[] {d_solver.getNullTerm()}));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.blockModelValues(new Term[] {new Solver().mkBoolean(false)}));
  }

  @Test void blockModelValues2() throws CVC5ApiException
  {
    d_solver.setOption("produce-models", "true");
    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
    d_solver.assertFormula(x.eqTerm(x));
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x}));
  }

  @Test void blockModelValues3() throws CVC5ApiException
  {
    d_solver.setOption("block-models", "literals");
    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
    d_solver.assertFormula(x.eqTerm(x));
    d_solver.checkSat();
    assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x}));
  }

  @Test void blockModelValues4() throws CVC5ApiException
  {
    d_solver.setOption("produce-models", "true");
    d_solver.setOption("block-models", "literals");
    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
    d_solver.assertFormula(x.eqTerm(x));
    assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x}));
  }

  @Test void blockModelValues5() throws CVC5ApiException
  {
    d_solver.setOption("produce-models", "true");
    d_solver.setOption("block-models", "literals");
    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
    d_solver.assertFormula(x.eqTerm(x));
    d_solver.checkSat();
    assertDoesNotThrow(() -> d_solver.blockModelValues(new Term[] {x}));
  }

  @Test void setInfo() throws CVC5ApiException
  {
    assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("cvc4-lagic", "QF_BV"));
    assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("cvc2-logic", "QF_BV"));
    assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("cvc4-logic", "asdf"));

    assertDoesNotThrow(() -> d_solver.setInfo("source", "asdf"));
    assertDoesNotThrow(() -> d_solver.setInfo("category", "asdf"));
    assertDoesNotThrow(() -> d_solver.setInfo("difficulty", "asdf"));
    assertDoesNotThrow(() -> d_solver.setInfo("filename", "asdf"));
    assertDoesNotThrow(() -> d_solver.setInfo("license", "asdf"));
    assertDoesNotThrow(() -> d_solver.setInfo("name", "asdf"));
    assertDoesNotThrow(() -> d_solver.setInfo("notes", "asdf"));

    assertDoesNotThrow(() -> d_solver.setInfo("smt-lib-version", "2"));
    assertDoesNotThrow(() -> d_solver.setInfo("smt-lib-version", "2.0"));
    assertDoesNotThrow(() -> d_solver.setInfo("smt-lib-version", "2.5"));
    assertDoesNotThrow(() -> d_solver.setInfo("smt-lib-version", "2.6"));
    assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("smt-lib-version", ".0"));

    assertDoesNotThrow(() -> d_solver.setInfo("status", "sat"));
    assertDoesNotThrow(() -> d_solver.setInfo("status", "unsat"));
    assertDoesNotThrow(() -> d_solver.setInfo("status", "unknown"));
    assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("status", "asdf"));
  }

  @Test void simplify() throws CVC5ApiException
  {
    assertThrows(CVC5ApiException.class, () -> d_solver.simplify(d_solver.getNullTerm()));

    Sort bvSort = d_solver.mkBitVectorSort(32);
    Sort uSort = d_solver.mkUninterpretedSort("u");
    Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
    Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
    DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
    cons.addSelector("head", d_solver.getIntegerSort());
    cons.addSelectorSelf("tail");
    consListSpec.addConstructor(cons);
    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
    consListSpec.addConstructor(nil);
    Sort consListSort = d_solver.mkDatatypeSort(consListSpec);

    Term x = d_solver.mkConst(bvSort, "x");
    assertDoesNotThrow(() -> d_solver.simplify(x));
    Term a = d_solver.mkConst(bvSort, "a");
    assertDoesNotThrow(() -> d_solver.simplify(a));
    Term b = d_solver.mkConst(bvSort, "b");
    assertDoesNotThrow(() -> d_solver.simplify(b));
    Term x_eq_x = d_solver.mkTerm(EQUAL, x, x);
    assertDoesNotThrow(() -> d_solver.simplify(x_eq_x));
    assertNotEquals(d_solver.mkTrue(), x_eq_x);
    assertEquals(d_solver.mkTrue(), d_solver.simplify(x_eq_x));
    Term x_eq_b = d_solver.mkTerm(EQUAL, x, b);
    assertDoesNotThrow(() -> d_solver.simplify(x_eq_b));
    assertNotEquals(d_solver.mkTrue(), x_eq_b);
    assertNotEquals(d_solver.mkTrue(), d_solver.simplify(x_eq_b));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.simplify(x));

    Term i1 = d_solver.mkConst(d_solver.getIntegerSort(), "i1");
    assertDoesNotThrow(() -> d_solver.simplify(i1));
    Term i2 = d_solver.mkTerm(MULT, i1, d_solver.mkInteger("23"));
    assertDoesNotThrow(() -> d_solver.simplify(i2));
    assertNotEquals(i1, i2);
    assertNotEquals(i1, d_solver.simplify(i2));
    Term i3 = d_solver.mkTerm(PLUS, i1, d_solver.mkInteger(0));
    assertDoesNotThrow(() -> d_solver.simplify(i3));
    assertNotEquals(i1, i3);
    assertEquals(i1, d_solver.simplify(i3));

    Datatype consList = consListSort.getDatatype();
    Term dt1 = d_solver.mkTerm(APPLY_CONSTRUCTOR,
        consList.getConstructorTerm("cons"),
        d_solver.mkInteger(0),
        d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
    assertDoesNotThrow(() -> d_solver.simplify(dt1));
    Term dt2 = d_solver.mkTerm(
        APPLY_SELECTOR, consList.getConstructor("cons").getSelectorTerm("head"), dt1);
    assertDoesNotThrow(() -> d_solver.simplify(dt2));

    Term b1 = d_solver.mkVar(bvSort, "b1");
    assertDoesNotThrow(() -> d_solver.simplify(b1));
    Term b2 = d_solver.mkVar(bvSort, "b1");
    assertDoesNotThrow(() -> d_solver.simplify(b2));
    Term b3 = d_solver.mkVar(uSort, "b3");
    assertDoesNotThrow(() -> d_solver.simplify(b3));
    Term v1 = d_solver.mkConst(bvSort, "v1");
    assertDoesNotThrow(() -> d_solver.simplify(v1));
    Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
    assertDoesNotThrow(() -> d_solver.simplify(v2));
    Term f1 = d_solver.mkConst(funSort1, "f1");
    assertDoesNotThrow(() -> d_solver.simplify(f1));
    Term f2 = d_solver.mkConst(funSort2, "f2");
    assertDoesNotThrow(() -> d_solver.simplify(f2));
    d_solver.defineFunsRec(new Term[] {f1, f2}, new Term[][] {{b1, b2}, {b3}}, new Term[] {v1, v2});
    assertDoesNotThrow(() -> d_solver.simplify(f1));
    assertDoesNotThrow(() -> d_solver.simplify(f2));
  }

  @Test void assertFormula()
  {
    assertDoesNotThrow(() -> d_solver.assertFormula(d_solver.mkTrue()));
    assertThrows(CVC5ApiException.class, () -> d_solver.assertFormula(d_solver.getNullTerm()));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.assertFormula(d_solver.mkTrue()));
  }

  @Test void checkEntailed()
  {
    d_solver.setOption("incremental", "false");
    assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue()));
    assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(d_solver.mkTrue()));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
  }

  @Test void checkEntailed1()
  {
    Sort boolSort = d_solver.getBooleanSort();
    Term x = d_solver.mkConst(boolSort, "x");
    Term y = d_solver.mkConst(boolSort, "y");
    Term z = d_solver.mkTerm(AND, x, y);
    d_solver.setOption("incremental", "true");
    assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue()));
    assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(d_solver.getNullTerm()));
    assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue()));
    assertDoesNotThrow(() -> d_solver.checkEntailed(z));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
  }

  @Test void checkEntailed2()
  {
    d_solver.setOption("incremental", "true");

    Sort uSort = d_solver.mkUninterpretedSort("u");
    Sort intSort = d_solver.getIntegerSort();
    Sort boolSort = d_solver.getBooleanSort();
    Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
    Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);

    Term n = d_solver.getNullTerm();
    // Constants
    Term x = d_solver.mkConst(uSort, "x");
    Term y = d_solver.mkConst(uSort, "y");
    // Functions
    Term f = d_solver.mkConst(uToIntSort, "f");
    Term p = d_solver.mkConst(intPredSort, "p");
    // Values
    Term zero = d_solver.mkInteger(0);
    Term one = d_solver.mkInteger(1);
    // Terms
    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
    Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
    Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
    Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
    // Assertions
    Term assertions = d_solver.mkTerm(AND,
        new Term[] {
            d_solver.mkTerm(LEQ, zero, f_x), // 0 <= f(x)
            d_solver.mkTerm(LEQ, zero, f_y), // 0 <= f(y)
            d_solver.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1
            p_0.notTerm(), // not p(0)
            p_f_y // p(f(y))
        });

    assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue()));
    d_solver.assertFormula(assertions);
    assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTerm(DISTINCT, x, y)));
    assertDoesNotThrow(()
                           -> d_solver.checkEntailed(
                               new Term[] {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)}));
    assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(n));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.checkEntailed(new Term[] {n, d_solver.mkTerm(DISTINCT, x, y)}));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
  }

  @Test void checkSat() throws CVC5ApiException
  {
    d_solver.setOption("incremental", "false");
    assertDoesNotThrow(() -> d_solver.checkSat());
    assertThrows(CVC5ApiException.class, () -> d_solver.checkSat());
  }

  @Test void checkSatAssuming() throws CVC5ApiException
  {
    d_solver.setOption("incremental", "false");
    assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTrue()));
    assertThrows(CVC5ApiException.class, () -> d_solver.checkSatAssuming(d_solver.mkTrue()));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
  }

  @Test void checkSatAssuming1() throws CVC5ApiException
  {
    Sort boolSort = d_solver.getBooleanSort();
    Term x = d_solver.mkConst(boolSort, "x");
    Term y = d_solver.mkConst(boolSort, "y");
    Term z = d_solver.mkTerm(AND, x, y);
    d_solver.setOption("incremental", "true");
    assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTrue()));
    assertThrows(CVC5ApiException.class, () -> d_solver.checkSatAssuming(d_solver.getNullTerm()));
    assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTrue()));
    assertDoesNotThrow(() -> d_solver.checkSatAssuming(z));
    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
  }

  @Test void checkSatAssuming2() throws CVC5ApiException
  {
    d_solver.setOption("incremental", "true");

    Sort uSort = d_solver.mkUninterpretedSort("u");
    Sort intSort = d_solver.getIntegerSort();
    Sort boolSort = d_solver.getBooleanSort();
    Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
    Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);

    Term n = d_solver.getNullTerm();
    // Constants
    Term x = d_solver.mkConst(uSort, "x");
    Term y = d_solver.mkConst(uSort, "y");
    // Functions
    Term f = d_solver.mkConst(uToIntSort, "f");
    Term p = d_solver.mkConst(intPredSort, "p");
    // Values
    Term zero = d_solver.mkInteger(0);
    Term one = d_solver.mkInteger(1);
    // Terms
    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
    Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
    Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
    Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
    // Assertions
    Term assertions = d_solver.mkTerm(AND,
        new Term[] {
            d_solver.mkTerm(LEQ, zero, f_x), // 0 <= f(x)
            d_solver.mkTerm(LEQ, zero, f_y), // 0 <= f(y)
            d_solver.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1
            p_0.notTerm(), // not p(0)
            p_f_y // p(f(y))
        });

    assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTrue()));
    d_solver.assertFormula(assertions);
    assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTerm(DISTINCT, x, y)));
    assertDoesNotThrow(()
                           -> d_solver.checkSatAssuming(
                               new Term[] {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)}));
    assertThrows(CVC5ApiException.class, () -> d_solver.checkSatAssuming(n));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.checkSatAssuming(new Term[] {n, d_solver.mkTerm(DISTINCT, x, y)}));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
  }

  @Test void setLogic() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_solver.setLogic("AUFLIRA"));
    assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AF_BV"));
    d_solver.assertFormula(d_solver.mkTrue());
    assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AUFLIRA"));
  }

  @Test void setOption() throws CVC5ApiException
  {
    assertDoesNotThrow(() -> d_solver.setOption("bv-sat-solver", "minisat"));
    assertThrows(CVC5ApiException.class, () -> d_solver.setOption("bv-sat-solver", "1"));
    d_solver.assertFormula(d_solver.mkTrue());
    assertThrows(CVC5ApiException.class, () -> d_solver.setOption("bv-sat-solver", "minisat"));
  }

  @Test void resetAssertions() throws CVC5ApiException
  {
    d_solver.setOption("incremental", "true");

    Sort bvSort = d_solver.mkBitVectorSort(4);
    Term one = d_solver.mkBitVector(4, 1);
    Term x = d_solver.mkConst(bvSort, "x");
    Term ule = d_solver.mkTerm(BITVECTOR_ULE, x, one);
    Term srem = d_solver.mkTerm(BITVECTOR_SREM, one, x);
    d_solver.push(4);
    Term slt = d_solver.mkTerm(BITVECTOR_SLT, srem, one);
    d_solver.resetAssertions();
    d_solver.checkSatAssuming(new Term[] {slt, ule});
  }

  @Test void mkSygusVar() throws CVC5ApiException
  {
    Sort boolSort = d_solver.getBooleanSort();
    Sort intSort = d_solver.getIntegerSort();
    Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);

    assertDoesNotThrow(() -> d_solver.mkSygusVar(boolSort));
    assertDoesNotThrow(() -> d_solver.mkSygusVar(funSort));
    assertDoesNotThrow(() -> d_solver.mkSygusVar(boolSort, ("b")));
    assertDoesNotThrow(() -> d_solver.mkSygusVar(funSort, ""));

    assertThrows(CVC5ApiException.class, () -> d_solver.mkSygusVar(d_solver.getNullSort()));
    assertThrows(CVC5ApiException.class, () -> d_solver.mkSygusVar(d_solver.getNullSort(), "a"));

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

  @Test void mkSygusGrammar() throws CVC5ApiException
  {
    Term nullTerm = d_solver.getNullTerm();
    Term boolTerm = d_solver.mkBoolean(true);
    Term boolVar = d_solver.mkVar(d_solver.getBooleanSort());
    Term intVar = d_solver.mkVar(d_solver.getIntegerSort());

    assertDoesNotThrow(() -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {intVar}));
    assertDoesNotThrow(() -> d_solver.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar}));

    assertThrows(
        CVC5ApiException.class, () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {}));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {nullTerm}));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {boolTerm}));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.mkSygusGrammar(new Term[] {boolTerm}, new Term[] {intVar}));

    Solver slv = new Solver();
    Term boolVar2 = slv.mkVar(slv.getBooleanSort());
    Term intVar2 = slv.mkVar(slv.getIntegerSort());
    assertDoesNotThrow(() -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar2}));

    assertThrows(CVC5ApiException.class,
        () -> slv.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar2}));
    assertThrows(CVC5ApiException.class,
        () -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar}));
  }

  @Test void synthFun() throws CVC5ApiException
  {
    Sort nullSort = d_solver.getNullSort();
    Sort bool = d_solver.getBooleanSort();
    Sort integer = d_solver.getIntegerSort();

    Term nullTerm = d_solver.getNullTerm();
    Term x = d_solver.mkVar(bool);

    Term start1 = d_solver.mkVar(bool);
    Term start2 = d_solver.mkVar(integer);

    Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start1});
    g1.addRule(start1, d_solver.mkBoolean(false));

    Grammar g2 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start2});
    g2.addRule(start2, d_solver.mkInteger(0));

    assertDoesNotThrow(() -> d_solver.synthFun("", new Term[] {}, bool));
    assertDoesNotThrow(() -> d_solver.synthFun("f1", new Term[] {x}, bool));
    assertDoesNotThrow(() -> d_solver.synthFun("f2", new Term[] {x}, bool, g1));

    assertThrows(
        CVC5ApiException.class, () -> d_solver.synthFun("f3", new Term[] {nullTerm}, bool));
    assertThrows(CVC5ApiException.class, () -> d_solver.synthFun("f4", new Term[] {}, nullSort));
    assertThrows(CVC5ApiException.class, () -> d_solver.synthFun("f6", new Term[] {x}, bool, g2));

    Solver slv = new Solver();
    Term x2 = slv.mkVar(slv.getBooleanSort());
    assertDoesNotThrow(() -> slv.synthFun("f1", new Term[] {x2}, slv.getBooleanSort()));

    assertThrows(
        CVC5ApiException.class, () -> slv.synthFun("", new Term[] {}, d_solver.getBooleanSort()));
    assertThrows(CVC5ApiException.class,
        () -> slv.synthFun("f1", new Term[] {x}, d_solver.getBooleanSort()));
  }

  @Test void synthInv() throws CVC5ApiException
  {
    Sort bool = d_solver.getBooleanSort();
    Sort integer = d_solver.getIntegerSort();

    Term nullTerm = d_solver.getNullTerm();
    Term x = d_solver.mkVar(bool);

    Term start1 = d_solver.mkVar(bool);
    Term start2 = d_solver.mkVar(integer);

    Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start1});
    g1.addRule(start1, d_solver.mkBoolean(false));

    Grammar g2 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start2});
    g2.addRule(start2, d_solver.mkInteger(0));

    assertDoesNotThrow(() -> d_solver.synthInv("", new Term[] {}));
    assertDoesNotThrow(() -> d_solver.synthInv("i1", new Term[] {x}));
    assertDoesNotThrow(() -> d_solver.synthInv("i2", new Term[] {x}, g1));

    assertThrows(CVC5ApiException.class, () -> d_solver.synthInv("i3", new Term[] {nullTerm}));
    assertThrows(CVC5ApiException.class, () -> d_solver.synthInv("i4", new Term[] {x}, g2));
  }

  @Test void addSygusConstraint() throws CVC5ApiException
  {
    Term nullTerm = d_solver.getNullTerm();
    Term boolTerm = d_solver.mkBoolean(true);
    Term intTerm = d_solver.mkInteger(1);

    assertDoesNotThrow(() -> d_solver.addSygusConstraint(boolTerm));
    assertThrows(CVC5ApiException.class, () -> d_solver.addSygusConstraint(nullTerm));
    assertThrows(CVC5ApiException.class, () -> d_solver.addSygusConstraint(intTerm));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.addSygusConstraint(boolTerm));
  }

  @Test void addSygusInvConstraint() throws CVC5ApiException
  {
    Sort bool = d_solver.getBooleanSort();
    Sort real = d_solver.getRealSort();

    Term nullTerm = d_solver.getNullTerm();
    Term intTerm = d_solver.mkInteger(1);

    Term inv = d_solver.declareFun("inv", new Sort[] {real}, bool);
    Term pre = d_solver.declareFun("pre", new Sort[] {real}, bool);
    Term trans = d_solver.declareFun("trans", new Sort[] {real, real}, bool);
    Term post = d_solver.declareFun("post", new Sort[] {real}, bool);

    Term inv1 = d_solver.declareFun("inv1", new Sort[] {real}, real);

    Term trans1 = d_solver.declareFun("trans1", new Sort[] {bool, real}, bool);
    Term trans2 = d_solver.declareFun("trans2", new Sort[] {real, bool}, bool);
    Term trans3 = d_solver.declareFun("trans3", new Sort[] {real, real}, real);

    assertDoesNotThrow(() -> d_solver.addSygusInvConstraint(inv, pre, trans, post));

    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(nullTerm, pre, trans, post));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, nullTerm, trans, post));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, nullTerm, post));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans, nullTerm));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(intTerm, pre, trans, post));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv1, pre, trans, post));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, trans, trans, post));
    assertThrows(CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, pre, post));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans1, post));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans2, post));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans3, post));
    assertThrows(
        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans, trans));

    Solver slv = new Solver();
    Sort boolean2 = slv.getBooleanSort();
    Sort real2 = slv.getRealSort();
    Term inv22 = slv.declareFun("inv", new Sort[] {real2}, boolean2);
    Term pre22 = slv.declareFun("pre", new Sort[] {real2}, boolean2);
    Term trans22 = slv.declareFun("trans", new Sort[] {real2, real2}, boolean2);
    Term post22 = slv.declareFun("post", new Sort[] {real2}, boolean2);
    assertDoesNotThrow(() -> slv.addSygusInvConstraint(inv22, pre22, trans22, post22));

    assertThrows(
        CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv, pre22, trans22, post22));
    assertThrows(
        CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre, trans22, post22));
    assertThrows(
        CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans, post22));
    assertThrows(
        CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans22, post));
  }

  @Test void getSynthSolution() throws CVC5ApiException
  {
    d_solver.setOption("lang", "sygus2");
    d_solver.setOption("incremental", "false");

    Term nullTerm = d_solver.getNullTerm();
    Term x = d_solver.mkBoolean(false);
    Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());

    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolution(f));

    d_solver.checkSynth();

    assertDoesNotThrow(() -> d_solver.getSynthSolution(f));
    assertDoesNotThrow(() -> d_solver.getSynthSolution(f));

    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolution(nullTerm));
    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolution(x));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.getSynthSolution(f));
  }

  @Test void getSynthSolutions() throws CVC5ApiException
  {
    d_solver.setOption("lang", "sygus2");
    d_solver.setOption("incremental", "false");

    Term nullTerm = d_solver.getNullTerm();
    Term x = d_solver.mkBoolean(false);
    Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());

    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolutions(new Term[] {}));
    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolutions(new Term[] {f}));

    d_solver.checkSynth();

    assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
    assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f, f}));

    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolutions(new Term[] {}));
    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolutions(new Term[] {nullTerm}));
    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolutions(new Term[] {x}));

    Solver slv = new Solver();
    assertThrows(CVC5ApiException.class, () -> slv.getSynthSolutions(new Term[] {x}));
  }

  @Test void tupleProject() throws CVC5ApiException
  {
    Sort[] sorts = new Sort[] {d_solver.getBooleanSort(),
        d_solver.getIntegerSort(),
        d_solver.getStringSort(),
        d_solver.mkSetSort(d_solver.getStringSort())};
    Term[] elements = new Term[] {d_solver.mkBoolean(true),
        d_solver.mkInteger(3),
        d_solver.mkString("C"),
        d_solver.mkTerm(SINGLETON, d_solver.mkString("Z"))};

    Term tuple = d_solver.mkTuple(sorts, elements);

    int[] indices1 = new int[] {};
    int[] indices2 = new int[] {0};
    int[] indices3 = new int[] {0, 1};
    int[] indices4 = new int[] {0, 0, 2, 2, 3, 3, 0};
    int[] indices5 = new int[] {4};
    int[] indices6 = new int[] {0, 4};

    assertDoesNotThrow(() -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices1), tuple));
    assertDoesNotThrow(() -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices2), tuple));
    assertDoesNotThrow(() -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices3), tuple));
    assertDoesNotThrow(() -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices4), tuple));

    assertThrows(CVC5ApiException.class,
        () -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices5), tuple));
    assertThrows(CVC5ApiException.class,
        () -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices6), tuple));

    int[] indices = new int[] {0, 3, 2, 0, 1, 2};

    Op op = d_solver.mkOp(TUPLE_PROJECT, indices);
    Term projection = d_solver.mkTerm(op, tuple);

    Datatype datatype = tuple.getSort().getDatatype();
    DatatypeConstructor constructor = datatype.getConstructor(0);

    for (int i = 0; i < indices.length; i++)
    {
      Term selectorTerm = constructor.getSelector(indices[i]).getSelectorTerm();
      Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, selectorTerm, tuple);
      Term simplifiedTerm = d_solver.simplify(selectedTerm);
      assertEquals(elements[indices[i]], simplifiedTerm);
    }

    assertEquals("((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (singleton "
            + "\"Z\")))",
        projection.toString());
  }
}