{
private Solver d_solver;
- @BeforeEach void setUp()
+ @BeforeEach
+ void setUp()
{
d_solver = new Solver();
}
- @AfterEach void tearDown()
+ @AfterEach
+ void tearDown()
{
d_solver.close();
}
- @Test void recoverableException() throws CVC5ApiException
+ @Test
+ void recoverableException() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
assertThrows(CVC5ApiRecoverableException.class, () -> d_solver.getValue(x));
}
- @Test void supportsFloatingPoint() throws CVC5ApiException
+ @Test
+ void supportsFloatingPoint() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
}
- @Test void getBooleanSort() throws CVC5ApiException
+ @Test
+ void getBooleanSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.getBooleanSort());
}
- @Test void getIntegerSort()
+ @Test
+ void getIntegerSort()
{
assertDoesNotThrow(() -> d_solver.getIntegerSort());
}
- @Test void getNullSort() throws CVC5ApiException
+ @Test
+ void getNullSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.getNullSort());
}
- @Test void getRealSort() throws CVC5ApiException
+ @Test
+ void getRealSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.getRealSort());
}
- @Test void getRegExpSort() throws CVC5ApiException
+ @Test
+ void getRegExpSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.getRegExpSort());
}
- @Test void getStringSort() throws CVC5ApiException
+ @Test
+ void getStringSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.getStringSort());
}
- @Test void getRoundingModeSort() throws CVC5ApiException
+ @Test
+ void getRoundingModeSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.getRoundingModeSort());
}
- @Test void mkArraySort() throws CVC5ApiException
+ @Test
+ void mkArraySort() throws CVC5ApiException
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
slv.close();
}
- @Test void mkBitVectorSort() throws CVC5ApiException
+ @Test
+ void mkBitVectorSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkBitVectorSort(32));
assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVectorSort(0));
}
- @Test void mkFloatingPointSort() throws CVC5ApiException
+ @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
+ @Test
+ void mkDatatypeSort() throws CVC5ApiException
{
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
slv.close();
}
- @Test void mkDatatypeSorts() throws CVC5ApiException
+ @Test
+ void mkDatatypeSorts() throws CVC5ApiException
{
Solver slv = new Solver();
/* Note: More tests are in datatype_api_black. */
}
- @Test void mkFunctionSort() throws CVC5ApiException
+ @Test
+ void mkFunctionSort() throws CVC5ApiException
{
assertDoesNotThrow(()
-> d_solver.mkFunctionSort(
slv.close();
}
- @Test void mkParamSort() throws CVC5ApiException
+ @Test
+ void mkParamSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkParamSort("T"));
assertDoesNotThrow(() -> d_solver.mkParamSort(""));
}
- @Test void mkPredicateSort()
+ @Test
+ void mkPredicateSort()
{
assertDoesNotThrow(() -> d_solver.mkPredicateSort(new Sort[] {d_solver.getIntegerSort()}));
assertThrows(CVC5ApiException.class, () -> d_solver.mkPredicateSort(new Sort[] {}));
slv.close();
}
- @Test void mkRecordSort() throws CVC5ApiException
+ @Test
+ void mkRecordSort() throws CVC5ApiException
{
Pair<String, Sort>[] fields = new Pair[] {new Pair<>("b", d_solver.getBooleanSort()),
new Pair<>("bv", d_solver.mkBitVectorSort(8)),
slv.close();
}
- @Test void mkSetSort() throws CVC5ApiException
+ @Test
+ void mkSetSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkSetSort(d_solver.getBooleanSort()));
assertDoesNotThrow(() -> d_solver.mkSetSort(d_solver.getIntegerSort()));
slv.close();
}
- @Test void mkBagSort() throws CVC5ApiException
+ @Test
+ void mkBagSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkBagSort(d_solver.getBooleanSort()));
assertDoesNotThrow(() -> d_solver.mkBagSort(d_solver.getIntegerSort()));
slv.close();
}
- @Test void mkSequenceSort() throws CVC5ApiException
+ @Test
+ void mkSequenceSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkSequenceSort(d_solver.getBooleanSort()));
assertDoesNotThrow(
slv.close();
}
- @Test void mkUninterpretedSort() throws CVC5ApiException
+ @Test
+ void mkUninterpretedSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkUninterpretedSort("u"));
assertDoesNotThrow(() -> d_solver.mkUninterpretedSort(""));
}
- @Test void mkUnresolvedSort() throws CVC5ApiException
+ @Test
+ void mkUnresolvedSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u"));
assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u", 1));
assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("", 1));
}
- @Test void mkUninterpretedSortConstructorSort() throws CVC5ApiException
+ @Test
+ void mkUninterpretedSortConstructorSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort("s", 2));
assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort("", 2));
assertThrows(CVC5ApiException.class, () -> d_solver.mkUninterpretedSortConstructorSort("", 0));
}
- @Test void mkTupleSort() throws CVC5ApiException
+ @Test
+ void mkTupleSort() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkTupleSort(new Sort[] {d_solver.getIntegerSort()}));
Sort funSort =
slv.close();
}
- @Test void mkBitVector() throws CVC5ApiException
+ @Test
+ void mkBitVector() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkBitVector(8, 2));
assertDoesNotThrow(() -> d_solver.mkBitVector(32, 2));
assertEquals(d_solver.mkBitVector(8, "-1", 10), d_solver.mkBitVector(8, "FF", 16));
}
- @Test void mkVar() throws CVC5ApiException
+ @Test
+ void mkVar() throws CVC5ApiException
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
slv.close();
}
- @Test void mkBoolean() throws CVC5ApiException
+ @Test
+ void mkBoolean() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkBoolean(true));
assertDoesNotThrow(() -> d_solver.mkBoolean(false));
}
- @Test void mkRoundingMode() throws CVC5ApiException
+ @Test
+ void mkRoundingMode() throws CVC5ApiException
{
assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).toString(),
"roundNearestTiesToEven");
"roundNearestTiesToAway");
}
- @Test void mkFloatingPoint() throws CVC5ApiException
+ @Test
+ void mkFloatingPoint() throws CVC5ApiException
{
Term t1 = d_solver.mkBitVector(8);
Term t2 = d_solver.mkBitVector(4);
slv.close();
}
- @Test void mkCardinalityConstraint() throws CVC5ApiException
+ @Test
+ void mkCardinalityConstraint() throws CVC5ApiException
{
Sort su = d_solver.mkUninterpretedSort("u");
Sort si = d_solver.getIntegerSort();
slv.close();
}
- @Test void mkEmptySet() throws CVC5ApiException
+ @Test
+ void mkEmptySet() throws CVC5ApiException
{
Solver slv = new Solver();
Sort s = d_solver.mkSetSort(d_solver.getBooleanSort());
slv.close();
}
- @Test void mkEmptyBag() throws CVC5ApiException
+ @Test
+ void mkEmptyBag() throws CVC5ApiException
{
Solver slv = new Solver();
Sort s = d_solver.mkBagSort(d_solver.getBooleanSort());
slv.close();
}
- @Test void mkEmptySequence() throws CVC5ApiException
+ @Test
+ void mkEmptySequence() throws CVC5ApiException
{
Solver slv = new Solver();
Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort());
slv.close();
}
- @Test void mkFalse() throws CVC5ApiException
+ @Test
+ void mkFalse() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkFalse());
assertDoesNotThrow(() -> d_solver.mkFalse());
}
- @Test void mkFloatingPointNaN() throws CVC5ApiException
+ @Test
+ void mkFloatingPointNaN() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkFloatingPointNaN(3, 5));
}
- @Test void mkFloatingPointNegZero() throws CVC5ApiException
+ @Test
+ void mkFloatingPointNegZero() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.mkFloatingPointNegZero(3, 5));
}
- @Test void mkFloatingPointNegInf()
+ @Test
+ void mkFloatingPointNegInf()
{
assertDoesNotThrow(() -> d_solver.mkFloatingPointNegInf(3, 5));
}
- @Test void mkFloatingPointPosInf()
+ @Test
+ void mkFloatingPointPosInf()
{
assertDoesNotThrow(() -> d_solver.mkFloatingPointPosInf(3, 5));
}
- @Test void mkFloatingPointPosZero()
+ @Test
+ void mkFloatingPointPosZero()
{
assertDoesNotThrow(() -> d_solver.mkFloatingPointPosZero(3, 5));
}
- @Test void mkOp()
+ @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));
assertDoesNotThrow(() -> d_solver.mkOp(TUPLE_PROJECT, args));
}
- @Test void mkPi()
+ @Test
+ void mkPi()
{
assertDoesNotThrow(() -> d_solver.mkPi());
}
- @Test void mkInteger()
+ @Test
+ void mkInteger()
{
assertDoesNotThrow(() -> d_solver.mkInteger("123"));
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("1.23"));
assertDoesNotThrow(() -> d_solver.mkInteger(val4));
}
- @Test void mkReal()
+ @Test
+ void mkReal()
{
assertDoesNotThrow(() -> d_solver.mkReal("123"));
assertDoesNotThrow(() -> d_solver.mkReal("1.23"));
assertDoesNotThrow(() -> d_solver.mkReal(val4, val4));
}
- @Test void mkRegexpNone()
+ @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()
+ @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()
+ @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()
+ @Test
+ void mkSepEmp()
{
assertDoesNotThrow(() -> d_solver.mkSepEmp());
}
- @Test void mkSepNil()
+ @Test
+ void mkSepNil()
{
assertDoesNotThrow(() -> d_solver.mkSepNil(d_solver.getBooleanSort()));
assertThrows(CVC5ApiException.class, () -> d_solver.mkSepNil(d_solver.getNullSort()));
slv.close();
}
- @Test void mkString()
+ @Test
+ void mkString()
{
assertDoesNotThrow(() -> d_solver.mkString(""));
assertDoesNotThrow(() -> d_solver.mkString("asdfasdf"));
assertEquals(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(), "\"asdf\\u{5c}nasdf\"");
}
- @Test void mkTerm() throws CVC5ApiException
+ @Test
+ void mkTerm() throws CVC5ApiException
{
Sort bv32 = d_solver.mkBitVectorSort(32);
Term a = d_solver.mkConst(bv32, "a");
slv.close();
}
- @Test void mkTermFromOp() throws CVC5ApiException
+ @Test
+ void mkTermFromOp() throws CVC5ApiException
{
Sort bv32 = d_solver.mkBitVectorSort(32);
Term a = d_solver.mkConst(bv32, "a");
slv.close();
}
- @Test void mkTrue()
+ @Test
+ void mkTrue()
{
assertDoesNotThrow(() -> d_solver.mkTrue());
assertDoesNotThrow(() -> d_solver.mkTrue());
}
- @Test void mkTuple()
+ @Test
+ void mkTuple()
{
assertDoesNotThrow(()
-> d_solver.mkTuple(new Sort[] {d_solver.mkBitVectorSort(3)},
slv.close();
}
- @Test void mkUniverseSet()
+ @Test
+ void mkUniverseSet()
{
assertDoesNotThrow(() -> d_solver.mkUniverseSet(d_solver.getBooleanSort()));
assertThrows(CVC5ApiException.class, () -> d_solver.mkUniverseSet(d_solver.getNullSort()));
slv.close();
}
- @Test void mkConst()
+ @Test
+ void mkConst()
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
slv.close();
}
- @Test void mkConstArray()
+ @Test
+ void mkConstArray()
{
Sort intSort = d_solver.getIntegerSort();
Sort arrSort = d_solver.mkArraySort(intSort, intSort);
slv.close();
}
- @Test void declareDatatype()
+ @Test
+ void declareDatatype()
{
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
DatatypeConstructorDecl[] ctors1 = new DatatypeConstructorDecl[] {nil};
slv.close();
}
- @Test void declareFun() throws CVC5ApiException
+ @Test
+ void declareFun() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort funSort =
slv.close();
}
- @Test void declareSort()
+ @Test
+ void declareSort()
{
assertDoesNotThrow(() -> d_solver.declareSort("s", 0));
assertDoesNotThrow(() -> d_solver.declareSort("s", 2));
assertDoesNotThrow(() -> d_solver.declareSort("", 2));
}
- @Test void defineSort()
+ @Test
+ void defineSort()
{
Sort sortVar0 = d_solver.mkParamSort("T0");
Sort sortVar1 = d_solver.mkParamSort("T1");
new Sort[] {sortVar0, sortVar1}, new Sort[] {intSort, realSort}));
}
- @Test void defineFun() throws CVC5ApiException
+ @Test
+ void defineFun() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort funSort =
slv.close();
}
- @Test void defineFunGlobal()
+ @Test
+ void defineFunGlobal()
{
Sort bSort = d_solver.getBooleanSort();
assertTrue(d_solver.checkSat().isUnsat());
}
- @Test void defineFunRec() throws CVC5ApiException
+ @Test
+ void defineFunRec() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
slv.close();
}
- @Test void defineFunRecWrongLogic() throws CVC5ApiException
+ @Test
+ void defineFunRecWrongLogic() throws CVC5ApiException
{
d_solver.setLogic("QF_BV");
Sort bvSort = d_solver.mkBitVectorSort(32);
assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f, new Term[] {b, b}, v));
}
- @Test void defineFunRecGlobal() throws CVC5ApiException
+ @Test
+ void defineFunRecGlobal() throws CVC5ApiException
{
Sort bSort = d_solver.getBooleanSort();
Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
assertTrue(d_solver.checkSat().isUnsat());
}
- @Test void defineFunsRec() throws CVC5ApiException
+ @Test
+ void defineFunsRec() throws CVC5ApiException
{
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort bvSort = d_solver.mkBitVectorSort(32);
slv.close();
}
- @Test void defineFunsRecWrongLogic() throws CVC5ApiException
+ @Test
+ void defineFunsRecWrongLogic() throws CVC5ApiException
{
d_solver.setLogic("QF_BV");
Sort uSort = d_solver.mkUninterpretedSort("u");
new Term[] {f1, f2}, new Term[][] {{b, b}, {u}}, new Term[] {v1, v2}));
}
- @Test void defineFunsRecGlobal() throws CVC5ApiException
+ @Test
+ void defineFunsRecGlobal() throws CVC5ApiException
{
Sort bSort = d_solver.getBooleanSort();
Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
assertTrue(d_solver.checkSat().isUnsat());
}
- @Test void uFIteration()
+ @Test
+ void uFIteration()
{
Sort intSort = d_solver.getIntegerSort();
Sort funSort = d_solver.mkFunctionSort(new Sort[] {intSort, intSort}, intSort);
}
}
- @Test void getInfo()
+ @Test
+ void getInfo()
{
assertDoesNotThrow(() -> d_solver.getInfo("name"));
assertThrows(CVC5ApiException.class, () -> d_solver.getInfo("asdf"));
}
- @Test void getAbduct() throws CVC5ApiException
+ @Test
+ void getAbduct() throws CVC5ApiException
{
d_solver.setLogic("QF_LIA");
d_solver.setOption("produce-abducts", "true");
assertEquals(output2, truen);
}
- @Test void getAbduct2() throws CVC5ApiException
+ @Test
+ void getAbduct2() throws CVC5ApiException
{
d_solver.setLogic("QF_LIA");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getAbduct(conj));
}
- @Test void getAbductNext() throws CVC5ApiException
+ @Test
+ void getAbductNext() throws CVC5ApiException
{
d_solver.setLogic("QF_LIA");
d_solver.setOption("produce-abducts", "true");
assertNotEquals(output, output2);
}
- @Test void getInterpolant() throws CVC5ApiException
+ @Test
+ void getInterpolant() throws CVC5ApiException
{
d_solver.setLogic("QF_LIA");
d_solver.setOption("produce-interpolants", "true");
assertTrue(output.getSort().isBoolean());
}
- @Test void getInterpolantNext() throws CVC5ApiException
+ @Test
+ void getInterpolantNext() throws CVC5ApiException
{
d_solver.setLogic("QF_LIA");
d_solver.setOption("produce-interpolants", "true");
assertNotEquals(output, output2);
}
- @Test void getOp() throws CVC5ApiException
+ @Test
+ void getOp() throws CVC5ApiException
{
Sort bv32 = d_solver.mkBitVectorSort(32);
Term a = d_solver.mkConst(bv32, "a");
assertTrue(listhead.hasOp());
}
- @Test void getOption()
+ @Test
+ void getOption()
{
assertDoesNotThrow(() -> d_solver.getOption("incremental"));
assertThrows(CVC5ApiException.class, () -> d_solver.getOption("asdf"));
}
- @Test void getOptionNames()
+ @Test
+ void getOptionNames()
{
String[] names = d_solver.getOptionNames();
assertTrue(names.length > 100);
assertFalse(Arrays.asList(names).contains("foobar"));
}
- @Test void getOptionInfo()
+ @Test
+ void getOptionInfo()
{
List<Executable> assertions = new ArrayList<>();
{
assertAll(assertions);
}
- @Test void getStatistics()
+ @Test
+ void getStatistics()
{
// do some array reasoning to make sure we have a double statistics
{
}
}
- @Test void getUnsatAssumptions1()
+ @Test
+ void getUnsatAssumptions1()
{
d_solver.setOption("incremental", "false");
d_solver.checkSatAssuming(d_solver.mkFalse());
assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions());
}
- @Test void getUnsatAssumptions2()
+ @Test
+ void getUnsatAssumptions2()
{
d_solver.setOption("incremental", "true");
d_solver.setOption("produce-unsat-assumptions", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions());
}
- @Test void getUnsatAssumptions3()
+ @Test
+ void getUnsatAssumptions3()
{
d_solver.setOption("incremental", "true");
d_solver.setOption("produce-unsat-assumptions", "true");
assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions());
}
- @Test void getUnsatCore1()
+ @Test
+ void getUnsatCore1()
{
d_solver.setOption("incremental", "false");
d_solver.assertFormula(d_solver.mkFalse());
assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatCore());
}
- @Test void getUnsatCore2()
+ @Test
+ void getUnsatCore2()
{
d_solver.setOption("incremental", "false");
d_solver.setOption("produce-unsat-cores", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatCore());
}
- @Test void getUnsatCoreAndProof()
+ @Test
+ void getUnsatCoreAndProof()
{
d_solver.setOption("incremental", "true");
d_solver.setOption("produce-unsat-cores", "true");
assertDoesNotThrow(() -> d_solver.getProof());
}
- @Test void getDifficulty()
+ @Test
+ void getDifficulty()
{
d_solver.setOption("produce-difficulty", "true");
// cannot ask before a check sat
assertDoesNotThrow(() -> d_solver.getDifficulty());
}
- @Test void getDifficulty2()
+ @Test
+ void getDifficulty2()
{
d_solver.checkSat();
// option is not set
assertThrows(CVC5ApiException.class, () -> d_solver.getDifficulty());
}
- @Test void getDifficulty3() throws CVC5ApiException
+ @Test
+ void getDifficulty3() throws CVC5ApiException
{
d_solver.setOption("produce-difficulty", "true");
Sort intSort = d_solver.getIntegerSort();
}
}
- @Test void getLearnedLiterals()
+ @Test
+ void getLearnedLiterals()
{
d_solver.setOption("produce-learned-literals", "true");
// cannot ask before a check sat
assertDoesNotThrow(() -> d_solver.getLearnedLiterals());
}
- @Test void getLearnedLiterals2()
+ @Test
+ void getLearnedLiterals2()
{
d_solver.setOption("produce-learned-literals", "true");
Sort intSort = d_solver.getIntegerSort();
assertDoesNotThrow(() -> d_solver.getLearnedLiterals());
}
- @Test void getValue1()
+ @Test
+ void getValue1()
{
d_solver.setOption("produce-models", "false");
Term t = d_solver.mkTrue();
assertThrows(CVC5ApiException.class, () -> d_solver.getValue(t));
}
- @Test void getValue2()
+ @Test
+ void getValue2()
{
d_solver.setOption("produce-models", "true");
Term t = d_solver.mkFalse();
assertThrows(CVC5ApiException.class, () -> d_solver.getValue(t));
}
- @Test void getValue3()
+ @Test
+ void getValue3()
{
d_solver.setOption("produce-models", "true");
Sort uSort = d_solver.mkUninterpretedSort("u");
slv.close();
}
- @Test void getModelDomainElements()
+ @Test
+ void getModelDomainElements()
{
d_solver.setOption("produce-models", "true");
Sort uSort = d_solver.mkUninterpretedSort("u");
assertThrows(CVC5ApiException.class, () -> d_solver.getModelDomainElements(intSort));
}
- @Test void getModelDomainElements2()
+ @Test
+ void getModelDomainElements2()
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("finite-model-find", "true");
assertTrue(d_solver.getModelDomainElements(uSort).length == 1);
}
- @Test void isModelCoreSymbol()
+ @Test
+ void isModelCoreSymbol()
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("model-cores", "simple");
assertThrows(CVC5ApiException.class, () -> d_solver.isModelCoreSymbol(zero));
}
- @Test void getModel()
+ @Test
+ void getModel()
{
d_solver.setOption("produce-models", "true");
Sort uSort = d_solver.mkUninterpretedSort("u");
assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts, terms2));
}
- @Test void getModel2()
+ @Test
+ void getModel2()
{
d_solver.setOption("produce-models", "true");
Sort[] sorts = new Sort[] {};
assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts, terms));
}
- @Test void getModel3()
+ @Test
+ void getModel3()
{
d_solver.setOption("produce-models", "true");
Sort[] sorts = new Sort[] {};
assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts2, terms));
}
- @Test void getQuantifierElimination()
+ @Test
+ void getQuantifierElimination()
{
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
Term forall = d_solver.mkTerm(
slv.close();
}
- @Test void getQuantifierEliminationDisjunct()
+ @Test
+ void getQuantifierEliminationDisjunct()
{
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
Term forall = d_solver.mkTerm(
slv.close();
}
- @Test void declareSepHeap() throws CVC5ApiException
+ @Test
+ void declareSepHeap() throws CVC5ApiException
{
d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
solver.checkSat();
}
- @Test void getValueSepHeap1() throws CVC5ApiException
+ @Test
+ void getValueSepHeap1() throws CVC5ApiException
{
d_solver.setLogic("QF_BV");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap());
}
- @Test void getValueSepHeap2() throws CVC5ApiException
+ @Test
+ void getValueSepHeap2() throws CVC5ApiException
{
d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap());
}
- @Test void getValueSepHeap3() throws CVC5ApiException
+ @Test
+ void getValueSepHeap3() throws CVC5ApiException
{
d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap());
}
- @Test void getValueSepHeap4() throws CVC5ApiException
+ @Test
+ void getValueSepHeap4() throws CVC5ApiException
{
d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap());
}
- @Test void getValueSepHeap5() throws CVC5ApiException
+ @Test
+ void getValueSepHeap5() throws CVC5ApiException
{
d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
assertDoesNotThrow(() -> d_solver.getValueSepHeap());
}
- @Test void getValueSepNil1() throws CVC5ApiException
+ @Test
+ void getValueSepNil1() throws CVC5ApiException
{
d_solver.setLogic("QF_BV");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil());
}
- @Test void getValueSepNil2() throws CVC5ApiException
+ @Test
+ void getValueSepNil2() throws CVC5ApiException
{
d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil());
}
- @Test void getValueSepNil3() throws CVC5ApiException
+ @Test
+ void getValueSepNil3() throws CVC5ApiException
{
d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil());
}
- @Test void getValueSepNil4() throws CVC5ApiException
+ @Test
+ void getValueSepNil4() throws CVC5ApiException
{
d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil());
}
- @Test void getValueSepNil5() throws CVC5ApiException
+ @Test
+ void getValueSepNil5() throws CVC5ApiException
{
d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
assertDoesNotThrow(() -> d_solver.getValueSepNil());
}
- @Test void push1()
+ @Test
+ void push1()
{
d_solver.setOption("incremental", "true");
assertDoesNotThrow(() -> d_solver.push(1));
assertThrows(CVC5ApiException.class, () -> d_solver.setOption("incremental", "true"));
}
- @Test void push2()
+ @Test
+ void push2()
{
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.push(1));
}
- @Test void pop1()
+ @Test
+ void pop1()
{
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.pop(1));
}
- @Test void pop2()
+ @Test
+ void pop2()
{
d_solver.setOption("incremental", "true");
assertThrows(CVC5ApiException.class, () -> d_solver.pop(1));
}
- @Test void pop3()
+ @Test
+ void pop3()
{
d_solver.setOption("incremental", "true");
assertDoesNotThrow(() -> d_solver.push(1));
assertThrows(CVC5ApiException.class, () -> d_solver.pop(1));
}
- @Test void blockModel1()
+ @Test
+ void blockModel1()
{
d_solver.setOption("produce-models", "true");
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
assertThrows(CVC5ApiException.class, () -> d_solver.blockModel());
}
- @Test void blockModel2() throws CVC5ApiException
+ @Test
+ void blockModel2() throws CVC5ApiException
{
d_solver.setOption("block-models", "literals");
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
assertThrows(CVC5ApiException.class, () -> d_solver.blockModel());
}
- @Test void blockModel3() throws CVC5ApiException
+ @Test
+ void blockModel3() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("block-models", "literals");
assertThrows(CVC5ApiException.class, () -> d_solver.blockModel());
}
- @Test void blockModel4() throws CVC5ApiException
+ @Test
+ void blockModel4() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("block-models", "literals");
assertDoesNotThrow(() -> d_solver.blockModel());
}
- @Test void blockModelValues1() throws CVC5ApiException
+ @Test
+ void blockModelValues1() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("block-models", "literals");
slv.close();
}
- @Test void blockModelValues2() throws CVC5ApiException
+ @Test
+ void blockModelValues2() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
assertDoesNotThrow(() -> d_solver.blockModelValues(new Term[] {x}));
}
- @Test void blockModelValues3() throws CVC5ApiException
+ @Test
+ void blockModelValues3() throws CVC5ApiException
{
d_solver.setOption("block-models", "literals");
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x}));
}
- @Test void blockModelValues4() throws CVC5ApiException
+ @Test
+ void blockModelValues4() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("block-models", "literals");
assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x}));
}
- @Test void blockModelValues5() throws CVC5ApiException
+ @Test
+ void blockModelValues5() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("block-models", "literals");
assertDoesNotThrow(() -> d_solver.blockModelValues(new Term[] {x}));
}
- @Test void setInfo() throws CVC5ApiException
+ @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("status", "asdf"));
}
- @Test void simplify() throws CVC5ApiException
+ @Test
+ void simplify() throws CVC5ApiException
{
assertThrows(CVC5ApiException.class, () -> d_solver.simplify(d_solver.getNullTerm()));
slv.close();
}
- @Test void assertFormula()
+ @Test
+ void assertFormula()
{
assertDoesNotThrow(() -> d_solver.assertFormula(d_solver.mkTrue()));
assertThrows(CVC5ApiException.class, () -> d_solver.assertFormula(d_solver.getNullTerm()));
slv.close();
}
- @Test void checkSat() throws CVC5ApiException
+ @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
+ @Test
+ void checkSatAssuming() throws CVC5ApiException
{
d_solver.setOption("incremental", "false");
assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTrue()));
slv.close();
}
- @Test void checkSatAssuming1() throws CVC5ApiException
+ @Test
+ void checkSatAssuming1() throws CVC5ApiException
{
Sort boolSort = d_solver.getBooleanSort();
Term x = d_solver.mkConst(boolSort, "x");
slv.close();
}
- @Test void checkSatAssuming2() throws CVC5ApiException
+ @Test
+ void checkSatAssuming2() throws CVC5ApiException
{
d_solver.setOption("incremental", "true");
slv.close();
}
- @Test void setLogic() throws CVC5ApiException
+ @Test
+ void setLogic() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.setLogic("AUFLIRA"));
assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AF_BV"));
assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AUFLIRA"));
}
- @Test void setOption() throws CVC5ApiException
+ @Test
+ void setOption() throws CVC5ApiException
{
assertDoesNotThrow(() -> d_solver.setOption("bv-sat-solver", "minisat"));
assertThrows(CVC5ApiException.class, () -> d_solver.setOption("bv-sat-solver", "1"));
assertThrows(CVC5ApiException.class, () -> d_solver.setOption("bv-sat-solver", "minisat"));
}
- @Test void resetAssertions() throws CVC5ApiException
+ @Test
+ void resetAssertions() throws CVC5ApiException
{
d_solver.setOption("incremental", "true");
d_solver.checkSatAssuming(new Term[] {slt, ule});
}
- @Test void declareSygusVar() throws CVC5ApiException
+ @Test
+ void declareSygusVar() throws CVC5ApiException
{
d_solver.setOption("sygus", "true");
Sort boolSort = d_solver.getBooleanSort();
slv.close();
}
- @Test void mkSygusGrammar() throws CVC5ApiException
+ @Test
+ void mkSygusGrammar() throws CVC5ApiException
{
Term nullTerm = d_solver.getNullTerm();
Term boolTerm = d_solver.mkBoolean(true);
slv.close();
}
- @Test void synthFun() throws CVC5ApiException
+ @Test
+ void synthFun() throws CVC5ApiException
{
d_solver.setOption("sygus", "true");
Sort nullSort = d_solver.getNullSort();
slv.close();
}
- @Test void synthInv() throws CVC5ApiException
+ @Test
+ void synthInv() throws CVC5ApiException
{
d_solver.setOption("sygus", "true");
Sort bool = d_solver.getBooleanSort();
assertThrows(CVC5ApiException.class, () -> d_solver.synthInv("i4", new Term[] {x}, g2));
}
- @Test void addSygusConstraint() throws CVC5ApiException
+ @Test
+ void addSygusConstraint() throws CVC5ApiException
{
d_solver.setOption("sygus", "true");
Term nullTerm = d_solver.getNullTerm();
slv.close();
}
- @Test void addSygusAssume()
+ @Test
+ void addSygusAssume()
{
d_solver.setOption("sygus", "true");
Term nullTerm = d_solver.getNullTerm();
slv.close();
}
- @Test void addSygusInvConstraint() throws CVC5ApiException
+ @Test
+ void addSygusInvConstraint() throws CVC5ApiException
{
d_solver.setOption("sygus", "true");
Sort bool = d_solver.getBooleanSort();
slv.close();
}
- @Test void checkSynth() throws CVC5ApiException
+ @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
+ @Test
+ void getSynthSolution() throws CVC5ApiException
{
d_solver.setOption("sygus", "true");
d_solver.setOption("incremental", "false");
slv.close();
}
- @Test void getSynthSolutions() throws CVC5ApiException
+ @Test
+ void getSynthSolutions() throws CVC5ApiException
{
d_solver.setOption("sygus", "true");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> slv.getSynthSolutions(new Term[] {x}));
slv.close();
}
- @Test void checkSynthNext() throws CVC5ApiException
+ @Test
+ void checkSynthNext() throws CVC5ApiException
{
d_solver.setOption("sygus", "true");
d_solver.setOption("incremental", "true");
assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
}
- @Test void checkSynthNext2() throws CVC5ApiException
+ @Test
+ void checkSynthNext2() throws CVC5ApiException
{
d_solver.setOption("sygus", "true");
d_solver.setOption("incremental", "false");
assertThrows(CVC5ApiException.class, () -> d_solver.checkSynthNext());
}
- @Test void checkSynthNext3() throws CVC5ApiException
+ @Test
+ void checkSynthNext3() throws CVC5ApiException
{
d_solver.setOption("sygus", "true");
d_solver.setOption("incremental", "true");
assertThrows(CVC5ApiException.class, () -> d_solver.checkSynthNext());
}
- @Test void tupleProject() throws CVC5ApiException
+ @Test
+ void tupleProject() throws CVC5ApiException
{
Sort[] sorts = new Sort[] {d_solver.getBooleanSort(),
d_solver.getIntegerSort(),
{
private Solver d_solver;
- @BeforeEach void setUp()
+ @BeforeEach
+ void setUp()
{
d_solver = new Solver();
}
- @AfterEach void tearDown()
+ @AfterEach
+ void tearDown()
{
d_solver.close();
}
return d_solver.mkDatatypeSort(paramDtypeSpec);
}
- @Test void operators_comparison()
+ @Test
+ void operators_comparison()
{
assertDoesNotThrow(() -> d_solver.getIntegerSort() == d_solver.getNullSort());
assertDoesNotThrow(() -> d_solver.getIntegerSort() != d_solver.getNullSort());
assertDoesNotThrow(() -> d_solver.getIntegerSort().compareTo(d_solver.getNullSort()));
}
- @Test void hasGetSymbol() throws CVC5ApiException
+ @Test
+ void hasGetSymbol() throws CVC5ApiException
{
Sort n = d_solver.getNullSort();
Sort b = d_solver.getBooleanSort();
assertEquals(s1.getSymbol(), "|s1\\|");
}
- @Test void isBoolean()
+ @Test
+ void isBoolean()
{
assertTrue(d_solver.getBooleanSort().isBoolean());
assertDoesNotThrow(() -> d_solver.getNullSort().isBoolean());
}
- @Test void isInteger()
+ @Test
+ void isInteger()
{
assertTrue(d_solver.getIntegerSort().isInteger());
assertTrue(!d_solver.getRealSort().isInteger());
assertDoesNotThrow(() -> d_solver.getNullSort().isInteger());
}
- @Test void isReal()
+ @Test
+ void isReal()
{
assertTrue(d_solver.getRealSort().isReal());
assertTrue(!d_solver.getIntegerSort().isReal());
assertDoesNotThrow(() -> d_solver.getNullSort().isReal());
}
- @Test void isString()
+ @Test
+ void isString()
{
assertTrue(d_solver.getStringSort().isString());
assertDoesNotThrow(() -> d_solver.getNullSort().isString());
}
- @Test void isRegExp()
+ @Test
+ void isRegExp()
{
assertTrue(d_solver.getRegExpSort().isRegExp());
assertDoesNotThrow(() -> d_solver.getNullSort().isRegExp());
}
- @Test void isRoundingMode() throws CVC5ApiException
+ @Test
+ void isRoundingMode() throws CVC5ApiException
{
assertTrue(d_solver.getRoundingModeSort().isRoundingMode());
assertDoesNotThrow(() -> d_solver.getNullSort().isRoundingMode());
}
- @Test void isBitVector() throws CVC5ApiException
+ @Test
+ void isBitVector() throws CVC5ApiException
{
assertTrue(d_solver.mkBitVectorSort(8).isBitVector());
assertDoesNotThrow(() -> d_solver.getNullSort().isBitVector());
}
- @Test void isFloatingPoint() throws CVC5ApiException
+ @Test
+ void isFloatingPoint() throws CVC5ApiException
{
assertTrue(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
assertDoesNotThrow(() -> d_solver.getNullSort().isFloatingPoint());
}
- @Test void isDatatype() throws CVC5ApiException
+ @Test
+ void isDatatype() throws CVC5ApiException
{
Sort dt_sort = create_datatype_sort();
assertTrue(dt_sort.isDatatype());
assertDoesNotThrow(() -> d_solver.getNullSort().isDatatype());
}
- @Test void isConstructor() throws CVC5ApiException
+ @Test
+ void isConstructor() throws CVC5ApiException
{
Sort dt_sort = create_datatype_sort();
Datatype dt = dt_sort.getDatatype();
assertDoesNotThrow(() -> d_solver.getNullSort().isConstructor());
}
- @Test void isSelector() throws CVC5ApiException
+ @Test
+ void isSelector() throws CVC5ApiException
{
Sort dt_sort = create_datatype_sort();
Datatype dt = dt_sort.getDatatype();
assertDoesNotThrow(() -> d_solver.getNullSort().isSelector());
}
- @Test void isTester() throws CVC5ApiException
+ @Test
+ void isTester() throws CVC5ApiException
{
Sort dt_sort = create_datatype_sort();
Datatype dt = dt_sort.getDatatype();
assertDoesNotThrow(() -> d_solver.getNullSort().isTester());
}
- @Test void isFunction()
+ @Test
+ void isFunction()
{
Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), d_solver.getIntegerSort());
assertTrue(fun_sort.isFunction());
assertDoesNotThrow(() -> d_solver.getNullSort().isFunction());
}
- @Test void isPredicate()
+ @Test
+ void isPredicate()
{
Sort pred_sort = d_solver.mkPredicateSort(new Sort[] {d_solver.getRealSort()});
assertTrue(pred_sort.isPredicate());
assertDoesNotThrow(() -> d_solver.getNullSort().isPredicate());
}
- @Test void isTuple()
+ @Test
+ void isTuple()
{
Sort tup_sort = d_solver.mkTupleSort(new Sort[] {d_solver.getRealSort()});
assertTrue(tup_sort.isTuple());
assertDoesNotThrow(() -> d_solver.getNullSort().isTuple());
}
- @Test void isRecord()
+ @Test
+ void isRecord()
{
Sort rec_sort =
d_solver.mkRecordSort(new Pair[] {new Pair<String, Sort>("asdf", d_solver.getRealSort())});
assertDoesNotThrow(() -> d_solver.getNullSort().isRecord());
}
- @Test void isArray()
+ @Test
+ void isArray()
{
Sort arr_sort = d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getIntegerSort());
assertTrue(arr_sort.isArray());
assertDoesNotThrow(() -> d_solver.getNullSort().isArray());
}
- @Test void isSet()
+ @Test
+ void isSet()
{
Sort set_sort = d_solver.mkSetSort(d_solver.getRealSort());
assertTrue(set_sort.isSet());
assertDoesNotThrow(() -> d_solver.getNullSort().isSet());
}
- @Test void isBag()
+ @Test
+ void isBag()
{
Sort bag_sort = d_solver.mkBagSort(d_solver.getRealSort());
assertTrue(bag_sort.isBag());
assertDoesNotThrow(() -> d_solver.getNullSort().isBag());
}
- @Test void isSequence()
+ @Test
+ void isSequence()
{
Sort seq_sort = d_solver.mkSequenceSort(d_solver.getRealSort());
assertTrue(seq_sort.isSequence());
assertDoesNotThrow(() -> d_solver.getNullSort().isSequence());
}
- @Test void isUninterpreted()
+ @Test
+ void isUninterpreted()
{
Sort un_sort = d_solver.mkUninterpretedSort("asdf");
assertTrue(un_sort.isUninterpretedSort());
assertDoesNotThrow(() -> d_solver.getNullSort().isUninterpretedSort());
}
- @Test void isUninterpretedSortSortConstructor() throws CVC5ApiException
+ @Test
+ void isUninterpretedSortSortConstructor() throws CVC5ApiException
{
Sort sc_sort = d_solver.mkUninterpretedSortConstructorSort("asdf", 1);
assertTrue(sc_sort.isUninterpretedSortConstructor());
assertDoesNotThrow(() -> d_solver.getNullSort().isUninterpretedSortConstructor());
}
- @Test void getDatatype() throws CVC5ApiException
+ @Test
+ void getDatatype() throws CVC5ApiException
{
Sort dtypeSort = create_datatype_sort();
assertDoesNotThrow(() -> dtypeSort.getDatatype());
assertThrows(CVC5ApiException.class, () -> bvSort.getDatatype());
}
- @Test void datatypeSorts() throws CVC5ApiException
+ @Test
+ void datatypeSorts() throws CVC5ApiException
{
Sort intSort = d_solver.getIntegerSort();
Sort dtypeSort = create_datatype_sort();
assertThrows(CVC5ApiException.class, () -> booleanSort.getSelectorCodomainSort());
}
- @Test void instantiate() throws CVC5ApiException
+ @Test
+ void instantiate() throws CVC5ApiException
{
// instantiate parametric datatype, check should not fail
Sort paramDtypeSort = create_param_datatype_sort();
assertDoesNotThrow(() -> sortConsSort.instantiate(new Sort[] {d_solver.getIntegerSort()}));
}
- @Test void isInstantiated() throws CVC5ApiException
+ @Test
+ void isInstantiated() throws CVC5ApiException
{
Sort paramDtypeSort = create_param_datatype_sort();
assertFalse(paramDtypeSort.isInstantiated());
assertFalse(d_solver.mkBitVectorSort(32).isInstantiated());
}
- @Test void getInstantiatedParameters() throws CVC5ApiException
+ @Test
+ void getInstantiatedParameters() throws CVC5ApiException
{
Sort intSort = d_solver.getIntegerSort();
Sort realSort = d_solver.getRealSort();
assertThrows(CVC5ApiException.class, () -> bvSort.getInstantiatedParameters());
}
- @Test void getUninterpretedSortConstructor() throws CVC5ApiException
+ @Test
+ void getUninterpretedSortConstructor() throws CVC5ApiException
{
Sort intSort = d_solver.getIntegerSort();
Sort realSort = d_solver.getRealSort();
assertEquals(sortConsSort, instSortConsSort.getUninterpretedSortConstructor());
}
- @Test void getFunctionArity() throws CVC5ApiException
+ @Test
+ void getFunctionArity() throws CVC5ApiException
{
Sort funSort =
d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
assertThrows(CVC5ApiException.class, () -> bvSort.getFunctionArity());
}
- @Test void getFunctionDomainSorts() throws CVC5ApiException
+ @Test
+ void getFunctionDomainSorts() throws CVC5ApiException
{
Sort funSort =
d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
assertThrows(CVC5ApiException.class, () -> bvSort.getFunctionDomainSorts());
}
- @Test void getFunctionCodomainSort() throws CVC5ApiException
+ @Test
+ void getFunctionCodomainSort() throws CVC5ApiException
{
Sort funSort =
d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
assertThrows(CVC5ApiException.class, () -> bvSort.getFunctionCodomainSort());
}
- @Test void getArrayIndexSort() throws CVC5ApiException
+ @Test
+ void getArrayIndexSort() throws CVC5ApiException
{
Sort elementSort = d_solver.mkBitVectorSort(32);
Sort indexSort = d_solver.mkBitVectorSort(32);
assertThrows(CVC5ApiException.class, () -> indexSort.getArrayIndexSort());
}
- @Test void getArrayElementSort() throws CVC5ApiException
+ @Test
+ void getArrayElementSort() throws CVC5ApiException
{
Sort elementSort = d_solver.mkBitVectorSort(32);
Sort indexSort = d_solver.mkBitVectorSort(32);
assertThrows(CVC5ApiException.class, () -> indexSort.getArrayElementSort());
}
- @Test void getSetElementSort() throws CVC5ApiException
+ @Test
+ void getSetElementSort() throws CVC5ApiException
{
Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
assertDoesNotThrow(() -> setSort.getSetElementSort());
assertThrows(CVC5ApiException.class, () -> bvSort.getSetElementSort());
}
- @Test void getBagElementSort() throws CVC5ApiException
+ @Test
+ void getBagElementSort() throws CVC5ApiException
{
Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort());
assertDoesNotThrow(() -> bagSort.getBagElementSort());
assertThrows(CVC5ApiException.class, () -> bvSort.getBagElementSort());
}
- @Test void getSequenceElementSort() throws CVC5ApiException
+ @Test
+ void getSequenceElementSort() throws CVC5ApiException
{
Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort());
assertTrue(seqSort.isSequence());
assertThrows(CVC5ApiException.class, () -> bvSort.getSequenceElementSort());
}
- @Test void getSymbol() throws CVC5ApiException
+ @Test
+ void getSymbol() throws CVC5ApiException
{
Sort uSort = d_solver.mkUninterpretedSort("u");
assertDoesNotThrow(() -> uSort.getSymbol());
assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol());
}
- @Test void getUninterpretedSortConstructorName() throws CVC5ApiException
+ @Test
+ void getUninterpretedSortConstructorName() throws CVC5ApiException
{
Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
assertDoesNotThrow(() -> sSort.getSymbol());
assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol());
}
- @Test void getUninterpretedSortConstructorArity() throws CVC5ApiException
+ @Test
+ void getUninterpretedSortConstructorArity() throws CVC5ApiException
{
Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
assertDoesNotThrow(() -> sSort.getUninterpretedSortConstructorArity());
assertThrows(CVC5ApiException.class, () -> bvSort.getUninterpretedSortConstructorArity());
}
- @Test void getBitVectorSize() throws CVC5ApiException
+ @Test
+ void getBitVectorSize() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(32);
assertDoesNotThrow(() -> bvSort.getBitVectorSize());
assertThrows(CVC5ApiException.class, () -> setSort.getBitVectorSize());
}
- @Test void getFloatingPointExponentSize() throws CVC5ApiException
+ @Test
+ void getFloatingPointExponentSize() throws CVC5ApiException
{
Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
assertDoesNotThrow(() -> fpSort.getFloatingPointExponentSize());
assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointExponentSize());
}
- @Test void getFloatingPointSignificandSize() throws CVC5ApiException
+ @Test
+ void getFloatingPointSignificandSize() throws CVC5ApiException
{
Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
assertDoesNotThrow(() -> fpSort.getFloatingPointSignificandSize());
assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointSignificandSize());
}
- @Test void getDatatypeArity() throws CVC5ApiException
+ @Test
+ void getDatatypeArity() throws CVC5ApiException
{
// create datatype sort, check should not fail
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
assertThrows(CVC5ApiException.class, () -> bvSort.getDatatypeArity());
}
- @Test void getTupleLength() throws CVC5ApiException
+ @Test
+ void getTupleLength() throws CVC5ApiException
{
Sort tupleSort =
d_solver.mkTupleSort(new Sort[] {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
assertThrows(CVC5ApiException.class, () -> bvSort.getTupleLength());
}
- @Test void getTupleSorts() throws CVC5ApiException
+ @Test
+ void getTupleSorts() throws CVC5ApiException
{
Sort tupleSort =
d_solver.mkTupleSort(new Sort[] {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
assertThrows(CVC5ApiException.class, () -> bvSort.getTupleSorts());
}
- @Test void sortCompare() throws CVC5ApiException
+ @Test
+ void sortCompare() throws CVC5ApiException
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
== (intSort.compareTo(bvSort) >= 0));
}
- @Test void sortScopedToString() throws CVC5ApiException
+ @Test
+ void sortScopedToString() throws CVC5ApiException
{
String name = "uninterp-sort";
Sort bvsort8 = d_solver.mkBitVectorSort(8);
{
private Solver d_solver;
- @BeforeEach void setUp()
+ @BeforeEach
+ void setUp()
{
d_solver = new Solver();
}
- @AfterEach void tearDown()
+ @AfterEach
+ void tearDown()
{
d_solver.close();
}
- @Test void eq()
+ @Test
+ void eq()
{
Sort uSort = d_solver.mkUninterpretedSort("u");
Term x = d_solver.mkVar(uSort, "x");
assertTrue(x != z);
}
- @Test void getId()
+ @Test
+ void getId()
{
Term n = d_solver.getNullTerm();
assertThrows(CVC5ApiException.class, () -> n.getId());
assertNotEquals(x.getId(), z.getId());
}
- @Test void getKind() throws CVC5ApiException
+ @Test
+ void getKind() throws CVC5ApiException
{
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort intSort = d_solver.getIntegerSort();
assertEquals(ss.getKind(), SEQ_CONCAT);
}
- @Test void getSort() throws CVC5ApiException
+ @Test
+ void getSort() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
assertEquals(p_f_y.getSort(), boolSort);
}
- @Test void getOp() throws CVC5ApiException
+ @Test
+ void getOp() throws CVC5ApiException
{
Sort intsort = d_solver.getIntegerSort();
Sort bvsort = d_solver.mkBitVectorSort(8);
Term nilOpTerm = list.getConstructorTerm("nil");
}
- @Test void hasGetSymbol() throws CVC5ApiException
+ @Test
+ void hasGetSymbol() throws CVC5ApiException
{
Term n = d_solver.getNullTerm();
Term t = d_solver.mkBoolean(true);
assertEquals(c.getSymbol(), "|\\|");
}
- @Test void isNull() throws CVC5ApiException
+ @Test
+ void isNull() throws CVC5ApiException
{
Term x = d_solver.getNullTerm();
assertTrue(x.isNull());
assertFalse(x.isNull());
}
- @Test void notTerm() throws CVC5ApiException
+ @Test
+ void notTerm() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
assertDoesNotThrow(() -> p_f_x.notTerm());
}
- @Test void andTerm() throws CVC5ApiException
+ @Test
+ void andTerm() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
assertDoesNotThrow(() -> p_f_x.andTerm(p_f_x));
}
- @Test void orTerm() throws CVC5ApiException
+ @Test
+ void orTerm() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
assertDoesNotThrow(() -> p_f_x.orTerm(p_f_x));
}
- @Test void xorTerm() throws CVC5ApiException
+ @Test
+ void xorTerm() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
assertDoesNotThrow(() -> p_f_x.xorTerm(p_f_x));
}
- @Test void eqTerm() throws CVC5ApiException
+ @Test
+ void eqTerm() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
assertDoesNotThrow(() -> p_f_x.eqTerm(p_f_x));
}
- @Test void impTerm() throws CVC5ApiException
+ @Test
+ void impTerm() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
assertDoesNotThrow(() -> p_f_x.impTerm(p_f_x));
}
- @Test void iteTerm() throws CVC5ApiException
+ @Test
+ void iteTerm() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
assertThrows(CVC5ApiException.class, () -> p_f_x.iteTerm(x, b));
}
- @Test void termAssignment()
+ @Test
+ void termAssignment()
{
Term t1 = d_solver.mkInteger(1);
Term t2 = t1;
assertEquals(t1, d_solver.mkInteger(1));
}
- @Test void termCompare()
+ @Test
+ void termCompare()
{
Term t1 = d_solver.mkInteger(1);
Term t2 = d_solver.mkTerm(ADD, d_solver.mkInteger(2), d_solver.mkInteger(2));
assertTrue((t1.compareTo(t2) > 0 || t1.equals(t2)) == (t1.compareTo(t2) >= 0));
}
- @Test void termChildren() throws CVC5ApiException
+ @Test
+ void termChildren() throws CVC5ApiException
{
// simple term 2+3
Term two = d_solver.mkInteger(2);
assertThrows(CVC5ApiException.class, () -> tnull.getChild(0));
}
- @Test void getIntegerValue() throws CVC5ApiException
+ @Test
+ void getIntegerValue() throws CVC5ApiException
{
Term int1 = d_solver.mkInteger("-18446744073709551616");
Term int2 = d_solver.mkInteger("-18446744073709551615");
assertEquals(int11.getIntegerValue().toString(), "18446744073709551616");
}
- @Test void getString()
+ @Test
+ void getString()
{
Term s1 = d_solver.mkString("abcde");
assertTrue(s1.isStringValue());
assertEquals(s1.getStringValue(), "abcde");
}
- @Test void getReal() throws CVC5ApiException
+ @Test
+ void getReal() throws CVC5ApiException
{
Term real1 = d_solver.mkReal("0");
Term real2 = d_solver.mkReal(".0");
assertEquals("23432343/10000", Utils.getRational(real10.getRealValue()));
}
- @Test void getConstArrayBase()
+ @Test
+ void getConstArrayBase()
{
Sort intsort = d_solver.getIntegerSort();
Sort arrsort = d_solver.mkArraySort(intsort, intsort);
assertEquals(one, constarr.getConstArrayBase());
}
- @Test void getBoolean()
+ @Test
+ void getBoolean()
{
Term b1 = d_solver.mkBoolean(true);
Term b2 = d_solver.mkBoolean(false);
assertFalse(b2.getBooleanValue());
}
- @Test void getBitVector() throws CVC5ApiException
+ @Test
+ void getBitVector() throws CVC5ApiException
{
Term b1 = d_solver.mkBitVector(8, 15);
Term b2 = d_solver.mkBitVector(8, "00001111", 2);
assertEquals("f", b7.getBitVectorValue(16));
}
- @Test void getUninterpretedSortValue() throws CVC5ApiException
+ @Test
+ void getUninterpretedSortValue() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
Sort uSort = d_solver.mkUninterpretedSort("u");
assertDoesNotThrow(() -> vy.getUninterpretedSortValue());
}
- @Test void isRoundingModeValue() throws CVC5ApiException
+ @Test
+ void isRoundingModeValue() throws CVC5ApiException
{
assertFalse(d_solver.mkInteger(15).isRoundingModeValue());
assertTrue(
assertFalse(d_solver.mkConst(d_solver.getRoundingModeSort()).isRoundingModeValue());
}
- @Test void getRoundingModeValue() throws CVC5ApiException
+ @Test
+ void getRoundingModeValue() throws CVC5ApiException
{
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(15).getRoundingModeValue());
assertEquals(
RoundingMode.ROUND_NEAREST_TIES_TO_AWAY);
}
- @Test void getTuple()
+ @Test
+ void getTuple()
{
Sort s1 = d_solver.getIntegerSort();
Sort s2 = d_solver.getRealSort();
assertEquals(Arrays.asList((new Term[] {t1, t2, t3})), Arrays.asList(tup.getTupleValue()));
}
- @Test void getFloatingPoint() throws CVC5ApiException
+ @Test
+ void getFloatingPoint() throws CVC5ApiException
{
Term bvval = d_solver.mkBitVector(16, "0000110000000011", 2);
Term fp = d_solver.mkFloatingPoint(5, 11, bvval);
assertTrue(d_solver.mkFloatingPointNaN(5, 11).isFloatingPointNaN());
}
- @Test void getSet()
+ @Test
+ void getSet()
{
Sort s = d_solver.mkSetSort(d_solver.getIntegerSort());
assertEquals(a, b);
}
- @Test void getSequence()
+ @Test
+ void getSequence()
{
Sort s = d_solver.mkSequenceSort(d_solver.getIntegerSort());
assertEquals(Arrays.asList(new Term[] {i1, i1, i2}), Arrays.asList(s5.getSequenceValue()));
}
- @Test void getCardinalityConstraint() throws CVC5ApiException
+ @Test
+ void getCardinalityConstraint() throws CVC5ApiException
{
Sort su = d_solver.mkUninterpretedSort("u");
Term t = d_solver.mkCardinalityConstraint(su, 3);
assertThrows(CVC5ApiException.class, () -> nullt.isCardinalityConstraint());
}
- @Test void substitute()
+ @Test
+ void substitute()
{
Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
Term one = d_solver.mkInteger(1);
assertThrows(CVC5ApiException.class, () -> xpx.substitute(es, rs));
}
- @Test void constArray() throws CVC5ApiException
+ @Test
+ void constArray() throws CVC5ApiException
{
Sort intsort = d_solver.getIntegerSort();
Sort arrsort = d_solver.mkArraySort(intsort, intsort);
stores = d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
}
- @Test void getSequenceValue() throws CVC5ApiException
+ @Test
+ void getSequenceValue() throws CVC5ApiException
{
Sort realsort = d_solver.getRealSort();
Sort seqsort = d_solver.mkSequenceSort(realsort);
assertThrows(CVC5ApiException.class, () -> su.getSequenceValue());
}
- @Test void termScopedToString()
+ @Test
+ void termScopedToString()
{
Sort intsort = d_solver.getIntegerSort();
Term x = d_solver.mkConst(intsort, "x");
projects / cvc5.git / commitdiff