cvc5/test/unit/api/python/test_solver.py

###############################################################################
# Top contributors (to current version):
#   Aina Niemetz, Ying Sheng, Yoni Zohar
#
# This file is part of the cvc5 project.
#
# Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
# in the top-level source directory and their institutional affiliations.
# All rights reserved.  See the file COPYING in the top-level source
# directory for licensing information.
# #############################################################################
##

import pytest
import cvc5
import sys
from math import isnan

from cvc5 import Kind, OptionCategory, SortKind, TermManager, Solver, Plugin
from cvc5 import RoundingMode
from cvc5 import BlockModelsMode, LearnedLitType, FindSynthTarget
from cvc5 import ProofComponent, ProofFormat


@pytest.fixture
def tm():
    return TermManager()
@pytest.fixture
def solver(tm):
    return Solver(tm)


def test_recoverable_exception(tm, solver):
    solver.setOption("produce-models", "true")
    x = tm.mkConst(solver.getBooleanSort(), "x")
    solver.assertFormula(x.eqTerm(x).notTerm())
    with pytest.raises(RuntimeError):
        c = solver.getValue(x)


def test_declare_fun_fresh(tm, solver):
    boolSort = tm.getBooleanSort()
    intSort = tm.getIntegerSort()
    t1 = solver.declareFun("b", [], boolSort, True)
    t2 = solver.declareFun("b", [], boolSort, False)
    t3 = solver.declareFun("b", [], boolSort, False)
    assert not t1 == t2
    assert not t1 == t3
    assert t2 == t3
    t4 = solver.declareFun("c", [], boolSort, False)
    assert not t2 == t4
    t5 = solver.declareFun("b", [], intSort, False)
    assert not t2 == t5

    ttm = TermManager()
    slv = Solver(ttm)
    with pytest.raises(RuntimeError):
        slv.declareFun("b", [], intSort, False)


def test_declare_fun(tm, solver):
    bvSort = tm.mkBitVectorSort(32)
    funSort = tm.mkFunctionSort(tm.mkUninterpretedSort("u"),\
                                    tm.getIntegerSort())
    solver.declareFun("f1", [], bvSort)
    solver.declareFun("f3", [bvSort, tm.getIntegerSort()], bvSort)
    with pytest.raises(RuntimeError):
        solver.declareFun("f2", [], funSort)
    # functions as arguments is allowed
    solver.declareFun("f4", [bvSort, funSort], bvSort)
    with pytest.raises(RuntimeError):
        solver.declareFun("f5", [bvSort, bvSort], funSort)
    slv = Solver(tm)
    slv.declareFun("f1", [], bvSort)

    ttm = TermManager()
    slv = Solver(ttm)
    with pytest.raises(RuntimeError):
        slv.declareFun("f1", [], bvSort)


def decalre_datatype(tm, solver):
    lin = tm.mkDatatypeConstructorDecl("lin")
    solver.declareDatatype("", [lin])

    nil = tm.mkDatatypeConstructorDecl("nil")
    solver.declareDatatype("a", [nil])

    cons = tm.mkDatatypeConstructorDecl("cons")
    nil2 = tm.mkDatatypeConstructorDecl("nil")
    solver.declareDatatype("b", [cons, nil2])

    cons2 = tm.mkDatatypeConstructorDecl("cons")
    nil3 = tm.mkDatatypeConstructorDecl("nil")
    solver.declareDatatype("", [cons2, nil3])

    # must have at least one constructor
    with pytest.raises(RuntimeError):
        solver.declareDatatype("c", [])
    # constructors may not be reused
    ctor1 = tm.mkDatatypeConstructorDecl("_x21")
    ctor2 = tm.mkDatatypeConstructorDecl("_x31")
    s3 = solver.declareDatatype("_x17", [ctor1, ctor2])
    with pytest.raises(RuntimeError):
        solver.declareDatatype("_x86", [ctor1, ctor2])

    ttm = TermManager()
    slv = Solver(ttm)
    with pytest.raises(RuntimeError):
        nnil = tm.mkDatatypeConstructorDecl("nil")
        slv.declareDatatype("a", [nnil])


def test_declare_sort(solver):
    solver.declareSort("s", 0)
    solver.declareSort("s", 2)
    solver.declareSort("", 2)


def test_declare_sort_fresh(solver):
    t1 = solver.declareSort("b", 0, True)
    t2 = solver.declareSort("b", 0, False)
    t3 = solver.declareSort("b", 0, False)
    assert t1!=t2
    assert t1!=t3
    assert t2==t3
    t4 = solver.declareSort("c", 0, False)
    assert t2!=t4
    t5 = solver.declareSort("b", 1, False)
    assert t2!=t5


def test_define_fun(tm, solver):
    bvSort = tm.mkBitVectorSort(32)
    funSort = tm.mkFunctionSort(tm.mkUninterpretedSort("u"),
                                    tm.getIntegerSort())
    b1 = tm.mkVar(bvSort, "b1")
    b2 = tm.mkVar(tm.getIntegerSort(), "b2")
    b3 = tm.mkVar(funSort, "b3")
    v1 = tm.mkConst(bvSort, "v1")
    v2 = tm.mkConst(funSort, "v2")
    solver.defineFun("f", [], bvSort, v1)
    solver.defineFun("ff", [b1, b2], bvSort, v1)
    with pytest.raises(RuntimeError):
        solver.defineFun("ff", [v1, b2], bvSort, v1)
    with pytest.raises(RuntimeError):
        solver.defineFun("fff", [b1], bvSort, v2)
    with pytest.raises(RuntimeError):
        solver.defineFun("ffff", [b1], funSort, v2)
    # b3 has function sort, which is allowed as an argument
    solver.defineFun("fffff", [b1, b3], bvSort, v1)

    ttm = TermManager()
    slv = Solver(ttm)
    bvSort2 = ttm.mkBitVectorSort(32)
    v12 = ttm.mkConst(bvSort2, "v1")
    b12 = ttm.mkVar(bvSort2, "b1")
    b22 = ttm.mkVar(ttm.getIntegerSort(), "b2")
    with pytest.raises(RuntimeError):
        slv.defineFun("f", [], bvSort, v12)
    with pytest.raises(RuntimeError):
        slv.defineFun("f", [], bvSort2, v1)
    with pytest.raises(RuntimeError):
        slv.defineFun("ff", [b1, b22], bvSort2, v12)
    with pytest.raises(RuntimeError):
        slv.defineFun("ff", [b12, b2], bvSort2, v12)
    with pytest.raises(RuntimeError):
        slv.defineFun("ff", [b12, b22], bvSort, v12)
    with pytest.raises(RuntimeError):
        slv.defineFun("ff", [b12, b22], bvSort2, v1)


def test_define_fun_global(tm, solver):
    bSort = solver.getBooleanSort()

    bTrue = tm.mkBoolean(True)
    # (define-fun f () Bool true)
    f = solver.defineFun("f", [], bSort, bTrue, True)
    b = tm.mkVar(bSort, "b")
    # (define-fun g (b Bool) Bool b)
    g = solver.defineFun("g", [b], bSort, b, True)

    # (assert (or (not f) (not (g true))))
    solver.assertFormula(
        tm.mkTerm(Kind.OR, f.notTerm(),
                      tm.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
    assert solver.checkSat().isUnsat()
    solver.resetAssertions()
    # (assert (or (not f) (not (g true))))
    solver.assertFormula(
        tm.mkTerm(Kind.OR, f.notTerm(),
                      tm.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
    assert solver.checkSat().isUnsat()

    ttm = TermManager()
    slv = Solver(ttm)
    with pytest.raises(RuntimeError):
        slv.defineFun("f", [], bSort, bTrue, True)


def test_define_fun_rec(tm, solver):
    bvSort = tm.mkBitVectorSort(32)
    funSort1 = tm.mkFunctionSort([bvSort, bvSort], bvSort)
    funSort2 = tm.mkFunctionSort(
            tm.mkUninterpretedSort("u"), tm.getIntegerSort())
    b1 = tm.mkVar(bvSort, "b1")
    b11 = tm.mkVar(bvSort, "b1")
    b2 = tm.mkVar(tm.getIntegerSort(), "b2")
    b3 = tm.mkVar(funSort2, "b3")
    v1 = tm.mkConst(bvSort, "v1")
    v2 = tm.mkConst(tm.getIntegerSort(), "v2")
    v3 = tm.mkConst(funSort2, "v3")
    f1 = tm.mkConst(funSort1, "f1")
    f2 = tm.mkConst(funSort2, "f2")
    f3 = tm.mkConst(bvSort, "f3")
    solver.defineFunRec("f", [], bvSort, v1)
    solver.defineFunRec("ff", [b1, b2], bvSort, v1)
    solver.defineFunRec(f1, [b1, b11], v1)
    with pytest.raises(RuntimeError):
        solver.defineFunRec("fff", [b1], bvSort, v3)
    with pytest.raises(RuntimeError):
        solver.defineFunRec("ff", [b1, v2], bvSort, v1)
    with pytest.raises(RuntimeError):
        solver.defineFunRec("ffff", [b1], funSort2, v3)
    # b3 has function sort, which is allowed as an argument
    solver.defineFunRec("fffff", [b1, b3], bvSort, v1)
    with pytest.raises(RuntimeError):
        solver.defineFunRec(f1, [b1], v1)
    with pytest.raises(RuntimeError):
        solver.defineFunRec(f1, [b1, b11], v2)
    with pytest.raises(RuntimeError):
        solver.defineFunRec(f1, [b1, b11], v3)
    with pytest.raises(RuntimeError):
        solver.defineFunRec(f2, [b1], v2)
    with pytest.raises(RuntimeError):
        solver.defineFunRec(f3, [b1], v1)

    ttm = TermManager()
    slv = Solver(ttm)
    bvSort2 = ttm.mkBitVectorSort(32)
    v12 = ttm.mkConst(bvSort2, "v1")
    b12 = ttm.mkVar(bvSort2, "b1")
    b22 = ttm.mkVar(ttm.getIntegerSort(), "b2")
    slv.defineFunRec("f", [], bvSort2, v12)
    slv.defineFunRec("ff", [b12, b22], bvSort2, v12)
    with pytest.raises(RuntimeError):
        slv.defineFunRec("f", [], bvSort, v12)
    with pytest.raises(RuntimeError):
        slv.defineFunRec("f", [], bvSort2, v1)
    with pytest.raises(RuntimeError):
        slv.defineFunRec("ff", [b1, b22], bvSort2, v12)
    with pytest.raises(RuntimeError):
        slv.defineFunRec("ff", [b12, b2], bvSort2, v12)
    with pytest.raises(RuntimeError):
        slv.defineFunRec("ff", [b12, b22], bvSort, v12)
    with pytest.raises(RuntimeError):
        slv.defineFunRec("ff", [b12, b22], bvSort2, v1)


def test_define_fun_rec_wrong_logic(tm, solver):
    solver.setLogic("QF_BV")
    bvSort = tm.mkBitVectorSort(32)
    funSort = tm.mkFunctionSort([bvSort, bvSort], bvSort)
    b = tm.mkVar(bvSort, "b")
    v = tm.mkConst(bvSort, "v")
    f = tm.mkConst(funSort, "f")
    with pytest.raises(RuntimeError):
        solver.defineFunRec("f", [], bvSort, v)
    with pytest.raises(RuntimeError):
        solver.defineFunRec(f, [b, b], v)


def test_define_fun_rec_global(tm, solver):
    bSort = tm.getBooleanSort()
    fSort = tm.mkFunctionSort([bSort], bSort)

    solver.push()
    bTrue = tm.mkBoolean(True)
    # (define-fun f () Bool true)
    f = solver.defineFunRec("f", [], bSort, bTrue, True)
    b = tm.mkVar(bSort, "b")
    gSym = tm.mkConst(fSort, "g")
    # (define-fun g (b Bool) Bool b)
    g = solver.defineFunRec(gSym, [b], b, glbl=True)

    # (assert (or (not f) (not (g true))))
    solver.assertFormula(tm.mkTerm(
        Kind.OR, f.notTerm(), tm.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
    assert solver.checkSat().isUnsat()
    solver.pop()
    # (assert (or (not f) (not (g true))))
    solver.assertFormula(tm.mkTerm(
        Kind.OR, f.notTerm(), tm.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
    assert solver.checkSat().isUnsat()

    ttm = TermManager()
    slv = Solver(ttm)
    bb = ttm.mkVar(ttm.getBooleanSort(), "b")
    with pytest.raises(RuntimeError):
        slv.defineFunRec(
          tm.mkConst(
              tm.mkFunctionSort({tm.getBooleanSort()}, tm.getBooleanSort()),
              "g"),
          [bb],
          bb,
          True)
    with pytest.raises(RuntimeError):
        slv.defineFunRec(
          ttm.mkConst(
            ttm.mkFunctionSort({ttm.getBooleanSort()}, ttm.getBooleanSort()),
            "g"),
          [b],
          b,
          True)


def test_define_funs_rec(tm, solver):
    uSort = tm.mkUninterpretedSort("u")
    bvSort = tm.mkBitVectorSort(32)
    funSort1 = tm.mkFunctionSort([bvSort, bvSort], bvSort)
    funSort2 = tm.mkFunctionSort([uSort], tm.getIntegerSort())
    b1 = tm.mkVar(bvSort, "b1")
    b11 = tm.mkVar(bvSort, "b1")
    b2 = tm.mkVar(tm.getIntegerSort(), "b2")
    b3 = tm.mkVar(funSort2, "b3")
    b4 = tm.mkVar(uSort, "b4")
    v1 = tm.mkConst(bvSort, "v1")
    v2 = tm.mkConst(tm.getIntegerSort(), "v2")
    v3 = tm.mkConst(funSort2, "v3")
    v4 = tm.mkConst(uSort, "v4")
    f1 = tm.mkConst(funSort1, "f1")
    f2 = tm.mkConst(funSort2, "f2")
    f3 = tm.mkConst(bvSort, "f3")
    solver.defineFunsRec([f1, f2], [[b1, b11], [b4]], [v1, v2])
    with pytest.raises(RuntimeError):
      solver.defineFunsRec([f1, f2], [[v1, b11], [b4]], [v1, v2])
    with pytest.raises(RuntimeError):
      solver.defineFunsRec([f1, f3], [[b1, b11], [b4]], [v1, v2])
    with pytest.raises(RuntimeError):
      solver.defineFunsRec([f1, f2], [[b1], [b4]], [v1, v2])
    with pytest.raises(RuntimeError):
      solver.defineFunsRec([f1, f2], [[b1, b2], [b4]], [v1, v2])
    with pytest.raises(RuntimeError):
      solver.defineFunsRec([f1, f2], [[b1, b11], [b4]], [v1, v4])

    ttm = TermManager()
    slv = Solver(ttm)
    bb = ttm.mkVar(ttm.getBooleanSort(), "b")
    uSort2 = ttm.mkUninterpretedSort("u")
    bvSort2 = ttm.mkBitVectorSort(32)
    funSort12 = ttm.mkFunctionSort([bvSort2, bvSort2], bvSort2)
    funSort22 = ttm.mkFunctionSort([uSort2], ttm.getIntegerSort())
    b12 = ttm.mkVar(bvSort2, "b1")
    b112 = ttm.mkVar(bvSort2, "b1")
    b42 = ttm.mkVar(uSort2, "b4")
    v12 = ttm.mkConst(bvSort2, "v1")
    v22 = ttm.mkConst(ttm.getIntegerSort(), "v2")
    f12 = ttm.mkConst(funSort12, "f1")
    f22 = ttm.mkConst(funSort22, "f2")
    slv.defineFunsRec([f12, f22], [[b12, b112], [b42]], [v12, v22])
    with pytest.raises(RuntimeError):
        slv.defineFunsRec([f1, f22], [[b12, b112], [b42]], [v12, v22])
    with pytest.raises(RuntimeError):
        slv.defineFunsRec([f12, f22], [[b1, b112], [b42]], [v12, v22])
    with pytest.raises(RuntimeError):
        slv.defineFunsRec([f12, f22], [[b12, b11], [b42]], [v12, v22])
    with pytest.raises(RuntimeError):
        slv.defineFunsRec([f12, f22], [[b12, b112], [b42]], [v1, v22])
    with pytest.raises(RuntimeError):
        slv.defineFunsRec([f12, f22], [[b12, b112], [b42]], [v12, v2])
    with pytest.raises(RuntimeError):
      slv.defineFunsRec([f12, f2], [[b12, b112], [b42]], [v12, v22])
    with pytest.raises(RuntimeError):
      slv.defineFunsRec([f12, f22], [[b12, b112], [b4]], [v12, v22])


def test_define_funs_rec_wrong_logic(tm, solver):
  solver.setLogic("QF_BV")
  uSort = tm.mkUninterpretedSort("u")
  bvSort = tm.mkBitVectorSort(32)
  funSort1 = tm.mkFunctionSort([bvSort, bvSort], bvSort)
  funSort2 = tm.mkFunctionSort([uSort], tm.getIntegerSort())
  b = tm.mkVar(bvSort, "b")
  u = tm.mkVar(uSort, "u")
  v1 = tm.mkConst(bvSort, "v1")
  v2 = tm.mkConst(tm.getIntegerSort(), "v2")
  f1 = tm.mkConst(funSort1, "f1")
  f2 = tm.mkConst(funSort2, "f2")
  with pytest.raises(RuntimeError):
    solver.defineFunsRec([f1, f2], [[b, b], [u]], [v1, v2])


def test_define_funs_rec_global(tm, solver):
  bSort = tm.getBooleanSort()
  fSort = tm.mkFunctionSort([bSort], bSort)

  solver.push()
  bTrue = tm.mkBoolean(True)
  b = tm.mkVar(bSort, "b")
  gSym = tm.mkConst(fSort, "g")
  # (define-funs-rec ((g ((b Bool)) Bool)) (b))
  solver.defineFunsRec([gSym], [[b]], [b], True)

  # (assert (not (g true)))
  solver.assertFormula(tm.mkTerm(Kind.APPLY_UF, gSym, bTrue).notTerm())
  assert solver.checkSat().isUnsat()
  solver.pop()
  # (assert (not (g true)))
  solver.assertFormula(tm.mkTerm(Kind.APPLY_UF, gSym, bTrue).notTerm())
  assert solver.checkSat().isUnsat()


def test_get_assertions(tm, solver):
    a = tm.mkConst(tm.getBooleanSort(), 'a')
    b = tm.mkConst(tm.getBooleanSort(), 'b')
    solver.assertFormula(a)
    solver.assertFormula(b)
    asserts = [a,b]
    assert solver.getAssertions() == asserts


def test_get_info(solver):
    solver.getInfo("name")
    with pytest.raises(RuntimeError):
        solver.getInfo("asdf")


def test_get_option(solver):
    solver.setOption("incremental", "true")
    assert solver.getOption("incremental") == "true"
    with pytest.raises(RuntimeError):
        solver.getOption("asdf")


def test_get_option_names(solver):
    opts = solver.getOptionNames()
    assert len(opts) > 100
    assert "verbose" in opts
    assert "foobar" not in opts


def test_get_option_info(solver):
    with pytest.raises(RuntimeError):
        solver.getOptionInfo("asdf-invalid")

    info = solver.getOptionInfo("verbose")
    assert info['name'] == "verbose"
    assert info['category'] == OptionCategory.COMMON
    assert info['aliases'] == []
    assert not info['setByUser']
    assert info['type'] is None

    info = solver.getOptionInfo("print-success")
    assert info['name'] == "print-success"
    assert info['category'] == OptionCategory.COMMON
    assert info['aliases'] == []
    assert not info['setByUser']
    assert info['type'] is bool
    assert info['current'] == False
    assert info['default'] == False

    info = solver.getOptionInfo("verbosity")
    assert info['name'] == "verbosity"
    assert info['category'] == OptionCategory.COMMON
    assert info['aliases'] == []
    assert not info['setByUser']
    assert info['type'] is int
    assert info['current'] == 0
    assert info['default'] == 0
    assert info['minimum'] is None and info['maximum'] is None

    info = solver.getOptionInfo("rlimit")
    assert info['name'] == "rlimit"
    assert info['category'] == OptionCategory.COMMON
    assert info['aliases'] == []
    assert not info['setByUser']
    assert info['type'] is int
    assert info['current'] == 0
    assert info['default'] == 0
    assert info['minimum'] is None and info['maximum'] is None

    info = solver.getOptionInfo("random-freq")
    assert info['name'] == "random-freq"
    assert info['category'] == OptionCategory.EXPERT
    assert info['aliases'] == ["random-frequency"]
    assert not info['setByUser']
    assert info['type'] is float
    assert info['current'] == 0.0
    assert info['default'] == 0.0
    assert info['minimum'] == 0.0 and info['maximum'] == 1.0

    info = solver.getOptionInfo("force-logic")
    assert info['name'] == "force-logic"
    assert info['category'] == OptionCategory.COMMON
    assert info['aliases'] == []
    assert not info['setByUser']
    assert info['type'] is str
    assert info['current'] == ""
    assert info['default'] == ""

    info = solver.getOptionInfo("simplification")
    assert info['name'] == "simplification"
    assert info['category'] == OptionCategory.REGULAR
    assert info['aliases'] == ["simplification-mode"]
    assert not info['setByUser']
    assert info['type'] == 'mode'
    assert info['current'] == 'batch'
    assert info['default'] == 'batch'
    assert info['modes'] == ['batch', 'none']


def test_get_unsat_assumptions1(solver):
    solver.setOption("incremental", "false")
    solver.checkSatAssuming(solver.mkFalse())
    with pytest.raises(RuntimeError):
        solver.getUnsatAssumptions()


def test_get_unsat_assumptions2(solver):
    solver.setOption("incremental", "true")
    solver.setOption("produce-unsat-assumptions", "false")
    solver.checkSatAssuming(solver.mkFalse())
    with pytest.raises(RuntimeError):
        solver.getUnsatAssumptions()


def test_get_unsat_assumptions3(solver):
    solver.setOption("incremental", "true")
    solver.setOption("produce-unsat-assumptions", "true")
    solver.checkSatAssuming(solver.mkFalse())
    solver.getUnsatAssumptions()
    solver.checkSatAssuming(solver.mkTrue())
    with pytest.raises(RuntimeError):
        solver.getUnsatAssumptions()


def test_get_unsat_core1(solver):
    solver.setOption("incremental", "false")
    solver.assertFormula(solver.mkFalse())
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getUnsatCore()


def test_get_unsat_core2(solver):
    solver.setOption("incremental", "false")
    solver.setOption("produce-unsat-cores", "false")
    solver.assertFormula(solver.mkFalse())
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getUnsatCore()


def test_get_unsat_core_and_proof(tm, solver):
    solver.setOption("incremental", "true")
    solver.setOption("produce-unsat-cores", "true")
    solver.setOption("produce-proofs", "true");

    uSort = solver.mkUninterpretedSort("u")
    intSort = tm.getIntegerSort()
    boolSort = solver.getBooleanSort()
    uToIntSort = solver.mkFunctionSort(uSort, intSort)
    intPredSort = solver.mkFunctionSort(intSort, boolSort)

    x = solver.mkConst(uSort, "x")
    y = solver.mkConst(uSort, "y")
    f = solver.mkConst(uToIntSort, "f")
    p = solver.mkConst(intPredSort, "p")
    zero = solver.mkInteger(0)
    one = solver.mkInteger(1)
    f_x = solver.mkTerm(Kind.APPLY_UF, f, x)
    f_y = solver.mkTerm(Kind.APPLY_UF, f, y)
    summ = solver.mkTerm(Kind.ADD, f_x, f_y)
    p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero)
    p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y)
    solver.assertFormula(solver.mkTerm(Kind.GT, zero, f_x))
    solver.assertFormula(solver.mkTerm(Kind.GT, zero, f_y))
    solver.assertFormula(solver.mkTerm(Kind.GT, summ, one))
    solver.assertFormula(p_0)
    solver.assertFormula(p_f_y.notTerm())
    assert solver.checkSat().isUnsat()

    unsat_core = solver.getUnsatCore()

    solver.getProof()
    solver.getProof(ProofComponent.SAT)

    solver.resetAssertions()
    for t in unsat_core:
        solver.assertFormula(t)
    res = solver.checkSat()
    assert res.isUnsat()
    solver.getProof()


def test_get_unsat_core_and_proof_to_string(tm, solver):
    solver.setOption("produce-proofs", "true")

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

    x = tm.mkConst(uSort, "x")
    y = tm.mkConst(uSort, "y")
    f = tm.mkConst(uToIntSort, "f")
    p = tm.mkConst(intPredSort, "p")
    zero = tm.mkInteger(0)
    one = tm.mkInteger(1)
    f_x = tm.mkTerm(Kind.APPLY_UF, f, x)
    f_y = tm.mkTerm(Kind.APPLY_UF, f, y)
    summ = tm.mkTerm(Kind.ADD, f_x, f_y)
    p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero)
    p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y)
    solver.assertFormula(tm.mkTerm(Kind.GT, zero, f_x))
    solver.assertFormula(tm.mkTerm(Kind.GT, zero, f_y))
    solver.assertFormula(tm.mkTerm(Kind.GT, summ, one))
    solver.assertFormula(p_0)
    solver.assertFormula(p_f_y.notTerm())
    assert solver.checkSat().isUnsat()

    proofs = solver.getProof()
    assert len(proofs) > 0
    printedProof = solver.proofToString(proofs[0])
    assert len(printedProof) > 0
    printedProof = solver.proofToString(proofs[0], ProofFormat.ALETHE)
    assert len(printedProof) > 0

    proofs = solver.getProof(ProofComponent.SAT)
    printedProof = solver.proofToString(proofs[0], ProofFormat.NONE)
    assert len(printedProof) > 0


def test_proof_to_string_assertion_names(tm, solver):
    solver.setOption("produce-proofs", "true")
    uSort = tm.mkUninterpretedSort("u")
    x = tm.mkConst(uSort, "x")
    y = tm.mkConst(uSort, "y")

    x_eq_y = tm.mkTerm(Kind.EQUAL, x, y)
    not_x_eq_y = tm.mkTerm(Kind.NOT, x_eq_y)

    names = {x_eq_y: "as1", not_x_eq_y: "as2"}

    solver.assertFormula(x_eq_y)
    solver.assertFormula(not_x_eq_y)

    assert solver.checkSat().isUnsat()

    proofs = solver.getProof()
    assert len(proofs) > 0
    printedProof = solver.proofToString(proofs[0], ProofFormat.ALETHE, names)
    assert len(printedProof) > 0
    assert b"as1" in printedProof
    assert b"as2" in printedProof


def test_learned_literals(solver):
    solver.setOption("produce-learned-literals", "true")
    with pytest.raises(RuntimeError):
        solver.getLearnedLiterals()
    solver.checkSat()
    solver.getLearnedLiterals()
    solver.getLearnedLiterals(LearnedLitType.PREPROCESS)

def test_learned_literals2(tm, solver):
    solver.setOption("produce-learned-literals", "true")
    intSort = tm.getIntegerSort()
    x = tm.mkConst(intSort, "x")
    y = tm.mkConst(intSort, "y")
    zero = tm.mkInteger(0)
    ten = tm.mkInteger(10)
    f0 = tm.mkTerm(Kind.GEQ, x, ten)
    f1 = tm.mkTerm(
            Kind.OR,
            tm.mkTerm(Kind.GEQ, zero, x),
            tm.mkTerm(Kind.GEQ, y, zero))
    solver.assertFormula(f0)
    solver.assertFormula(f1)
    solver.checkSat()
    solver.getLearnedLiterals(LearnedLitType.INPUT)

def test_get_timeout_core_unsat(tm, solver):
  solver.setOption("timeout-core-timeout", "100")
  solver.setOption("produce-unsat-cores", "true")
  intSort = tm.getIntegerSort()
  x = tm.mkConst(intSort, "x")
  tt = tm.mkBoolean(True)
  hard = tm.mkTerm(Kind.EQUAL,
                       tm.mkTerm(Kind.MULT, x, x),
                       tm.mkInteger("501240912901901249014210220059591"))
  solver.assertFormula(tt)
  solver.assertFormula(hard)
  res = solver.getTimeoutCore()
  assert res[0].isUnknown()
  assert len(res[1]) == 1
  assert res[1][0] == hard

def test_get_timeout_core(tm, solver):
  solver.setOption("produce-unsat-cores", "true")
  ff = tm.mkBoolean(False)
  tt = tm.mkBoolean(True)
  solver.assertFormula(tt)
  solver.assertFormula(ff)
  solver.assertFormula(tt)
  res = solver.getTimeoutCore()
  assert res[0].isUnsat()
  assert len(res[1]) == 1
  assert res[1][0] == ff

def test_get_timeout_core_assuming(tm, solver):
  solver.setOption("produce-unsat-cores", "true")
  ff = tm.mkBoolean(False)
  tt = tm.mkBoolean(True)
  solver.assertFormula(tt)
  res = solver.getTimeoutCoreAssuming(ff, tt)
  assert res[0].isUnsat()
  assert len(res[1]) == 1
  assert res[1][0] == ff

def test_get_timeout_core_assuming_empty(solver):
  solver.setOption("produce-unsat-cores", "true")
  with pytest.raises(RuntimeError):
    res = solver.getTimeoutCoreAssuming()

def test_get_value1(tm, solver):
    solver.setOption("produce-models", "false")
    t = tm.mkTrue()
    solver.assertFormula(t)
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getValue(t)


def test_get_value2(tm, solver):
    solver.setOption("produce-models", "true")
    t = tm.mkFalse()
    solver.assertFormula(t)
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getValue(t)


def test_get_value3(tm, solver):
    solver.setOption("produce-models", "true")
    uSort = tm.mkUninterpretedSort("u")
    intSort = tm.getIntegerSort()
    boolSort = tm.getBooleanSort()
    uToIntSort = tm.mkFunctionSort(uSort, intSort)
    intPredSort = tm.mkFunctionSort(intSort, boolSort)

    x = tm.mkConst(uSort, "x")
    y = tm.mkConst(uSort, "y")
    z = tm.mkConst(uSort, "z")
    f = tm.mkConst(uToIntSort, "f")
    p = tm.mkConst(intPredSort, "p")
    zero = tm.mkInteger(0)
    one = tm.mkInteger(1)
    f_x = tm.mkTerm(Kind.APPLY_UF, f, x)
    f_y = tm.mkTerm(Kind.APPLY_UF, f, y)
    summ = tm.mkTerm(Kind.ADD, f_x, f_y)
    p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero)
    p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y)

    solver.assertFormula(tm.mkTerm(Kind.LEQ, zero, f_x))
    solver.assertFormula(tm.mkTerm(Kind.LEQ, zero, f_y))
    solver.assertFormula(tm.mkTerm(Kind.LEQ, summ, one))
    solver.assertFormula(p_0.notTerm())
    solver.assertFormula(p_f_y)
    assert solver.checkSat().isSat()
    solver.getValue(x)
    solver.getValue(y)
    solver.getValue(z)
    solver.getValue(summ)
    solver.getValue(p_f_y)

    a = [solver.getValue(x), solver.getValue(y), solver.getValue(z)]
    b = solver.getValue([x,y,z])
    assert a == b

    with pytest.raises(RuntimeError):
        Solver(tm).getValue(x)

    slv = Solver(tm)
    slv.setOption("produce-models", "true")
    slv.checkSat()
    slv.getValue(x)

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("produce-models", "true")
    slv.checkSat()
    with pytest.raises(RuntimeError):
        slv.getValue(tm.mkConst(tm.getBooleanSort(), "x"))


def test_declare_sep_heap(tm, solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    integer = tm.getIntegerSort()
    solver.declareSepHeap(integer, integer)
    # cannot declare separation logic heap more than once
    with pytest.raises(RuntimeError):
        solver.declareSepHeap(integer, integer)

    with pytest.raises(RuntimeError):
        # no logic set yet
        Solver(tm).declareSepHeap(tm.getIntegerSort(), tm.getIntegerSort())

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setLogic("ALL")
    with pytest.raises(RuntimeError):
        slv.declareSepHeap(integer, ttm.getRealSort())

    slv = Solver(ttm)
    slv.setLogic("ALL");
    with pytest.raises(RuntimeError):
        slv.declareSepHeap(ttm.getBooleanSort(), integer)


# Helper function for test_get_separation_{heap,nil}_termX. Asserts and checks
# some simple separation logic constraints.
def checkSimpleSeparationConstraints(slv):
    tm = slv.getTermManager()
    integer = tm.getIntegerSort()
    # declare the separation heap
    slv.declareSepHeap(integer, integer)
    x = tm.mkConst(integer, "x")
    p = tm.mkConst(integer, "p")
    heap = tm.mkTerm(Kind.SEP_PTO, p, x)
    slv.assertFormula(heap)
    nil = tm.mkSepNil(integer)
    slv.assertFormula(nil.eqTerm(tm.mkInteger(5)))
    slv.checkSat()


def test_get_value_sep_heap_1(tm, solver):
    solver.setLogic("QF_BV")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkTrue()
    solver.assertFormula(t)
    with pytest.raises(RuntimeError):
        solver.getValueSepHeap()


def test_get_value_sep_heap_2(solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "false")
    checkSimpleSeparationConstraints(solver)
    with pytest.raises(RuntimeError):
        solver.getValueSepHeap()


def test_get_value_sep_heap_3(tm, solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkFalse()
    solver.assertFormula(t)
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getValueSepHeap()


def test_get_value_sep_heap_4(tm, solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkTrue()
    solver.assertFormula(t)
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getValueSepHeap()


def test_get_value_sep_heap_5(solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    checkSimpleSeparationConstraints(solver)
    solver.getValueSepHeap()


def test_get_value_sep_nil_1(tm, solver):
    solver.setLogic("QF_BV")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkTrue()
    solver.assertFormula(t)
    with pytest.raises(RuntimeError):
        solver.getValueSepNil()


def test_get_value_sep_nil_2(solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "false")
    checkSimpleSeparationConstraints(solver)
    with pytest.raises(RuntimeError):
        solver.getValueSepNil()


def test_get_value_sep_nil_3(tm, solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkFalse()
    solver.assertFormula(t)
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getValueSepNil()


def test_get_value_sep_nil_4(tm, solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkTrue()
    solver.assertFormula(t)
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getValueSepNil()


def test_get_value_sep_nil_5(solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    checkSimpleSeparationConstraints(solver)
    solver.getValueSepNil()


def test_push1(solver):
    solver.setOption("incremental", "true")
    solver.push(1)
    with pytest.raises(RuntimeError):
        solver.setOption("incremental", "false")
    with pytest.raises(RuntimeError):
        solver.setOption("incremental", "true")


def test_push2(solver):
    solver.setOption("incremental", "false")
    with pytest.raises(RuntimeError):
        solver.push(1)


def test_pop1(solver):
    solver.setOption("incremental", "false")
    with pytest.raises(RuntimeError):
        solver.pop(1)


def test_pop2(solver):
    solver.setOption("incremental", "true")
    with pytest.raises(RuntimeError):
        solver.pop(1)


def test_pop3(solver):
    solver.setOption("incremental", "true")
    solver.push(1)
    solver.pop(1)
    with pytest.raises(RuntimeError):
        solver.pop(1)

def test_block_model1(tm, solver):
    x = tm.mkConst(solver.getBooleanSort(), "x")
    solver.assertFormula(x.eqTerm(x))
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.blockModel(BlockModelsMode.LITERALS)

def test_block_model2(tm, solver):
    solver.setOption("produce-models", "true")
    x = tm.mkConst(solver.getBooleanSort(), "x")
    solver.assertFormula(x.eqTerm(x))
    with pytest.raises(RuntimeError):
        solver.blockModel(BlockModelsMode.LITERALS)

def test_block_model3(tm, solver):
    solver.setOption("produce-models", "true")
    x = tm.mkConst(solver.getBooleanSort(), "x");
    solver.assertFormula(x.eqTerm(x))
    solver.checkSat()
    solver.blockModel(BlockModelsMode.LITERALS)

def test_block_model_values1(tm, solver):
    solver.setOption("produce-models", "true")
    x = tm.mkConst(solver.getBooleanSort(), "x");
    solver.assertFormula(x.eqTerm(x))
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.blockModelValues([])
    solver.blockModelValues([tm.mkBoolean(False)])

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("produce-models", "true")
    slv.checkSat()
    with pytest.raises(RuntimeError):
        slv.blockModelValues([tm.mkFalse()])

def test_block_model_values2(tm, solver):
    solver.setOption("produce-models", "true")
    x = tm.mkConst(solver.getBooleanSort(), "x")
    solver.assertFormula(x.eqTerm(x))
    solver.checkSat()
    solver.blockModelValues([x])

def test_block_model_values3(tm, solver):
    x = tm.mkConst(solver.getBooleanSort(), "x")
    solver.assertFormula(x.eqTerm(x))
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.blockModelValues([x])

def test_block_model_values4(tm, solver):
    solver.setOption("produce-models", "true")
    x = tm.mkConst(solver.getBooleanSort(), "x")
    solver.assertFormula(x.eqTerm(x))
    with pytest.raises(RuntimeError):
        solver.blockModelValues([x])

def test_block_model_values5(tm, solver):
    solver.setOption("produce-models", "true")
    x = tm.mkConst(solver.getBooleanSort(), "x")
    solver.assertFormula(x.eqTerm(x))
    solver.checkSat()
    solver.blockModelValues([x])

def test_get_instantiations(tm, solver):
    iSort = tm.getIntegerSort()
    boolSort = solver.getBooleanSort()
    p = solver.declareFun("p", [iSort], boolSort)
    x = tm.mkVar(iSort, "x")
    bvl = tm.mkTerm(Kind.VARIABLE_LIST, x)
    app = tm.mkTerm(Kind.APPLY_UF, p, x)
    q = tm.mkTerm(Kind.FORALL, bvl, app)
    solver.assertFormula(q)
    five = tm.mkInteger(5)
    app2 = tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.APPLY_UF, p, five))
    solver.assertFormula(app2)
    with pytest.raises(RuntimeError):
        solver.getInstantiations()
    solver.checkSat()
    solver.getInstantiations()

def test_get_statistics(tm, solver):
    # do some array reasoning to make sure we have a double statistics
    s1 = tm.getIntegerSort()
    s2 = tm.mkArraySort(s1, s1)
    t1 = tm.mkConst(s1, "i")
    t2 = tm.mkVar(s2, "a")
    t3 = tm.mkTerm(Kind.SELECT, t2, t1)
    solver.checkSat()

    stats = solver.getStatistics()

    assert not stats['global::totalTime']['internal']
    assert not stats['global::totalTime']['default']
    assert stats['global::totalTime']['value'][-2:] == 'ms' # ends with 'ms'
    assert stats['resource::resourceUnitsUsed']['internal']
    assert not stats['resource::resourceUnitsUsed']['default']
    assert stats.get(True)['resource::resourceUnitsUsed']['internal']
    assert not stats.get(True)['resource::resourceUnitsUsed']['default']

    assert '' not in stats
    assert len([s for s in stats]) > 0

    for s in stats:
        str(s)
        if s[0] == 'theory::arrays::avgIndexListLength':
            assert s[1]['internal']
            assert s[1]['default']
            assert isnan(s[1]['value'])


def test_set_info(solver):
    with pytest.raises(RuntimeError):
        solver.setInfo("cvc5-lagic", "QF_BV")
    with pytest.raises(RuntimeError):
        solver.setInfo("cvc2-logic", "QF_BV")
    with pytest.raises(RuntimeError):
        solver.setInfo("cvc5-logic", "asdf")

    solver.setInfo("source", "asdf")
    solver.setInfo("category", "asdf")
    solver.setInfo("difficulty", "asdf")
    solver.setInfo("filename", "asdf")
    solver.setInfo("license", "asdf")
    solver.setInfo("name", "asdf")
    solver.setInfo("notes", "asdf")

    solver.setInfo("smt-lib-version", "2")
    solver.setInfo("smt-lib-version", "2.0")
    solver.setInfo("smt-lib-version", "2.5")
    solver.setInfo("smt-lib-version", "2.6")
    with pytest.raises(RuntimeError):
        solver.setInfo("smt-lib-version", ".0")

    solver.setInfo("status", "sat")
    solver.setInfo("status", "unsat")
    solver.setInfo("status", "unknown")
    with pytest.raises(RuntimeError):
        solver.setInfo("status", "asdf")


def test_simplify(tm, solver):
    bvSort = tm.mkBitVectorSort(32)
    uSort = tm.mkUninterpretedSort("u")
    funSort1 = tm.mkFunctionSort([bvSort, bvSort], bvSort)
    funSort2 = tm.mkFunctionSort(uSort, tm.getIntegerSort())
    consListSpec = tm.mkDatatypeDecl("list")
    cons = tm.mkDatatypeConstructorDecl("cons")
    cons.addSelector("head", tm.getIntegerSort())
    cons.addSelectorSelf("tail")
    consListSpec.addConstructor(cons)
    nil = tm.mkDatatypeConstructorDecl("nil")
    consListSpec.addConstructor(nil)
    consListSort = tm.mkDatatypeSort(consListSpec)

    x = tm.mkConst(bvSort, "x")
    solver.simplify(x)
    a = tm.mkConst(bvSort, "a")
    solver.simplify(a)
    b = tm.mkConst(bvSort, "b")
    solver.simplify(b)
    x_eq_x = tm.mkTerm(Kind.EQUAL, x, x)
    solver.simplify(x_eq_x)
    assert tm.mkTrue() != x_eq_x
    assert tm.mkTrue() == solver.simplify(x_eq_x)
    x_eq_b = tm.mkTerm(Kind.EQUAL, x, b)
    solver.simplify(x_eq_b)
    assert tm.mkTrue() != x_eq_b
    assert tm.mkTrue() != solver.simplify(x_eq_b)
    slv = Solver(tm)
    slv.simplify(x)

    i1 = tm.mkConst(tm.getIntegerSort(), "i1")
    solver.simplify(i1)
    i2 = tm.mkTerm(Kind.MULT, i1, tm.mkInteger("23"))
    solver.simplify(i2)
    assert i1 != i2
    assert i1 != solver.simplify(i2)
    i3 = tm.mkTerm(Kind.ADD, i1, tm.mkInteger(0))
    solver.simplify(i3)
    assert i1 != i3
    assert i1 == solver.simplify(i3)

    consList = consListSort.getDatatype()
    dt1 = tm.mkTerm(
        Kind.APPLY_CONSTRUCTOR,
        consList.getConstructor("cons").getTerm(),
        tm.mkInteger(0),
        tm.mkTerm(
            Kind.APPLY_CONSTRUCTOR,
            consList.getConstructor("nil").getTerm()))
    solver.simplify(dt1)
    dt2 = tm.mkTerm(
      Kind.APPLY_SELECTOR,
      consList["cons"].getSelector("head").getTerm(),
      dt1)
    solver.simplify(dt2)

    b1 = tm.mkVar(bvSort, "b1")
    solver.simplify(b1)
    b2 = tm.mkVar(bvSort, "b1")
    solver.simplify(b2)
    b3 = tm.mkVar(uSort, "b3")
    solver.simplify(b3)
    v1 = tm.mkConst(bvSort, "v1")
    solver.simplify(v1)
    v2 = tm.mkConst(tm.getIntegerSort(), "v2")
    solver.simplify(v2)
    f1 = tm.mkConst(funSort1, "f1")
    solver.simplify(f1)
    f2 = tm.mkConst(funSort2, "f2")
    solver.simplify(f2)
    solver.defineFunsRec([f1, f2], [[b1, b2], [b3]], [v1, v2])
    solver.simplify(f1)
    solver.simplify(f2)

    ttm = TermManager()
    slv = Solver(ttm)
    with pytest.raises(RuntimeError):
        slv.simplify(x)

def test_simplify_apply_subs(tm, solver):
    solver.setOption("incremental", "true")
    intSort = tm.getIntegerSort()
    x = tm.mkConst(intSort, "x")
    zero = tm.mkInteger(0)
    eq = tm.mkTerm(Kind.EQUAL, x, zero)
    solver.assertFormula(eq)
    solver.checkSat()

    assert solver.simplify(x, False) == x
    assert solver.simplify(x, True) == zero

def test_assert_formula(tm, solver):
    solver.assertFormula(tm.mkTrue())
    slv = Solver(tm)
    slv.assertFormula(tm.mkTrue())

    ttm = TermManager()
    slv = Solver(ttm)
    with pytest.raises(RuntimeError):
        slv.assertFormula(tm.mkTrue())


def test_check_sat(solver):
    solver.setOption("incremental", "false")
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.checkSat()


def test_check_sat_assuming(tm, solver):
    solver.setOption("incremental", "false")
    solver.checkSatAssuming(tm.mkTrue())
    with pytest.raises(RuntimeError):
        solver.checkSatAssuming(tm.mkTrue())
    slv = Solver(tm)
    slv.checkSatAssuming(tm.mkTrue())

    ttm = TermManager()
    slv = Solver(ttm)
    with pytest.raises(RuntimeError):
        slv.checkSatAssuming(tm.mkTrue())


def test_check_sat_assuming1(tm, solver):
    boolSort = tm.getBooleanSort()
    x = tm.mkConst(boolSort, "x")
    y = tm.mkConst(boolSort, "y")
    z = tm.mkTerm(Kind.AND, x, y)
    solver.setOption("incremental", "true")
    solver.checkSatAssuming(tm.mkTrue())
    solver.checkSatAssuming(tm.mkTrue())
    solver.checkSatAssuming(z)
    slv = Solver(tm)
    slv.checkSatAssuming(tm.mkTrue())


def test_check_sat_assuming2(tm, solver):
    solver.setOption("incremental", "true")

    uSort = tm.mkUninterpretedSort("u")
    intSort = tm.getIntegerSort()
    boolSort = solver.getBooleanSort()
    uToIntSort = tm.mkFunctionSort(uSort, intSort)
    intPredSort = tm.mkFunctionSort(intSort, boolSort)

    # Constants
    x = tm.mkConst(uSort, "x")
    y = tm.mkConst(uSort, "y")
    # Functions
    f = tm.mkConst(uToIntSort, "f")
    p = tm.mkConst(intPredSort, "p")
    # Values
    zero = tm.mkInteger(0)
    one = tm.mkInteger(1)
    # Terms
    f_x = tm.mkTerm(Kind.APPLY_UF, f, x)
    f_y = tm.mkTerm(Kind.APPLY_UF, f, y)
    summ = tm.mkTerm(Kind.ADD, f_x, f_y)
    p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero)
    p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y)
    # Assertions
    assertions =\
        tm.mkTerm(Kind.AND,\
                      tm.mkTerm(Kind.LEQ, zero, f_x),  # 0 <= f(x)
                       tm.mkTerm(Kind.LEQ, zero, f_y),  # 0 <= f(y)
                       tm.mkTerm(Kind.LEQ, summ, one),  # f(x) + f(y) <= 1
                       p_0.notTerm(),                        # not p(0)
                       p_f_y                                 # p(f(y))
                      )

    solver.checkSatAssuming(tm.mkTrue())
    solver.assertFormula(assertions)
    solver.checkSatAssuming(tm.mkTerm(Kind.DISTINCT, x, y))
    solver.checkSatAssuming(
        tm.mkFalse(),
         tm.mkTerm(Kind.DISTINCT, x, y))
    slv = Solver(tm)
    slv.checkSatAssuming(tm.mkTrue())


def test_set_logic(tm, solver):
    solver.setLogic("AUFLIRA")
    with pytest.raises(RuntimeError):
        solver.setLogic("AF_BV")
    solver.assertFormula(tm.mkTrue())
    with pytest.raises(RuntimeError):
        solver.setLogic("AUFLIRA")

def test_is_logic_set(solver):
    assert solver.isLogicSet() == False
    solver.setLogic("QF_BV")
    assert solver.isLogicSet() == True

def test_get_logic(solver):
    with pytest.raises(RuntimeError):
        solver.getLogic()
    solver.setLogic("QF_BV")
    assert solver.getLogic() == "QF_BV"

def test_set_option(tm, solver):
    solver.setOption("bv-sat-solver", "minisat")
    with pytest.raises(RuntimeError):
        solver.setOption("bv-sat-solver", "1")
    solver.assertFormula(tm.mkTrue())
    with pytest.raises(RuntimeError):
        solver.setOption("bv-sat-solver", "minisat")


def test_reset_assertions(tm, solver):
    solver.setOption("incremental", "true")

    bvSort = tm.mkBitVectorSort(4)
    one = tm.mkBitVector(4, 1)
    x = tm.mkConst(bvSort, "x")
    ule = tm.mkTerm(Kind.BITVECTOR_ULE, x, one)
    srem = tm.mkTerm(Kind.BITVECTOR_SREM, one, x)
    solver.push(4)
    slt = tm.mkTerm(Kind.BITVECTOR_SLT, srem, one)
    solver.resetAssertions()
    solver.checkSatAssuming(slt, ule)

def test_declare_sygus_var(tm, solver):
    solver.setOption("sygus", "true")
    boolSort = tm.getBooleanSort()
    intSort = tm.getIntegerSort()
    funSort = tm.mkFunctionSort([intSort], boolSort)

    solver.declareSygusVar("", boolSort)
    solver.declareSygusVar("", funSort)
    solver.declareSygusVar("b", boolSort)
    with pytest.raises(RuntimeError):
        solver.declareSygusVar("", cvc5.Sort())
    with pytest.raises(RuntimeError):
        solver.declareSygusVar("a", cvc5.Sort())
    with pytest.raises(RuntimeError):
        Solver(tm).declareSygusVar("", boolSort)

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("sygus", "true")
    with pytest.raises(RuntimeError):
        slv.declareSygusVar("", boolSort)


def test_mk_sygus_grammar(tm, solver):
    boolTerm = tm.mkBoolean(True)
    boolVar = tm.mkVar(solver.getBooleanSort())
    intVar = tm.mkVar(tm.getIntegerSort())

    solver.mkGrammar([], [intVar])
    solver.mkGrammar([boolVar], [intVar])
    with pytest.raises(RuntimeError):
        solver.mkGrammar([], [])
    with pytest.raises(RuntimeError):
        solver.mkGrammar([], [boolTerm])
    with pytest.raises(RuntimeError):
        solver.mkGrammar([boolTerm], [intVar])
    slv = Solver(tm)
    boolVar2 = tm.mkVar(tm.getBooleanSort())
    intVar2 = tm.mkVar(tm.getIntegerSort())
    slv.mkGrammar([boolVar2], [intVar2])
    slv.mkGrammar([boolVar], [intVar2])
    slv.mkGrammar([boolVar2], [intVar])

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("sygus", "true")
    boolVar2 = ttm.mkVar(ttm.getBooleanSort())
    intVar2 = ttm.mkVar(ttm.getIntegerSort())
    slv.mkGrammar([boolVar2], [intVar2])
    with pytest.raises(RuntimeError):
        slv.mkGrammar([boolVar], [intVar2])
    with pytest.raises(RuntimeError):
        slv.mkGrammar([boolVar2], [intVar])


def test_add_sygus_constraint(tm, solver):
    solver.setOption("sygus", "true")
    boolTerm = tm.mkBoolean(True)
    intTerm = tm.mkInteger(1)

    solver.addSygusConstraint(boolTerm)
    with pytest.raises(RuntimeError):
        solver.addSygusConstraint(intTerm)

    slv = Solver(tm)
    with pytest.raises(RuntimeError):
        slv.addSygusConstraint(boolTerm)

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("sygus", "true")
    with pytest.raises(RuntimeError):
        slv.addSygusConstraint(boolTerm)


def test_get_sygus_constraints(tm, solver):
    solver.setOption("sygus", "true")
    true_term = tm.mkBoolean(True)
    false_term = tm.mkBoolean(False)
    solver.addSygusConstraint(true_term)
    solver.addSygusConstraint(false_term)
    constraints = [true_term, false_term]
    assert solver.getSygusConstraints() == constraints


def test_add_sygus_assume(tm, solver):
    solver.setOption("sygus", "true")
    boolTerm = tm.mkBoolean(False)
    intTerm = tm.mkInteger(1)
    solver.addSygusAssume(boolTerm)
    with pytest.raises(RuntimeError):
        solver.addSygusAssume(intTerm)
    slv = Solver(tm)
    with pytest.raises(RuntimeError):
        slv.addSygusAssume(boolTerm)

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("sygus", "true")
    with pytest.raises(RuntimeError):
        slv.addSygusAssume(boolTerm)


def test_get_sygus_assumptions(tm, solver):
    solver.setOption("sygus", "true")
    true_term = tm.mkBoolean(True)
    false_term = tm.mkBoolean(False)
    solver.addSygusAssume(true_term)
    solver.addSygusAssume(false_term)
    assumptions = [true_term, false_term]
    assert solver.getSygusAssumptions() == assumptions


def test_add_sygus_inv_constraint(tm, solver):
    solver.setOption("sygus", "true")
    boolean = solver.getBooleanSort()
    real = solver.getRealSort()

    intTerm = tm.mkInteger(1)

    inv = solver.declareFun("inv", [real], boolean)
    pre = solver.declareFun("pre", [real], boolean)
    trans = solver.declareFun("trans", [real, real], boolean)
    post = solver.declareFun("post", [real], boolean)

    inv1 = solver.declareFun("inv1", [real], real)

    trans1 = solver.declareFun("trans1", [boolean, real], boolean)
    trans2 = solver.declareFun("trans2", [real, boolean], boolean)
    trans3 = solver.declareFun("trans3", [real, real], real)

    solver.addSygusInvConstraint(inv, pre, trans, post)

    with pytest.raises(RuntimeError):
        solver.addSygusInvConstraint(intTerm, pre, trans, post)

    with pytest.raises(RuntimeError):
        solver.addSygusInvConstraint(inv1, pre, trans, post)

    with pytest.raises(RuntimeError):
        solver.addSygusInvConstraint(inv, trans, trans, post)

    with pytest.raises(RuntimeError):
        solver.addSygusInvConstraint(inv, pre, intTerm, post)
    with pytest.raises(RuntimeError):
        solver.addSygusInvConstraint(inv, pre, pre, post)
    with pytest.raises(RuntimeError):
        solver.addSygusInvConstraint(inv, pre, trans1, post)
    with pytest.raises(RuntimeError):
        solver.addSygusInvConstraint(inv, pre, trans2, post)
    with pytest.raises(RuntimeError):
        solver.addSygusInvConstraint(inv, pre, trans3, post)

    with pytest.raises(RuntimeError):
        solver.addSygusInvConstraint(inv, pre, trans, trans)
    slv = Solver(tm)
    slv.setOption("sygus", "true")
    boolean2 = tm.getBooleanSort()
    real2 = tm.getRealSort()
    inv22 = solver.declareFun("inv", [real2], boolean2)
    pre22 = solver.declareFun("pre", [real2], boolean2)
    trans22 = solver.declareFun("trans", [real2, real2], boolean2)
    post22 = solver.declareFun("post", [real2], boolean2)
    slv.addSygusInvConstraint(inv22, pre22, trans22, post22)
    slv.addSygusInvConstraint(inv, pre22, trans22, post22)
    slv.addSygusInvConstraint(inv22, pre, trans22, post22)
    slv.addSygusInvConstraint(inv22, pre22, trans, post22)
    slv.addSygusInvConstraint(inv22, pre22, trans22, post)

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("sygus", "true")
    boolean2 = ttm.getBooleanSort()
    real2 = ttm.getRealSort()
    inv22 = slv.declareFun("inv", [real2], boolean2)
    pre22 = slv.declareFun("pre", [real2], boolean2)
    trans22 = slv.declareFun("trans", [real2, real2], boolean2)
    post22 = slv.declareFun("post", [real2], boolean2)
    slv.addSygusInvConstraint(inv22, pre22, trans22, post22)
    with pytest.raises(RuntimeError):
        slv.addSygusInvConstraint(inv, pre22, trans22, post22)
    with pytest.raises(RuntimeError):
        slv.addSygusInvConstraint(inv22, pre, trans22, post22)
    with pytest.raises(RuntimeError):
        slv.addSygusInvConstraint(inv22, pre22, trans, post22)
    with pytest.raises(RuntimeError):
        slv.addSygusInvConstraint(inv22, pre22, trans22, post)


def test_check_synth(solver):
    with pytest.raises(RuntimeError):
        solver.checkSynth()
    solver.setOption("sygus", "true")
    solver.checkSynth()


def test_get_synth_solution(tm, solver):
    solver.setOption("sygus", "true")
    solver.setOption("incremental", "false")

    x = tm.mkBoolean(False)
    f = solver.synthFun("f", [], solver.getBooleanSort())

    with pytest.raises(RuntimeError):
        solver.getSynthSolution(f)

    res = solver.checkSynth()
    assert res.hasSolution()

    solver.getSynthSolution(f)
    solver.getSynthSolution(f)

    with pytest.raises(RuntimeError):
        solver.getSynthSolution(x)

    slv = Solver(tm)
    with pytest.raises(RuntimeError):
        slv.getSynthSolution(f)


def test_check_synth_next(solver):
    solver.setOption("sygus", "true")
    solver.setOption("incremental", "true")
    f = solver.synthFun("f", [], solver.getBooleanSort())

    res = solver.checkSynth()
    assert res.hasSolution()
    solver.getSynthSolutions([f])

    res = solver.checkSynthNext()
    assert res.hasSolution()
    solver.getSynthSolutions([f])


def test_check_synth_next2(solver):
    solver.setOption("sygus", "true")
    solver.setOption("incremental", "false")
    f = solver.synthFun("f", [], solver.getBooleanSort())

    solver.checkSynth()
    with pytest.raises(RuntimeError):
        solver.checkSynthNext()


def test_check_synth_next3(solver):
    solver.setOption("sygus", "true")
    solver.setOption("incremental", "true")
    f = solver.synthFun("f", [], solver.getBooleanSort())
    with pytest.raises(RuntimeError):
        solver.checkSynthNext()


def test_find_synth(tm, solver):
    solver.setOption("sygus", "true")
    boolSort = solver.getBooleanSort()
    start = tm.mkVar(boolSort)
    g = solver.mkGrammar([], [start])
    truen = tm.mkBoolean(True)
    falsen = tm.mkBoolean(False)
    g.addRule(start, truen)
    g.addRule(start, falsen)
    f = solver.synthFun("f", [], solver.getBooleanSort(), g)

    # should enumerate based on the grammar of the function to synthesize above
    t = solver.findSynth(FindSynthTarget.ENUM)
    assert not t.isNull() and t.getSort().isBoolean()


def test_find_synth2(tm, solver):
    solver.setOption("sygus", "true")
    solver.setOption("incremental", "true")
    boolSort = solver.getBooleanSort()
    start = tm.mkVar(boolSort)
    g = solver.mkGrammar([], [start])
    truen = tm.mkBoolean(True)
    falsen = tm.mkBoolean(False)
    g.addRule(start, truen)
    g.addRule(start, falsen)

    # should enumerate true/false
    t = solver.findSynth(FindSynthTarget.ENUM, g)
    assert not t.isNull() and t.getSort().isBoolean()
    t = solver.findSynthNext()
    assert not t.isNull() and t.getSort().isBoolean()


def test_get_abduct(tm, solver):
    solver.setLogic("QF_LIA")
    solver.setOption("produce-abducts", "true")
    solver.setOption("incremental", "false")

    intSort = tm.getIntegerSort()
    zero = tm.mkInteger(0)
    x = tm.mkConst(intSort, "x")
    y = tm.mkConst(intSort, "y")

    solver.assertFormula(tm.mkTerm(Kind.GT, x, zero))
    conj = tm.mkTerm(Kind.GT, y, zero)
    output = solver.getAbduct(conj)
    assert not output.isNull() and output.getSort().isBoolean()

    boolean = solver.getBooleanSort()
    truen = tm.mkBoolean(True)
    start = tm.mkVar(boolean)
    g = solver.mkGrammar([], [start])
    conj2 = tm.mkTerm(Kind.GT, x, zero)
    g.addRule(start, truen)
    output2 = solver.getAbduct(conj2, g)
    assert output2 == truen

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("produce-abducts", "true")
    intSort2 = ttm.getIntegerSort()
    xx = ttm.mkConst(intSort2, "x")
    yy = ttm.mkConst(intSort2, "y")
    zzero = ttm.mkInteger(0)
    sstart = ttm.mkVar(ttm.getBooleanSort())
    slv.assertFormula(
        ttm.mkTerm(Kind.GT, ttm.mkTerm(Kind.ADD, xx, yy), zzero))
    gg = slv.mkGrammar([], [sstart])
    gg.addRule(sstart, ttm.mkTrue())
    cconj2 = ttm.mkTerm(Kind.EQUAL, zzero, zzero)
    slv.getAbduct(cconj2, gg)
    with pytest.raises(RuntimeError):
        slv.getAbduct(conj2)
    with pytest.raises(RuntimeError):
        slv.getAbduct(conj2, gg)
    with pytest.raises(RuntimeError):
        slv.getAbduct(cconj2, g)


def test_get_abduct2(tm, solver):
    solver.setLogic("QF_LIA")
    solver.setOption("incremental", "false")
    intSort = tm.getIntegerSort()
    zero = tm.mkInteger(0)
    x = tm.mkConst(intSort, "x")
    y = tm.mkConst(intSort, "y")
    solver.assertFormula(tm.mkTerm(Kind.GT, x, zero))
    conj = tm.mkTerm(Kind.GT, y, zero)
    with pytest.raises(RuntimeError):
        solver.getAbduct(conj)


def test_get_abduct_next(tm, solver):
    solver.setLogic("QF_LIA")
    solver.setOption("produce-abducts", "true")
    solver.setOption("incremental", "true")

    intSort = tm.getIntegerSort()
    zero = tm.mkInteger(0)
    x = tm.mkConst(intSort, "x")
    y = tm.mkConst(intSort, "y")

    solver.assertFormula(tm.mkTerm(Kind.GT, x, zero))
    conj = tm.mkTerm(Kind.GT, y, zero)
    output = solver.getAbduct(conj)
    output2 = solver.getAbductNext()
    assert output != output2


def test_get_interpolant(tm, solver):
    solver.setLogic("QF_LIA")
    solver.setOption("produce-interpolants", "true")
    solver.setOption("incremental", "false")

    intSort = tm.getIntegerSort()
    zero = tm.mkInteger(0)
    x = tm.mkConst(intSort, "x")
    y = tm.mkConst(intSort, "y")
    z = tm.mkConst(intSort, "z")

    solver.assertFormula(tm.mkTerm(
        Kind.GT, tm.mkTerm(Kind.ADD, x, y), zero))
    solver.assertFormula(tm.mkTerm(Kind.LT, x, zero))
    conj = tm.mkTerm(
            Kind.OR,
            tm.mkTerm(Kind.GT, tm.mkTerm(Kind.ADD, y, z), zero),
            tm.mkTerm(Kind.LT, z, zero))
    output = solver.getInterpolant(conj)
    assert output.getSort().isBoolean()

    boolean = solver.getBooleanSort()
    truen = tm.mkBoolean(True)
    start = tm.mkVar(boolean)
    g = solver.mkGrammar([], [start])
    conj2 = tm.mkTerm(Kind.EQUAL, zero, zero)
    g.addRule(start, truen)
    output2 = solver.getInterpolant(conj2, g)
    assert output2 == truen

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("produce-interpolants", "true")
    intSort2 = ttm.getIntegerSort()
    xx = ttm.mkConst(intSort2, "x")
    yy = ttm.mkConst(intSort2, "y")
    zzero = ttm.mkInteger(0)
    sstart = ttm.mkVar(ttm.getBooleanSort())
    slv.assertFormula(
        ttm.mkTerm(Kind.GT, ttm.mkTerm(Kind.ADD, xx, yy), zzero))
    gg = slv.mkGrammar([], [sstart])
    gg.addRule(sstart, ttm.mkTrue())
    cconj2 = ttm.mkTerm(Kind.EQUAL, zzero, zzero)
    slv.getInterpolant(cconj2, gg)
    with pytest.raises(RuntimeError):
        slv.getInterpolant(conj2)
    with pytest.raises(RuntimeError):
        slv.getInterpolant(conj2, gg)
    with pytest.raises(RuntimeError):
        slv.getInterpolant(cconj2, g)


def test_get_interpolant_next(tm, solver):
    solver.setLogic("QF_LIA")
    solver.setOption("produce-interpolants", "true")
    solver.setOption("incremental", "true")

    intSort = tm.getIntegerSort()
    zero = tm.mkInteger(0)
    x = tm.mkConst(intSort, "x")
    y = tm.mkConst(intSort, "y")
    z = tm.mkConst(intSort, "z")

    solver.assertFormula(tm.mkTerm(
        Kind.GT, tm.mkTerm(Kind.ADD, x, y), zero))
    solver.assertFormula(tm.mkTerm(Kind.LT, x, zero))
    conj = tm.mkTerm(
            Kind.OR,
            tm.mkTerm(Kind.GT, tm.mkTerm(Kind.ADD, y, z), zero),
            tm.mkTerm(Kind.LT, z, zero))
    output = solver.getInterpolant(conj)
    output2 = solver.getInterpolantNext()

    assert output != output2


def test_declare_pool(tm, solver):
    intSort = tm.getIntegerSort()
    setSort = tm.mkSetSort(intSort)
    zero = tm.mkInteger(0)
    x = tm.mkConst(intSort, "x")
    y = tm.mkConst(intSort, "y")
    # declare a pool with initial value  0, x, y
    p = solver.declarePool("p", intSort, [zero, x, y])
    # pool should have the same sort
    assert p.getSort() == setSort

    ttm = TermManager()
    slv = Solver(ttm)
    with pytest.raises(RuntimeError):
        slv.declarePool(
          "p",
          tm.getIntegerSort(),
          [tm.mkInteger(0), tm.mkConst(intSort, "x"), tm.mkConst(intSort, "y")])
    with pytest.raises(RuntimeError):
        slv.declarePool(
          "p",
          tm.getIntegerSort(),
          [tm.mkInteger(0), tm.mkConst(intSort, "x"), tm.mkConst(intSort, "y")])
    with pytest.raises(RuntimeError):
        slv.declarePool(
          "p",
          tm.getIntegerSort(),
          [tm.mkInteger(0), tm.mkConst(intSort, "x"), tm.mkConst(intSort, "y")])
    with pytest.raises(RuntimeError):
        slv.declarePool(
          "p",
          tm.getIntegerSort(),
          [tm.mkInteger(0), tm.mkConst(intSort, "x"), tm.mkConst(intSort, "y")])


def test_get_model_domain_elements(tm, solver):
    solver.setOption("produce-models", "true")
    uSort = tm.mkUninterpretedSort("u")
    intSort = tm.getIntegerSort()
    x = tm.mkConst(uSort, "x")
    y = tm.mkConst(uSort, "y")
    z = tm.mkConst(uSort, "z")
    f = tm.mkTerm(Kind.DISTINCT, x, y, z)
    solver.assertFormula(f)
    solver.checkSat()
    solver.getModelDomainElements(uSort)
    assert len(solver.getModelDomainElements(uSort)) >= 3
    with pytest.raises(RuntimeError):
        solver.getModelDomainElements(intSort)

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("produce-models", "true")
    slv.checkSat()
    with pytest.raises(RuntimeError):
        slv.getModelDomainElements(tm.mkUninterpretedSort("u"))

def test_get_model_domain_elements2(tm, solver):
    solver.setOption("produce-models", "true")
    solver.setOption("finite-model-find", "true")
    uSort = tm.mkUninterpretedSort("u")
    x = tm.mkVar(uSort, "x")
    y = tm.mkVar(uSort, "y")
    eq = tm.mkTerm(Kind.EQUAL, x, y)
    bvl = tm.mkTerm(Kind.VARIABLE_LIST, x, y)
    f = tm.mkTerm(Kind.FORALL, bvl, eq)
    solver.assertFormula(f)
    solver.checkSat()
    solver.getModelDomainElements(uSort)
    assert len(solver.getModelDomainElements(uSort)) == 1


def test_get_synth_solutions(tm, solver):
    solver.setOption("sygus", "true")
    solver.setOption("incremental", "false")

    x = tm.mkBoolean(False)
    f = solver.synthFun("f", [], solver.getBooleanSort())

    with pytest.raises(RuntimeError):
        solver.getSynthSolutions([])
    with pytest.raises(RuntimeError):
        solver.getSynthSolutions([f])

    solver.checkSynth()

    solver.getSynthSolutions([f])
    solver.getSynthSolutions([f, f])

    with pytest.raises(RuntimeError):
        solver.getSynthSolutions([])
    with pytest.raises(RuntimeError):
        solver.getSynthSolutions([x])

    slv = Solver(tm)
    with pytest.raises(RuntimeError):
        slv.getSynthSolutions([x])


def test_get_value_sep_heap1(tm, solver):
    solver.setLogic("QF_BV")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkTrue()
    solver.assertFormula(t)
    with pytest.raises(RuntimeError):
        solver.getValueSepHeap()


def test_get_value_sep_heap2(solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "false")
    checkSimpleSeparationConstraints(solver)
    with pytest.raises(RuntimeError):
        solver.getValueSepHeap()


def test_get_value_sep_heap3(tm, solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkFalse()
    solver.assertFormula(t)
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getValueSepHeap()


def test_get_value_sep_heap4(tm, solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkTrue()
    solver.assertFormula(t)
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getValueSepHeap()


def test_get_value_sep_heap5(solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    checkSimpleSeparationConstraints(solver)
    solver.getValueSepHeap()


def test_get_value_sep_nil1(tm, solver):
    solver.setLogic("QF_BV")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkTrue()
    solver.assertFormula(t)
    with pytest.raises(RuntimeError):
        solver.getValueSepNil()


def test_get_value_sep_nil2(solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "false")
    checkSimpleSeparationConstraints(solver)
    with pytest.raises(RuntimeError):
        solver.getValueSepNil()


def test_get_value_sep_nil3(tm, solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkFalse()
    solver.assertFormula(t)
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getValueSepNil()


def test_get_value_sep_nil4(tm, solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    t = tm.mkTrue()
    solver.assertFormula(t)
    solver.checkSat()
    with pytest.raises(RuntimeError):
        solver.getValueSepNil()


def test_get_value_sep_nil5(solver):
    solver.setLogic("ALL")
    solver.setOption("incremental", "false")
    solver.setOption("produce-models", "true")
    checkSimpleSeparationConstraints(solver)
    solver.getValueSepNil()


def test_is_model_core_symbol(tm, solver):
    solver.setOption("produce-models", "true")
    solver.setOption("model-cores", "simple")
    uSort = tm.mkUninterpretedSort("u")
    x = tm.mkConst(uSort, "x")
    y = tm.mkConst(uSort, "y")
    z = tm.mkConst(uSort, "z")
    zero = tm.mkInteger(0)
    f = tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, x, y))
    solver.assertFormula(f)
    solver.checkSat()
    assert solver.isModelCoreSymbol(x)
    assert solver.isModelCoreSymbol(y)
    assert not solver.isModelCoreSymbol(z)
    with pytest.raises(RuntimeError):
        solver.isModelCoreSymbol(zero)

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("produce-models", "true")
    slv.checkSat()
    with pytest.raises(RuntimeError):
        slv.isModelCoreSymbol(tm.mkConst(uSort, "x"))


def test_get_model(tm, solver):
    solver.setOption("produce-models", "true")
    uSort = tm.mkUninterpretedSort("u")
    x = tm.mkConst(uSort, "x")
    y = tm.mkConst(uSort, "y")
    z = tm.mkConst(uSort, "z")
    f = tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, x, y))
    solver.assertFormula(f)
    solver.checkSat()
    sorts = [uSort]
    terms = [x, y]
    solver.getModel(sorts, terms)


def test_get_model2(tm):
    solver.setOption("produce-models", "true")
    sorts = []
    terms = []
    with pytest.raises(RuntimeError):
        solver.getModel(sorts, terms)


def test_get_model3(tm, solver):
    solver.setOption("produce-models", "true")
    sorts = []
    terms = []
    solver.checkSat()
    solver.getModel(sorts, terms)
    integer = tm.getIntegerSort()
    sorts.append(integer)
    with pytest.raises(RuntimeError):
        solver.getModel(sorts, terms)


def test_issue5893(tm):
    bvsort4 = tm.mkBitVectorSort(4)
    bvsort8 = tm.mkBitVectorSort(8)
    arrsort = tm.mkArraySort(bvsort4, bvsort8)
    arr = tm.mkConst(arrsort, "arr")
    idx = tm.mkConst(bvsort4, "idx")
    ten = tm.mkBitVector(8, "10", 10)
    sel = tm.mkTerm(Kind.SELECT, arr, idx)
    distinct = tm.mkTerm(Kind.DISTINCT, sel, ten)
    distinct.getOp()


def test_issue7000(tm, solver):
    s1 = tm.getIntegerSort()
    s2 = tm.mkFunctionSort(s1, s1)
    s3 = solver.getRealSort()
    t4 = tm.mkPi()
    t7 = tm.mkConst(s3, "_x5")
    t37 = tm.mkConst(s2, "_x32")
    t59 = tm.mkConst(s2, "_x51")
    t72 = tm.mkTerm(Kind.EQUAL, t37, t59)
    t74 = tm.mkTerm(Kind.GT, t4, t7)
    query = tm.mkTerm(Kind.AND, t72, t74, t72, t72)
    # throws logic exception since logic is not higher order by default
    with pytest.raises(RuntimeError):
        solver.checkSatAssuming(query.notTerm())


def test_mk_sygus_var(tm, solver):
    solver.setOption("sygus", "true")
    boolSort = solver.getBooleanSort()
    intSort = tm.getIntegerSort()
    funSort = tm.mkFunctionSort(intSort, boolSort)

    solver.declareSygusVar("", boolSort)
    solver.declareSygusVar("", funSort)
    solver.declareSygusVar("b", boolSort)
    slv = Solver(tm)
    with pytest.raises(RuntimeError):
        slv.declareSygusVar("", boolSort)


def test_synth_fun(tm, solver):
    solver.setOption("sygus", "true")
    boolean = solver.getBooleanSort()
    integer = tm.getIntegerSort()

    x = tm.mkVar(boolean)

    start1 = tm.mkVar(boolean)
    start2 = tm.mkVar(integer)

    g1 = solver.mkGrammar(x, [start1])
    g1.addRule(start1, tm.mkBoolean(False))

    g2 = solver.mkGrammar(x, [start2])
    g2.addRule(start2, tm.mkInteger(0))

    solver.synthFun("", [], boolean)
    solver.synthFun("f1", [x], boolean)
    solver.synthFun("f2", [x], boolean, g1)

    with pytest.raises(RuntimeError):
        solver.synthFun("f6", [x], boolean, g2)
    slv = Solver(tm)
    slv.setOption("sygus", "true")
    x2 = tm.mkVar(tm.getBooleanSort())
    slv.synthFun("f1", [x2], tm.getBooleanSort())
    slv.synthFun("", [], tm.getBooleanSort())
    slv.synthFun("f1", [x], tm.getBooleanSort())

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("sygus", "true")
    slv.checkSat()
    x2 = ttm.mkVar(ttm.getBooleanSort())
    with pytest.raises(RuntimeError):
        slv.synthFun("f1", [x2], tm.getBooleanSort())
    with pytest.raises(RuntimeError):
        slv.synthFun("", [], tm.getBooleanSort())
    with pytest.raises(RuntimeError):
        slv.synthFun("f1", [x], ttm.getBooleanSort())


def test_tuple_project(tm, solver):
    elements = [\
        tm.mkBoolean(True), \
        tm.mkInteger(3),\
        tm.mkString("C"),\
        tm.mkTerm(Kind.SET_SINGLETON, tm.mkString("Z"))]

    tuple = tm.mkTuple(elements)

    indices1 = []
    indices2 = [0]
    indices3 = [0, 1]
    indices4 = [0, 0, 2, 2, 3, 3, 0]
    indices5 = [4]
    indices6 = [0, 4]

    tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices1), tuple)

    tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices2), tuple)

    tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices3), tuple)

    tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices4), tuple)

    with pytest.raises(RuntimeError):
        tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices5), tuple)
    with pytest.raises(RuntimeError):
        tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices6), tuple)

    indices = [0, 3, 2, 0, 1, 2]

    op = tm.mkOp(Kind.TUPLE_PROJECT, *indices)
    projection = tm.mkTerm(op, tuple)

    datatype = tuple.getSort().getDatatype()
    constructor = datatype[0]

    for i in indices:

        selectorTerm = constructor[i].getTerm()
        selectedTerm = tm.mkTerm(Kind.APPLY_SELECTOR, selectorTerm, tuple)
        simplifiedTerm = solver.simplify(selectedTerm)
        assert elements[i] == simplifiedTerm

        assert "((_ tuple.project 0 3 2 0 1 2) "\
               "(tuple true 3 \"C\" (set.singleton \"Z\")))" == \
               str(projection)


def test_get_data_type_arity(tm, solver):
  ctor1 = tm.mkDatatypeConstructorDecl("_x21")
  ctor2 = tm.mkDatatypeConstructorDecl("_x31")
  s3 = solver.declareDatatype("_x17", ctor1, ctor2)
  assert s3.getDatatypeArity() == 0


def test_get_unsat_core_lemmas1(tm, solver):
  solver.setOption("produce-unsat-cores", "true")
  solver.setOption("unsat-cores-mode", "sat-proof")
  # cannot ask before a check sat
  with pytest.raises(RuntimeError):
      solver.getUnsatCoreLemmas()

  solver.assertFormula(tm.mkFalse())
  assert solver.checkSat().isUnsat()
  solver.getUnsatCoreLemmas()


def test_get_unsat_core_lemmas2(tm, solver):
  solver.setOption("produce-unsat-cores", "true")
  solver.setOption("unsat-cores-mode", "sat-proof")
  uSort = tm.mkUninterpretedSort("u")
  intSort = tm.getIntegerSort()
  boolSort = solver.getBooleanSort()
  uToIntSort = tm.mkFunctionSort(uSort, intSort)
  intPredSort = tm.mkFunctionSort(intSort, boolSort)

  x = tm.mkConst(uSort, "x")
  y = tm.mkConst(uSort, "y")
  f = tm.mkConst(uToIntSort, "f")
  p = tm.mkConst(intPredSort, "p")
  zero = tm.mkInteger(0)
  one = tm.mkInteger(1)
  f_x = tm.mkTerm(Kind.APPLY_UF, f, x)
  f_y = tm.mkTerm(Kind.APPLY_UF, f, y)
  summ = tm.mkTerm(Kind.ADD, f_x, f_y)
  p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero)
  p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y)
  solver.assertFormula(tm.mkTerm(Kind.GT, zero, f_x))
  solver.assertFormula(tm.mkTerm(Kind.GT, zero, f_y))
  solver.assertFormula(tm.mkTerm(Kind.GT, summ, one))
  solver.assertFormula(p_0)
  solver.assertFormula(p_f_y.notTerm())
  assert solver.checkSat().isUnsat()
  solver.getUnsatCoreLemmas()

def test_get_difficulty(solver):
  solver.setOption("produce-difficulty", "true")
  # cannot ask before a check sat
  with pytest.raises(RuntimeError):
      solver.getDifficulty()
  solver.checkSat()
  solver.getDifficulty()

def test_get_difficulty2(solver):
  solver.checkSat()
  with pytest.raises(RuntimeError):
  # option is not set
      solver.getDifficulty()

def test_get_difficulty3(tm, solver):
  solver.setOption("produce-difficulty", "true")
  intSort = tm.getIntegerSort()
  x = tm.mkConst(intSort, "x")
  zero = tm.mkInteger(0)
  ten = tm.mkInteger(10)
  f0 = tm.mkTerm(Kind.GEQ, x, ten)
  f1 = tm.mkTerm(Kind.GEQ, zero, x)
  solver.checkSat()
  dmap = solver.getDifficulty()
  # difficulty should map assertions to integer values
  for key, value in dmap.items():
    assert key == f0 or key == f1
    assert value.getKind() == Kind.CONST_INTEGER

def test_get_model(tm, solver):
    solver.setOption("produce-models", "true")
    uSort = tm.mkUninterpretedSort("u")
    x = tm.mkConst(uSort, "x")
    y = tm.mkConst(uSort, "y")
    z = tm.mkConst(uSort, "z")
    f = tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, x, y));
    solver.assertFormula(f)
    solver.checkSat()
    sorts = [uSort]
    terms = [x, y]
    solver.getModel(sorts, terms)

def test_get_model2(solver):
    solver.setOption("produce-models", "true")
    sorts = []
    terms = []
    with pytest.raises(RuntimeError):
        solver.getModel(sorts, terms)

def test_get_model_3(tm, solver):
    solver.setOption("produce-models", "true")
    sorts = []
    terms = []
    solver.checkSat()
    solver.getModel(sorts, terms)
    integer = tm.getIntegerSort()
    sorts += [integer]
    with pytest.raises(RuntimeError):
        solver.getModel(sorts, terms)

def test_get_option_names(solver):
    names = solver.getOptionNames()
    assert len(names) > 100
    assert "verbose" in names
    assert "foobar" not in names

def test_get_quantifier_elimination(tm, solver):
    x = tm.mkVar(solver.getBooleanSort(), "x")
    forall = tm.mkTerm(
            Kind.FORALL,
            tm.mkTerm(Kind.VARIABLE_LIST, x),
            tm.mkTerm(Kind.OR, x, tm.mkTerm(Kind.NOT, x)))
    with pytest.raises(RuntimeError):
        solver.getQuantifierElimination(tm.mkBoolean(False))
    solver.getQuantifierElimination(forall)

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("produce-models", "true")
    slv.checkSat()
    xx = tm.mkVar(tm.getBooleanSort(), "x")
    fforall = tm.mkTerm(
            Kind.FORALL,
            tm.mkTerm(Kind.VARIABLE_LIST, xx),
            tm.mkTerm(Kind.OR, xx, tm.mkTerm(Kind.NOT, xx)))
    with pytest.raises(RuntimeError):
        slv.getQuantifierElimination(fforall)


def test_get_quantifier_elimination_disjunct(tm, solver):
    x = tm.mkVar(solver.getBooleanSort(), "x")
    forall = tm.mkTerm(
            Kind.FORALL,
            tm.mkTerm(Kind.VARIABLE_LIST, x),
            tm.mkTerm(Kind.OR, x, tm.mkTerm(Kind.NOT, x)))
    with pytest.raises(RuntimeError):
        solver.getQuantifierEliminationDisjunct(tm.mkBoolean(False))
    solver.getQuantifierEliminationDisjunct(forall)

    ttm = TermManager()
    slv = Solver(ttm)
    slv.setOption("produce-models", "true")
    slv.checkSat()
    xx = tm.mkVar(tm.getBooleanSort(), "x")
    fforall = tm.mkTerm(
            Kind.FORALL,
            tm.mkTerm(Kind.VARIABLE_LIST, xx),
            tm.mkTerm(Kind.OR, xx, tm.mkTerm(Kind.NOT, xx)))
    with pytest.raises(RuntimeError):
        slv.getQuantifierEliminationDisjunct(fforall)


def test_get_version(solver):
    print(solver.getVersion())

class PluginUnsat(Plugin):
    def __init__(self, tm):
        super().__init__(tm)
        self.tm = tm

    def check(self):
        lemmas = [self.tm.mkBoolean(False)]
        return lemmas

    def getName(self):
        return "PluginUnsat"

def test_plugin_unsat(tm, solver):
    p = PluginUnsat(tm)
    solver.addPlugin(p)
    assert solver.checkSat().isUnsat()


class PluginListen(Plugin):
    def __init__(self, tm):
        super().__init__(tm)
        self.has_seen_theory_lemma = False
        self.has_seen_sat_clause = False

    def notifySatClause(self, cl):
        super().notifySatClause(cl)
        self.has_seen_sat_clause = True

    def hasSeenSatClause(self):
        return self.has_seen_sat_clause

    def notifyTheoryLemma(self, lem):
        super().notifyTheoryLemma(lem)
        self.has_seen_theory_lemma = True

    def hasSeenTheoryLemma(self):
        return self.has_seen_theory_lemma

    def getName(self):
        return "PluginListen"

def test_plugin_listen(tm, solver):
    # NOTE: this shouldn't be necessary but ensures notifySatClause is called here.
    solver.setOption("plugin-notify-sat-clause-in-solve", "false")
    pl = PluginListen(tm)
    solver.addPlugin(pl)
    stringSort = tm.getStringSort()
    x = tm.mkConst(stringSort, "x")
    y = tm.mkConst(stringSort, "y")
    ctn1 = tm.mkTerm(Kind.STRING_CONTAINS, x, y)
    ctn2 = tm.mkTerm(Kind.STRING_CONTAINS, y, x)
    solver.assertFormula(tm.mkTerm(Kind.OR, ctn1, ctn2))
    lx = tm.mkTerm(Kind.STRING_LENGTH, x)
    ly = tm.mkTerm(Kind.STRING_LENGTH, y)
    lc = tm.mkTerm(Kind.GT, lx, ly)
    solver.assertFormula(lc)
    assert solver.checkSat().isSat()
    # above input formulas should induce a theory lemma and SAT clause learning
    assert pl.hasSeenTheoryLemma()
    assert pl.hasSeenSatClause()