mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
430c11f879
This PR makes it so that common users of the datatypes API do not need to use "unresolved" datatypes sorts. Instead, these are automatically inferred by the NodeManager when calling mkMutualDatatypeTypes. API Changes: (1) adds addSelectorUnresolved to DatatypeConstructorDecl, which is the sole method needed to specify ordinary recursive selectors. (2) adds to unit test examples that use this variant instead of using unresolved sorts. (3) the API method mkUnresolvedSort is renamed to mkUnresolvedDatatypeSort and is marked experimental. Note that unresolved datatype sorts are still needed to support mixed parametric datatypes and nested recursive datatypes in the smt2 parser, so they cannot be deleted yet. Followup PR will add to documentation on elaborate further on how to use the datatypes API.
2955 lines
115 KiB
Java
2955 lines
115 KiB
Java
/******************************************************************************
|
|
* 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 tests;
|
|
|
|
import static io.github.cvc5.Kind.*;
|
|
import static io.github.cvc5.RoundingMode.*;
|
|
import static org.junit.jupiter.api.Assertions.*;
|
|
|
|
import io.github.cvc5.*;
|
|
import io.github.cvc5.modes.BlockModelsMode;
|
|
import java.math.BigInteger;
|
|
import java.util.*;
|
|
import java.util.concurrent.atomic.AtomicReference;
|
|
import org.junit.jupiter.api.*;
|
|
import org.junit.jupiter.api.function.Executable;
|
|
|
|
class SolverTest
|
|
{
|
|
private Solver d_solver;
|
|
|
|
@BeforeEach
|
|
void setUp()
|
|
{
|
|
d_solver = new Solver();
|
|
}
|
|
|
|
@AfterEach
|
|
void tearDown()
|
|
{
|
|
d_solver.close();
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@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.mkUnresolvedDatatypeSort("ulist", 1);
|
|
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)));
|
|
|
|
assertThrows(CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls)));
|
|
slv.close();
|
|
|
|
/* mutually recursive with unresolved parameterized sorts */
|
|
Sort p0 = d_solver.mkParamSort("p0");
|
|
Sort p1 = d_solver.mkParamSort("p1");
|
|
Sort u0 = d_solver.mkUnresolvedDatatypeSort("dt0", 1);
|
|
Sort u1 = d_solver.mkUnresolvedDatatypeSort("dt1", 1);
|
|
DatatypeDecl dtdecl0 = d_solver.mkDatatypeDecl("dt0", p0);
|
|
DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("dt1", p1);
|
|
DatatypeConstructorDecl ctordecl0 = d_solver.mkDatatypeConstructorDecl("c0");
|
|
ctordecl0.addSelector("s0", u1.instantiate(new Sort[] {p0}));
|
|
DatatypeConstructorDecl ctordecl1 = d_solver.mkDatatypeConstructorDecl("c1");
|
|
ctordecl1.addSelector("s1", u0.instantiate(new Sort[] {p1}));
|
|
dtdecl0.addConstructor(ctordecl0);
|
|
dtdecl1.addConstructor(ctordecl1);
|
|
Sort[] dt_sorts = d_solver.mkDatatypeSorts(new DatatypeDecl[] {dtdecl0, dtdecl1});
|
|
Sort isort1 = dt_sorts[1].instantiate(new Sort[] {d_solver.getBooleanSort()});
|
|
Term t1 = d_solver.mkConst(isort1, "t");
|
|
Term t0 = d_solver.mkTerm(APPLY_SELECTOR,
|
|
t1.getSort().getDatatype().getConstructor("c1").getSelector("s1").getSelectorTerm(),
|
|
t1);
|
|
assertEquals(dt_sorts[0].instantiate(new Sort[] {d_solver.getBooleanSort()}), t0.getSort());
|
|
|
|
/* 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()));
|
|
slv.close();
|
|
}
|
|
|
|
@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()}));
|
|
slv.close();
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@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)));
|
|
slv.close();
|
|
}
|
|
|
|
@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)));
|
|
slv.close();
|
|
}
|
|
|
|
@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()));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void mkUninterpretedSort() throws CVC5ApiException
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkUninterpretedSort("u"));
|
|
assertDoesNotThrow(() -> d_solver.mkUninterpretedSort(""));
|
|
}
|
|
|
|
@Test
|
|
void mkUnresolvedDatatypeSort() throws CVC5ApiException
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort("u"));
|
|
assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort("u", 1));
|
|
assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort(""));
|
|
assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort("", 1));
|
|
}
|
|
|
|
@Test
|
|
void mkUninterpretedSortConstructorSort() throws CVC5ApiException
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort(2, "s"));
|
|
assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort(2));
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.mkUninterpretedSortConstructorSort(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()}));
|
|
slv.close();
|
|
}
|
|
|
|
@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"));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void mkBoolean() throws CVC5ApiException
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkBoolean(true));
|
|
assertDoesNotThrow(() -> d_solver.mkBoolean(false));
|
|
}
|
|
|
|
@Test
|
|
void mkRoundingMode() throws CVC5ApiException
|
|
{
|
|
assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).toString(),
|
|
"roundNearestTiesToEven");
|
|
assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE).toString(),
|
|
"roundTowardPositive");
|
|
assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE).toString(),
|
|
"roundTowardNegative");
|
|
assertEquals(
|
|
d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO).toString(), "roundTowardZero");
|
|
assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY).toString(),
|
|
"roundNearestTiesToAway");
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void mkCardinalityConstraint() throws CVC5ApiException
|
|
{
|
|
Sort su = d_solver.mkUninterpretedSort("u");
|
|
Sort si = d_solver.getIntegerSort();
|
|
assertDoesNotThrow(() -> d_solver.mkCardinalityConstraint(su, 3));
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(si, 3));
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(su, 0));
|
|
Solver slv = new Solver();
|
|
assertThrows(CVC5ApiException.class, () -> slv.mkCardinalityConstraint(su, 3));
|
|
slv.close();
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void mkFalse() throws CVC5ApiException
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkFalse());
|
|
assertDoesNotThrow(() -> d_solver.mkFalse());
|
|
}
|
|
|
|
@Test
|
|
void mkFloatingPointNaN() throws CVC5ApiException
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkFloatingPointNaN(3, 5));
|
|
}
|
|
|
|
@Test
|
|
void mkFloatingPointNegZero() throws CVC5ApiException
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkFloatingPointNegZero(3, 5));
|
|
}
|
|
|
|
@Test
|
|
void mkFloatingPointNegInf()
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkFloatingPointNegInf(3, 5));
|
|
}
|
|
|
|
@Test
|
|
void mkFloatingPointPosInf()
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkFloatingPointPosInf(3, 5));
|
|
}
|
|
|
|
@Test
|
|
void mkFloatingPointPosZero()
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkFloatingPointPosZero(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 mkRegexpNone()
|
|
{
|
|
Sort strSort = d_solver.getStringSort();
|
|
Term s = d_solver.mkConst(strSort, "s");
|
|
assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone()));
|
|
}
|
|
|
|
@Test
|
|
void mkRegexpAll()
|
|
{
|
|
Sort strSort = d_solver.getStringSort();
|
|
Term s = d_solver.mkConst(strSort, "s");
|
|
assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll()));
|
|
}
|
|
|
|
@Test
|
|
void mkRegexpAllchar()
|
|
{
|
|
Sort strSort = d_solver.getStringSort();
|
|
Term s = d_solver.mkConst(strSort, "s");
|
|
assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar()));
|
|
}
|
|
|
|
@Test
|
|
void mkSepEmp()
|
|
{
|
|
assertDoesNotThrow(() -> d_solver.mkSepEmp());
|
|
}
|
|
|
|
@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()));
|
|
slv.close();
|
|
}
|
|
|
|
@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_NONE));
|
|
assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_ALLCHAR));
|
|
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));
|
|
slv.close();
|
|
}
|
|
|
|
@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 consTerm = list.getConstructor("cons").getConstructorTerm();
|
|
Term nilTerm = 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, nilTerm));
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, nilTerm));
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, consTerm));
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm));
|
|
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, nilTerm));
|
|
|
|
// 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, consTerm, 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,
|
|
consTerm,
|
|
d_solver.mkInteger(0),
|
|
d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm)));
|
|
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,
|
|
consTerm,
|
|
d_solver.mkInteger(0),
|
|
d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm)));
|
|
|
|
// 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));
|
|
slv.close();
|
|
}
|
|
|
|
@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)}));
|
|
slv.close();
|
|
}
|
|
|
|
@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()));
|
|
slv.close();
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@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));
|
|
slv.close();
|
|
}
|
|
|
|
@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 funSort =
|
|
d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
|
|
Term b1 = d_solver.mkVar(bvSort, "b1");
|
|
Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
|
|
Term b3 = d_solver.mkVar(funSort, "b3");
|
|
Term v1 = d_solver.mkConst(bvSort, "v1");
|
|
Term v2 = d_solver.mkConst(funSort, "v2");
|
|
assertDoesNotThrow(() -> d_solver.defineFun("f", new Term[] {}, bvSort, v1));
|
|
assertDoesNotThrow(() -> d_solver.defineFun("ff", new Term[] {b1, b2}, bvSort, 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, v2));
|
|
assertThrows(
|
|
CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort, v2));
|
|
|
|
// b3 has function sort, which is allowed as an argument
|
|
assertDoesNotThrow(() -> d_solver.defineFun("fffff", new Term[] {b1, b3}, bvSort, 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));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void defineFunGlobal()
|
|
{
|
|
Sort bSort = d_solver.getBooleanSort();
|
|
|
|
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");
|
|
// (define-fun g (b Bool) Bool b)
|
|
Term g = d_solver.defineFun("g", new Term[] {b}, bSort, 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));
|
|
slv.close();
|
|
}
|
|
|
|
@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}));
|
|
slv.close();
|
|
}
|
|
|
|
@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 getAbduct() throws CVC5ApiException
|
|
{
|
|
d_solver.setLogic("QF_LIA");
|
|
d_solver.setOption("produce-abducts", "true");
|
|
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");
|
|
|
|
// Assumptions for abduction: x > 0
|
|
d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
|
|
// Conjecture for abduction: y > 0
|
|
Term conj = d_solver.mkTerm(GT, y, zero);
|
|
Term output = d_solver.getNullTerm();
|
|
// Call the abduction api, while the resulting abduct is the output
|
|
output = d_solver.getAbduct(conj);
|
|
// We expect the resulting output to be a boolean formula
|
|
assertTrue(!output.isNull() && output.getSort().isBoolean());
|
|
|
|
// try with a grammar, a simple grammar admitting true
|
|
Sort bsort = d_solver.getBooleanSort();
|
|
Term truen = d_solver.mkBoolean(true);
|
|
Term start = d_solver.mkVar(bsort);
|
|
Term output2 = d_solver.getNullTerm();
|
|
Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
|
|
Term conj2 = d_solver.mkTerm(GT, x, zero);
|
|
assertDoesNotThrow(() -> g.addRule(start, truen));
|
|
// Call the abduction api, while the resulting abduct is the output
|
|
output2 = d_solver.getAbduct(conj2, g);
|
|
// abduct must be true
|
|
assertEquals(output2, truen);
|
|
}
|
|
|
|
@Test
|
|
void getAbduct2() throws CVC5ApiException
|
|
{
|
|
d_solver.setLogic("QF_LIA");
|
|
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");
|
|
// Assumptions for abduction: x > 0
|
|
d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
|
|
// Conjecture for abduction: y > 0
|
|
Term conj = d_solver.mkTerm(GT, y, zero);
|
|
Term output = d_solver.getNullTerm();
|
|
// Fails due to option not set
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.getAbduct(conj));
|
|
}
|
|
|
|
@Test
|
|
void getAbductNext() throws CVC5ApiException
|
|
{
|
|
d_solver.setLogic("QF_LIA");
|
|
d_solver.setOption("produce-abducts", "true");
|
|
d_solver.setOption("incremental", "true");
|
|
|
|
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");
|
|
|
|
// Assumptions for abduction: x > 0
|
|
d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
|
|
// Conjecture for abduction: y > 0
|
|
Term conj = d_solver.mkTerm(GT, y, zero);
|
|
// Call the abduction api, while the resulting abduct is the output
|
|
Term output = d_solver.getAbduct(conj);
|
|
Term output2 = d_solver.getAbductNext();
|
|
// should produce a different output
|
|
assertNotEquals(output, output2);
|
|
}
|
|
|
|
@Test
|
|
void getInterpolant() throws CVC5ApiException
|
|
{
|
|
d_solver.setLogic("QF_LIA");
|
|
d_solver.setOption("produce-interpolants", "true");
|
|
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(ADD, 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(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero));
|
|
// Call the interpolation api, while the resulting interpolant is the output
|
|
Term output = d_solver.getInterpolant(conj);
|
|
|
|
// We expect the resulting output to be a boolean formula
|
|
assertTrue(output.getSort().isBoolean());
|
|
}
|
|
|
|
@Test
|
|
void getInterpolantNext() throws CVC5ApiException
|
|
{
|
|
d_solver.setLogic("QF_LIA");
|
|
d_solver.setOption("produce-interpolants", "true");
|
|
d_solver.setOption("incremental", "true");
|
|
|
|
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");
|
|
|
|
d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(ADD, x, y), zero));
|
|
d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
|
|
Term conj = d_solver.mkTerm(
|
|
OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero));
|
|
Term output = d_solver.getInterpolant(conj);
|
|
Term output2 = d_solver.getInterpolantNext();
|
|
|
|
// We expect the next output to be distinct
|
|
assertNotEquals(output, output2);
|
|
}
|
|
|
|
@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.getConstructor("cons").getConstructorTerm();
|
|
Term nilTerm = consList.getConstructor("nil").getConstructorTerm();
|
|
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 getOptionNames()
|
|
{
|
|
String[] names = d_solver.getOptionNames();
|
|
assertTrue(names.length > 100);
|
|
assertTrue(Arrays.asList(names).contains("verbose"));
|
|
assertFalse(Arrays.asList(names).contains("foobar"));
|
|
}
|
|
|
|
@Test
|
|
void getOptionInfo()
|
|
{
|
|
List<Executable> assertions = new ArrayList<>();
|
|
{
|
|
assertions.add(
|
|
() -> assertThrows(CVC5ApiException.class, () -> d_solver.getOptionInfo("asdf-invalid")));
|
|
}
|
|
{
|
|
OptionInfo info = d_solver.getOptionInfo("verbose");
|
|
assertions.add(() -> assertEquals("verbose", info.getName()));
|
|
assertions.add(
|
|
() -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases())));
|
|
assertions.add(() -> assertTrue(info.getBaseInfo() instanceof OptionInfo.VoidInfo));
|
|
assertions.add(() -> assertEquals(info.toString(), "OptionInfo{ verbose | void }"));
|
|
}
|
|
{
|
|
// bool type with default
|
|
OptionInfo info = d_solver.getOptionInfo("print-success");
|
|
assertions.add(() -> assertEquals("print-success", info.getName()));
|
|
assertions.add(
|
|
() -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases())));
|
|
assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ValueInfo.class));
|
|
OptionInfo.ValueInfo<Boolean> valInfo = (OptionInfo.ValueInfo<Boolean>) info.getBaseInfo();
|
|
assertions.add(() -> assertEquals(false, valInfo.getDefaultValue().booleanValue()));
|
|
assertions.add(() -> assertEquals(false, valInfo.getCurrentValue().booleanValue()));
|
|
assertions.add(() -> assertEquals(info.booleanValue(), false));
|
|
assertions.add(()
|
|
-> assertEquals(info.toString(),
|
|
"OptionInfo{ print-success | bool | false | default false }"));
|
|
}
|
|
{
|
|
// int64 type with default
|
|
OptionInfo info = d_solver.getOptionInfo("verbosity");
|
|
assertions.add(() -> assertEquals("verbosity", info.getName()));
|
|
assertions.add(
|
|
() -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases())));
|
|
assertions.add(
|
|
() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.NumberInfo.class));
|
|
OptionInfo.NumberInfo<BigInteger> numInfo =
|
|
(OptionInfo.NumberInfo<BigInteger>) info.getBaseInfo();
|
|
assertions.add(() -> assertEquals(0, numInfo.getDefaultValue().intValue()));
|
|
assertions.add(() -> assertEquals(0, numInfo.getCurrentValue().intValue()));
|
|
assertions.add(
|
|
() -> assertTrue(numInfo.getMinimum() == null && numInfo.getMaximum() == null));
|
|
assertions.add(() -> assertEquals(info.intValue().intValue(), 0));
|
|
assertions.add(
|
|
() -> assertEquals(info.toString(), "OptionInfo{ verbosity | int64_t | 0 | default 0 }"));
|
|
}
|
|
assertAll(assertions);
|
|
{
|
|
OptionInfo info = d_solver.getOptionInfo("rlimit");
|
|
assertEquals(info.getName(), "rlimit");
|
|
assertEquals(Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
|
|
assertTrue(info.getBaseInfo().getClass() == OptionInfo.NumberInfo.class);
|
|
OptionInfo.NumberInfo<BigInteger> ni = (OptionInfo.NumberInfo<BigInteger>) info.getBaseInfo();
|
|
assertEquals(ni.getCurrentValue().intValue(), 0);
|
|
assertEquals(ni.getDefaultValue().intValue(), 0);
|
|
assertTrue(ni.getMinimum() == null && ni.getMaximum() == null);
|
|
assertEquals(info.intValue().intValue(), 0);
|
|
assertEquals(info.toString(), "OptionInfo{ rlimit | uint64_t | 0 | default 0 }");
|
|
}
|
|
{
|
|
OptionInfo info = d_solver.getOptionInfo("random-freq");
|
|
assertEquals(info.getName(), "random-freq");
|
|
assertEquals(
|
|
Arrays.asList(info.getAliases()), Arrays.asList(new String[] {"random-frequency"}));
|
|
assertTrue(info.getBaseInfo().getClass() == OptionInfo.NumberInfo.class);
|
|
OptionInfo.NumberInfo<Double> ni = (OptionInfo.NumberInfo<Double>) info.getBaseInfo();
|
|
assertEquals(ni.getCurrentValue(), 0.0);
|
|
assertEquals(ni.getDefaultValue(), 0.0);
|
|
assertTrue(ni.getMinimum() != null && ni.getMaximum() != null);
|
|
assertEquals(ni.getMinimum(), 0.0);
|
|
assertEquals(ni.getMaximum(), 1.0);
|
|
assertEquals(info.doubleValue(), 0.0);
|
|
assertEquals(info.toString(),
|
|
"OptionInfo{ random-freq, random-frequency | double | 0 | default 0 | 0 <= x <= 1 }");
|
|
}
|
|
{
|
|
OptionInfo info = d_solver.getOptionInfo("force-logic");
|
|
assertEquals(info.getName(), "force-logic");
|
|
assertEquals(Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
|
|
assertTrue(info.getBaseInfo().getClass() == OptionInfo.ValueInfo.class);
|
|
OptionInfo.ValueInfo<String> ni = (OptionInfo.ValueInfo<String>) info.getBaseInfo();
|
|
assertEquals(ni.getCurrentValue(), "");
|
|
assertEquals(ni.getDefaultValue(), "");
|
|
assertEquals(info.stringValue(), "");
|
|
assertEquals(info.toString(), "OptionInfo{ force-logic | string | \"\" | default \"\" }");
|
|
}
|
|
{
|
|
// mode option
|
|
OptionInfo info = d_solver.getOptionInfo("simplification");
|
|
assertions.clear();
|
|
assertions.add(() -> assertEquals("simplification", info.getName()));
|
|
assertions.add(()
|
|
-> assertEquals(Arrays.asList(new String[] {"simplification-mode"}),
|
|
Arrays.asList(info.getAliases())));
|
|
assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ModeInfo.class));
|
|
OptionInfo.ModeInfo modeInfo = (OptionInfo.ModeInfo) info.getBaseInfo();
|
|
assertions.add(() -> assertEquals("batch", modeInfo.getDefaultValue()));
|
|
assertions.add(() -> assertEquals("batch", modeInfo.getCurrentValue()));
|
|
assertions.add(() -> assertEquals(2, modeInfo.getModes().length));
|
|
assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("batch")));
|
|
assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("none")));
|
|
assertEquals(info.toString(),
|
|
"OptionInfo{ simplification, simplification-mode | mode | batch | default batch | modes: batch, none }");
|
|
}
|
|
assertAll(assertions);
|
|
}
|
|
|
|
@Test
|
|
void getStatistics()
|
|
{
|
|
// do some array reasoning to make sure we have a double statistics
|
|
{
|
|
Sort s1 = d_solver.getIntegerSort();
|
|
Sort s2 = d_solver.mkArraySort(s1, s1);
|
|
Term t1 = d_solver.mkConst(s1, "i");
|
|
Term t2 = d_solver.mkVar(s2, "a");
|
|
Term t3 = d_solver.mkTerm(Kind.SELECT, t2, t1);
|
|
d_solver.checkSat();
|
|
}
|
|
Statistics stats = d_solver.getStatistics();
|
|
stats.toString();
|
|
{
|
|
Stat s = stats.get("global::totalTime");
|
|
assertFalse(s.isInternal());
|
|
assertFalse(s.isDefault());
|
|
assertTrue(s.isString());
|
|
assertTrue(s.getString().endsWith("ms"));
|
|
s = stats.get("resource::resourceUnitsUsed");
|
|
assertTrue(s.isInternal());
|
|
assertFalse(s.isDefault());
|
|
assertTrue(s.isInt());
|
|
assertTrue(s.getInt() >= 0);
|
|
}
|
|
for (Map.Entry<String, Stat> s : stats)
|
|
{
|
|
assertFalse(s.getKey().isEmpty());
|
|
}
|
|
for (Statistics.ConstIterator it = stats.iterator(true, true); it.hasNext();)
|
|
{
|
|
Map.Entry<String, Stat> elem = it.next();
|
|
if (elem.getKey() == "cvc5::CONSTANT")
|
|
{
|
|
assertFalse(elem.getValue().isInternal());
|
|
assertFalse(elem.getValue().isDefault());
|
|
assertTrue(elem.getValue().isHistogram());
|
|
Map<String, Long> hist = elem.getValue().getHistogram();
|
|
assertFalse(hist.isEmpty());
|
|
assertEquals(elem.getValue().toString(), "{ integer type: 1 }");
|
|
}
|
|
else if (elem.getKey() == "theory::arrays::avgIndexListLength")
|
|
{
|
|
assertTrue(elem.getValue().isInternal());
|
|
assertTrue(elem.getValue().isDefault());
|
|
}
|
|
}
|
|
}
|
|
|
|
@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 getUnsatCoreAndProof()
|
|
{
|
|
d_solver.setOption("incremental", "true");
|
|
d_solver.setOption("produce-unsat-cores", "true");
|
|
d_solver.setOption("produce-proofs", "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 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(Kind.APPLY_UF, f, x);
|
|
Term f_y = d_solver.mkTerm(Kind.APPLY_UF, f, y);
|
|
Term sum = d_solver.mkTerm(Kind.ADD, f_x, f_y);
|
|
Term p_0 = d_solver.mkTerm(Kind.APPLY_UF, p, zero);
|
|
Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
|
|
d_solver.assertFormula(d_solver.mkTerm(Kind.GT, zero, f_x));
|
|
d_solver.assertFormula(d_solver.mkTerm(Kind.GT, zero, f_y));
|
|
d_solver.assertFormula(d_solver.mkTerm(Kind.GT, sum, one));
|
|
d_solver.assertFormula(p_0);
|
|
d_solver.assertFormula(p_f_y.notTerm());
|
|
assertTrue(d_solver.checkSat().isUnsat());
|
|
|
|
Term[] unsat_core = d_solver.getUnsatCore();
|
|
|
|
assertDoesNotThrow(() -> d_solver.getProof());
|
|
|
|
d_solver.resetAssertions();
|
|
for (Term t : unsat_core)
|
|
{
|
|
d_solver.assertFormula(t);
|
|
}
|
|
Result res = d_solver.checkSat();
|
|
assertTrue(res.isUnsat());
|
|
assertDoesNotThrow(() -> d_solver.getProof());
|
|
}
|
|
|
|
@Test
|
|
void getDifficulty()
|
|
{
|
|
d_solver.setOption("produce-difficulty", "true");
|
|
// cannot ask before a check sat
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.getDifficulty());
|
|
d_solver.checkSat();
|
|
assertDoesNotThrow(() -> d_solver.getDifficulty());
|
|
}
|
|
|
|
@Test
|
|
void getDifficulty2()
|
|
{
|
|
d_solver.checkSat();
|
|
// option is not set
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.getDifficulty());
|
|
}
|
|
|
|
@Test
|
|
void getDifficulty3() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("produce-difficulty", "true");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term ten = d_solver.mkInteger(10);
|
|
Term f0 = d_solver.mkTerm(GEQ, x, ten);
|
|
Term f1 = d_solver.mkTerm(GEQ, zero, x);
|
|
d_solver.assertFormula(f0);
|
|
d_solver.assertFormula(f1);
|
|
d_solver.checkSat();
|
|
Map<Term, Term> dmap = d_solver.getDifficulty();
|
|
// difficulty should map assertions to integer values
|
|
for (Map.Entry<Term, Term> t : dmap.entrySet())
|
|
{
|
|
assertTrue(t.getKey() == f0 || t.getKey() == f1);
|
|
assertTrue(t.getValue().getKind() == Kind.CONST_RATIONAL);
|
|
}
|
|
}
|
|
|
|
@Test
|
|
void getLearnedLiterals()
|
|
{
|
|
d_solver.setOption("produce-learned-literals", "true");
|
|
// cannot ask before a check sat
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.getLearnedLiterals());
|
|
d_solver.checkSat();
|
|
assertDoesNotThrow(() -> d_solver.getLearnedLiterals());
|
|
}
|
|
|
|
@Test
|
|
void getLearnedLiterals2()
|
|
{
|
|
d_solver.setOption("produce-learned-literals", "true");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term y = d_solver.mkConst(intSort, "y");
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term ten = d_solver.mkInteger(10);
|
|
Term f0 = d_solver.mkTerm(GEQ, x, ten);
|
|
Term f1 = d_solver.mkTerm(OR, d_solver.mkTerm(GEQ, zero, x), d_solver.mkTerm(GEQ, y, zero));
|
|
d_solver.assertFormula(f0);
|
|
d_solver.assertFormula(f1);
|
|
d_solver.checkSat();
|
|
assertDoesNotThrow(() -> d_solver.getLearnedLiterals());
|
|
}
|
|
|
|
@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(ADD, 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));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void getModelDomainElements()
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
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.mkTerm(DISTINCT, x, y, z);
|
|
d_solver.assertFormula(f);
|
|
d_solver.checkSat();
|
|
assertDoesNotThrow(() -> d_solver.getModelDomainElements(uSort));
|
|
assertTrue(d_solver.getModelDomainElements(uSort).length >= 3);
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.getModelDomainElements(intSort));
|
|
}
|
|
|
|
@Test
|
|
void getModelDomainElements2()
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
d_solver.setOption("finite-model-find", "true");
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Term x = d_solver.mkVar(uSort, "x");
|
|
Term y = d_solver.mkVar(uSort, "y");
|
|
Term eq = d_solver.mkTerm(EQUAL, x, y);
|
|
Term bvl = d_solver.mkTerm(VARIABLE_LIST, x, y);
|
|
Term f = d_solver.mkTerm(FORALL, bvl, eq);
|
|
d_solver.assertFormula(f);
|
|
d_solver.checkSat();
|
|
assertDoesNotThrow(() -> d_solver.getModelDomainElements(uSort));
|
|
// a model for the above must interpret u as size 1
|
|
assertTrue(d_solver.getModelDomainElements(uSort).length == 1);
|
|
}
|
|
|
|
@Test
|
|
void isModelCoreSymbol()
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
d_solver.setOption("model-cores", "simple");
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Term x = d_solver.mkConst(uSort, "x");
|
|
Term y = d_solver.mkConst(uSort, "y");
|
|
Term z = d_solver.mkConst(uSort, "z");
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term f = d_solver.mkTerm(NOT, d_solver.mkTerm(EQUAL, x, y));
|
|
d_solver.assertFormula(f);
|
|
d_solver.checkSat();
|
|
assertTrue(d_solver.isModelCoreSymbol(x));
|
|
assertTrue(d_solver.isModelCoreSymbol(y));
|
|
assertFalse(d_solver.isModelCoreSymbol(z));
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.isModelCoreSymbol(zero));
|
|
}
|
|
|
|
@Test
|
|
void getModel()
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
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.mkTerm(NOT, d_solver.mkTerm(EQUAL, x, y));
|
|
d_solver.assertFormula(f);
|
|
d_solver.checkSat();
|
|
Sort[] sorts = new Sort[] {uSort};
|
|
Term[] terms = new Term[] {x, y};
|
|
assertDoesNotThrow(() -> d_solver.getModel(sorts, terms));
|
|
Term nullTerm = d_solver.getNullTerm();
|
|
Term[] terms2 = new Term[] {x, y, nullTerm};
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts, terms2));
|
|
}
|
|
|
|
@Test
|
|
void getModel2()
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Sort[] sorts = new Sort[] {};
|
|
Term[] terms = new Term[] {};
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts, terms));
|
|
}
|
|
|
|
@Test
|
|
void getModel3()
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Sort[] sorts = new Sort[] {};
|
|
final Term[] terms = new Term[] {};
|
|
d_solver.checkSat();
|
|
assertDoesNotThrow(() -> d_solver.getModel(sorts, terms));
|
|
Sort integer = d_solver.getIntegerSort();
|
|
Sort[] sorts2 = new Sort[] {integer};
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts2, terms));
|
|
}
|
|
|
|
@Test
|
|
void getQuantifierElimination()
|
|
{
|
|
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
|
|
Term forall = d_solver.mkTerm(
|
|
FORALL, d_solver.mkTerm(VARIABLE_LIST, x), d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
|
|
assertThrows(
|
|
CVC5ApiException.class, () -> d_solver.getQuantifierElimination(d_solver.getNullTerm()));
|
|
Solver slv = new Solver();
|
|
assertThrows(
|
|
CVC5ApiException.class, () -> d_solver.getQuantifierElimination(slv.mkBoolean(false)));
|
|
|
|
assertDoesNotThrow(() -> d_solver.getQuantifierElimination(forall));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void getQuantifierEliminationDisjunct()
|
|
{
|
|
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
|
|
Term forall = d_solver.mkTerm(
|
|
FORALL, d_solver.mkTerm(VARIABLE_LIST, x), d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
|
|
assertThrows(CVC5ApiException.class,
|
|
() -> d_solver.getQuantifierEliminationDisjunct(d_solver.getNullTerm()));
|
|
|
|
Solver slv = new Solver();
|
|
assertThrows(CVC5ApiException.class,
|
|
() -> d_solver.getQuantifierEliminationDisjunct(slv.mkBoolean(false)));
|
|
|
|
assertDoesNotThrow(() -> d_solver.getQuantifierEliminationDisjunct(forall));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void declareSepHeap() throws CVC5ApiException
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
Sort integer = d_solver.getIntegerSort();
|
|
assertDoesNotThrow(() -> d_solver.declareSepHeap(integer, integer));
|
|
// cannot declare separation logic heap more than once
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.declareSepHeap(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.declareSepHeap(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 getValueSepHeap1() 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.getValueSepHeap());
|
|
}
|
|
|
|
@Test
|
|
void getValueSepHeap2() 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.getValueSepHeap());
|
|
}
|
|
|
|
@Test
|
|
void getValueSepHeap3() 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.getValueSepHeap());
|
|
}
|
|
|
|
@Test
|
|
void getValueSepHeap4() 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.getValueSepHeap());
|
|
}
|
|
|
|
@Test
|
|
void getValueSepHeap5() throws CVC5ApiException
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "true");
|
|
checkSimpleSeparationConstraints(d_solver);
|
|
assertDoesNotThrow(() -> d_solver.getValueSepHeap());
|
|
}
|
|
|
|
@Test
|
|
void getValueSepNil1() 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.getValueSepNil());
|
|
}
|
|
|
|
@Test
|
|
void getValueSepNil2() 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.getValueSepNil());
|
|
}
|
|
|
|
@Test
|
|
void getValueSepNil3() 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.getValueSepNil());
|
|
}
|
|
|
|
@Test
|
|
void getValueSepNil4() 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.getValueSepNil());
|
|
}
|
|
|
|
@Test
|
|
void getValueSepNil5() throws CVC5ApiException
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "true");
|
|
checkSimpleSeparationConstraints(d_solver);
|
|
assertDoesNotThrow(() -> d_solver.getValueSepNil());
|
|
}
|
|
|
|
@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()
|
|
{
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x));
|
|
d_solver.checkSat();
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.blockModel(BlockModelsMode.LITERALS));
|
|
}
|
|
|
|
@Test
|
|
void blockModel2() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x));
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.blockModel(BlockModelsMode.LITERALS));
|
|
}
|
|
|
|
@Test
|
|
void blockModel3() 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();
|
|
assertDoesNotThrow(() -> d_solver.blockModel(BlockModelsMode.LITERALS));
|
|
}
|
|
|
|
@Test
|
|
void blockModelValues1() 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[] {}));
|
|
assertThrows(CVC5ApiException.class,
|
|
() -> d_solver.blockModelValues(new Term[] {d_solver.getNullTerm()}));
|
|
Solver slv = new Solver();
|
|
assertThrows(
|
|
CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {slv.mkBoolean(false)}));
|
|
slv.close();
|
|
}
|
|
|
|
@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();
|
|
assertDoesNotThrow(() -> d_solver.blockModelValues(new Term[] {x}));
|
|
}
|
|
|
|
@Test
|
|
void blockModelValues3() throws CVC5ApiException
|
|
{
|
|
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");
|
|
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");
|
|
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(ADD, 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.getConstructor("cons").getConstructorTerm(),
|
|
d_solver.mkInteger(0),
|
|
d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructor("nil").getConstructorTerm()));
|
|
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));
|
|
slv.close();
|
|
}
|
|
|
|
@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()));
|
|
slv.close();
|
|
}
|
|
|
|
@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()));
|
|
slv.close();
|
|
}
|
|
|
|
@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()));
|
|
slv.close();
|
|
}
|
|
|
|
@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(ADD, 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()));
|
|
slv.close();
|
|
}
|
|
|
|
@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 declareSygusVar() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
|
|
|
|
assertDoesNotThrow(() -> d_solver.declareSygusVar("", boolSort));
|
|
assertDoesNotThrow(() -> d_solver.declareSygusVar("", funSort));
|
|
assertDoesNotThrow(() -> d_solver.declareSygusVar(("b"), boolSort));
|
|
|
|
assertThrows(
|
|
CVC5ApiException.class, () -> d_solver.declareSygusVar("", d_solver.getNullSort()));
|
|
assertThrows(
|
|
CVC5ApiException.class, () -> d_solver.declareSygusVar("a", d_solver.getNullSort()));
|
|
|
|
Solver slv = new Solver();
|
|
slv.setOption("sygus", "true");
|
|
assertThrows(CVC5ApiException.class, () -> slv.declareSygusVar("", boolSort));
|
|
slv.close();
|
|
}
|
|
|
|
@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();
|
|
slv.setOption("sygus", "true");
|
|
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}));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void synthFun() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
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();
|
|
slv.setOption("sygus", "true");
|
|
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()));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void synthInv() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
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
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
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();
|
|
slv.setOption("sygus", "true");
|
|
assertThrows(CVC5ApiException.class, () -> slv.addSygusConstraint(boolTerm));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void addSygusAssume()
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Term nullTerm = d_solver.getNullTerm();
|
|
Term boolTerm = d_solver.mkBoolean(false);
|
|
Term intTerm = d_solver.mkInteger(1);
|
|
|
|
assertDoesNotThrow(() -> d_solver.addSygusAssume(boolTerm));
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.addSygusAssume(nullTerm));
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.addSygusAssume(intTerm));
|
|
|
|
Solver slv = new Solver();
|
|
slv.setOption("sygus", "true");
|
|
assertThrows(CVC5ApiException.class, () -> slv.addSygusAssume(boolTerm));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void addSygusInvConstraint() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
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();
|
|
slv.setOption("sygus", "true");
|
|
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));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void checkSynth() throws CVC5ApiException
|
|
{
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.checkSynth());
|
|
d_solver.setOption("sygus", "true");
|
|
assertDoesNotThrow(() -> d_solver.checkSynth());
|
|
}
|
|
|
|
@Test
|
|
void getSynthSolution() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
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));
|
|
|
|
SynthResult sr = d_solver.checkSynth();
|
|
assertEquals(sr.hasSolution(), true);
|
|
|
|
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));
|
|
slv.close();
|
|
}
|
|
|
|
@Test
|
|
void getSynthSolutions() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
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}));
|
|
slv.close();
|
|
}
|
|
@Test
|
|
void checkSynthNext() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
d_solver.setOption("incremental", "true");
|
|
Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
|
|
|
|
SynthResult sr = d_solver.checkSynth();
|
|
assertEquals(sr.hasSolution(), true);
|
|
assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
|
|
sr = d_solver.checkSynthNext();
|
|
assertEquals(sr.hasSolution(), true);
|
|
assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
|
|
}
|
|
|
|
@Test
|
|
void checkSynthNext2() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
d_solver.setOption("incremental", "false");
|
|
Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
|
|
|
|
d_solver.checkSynth();
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.checkSynthNext());
|
|
}
|
|
|
|
@Test
|
|
void checkSynthNext3() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
d_solver.setOption("incremental", "true");
|
|
Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
|
|
|
|
assertThrows(CVC5ApiException.class, () -> d_solver.checkSynthNext());
|
|
}
|
|
|
|
@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(SET_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\" "
|
|
+ "(set.singleton \"Z\")))",
|
|
projection.toString());
|
|
}
|
|
}
|