ada/cvc5
0
0
Fork 0
mirror of https://github.com/AdaCore/cvc5.git synced 2026-02-12 12:32:16 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
cvc5/test/unit/api/java/TermTest.java
Daniel Larraz 27b2af6ebe ci: Use the lowest supported Java version for each platform (#11925) 
This PR uses Java 8 in CI, except on macOS arm64, where the minimum
supported Java version is 11. This ensures that the Java bindings, Java
API tests, and Java examples are compatible with the minimum required
Java version. It also ensures that the published Java bindings on GitHub
can run with this older version. Previously, CMake enforced
compatibility for the Java bindings, but not for the Java API tests or
the Java examples. This change provides a more centralized solution.

This PR also fixes a Java unit test to make it compatible with Java 8.
2025-06-02 20:54:09 +00:00

1242 lines
50 KiB
Java
Raw Permalink Blame History

/******************************************************************************
* Top contributors (to current version):
* Mudathir Mohamed, Aina Niemetz, Andrew Reynolds
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* Black box testing of the Term class.
*/
package tests;
import static io.github.cvc5.Kind.*;
import static org.junit.jupiter.api.Assertions.*;
import io.github.cvc5.*;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Set;
import java.util.stream.Collectors;
import org.junit.jupiter.api.AfterEach;
import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.Test;
class TermTest
{
private TermManager d_tm;
private Solver d_solver;
@BeforeEach
void setUp()
{
d_tm = new TermManager();
d_solver = new Solver(d_tm);
}
@AfterEach
void tearDown()
{
Context.deletePointers();
}
@Test
void equalHash()
{
Sort uSort = d_tm.mkUninterpretedSort("u");
Term x = d_tm.mkVar(uSort, "x");
Term y = d_tm.mkVar(uSort, "y");
Term z = new Term();
assertTrue(x.equals(x));
assertFalse(x.equals(y));
assertFalse(x.equals(z));
assertEquals(x.hashCode(), x.hashCode());
assertNotEquals(x.hashCode(), y.hashCode());
assertNotEquals(x.hashCode(), z.hashCode());
}
@Test
void getId()
{
Term n = new Term();
assertThrows(CVC5ApiException.class, () -> n.getId());
Term x = d_tm.mkVar(d_tm.getIntegerSort(), "x");
assertDoesNotThrow(() -> x.getId());
Term y = x;
assertEquals(x.getId(), y.getId());
Term z = d_tm.mkVar(d_tm.getIntegerSort(), "z");
assertNotEquals(x.getId(), z.getId());
}
@Test
void getKind() throws CVC5ApiException
{
Sort uSort = d_tm.mkUninterpretedSort("u");
Sort intSort = d_tm.getIntegerSort();
Sort boolSort = d_tm.getBooleanSort();
Sort funSort1 = d_tm.mkFunctionSort(uSort, intSort);
Sort funSort2 = d_tm.mkFunctionSort(intSort, boolSort);
Term n = new Term();
assertThrows(CVC5ApiException.class, () -> n.getKind());
Term x = d_tm.mkVar(uSort, "x");
assertDoesNotThrow(() -> x.getKind());
Term y = d_tm.mkVar(uSort, "y");
assertDoesNotThrow(() -> y.getKind());
Term f = d_tm.mkVar(funSort1, "f");
assertDoesNotThrow(() -> f.getKind());
Term p = d_tm.mkVar(funSort2, "p");
assertDoesNotThrow(() -> p.getKind());
Term zero = d_tm.mkInteger(0);
assertDoesNotThrow(() -> zero.getKind());
Term f_x = d_tm.mkTerm(APPLY_UF, f, x);
assertDoesNotThrow(() -> f_x.getKind());
Term f_y = d_tm.mkTerm(APPLY_UF, f, y);
assertDoesNotThrow(() -> f_y.getKind());
Term sum = d_tm.mkTerm(ADD, f_x, f_y);
assertDoesNotThrow(() -> sum.getKind());
Term p_0 = d_tm.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.getKind());
Term p_f_y = d_tm.mkTerm(APPLY_UF, p, f_y);
assertDoesNotThrow(() -> p_f_y.getKind());
// Sequence kinds do not exist internally, test that the API properly
// converts them back.
Sort seqSort = d_tm.mkSequenceSort(intSort);
Term s = d_tm.mkConst(seqSort, "s");
Term ss = d_tm.mkTerm(SEQ_CONCAT, s, s);
assertEquals(ss.getKind(), SEQ_CONCAT);
}
@Test
void getSort() throws CVC5ApiException
{
Sort bvSort = d_tm.mkBitVectorSort(8);
Sort intSort = d_tm.getIntegerSort();
Sort boolSort = d_tm.getBooleanSort();
Sort funSort1 = d_tm.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_tm.mkFunctionSort(intSort, boolSort);
Term n = new Term();
assertThrows(CVC5ApiException.class, () -> n.getSort());
Term x = d_tm.mkVar(bvSort, "x");
assertDoesNotThrow(() -> x.getSort());
assertEquals(x.getSort(), bvSort);
Term y = d_tm.mkVar(bvSort, "y");
assertDoesNotThrow(() -> y.getSort());
assertEquals(y.getSort(), bvSort);
Term f = d_tm.mkVar(funSort1, "f");
assertDoesNotThrow(() -> f.getSort());
assertEquals(f.getSort(), funSort1);
Term p = d_tm.mkVar(funSort2, "p");
assertDoesNotThrow(() -> p.getSort());
assertEquals(p.getSort(), funSort2);
Term zero = d_tm.mkInteger(0);
assertDoesNotThrow(() -> zero.getSort());
assertEquals(zero.getSort(), intSort);
Term f_x = d_tm.mkTerm(APPLY_UF, f, x);
assertDoesNotThrow(() -> f_x.getSort());
assertEquals(f_x.getSort(), intSort);
Term f_y = d_tm.mkTerm(APPLY_UF, f, y);
assertDoesNotThrow(() -> f_y.getSort());
assertEquals(f_y.getSort(), intSort);
Term sum = d_tm.mkTerm(ADD, f_x, f_y);
assertDoesNotThrow(() -> sum.getSort());
assertEquals(sum.getSort(), intSort);
Term p_0 = d_tm.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.getSort());
assertEquals(p_0.getSort(), boolSort);
Term p_f_y = d_tm.mkTerm(APPLY_UF, p, f_y);
assertDoesNotThrow(() -> p_f_y.getSort());
assertEquals(p_f_y.getSort(), boolSort);
}
@Test
void getOp() throws CVC5ApiException
{
Sort intsort = d_tm.getIntegerSort();
Sort bvsort = d_tm.mkBitVectorSort(8);
Sort arrsort = d_tm.mkArraySort(bvsort, intsort);
Sort funsort = d_tm.mkFunctionSort(intsort, bvsort);
Term x = d_tm.mkConst(intsort, "x");
Term a = d_tm.mkConst(arrsort, "a");
Term b = d_tm.mkConst(bvsort, "b");
assertFalse(x.hasOp());
assertThrows(CVC5ApiException.class, () -> x.getOp());
Term ab = d_tm.mkTerm(SELECT, a, b);
Op ext = d_tm.mkOp(BITVECTOR_EXTRACT, 4, 0);
Term extb = d_tm.mkTerm(ext, b);
assertTrue(ab.hasOp());
assertFalse(ab.getOp().isIndexed());
// can compare directly to a Kind (will invoke Op constructor)
assertTrue(extb.hasOp());
assertTrue(extb.getOp().isIndexed());
assertEquals(extb.getOp(), ext);
Op bit = d_tm.mkOp(BITVECTOR_BIT, 4);
Term bitb = d_tm.mkTerm(bit, b);
assertEquals(bitb.getKind(), BITVECTOR_BIT);
assertTrue(bitb.hasOp());
assertEquals(bitb.getOp(), bit);
assertTrue(bitb.getOp().isIndexed());
assertEquals(bit.getNumIndices(), 1);
assertEquals(bit.get(0), d_tm.mkInteger(4));
Term f = d_tm.mkConst(funsort, "f");
Term fx = d_tm.mkTerm(APPLY_UF, f, x);
assertFalse(f.hasOp());
assertThrows(CVC5ApiException.class, () -> f.getOp());
assertTrue(fx.hasOp());
List<Term> children = new ArrayList();
Iterator<Term> iterator = fx.iterator();
for (Term t : fx)
{
children.add(t);
}
// testing rebuild from op and children
assertEquals(fx, d_tm.mkTerm(fx.getOp(), children.toArray(new Term[0])));
// Test Datatypes Ops
Sort sort = d_tm.mkParamSort("T");
DatatypeDecl listDecl = d_tm.mkDatatypeDecl("paramlist", new Sort[] {sort});
DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
DatatypeConstructorDecl nil = d_tm.mkDatatypeConstructorDecl("nil");
cons.addSelector("head", sort);
cons.addSelectorSelf("tail");
listDecl.addConstructor(cons);
listDecl.addConstructor(nil);
Sort listSort = d_tm.mkDatatypeSort(listDecl);
Sort intListSort = listSort.instantiate(new Sort[] {d_tm.getIntegerSort()});
Term c = d_tm.mkConst(intListSort, "c");
Datatype list = listSort.getDatatype();
// list datatype constructor and selector operator terms
Term consOpTerm = list.getConstructor("cons").getTerm();
Term nilOpTerm = list.getConstructor("nil").getTerm();
}
@Test
void hasGetSymbol() throws CVC5ApiException
{
Term n = new Term();
Term t = d_tm.mkBoolean(true);
Term c = d_tm.mkConst(d_tm.getBooleanSort(), "|\\|");
assertThrows(CVC5ApiException.class, () -> n.hasSymbol());
assertFalse(t.hasSymbol());
assertTrue(c.hasSymbol());
assertThrows(CVC5ApiException.class, () -> n.getSymbol());
assertThrows(CVC5ApiException.class, () -> t.getSymbol());
assertEquals(c.getSymbol(), "|\\|");
}
@Test
void isNull() throws CVC5ApiException
{
Term x = new Term();
assertTrue(x.isNull());
x = d_tm.mkVar(d_tm.mkBitVectorSort(4), "x");
assertFalse(x.isNull());
}
@Test
void notTerm() throws CVC5ApiException
{
Sort bvSort = d_tm.mkBitVectorSort(8);
Sort intSort = d_tm.getIntegerSort();
Sort boolSort = d_tm.getBooleanSort();
Sort funSort1 = d_tm.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_tm.mkFunctionSort(intSort, boolSort);
assertThrows(CVC5ApiException.class, () -> new Term().notTerm());
Term b = d_tm.mkTrue();
assertDoesNotThrow(() -> b.notTerm());
Term x = d_tm.mkVar(d_tm.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.notTerm());
Term f = d_tm.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.notTerm());
Term p = d_tm.mkVar(funSort2, "p");
assertThrows(CVC5ApiException.class, () -> p.notTerm());
Term zero = d_tm.mkInteger(0);
assertThrows(CVC5ApiException.class, () -> zero.notTerm());
Term f_x = d_tm.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.notTerm());
Term sum = d_tm.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.notTerm());
Term p_0 = d_tm.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.notTerm());
Term p_f_x = d_tm.mkTerm(APPLY_UF, p, f_x);
assertDoesNotThrow(() -> p_f_x.notTerm());
}
@Test
void andTerm() throws CVC5ApiException
{
Sort bvSort = d_tm.mkBitVectorSort(8);
Sort intSort = d_tm.getIntegerSort();
Sort boolSort = d_tm.getBooleanSort();
Sort funSort1 = d_tm.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_tm.mkFunctionSort(intSort, boolSort);
Term b = d_tm.mkTrue();
assertThrows(CVC5ApiException.class, () -> new Term().andTerm(b));
assertThrows(CVC5ApiException.class, () -> b.andTerm(new Term()));
assertDoesNotThrow(() -> b.andTerm(b));
Term x = d_tm.mkVar(d_tm.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.andTerm(b));
assertThrows(CVC5ApiException.class, () -> x.andTerm(x));
Term f = d_tm.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.andTerm(b));
assertThrows(CVC5ApiException.class, () -> f.andTerm(x));
assertThrows(CVC5ApiException.class, () -> f.andTerm(f));
Term p = d_tm.mkVar(funSort2, "p");
assertThrows(CVC5ApiException.class, () -> p.andTerm(b));
assertThrows(CVC5ApiException.class, () -> p.andTerm(x));
assertThrows(CVC5ApiException.class, () -> p.andTerm(f));
assertThrows(CVC5ApiException.class, () -> p.andTerm(p));
Term zero = d_tm.mkInteger(0);
assertThrows(CVC5ApiException.class, () -> zero.andTerm(b));
assertThrows(CVC5ApiException.class, () -> zero.andTerm(x));
assertThrows(CVC5ApiException.class, () -> zero.andTerm(f));
assertThrows(CVC5ApiException.class, () -> zero.andTerm(p));
assertThrows(CVC5ApiException.class, () -> zero.andTerm(zero));
Term f_x = d_tm.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.andTerm(b));
assertThrows(CVC5ApiException.class, () -> f_x.andTerm(x));
assertThrows(CVC5ApiException.class, () -> f_x.andTerm(f));
assertThrows(CVC5ApiException.class, () -> f_x.andTerm(p));
assertThrows(CVC5ApiException.class, () -> f_x.andTerm(zero));
assertThrows(CVC5ApiException.class, () -> f_x.andTerm(f_x));
Term sum = d_tm.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.andTerm(b));
assertThrows(CVC5ApiException.class, () -> sum.andTerm(x));
assertThrows(CVC5ApiException.class, () -> sum.andTerm(f));
assertThrows(CVC5ApiException.class, () -> sum.andTerm(p));
assertThrows(CVC5ApiException.class, () -> sum.andTerm(zero));
assertThrows(CVC5ApiException.class, () -> sum.andTerm(f_x));
assertThrows(CVC5ApiException.class, () -> sum.andTerm(sum));
Term p_0 = d_tm.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.andTerm(b));
assertThrows(CVC5ApiException.class, () -> p_0.andTerm(x));
assertThrows(CVC5ApiException.class, () -> p_0.andTerm(f));
assertThrows(CVC5ApiException.class, () -> p_0.andTerm(p));
assertThrows(CVC5ApiException.class, () -> p_0.andTerm(zero));
assertThrows(CVC5ApiException.class, () -> p_0.andTerm(f_x));
assertThrows(CVC5ApiException.class, () -> p_0.andTerm(sum));
assertDoesNotThrow(() -> p_0.andTerm(p_0));
Term p_f_x = d_tm.mkTerm(APPLY_UF, p, f_x);
assertDoesNotThrow(() -> p_f_x.andTerm(b));
assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(x));
assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(f));
assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(p));
assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(zero));
assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(f_x));
assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(sum));
assertDoesNotThrow(() -> p_f_x.andTerm(p_0));
assertDoesNotThrow(() -> p_f_x.andTerm(p_f_x));
}
@Test
void orTerm() throws CVC5ApiException
{
Sort bvSort = d_tm.mkBitVectorSort(8);
Sort intSort = d_tm.getIntegerSort();
Sort boolSort = d_tm.getBooleanSort();
Sort funSort1 = d_tm.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_tm.mkFunctionSort(intSort, boolSort);
Term b = d_tm.mkTrue();
assertThrows(CVC5ApiException.class, () -> new Term().orTerm(b));
assertThrows(CVC5ApiException.class, () -> b.orTerm(new Term()));
assertDoesNotThrow(() -> b.orTerm(b));
Term x = d_tm.mkVar(d_tm.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.orTerm(b));
assertThrows(CVC5ApiException.class, () -> x.orTerm(x));
Term f = d_tm.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.orTerm(b));
assertThrows(CVC5ApiException.class, () -> f.orTerm(x));
assertThrows(CVC5ApiException.class, () -> f.orTerm(f));
Term p = d_tm.mkVar(funSort2, "p");
assertThrows(CVC5ApiException.class, () -> p.orTerm(b));
assertThrows(CVC5ApiException.class, () -> p.orTerm(x));
assertThrows(CVC5ApiException.class, () -> p.orTerm(f));
assertThrows(CVC5ApiException.class, () -> p.orTerm(p));
Term zero = d_tm.mkInteger(0);
assertThrows(CVC5ApiException.class, () -> zero.orTerm(b));
assertThrows(CVC5ApiException.class, () -> zero.orTerm(x));
assertThrows(CVC5ApiException.class, () -> zero.orTerm(f));
assertThrows(CVC5ApiException.class, () -> zero.orTerm(p));
assertThrows(CVC5ApiException.class, () -> zero.orTerm(zero));
Term f_x = d_tm.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.orTerm(b));
assertThrows(CVC5ApiException.class, () -> f_x.orTerm(x));
assertThrows(CVC5ApiException.class, () -> f_x.orTerm(f));
assertThrows(CVC5ApiException.class, () -> f_x.orTerm(p));
assertThrows(CVC5ApiException.class, () -> f_x.orTerm(zero));
assertThrows(CVC5ApiException.class, () -> f_x.orTerm(f_x));
Term sum = d_tm.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.orTerm(b));
assertThrows(CVC5ApiException.class, () -> sum.orTerm(x));
assertThrows(CVC5ApiException.class, () -> sum.orTerm(f));
assertThrows(CVC5ApiException.class, () -> sum.orTerm(p));
assertThrows(CVC5ApiException.class, () -> sum.orTerm(zero));
assertThrows(CVC5ApiException.class, () -> sum.orTerm(f_x));
assertThrows(CVC5ApiException.class, () -> sum.orTerm(sum));
Term p_0 = d_tm.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.orTerm(b));
assertThrows(CVC5ApiException.class, () -> p_0.orTerm(x));
assertThrows(CVC5ApiException.class, () -> p_0.orTerm(f));
assertThrows(CVC5ApiException.class, () -> p_0.orTerm(p));
assertThrows(CVC5ApiException.class, () -> p_0.orTerm(zero));
assertThrows(CVC5ApiException.class, () -> p_0.orTerm(f_x));
assertThrows(CVC5ApiException.class, () -> p_0.orTerm(sum));
assertDoesNotThrow(() -> p_0.orTerm(p_0));
Term p_f_x = d_tm.mkTerm(APPLY_UF, p, f_x);
assertDoesNotThrow(() -> p_f_x.orTerm(b));
assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(x));
assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(f));
assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(p));
assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(zero));
assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(f_x));
assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(sum));
assertDoesNotThrow(() -> p_f_x.orTerm(p_0));
assertDoesNotThrow(() -> p_f_x.orTerm(p_f_x));
}
@Test
void xorTerm() throws CVC5ApiException
{
Sort bvSort = d_tm.mkBitVectorSort(8);
Sort intSort = d_tm.getIntegerSort();
Sort boolSort = d_tm.getBooleanSort();
Sort funSort1 = d_tm.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_tm.mkFunctionSort(intSort, boolSort);
Term b = d_tm.mkTrue();
assertThrows(CVC5ApiException.class, () -> new Term().xorTerm(b));
assertThrows(CVC5ApiException.class, () -> b.xorTerm(new Term()));
assertDoesNotThrow(() -> b.xorTerm(b));
Term x = d_tm.mkVar(d_tm.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> x.xorTerm(x));
Term f = d_tm.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> f.xorTerm(x));
assertThrows(CVC5ApiException.class, () -> f.xorTerm(f));
Term p = d_tm.mkVar(funSort2, "p");
assertThrows(CVC5ApiException.class, () -> p.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> p.xorTerm(x));
assertThrows(CVC5ApiException.class, () -> p.xorTerm(f));
assertThrows(CVC5ApiException.class, () -> p.xorTerm(p));
Term zero = d_tm.mkInteger(0);
assertThrows(CVC5ApiException.class, () -> zero.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> zero.xorTerm(x));
assertThrows(CVC5ApiException.class, () -> zero.xorTerm(f));
assertThrows(CVC5ApiException.class, () -> zero.xorTerm(p));
assertThrows(CVC5ApiException.class, () -> zero.xorTerm(zero));
Term f_x = d_tm.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(x));
assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(f));
assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(p));
assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(zero));
assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(f_x));
Term sum = d_tm.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> sum.xorTerm(x));
assertThrows(CVC5ApiException.class, () -> sum.xorTerm(f));
assertThrows(CVC5ApiException.class, () -> sum.xorTerm(p));
assertThrows(CVC5ApiException.class, () -> sum.xorTerm(zero));
assertThrows(CVC5ApiException.class, () -> sum.xorTerm(f_x));
assertThrows(CVC5ApiException.class, () -> sum.xorTerm(sum));
Term p_0 = d_tm.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(x));
assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(f));
assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(p));
assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(zero));
assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(f_x));
assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(sum));
assertDoesNotThrow(() -> p_0.xorTerm(p_0));
Term p_f_x = d_tm.mkTerm(APPLY_UF, p, f_x);
assertDoesNotThrow(() -> p_f_x.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(x));
assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(f));
assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(p));
assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(zero));
assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(f_x));
assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(sum));
assertDoesNotThrow(() -> p_f_x.xorTerm(p_0));
assertDoesNotThrow(() -> p_f_x.xorTerm(p_f_x));
}
@Test
void eqTerm() throws CVC5ApiException
{
Sort bvSort = d_tm.mkBitVectorSort(8);
Sort intSort = d_tm.getIntegerSort();
Sort boolSort = d_tm.getBooleanSort();
Sort funSort1 = d_tm.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_tm.mkFunctionSort(intSort, boolSort);
Term b = d_tm.mkTrue();
assertThrows(CVC5ApiException.class, () -> new Term().eqTerm(b));
assertThrows(CVC5ApiException.class, () -> b.eqTerm(new Term()));
assertDoesNotThrow(() -> b.eqTerm(b));
Term x = d_tm.mkVar(d_tm.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.eqTerm(b));
assertDoesNotThrow(() -> x.eqTerm(x));
Term f = d_tm.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.eqTerm(b));
assertThrows(CVC5ApiException.class, () -> f.eqTerm(x));
assertDoesNotThrow(() -> f.eqTerm(f));
Term p = d_tm.mkVar(funSort2, "p");
assertThrows(CVC5ApiException.class, () -> p.eqTerm(b));
assertThrows(CVC5ApiException.class, () -> p.eqTerm(x));
assertThrows(CVC5ApiException.class, () -> p.eqTerm(f));
assertDoesNotThrow(() -> p.eqTerm(p));
Term zero = d_tm.mkInteger(0);
assertThrows(CVC5ApiException.class, () -> zero.eqTerm(b));
assertThrows(CVC5ApiException.class, () -> zero.eqTerm(x));
assertThrows(CVC5ApiException.class, () -> zero.eqTerm(f));
assertThrows(CVC5ApiException.class, () -> zero.eqTerm(p));
assertDoesNotThrow(() -> zero.eqTerm(zero));
Term f_x = d_tm.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(b));
assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(x));
assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(f));
assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(p));
assertDoesNotThrow(() -> f_x.eqTerm(zero));
assertDoesNotThrow(() -> f_x.eqTerm(f_x));
Term sum = d_tm.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.eqTerm(b));
assertThrows(CVC5ApiException.class, () -> sum.eqTerm(x));
assertThrows(CVC5ApiException.class, () -> sum.eqTerm(f));
assertThrows(CVC5ApiException.class, () -> sum.eqTerm(p));
assertDoesNotThrow(() -> sum.eqTerm(zero));
assertDoesNotThrow(() -> sum.eqTerm(f_x));
assertDoesNotThrow(() -> sum.eqTerm(sum));
Term p_0 = d_tm.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.eqTerm(b));
assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(x));
assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(f));
assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(p));
assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(zero));
assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(f_x));
assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(sum));
assertDoesNotThrow(() -> p_0.eqTerm(p_0));
Term p_f_x = d_tm.mkTerm(APPLY_UF, p, f_x);
assertDoesNotThrow(() -> p_f_x.eqTerm(b));
assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(x));
assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(f));
assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(p));
assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(zero));
assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(f_x));
assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(sum));
assertDoesNotThrow(() -> p_f_x.eqTerm(p_0));
assertDoesNotThrow(() -> p_f_x.eqTerm(p_f_x));
}
@Test
void impTerm() throws CVC5ApiException
{
Sort bvSort = d_tm.mkBitVectorSort(8);
Sort intSort = d_tm.getIntegerSort();
Sort boolSort = d_tm.getBooleanSort();
Sort funSort1 = d_tm.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_tm.mkFunctionSort(intSort, boolSort);
Term b = d_tm.mkTrue();
assertThrows(CVC5ApiException.class, () -> new Term().impTerm(b));
assertThrows(CVC5ApiException.class, () -> b.impTerm(new Term()));
assertDoesNotThrow(() -> b.impTerm(b));
Term x = d_tm.mkVar(d_tm.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.impTerm(b));
assertThrows(CVC5ApiException.class, () -> x.impTerm(x));
Term f = d_tm.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.impTerm(b));
assertThrows(CVC5ApiException.class, () -> f.impTerm(x));
assertThrows(CVC5ApiException.class, () -> f.impTerm(f));
Term p = d_tm.mkVar(funSort2, "p");
assertThrows(CVC5ApiException.class, () -> p.impTerm(b));
assertThrows(CVC5ApiException.class, () -> p.impTerm(x));
assertThrows(CVC5ApiException.class, () -> p.impTerm(f));
assertThrows(CVC5ApiException.class, () -> p.impTerm(p));
Term zero = d_tm.mkInteger(0);
assertThrows(CVC5ApiException.class, () -> zero.impTerm(b));
assertThrows(CVC5ApiException.class, () -> zero.impTerm(x));
assertThrows(CVC5ApiException.class, () -> zero.impTerm(f));
assertThrows(CVC5ApiException.class, () -> zero.impTerm(p));
assertThrows(CVC5ApiException.class, () -> zero.impTerm(zero));
Term f_x = d_tm.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.impTerm(b));
assertThrows(CVC5ApiException.class, () -> f_x.impTerm(x));
assertThrows(CVC5ApiException.class, () -> f_x.impTerm(f));
assertThrows(CVC5ApiException.class, () -> f_x.impTerm(p));
assertThrows(CVC5ApiException.class, () -> f_x.impTerm(zero));
assertThrows(CVC5ApiException.class, () -> f_x.impTerm(f_x));
Term sum = d_tm.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.impTerm(b));
assertThrows(CVC5ApiException.class, () -> sum.impTerm(x));
assertThrows(CVC5ApiException.class, () -> sum.impTerm(f));
assertThrows(CVC5ApiException.class, () -> sum.impTerm(p));
assertThrows(CVC5ApiException.class, () -> sum.impTerm(zero));
assertThrows(CVC5ApiException.class, () -> sum.impTerm(f_x));
assertThrows(CVC5ApiException.class, () -> sum.impTerm(sum));
Term p_0 = d_tm.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.impTerm(b));
assertThrows(CVC5ApiException.class, () -> p_0.impTerm(x));
assertThrows(CVC5ApiException.class, () -> p_0.impTerm(f));
assertThrows(CVC5ApiException.class, () -> p_0.impTerm(p));
assertThrows(CVC5ApiException.class, () -> p_0.impTerm(zero));
assertThrows(CVC5ApiException.class, () -> p_0.impTerm(f_x));
assertThrows(CVC5ApiException.class, () -> p_0.impTerm(sum));
assertDoesNotThrow(() -> p_0.impTerm(p_0));
Term p_f_x = d_tm.mkTerm(APPLY_UF, p, f_x);
assertDoesNotThrow(() -> p_f_x.impTerm(b));
assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(x));
assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(f));
assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(p));
assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(zero));
assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(f_x));
assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(sum));
assertDoesNotThrow(() -> p_f_x.impTerm(p_0));
assertDoesNotThrow(() -> p_f_x.impTerm(p_f_x));
}
@Test
void iteTerm() throws CVC5ApiException
{
Sort bvSort = d_tm.mkBitVectorSort(8);
Sort intSort = d_tm.getIntegerSort();
Sort boolSort = d_tm.getBooleanSort();
Sort funSort1 = d_tm.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_tm.mkFunctionSort(intSort, boolSort);
Term b = d_tm.mkTrue();
assertThrows(CVC5ApiException.class, () -> new Term().iteTerm(b, b));
assertThrows(CVC5ApiException.class, () -> b.iteTerm(new Term(), b));
assertThrows(CVC5ApiException.class, () -> b.iteTerm(b, new Term()));
assertDoesNotThrow(() -> b.iteTerm(b, b));
Term x = d_tm.mkVar(d_tm.mkBitVectorSort(8), "x");
assertDoesNotThrow(() -> b.iteTerm(x, x));
assertDoesNotThrow(() -> b.iteTerm(b, b));
assertThrows(CVC5ApiException.class, () -> b.iteTerm(x, b));
assertThrows(CVC5ApiException.class, () -> x.iteTerm(x, x));
assertThrows(CVC5ApiException.class, () -> x.iteTerm(x, b));
Term f = d_tm.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.iteTerm(b, b));
assertThrows(CVC5ApiException.class, () -> x.iteTerm(b, x));
Term p = d_tm.mkVar(funSort2, "p");
assertThrows(CVC5ApiException.class, () -> p.iteTerm(b, b));
assertThrows(CVC5ApiException.class, () -> p.iteTerm(x, b));
Term zero = d_tm.mkInteger(0);
assertThrows(CVC5ApiException.class, () -> zero.iteTerm(x, x));
assertThrows(CVC5ApiException.class, () -> zero.iteTerm(x, b));
Term f_x = d_tm.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, b));
assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, x));
Term sum = d_tm.mkTerm(ADD, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.iteTerm(x, x));
assertThrows(CVC5ApiException.class, () -> sum.iteTerm(b, x));
Term p_0 = d_tm.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.iteTerm(b, b));
assertDoesNotThrow(() -> p_0.iteTerm(x, x));
assertThrows(CVC5ApiException.class, () -> p_0.iteTerm(x, b));
Term p_f_x = d_tm.mkTerm(APPLY_UF, p, f_x);
assertDoesNotThrow(() -> p_f_x.iteTerm(b, b));
assertDoesNotThrow(() -> p_f_x.iteTerm(x, x));
assertThrows(CVC5ApiException.class, () -> p_f_x.iteTerm(x, b));
}
@Test
void termAssignment()
{
Term t1 = d_tm.mkInteger(1);
Term t2 = t1;
t2 = d_tm.mkInteger(2);
assertEquals(t1, d_tm.mkInteger(1));
}
@Test
void termCompare()
{
Term t1 = d_tm.mkInteger(1);
Term t2 = d_tm.mkTerm(ADD, d_tm.mkInteger(2), d_tm.mkInteger(2));
Term t3 = d_tm.mkTerm(ADD, d_tm.mkInteger(2), d_tm.mkInteger(2));
assertTrue(t2.compareTo(t3) >= 0);
assertTrue(t2.compareTo(t3) <= 0);
assertTrue((t1.compareTo(t2) > 0) != (t1.compareTo(t2) < 0));
assertTrue((t1.compareTo(t2) > 0 || t1.equals(t2)) == (t1.compareTo(t2) >= 0));
}
@Test
void termChildren() throws CVC5ApiException
{
// simple term 2+3
Term two = d_tm.mkInteger(2);
Term t1 = d_tm.mkTerm(ADD, two, d_tm.mkInteger(3));
assertEquals(t1.getChild(0), two);
assertEquals(t1.getNumChildren(), 2);
Term tnull = new Term();
assertThrows(CVC5ApiException.class, () -> tnull.getNumChildren());
// apply term f(2)
Sort intSort = d_tm.getIntegerSort();
Sort fsort = d_tm.mkFunctionSort(intSort, intSort);
Term f = d_tm.mkConst(fsort, "f");
Term t2 = d_tm.mkTerm(APPLY_UF, f, two);
// due to our higher-order view of terms, we treat f as a child of APPLY_UF
assertEquals(t2.getNumChildren(), 2);
assertEquals(t2.getChild(0), f);
assertEquals(t2.getChild(1), two);
assertThrows(CVC5ApiException.class, () -> tnull.getChild(0));
}
@Test
void getIntegerValue() throws CVC5ApiException
{
Term int1 = d_tm.mkInteger("-18446744073709551616");
Term int2 = d_tm.mkInteger("-18446744073709551615");
Term int3 = d_tm.mkInteger("-4294967296");
Term int4 = d_tm.mkInteger("-4294967295");
Term int5 = d_tm.mkInteger("-10");
Term int6 = d_tm.mkInteger("0");
Term int7 = d_tm.mkInteger("10");
Term int8 = d_tm.mkInteger("4294967295");
Term int9 = d_tm.mkInteger("4294967296");
Term int10 = d_tm.mkInteger("18446744073709551615");
Term int11 = d_tm.mkInteger("18446744073709551616");
Term int12 = d_tm.mkInteger("-0");
assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(""));
assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("-"));
assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("-1-"));
assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("0.0"));
assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("-0.1"));
assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("012"));
assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("0000"));
assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("-01"));
assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger("-00"));
assertTrue(int1.isIntegerValue());
assertEquals(int1.getIntegerValue().toString(), "-18446744073709551616");
assertEquals(int1.getRealOrIntegerValueSign(), -1);
assertTrue(int2.isIntegerValue());
assertEquals(int2.getIntegerValue().toString(), "-18446744073709551615");
assertTrue(int3.isIntegerValue());
assertEquals(int3.getIntegerValue().longValue(), -4294967296L);
assertEquals(int3.getIntegerValue().toString(), "-4294967296");
assertTrue(int4.isIntegerValue());
assertEquals(int4.getIntegerValue().longValue(), -4294967295L);
assertEquals(int4.getIntegerValue().toString(), "-4294967295");
assertTrue(int5.isIntegerValue());
assertEquals(int5.getIntegerValue().intValue(), -10);
assertEquals(int5.getIntegerValue().intValue(), -10);
assertEquals(int5.getIntegerValue().toString(), "-10");
assertTrue(int6.isIntegerValue());
assertEquals(int6.getIntegerValue().intValue(), 0);
assertEquals(int6.getIntegerValue().intValue(), 0);
assertEquals(int6.getIntegerValue().toString(), "0");
assertEquals(int6.getRealOrIntegerValueSign(), 0);
assertTrue(int7.isIntegerValue());
assertEquals(int7.getIntegerValue().intValue(), 10);
assertEquals(int7.getIntegerValue().intValue(), 10);
assertEquals(int7.getIntegerValue().toString(), "10");
assertEquals(int7.getRealOrIntegerValueSign(), 1);
assertTrue(int8.isIntegerValue());
assertEquals(int8.getIntegerValue().longValue(), 4294967295L);
assertEquals(int8.getIntegerValue().toString(), "4294967295");
assertTrue(int9.isIntegerValue());
assertEquals(int9.getIntegerValue().longValue(), 4294967296L);
assertEquals(int9.getIntegerValue().toString(), "4294967296");
assertTrue(int10.isIntegerValue());
assertEquals(int10.getIntegerValue().toString(), "18446744073709551615");
assertTrue(int11.isIntegerValue());
assertEquals(int11.getIntegerValue().toString(), "18446744073709551616");
}
@Test
void getString()
{
Term s1 = d_tm.mkString("abcde");
assertTrue(s1.isStringValue());
assertEquals(s1.getStringValue(), "abcde");
Term s2 = d_tm.mkString("\\u{200cb}", true);
assertEquals(s2.getStringValue(), new String(Character.toChars(0x200cb)));
}
@Test
void getReal() throws CVC5ApiException
{
Term real1 = d_tm.mkReal("0");
Term real2 = d_tm.mkReal(".0");
Term real3 = d_tm.mkReal("-17");
Term real4 = d_tm.mkReal("-3/5");
Term real5 = d_tm.mkReal("12.7");
Term real6 = d_tm.mkReal("1/4294967297");
Term real7 = d_tm.mkReal("4294967297");
Term real8 = d_tm.mkReal("1/18446744073709551617");
Term real9 = d_tm.mkReal("18446744073709551617");
Term real10 = d_tm.mkReal("2343.2343");
assertTrue(real1.isRealValue());
assertTrue(real2.isRealValue());
assertTrue(real3.isRealValue());
assertTrue(real4.isRealValue());
assertTrue(real5.isRealValue());
assertTrue(real6.isRealValue());
assertTrue(real7.isRealValue());
assertTrue(real8.isRealValue());
assertTrue(real9.isRealValue());
assertTrue(real10.isRealValue());
assertEquals("0/1", Utils.getRational(real1.getRealValue()));
assertEquals("0/1", Utils.getRational(real2.getRealValue()));
assertEquals("-17/1", Utils.getRational(real3.getRealValue()));
assertEquals("-3/5", Utils.getRational(real4.getRealValue()));
assertEquals("127/10", Utils.getRational(real5.getRealValue()));
assertEquals("1/4294967297", Utils.getRational(real6.getRealValue()));
assertEquals("4294967297/1", Utils.getRational(real7.getRealValue()));
assertEquals("1/18446744073709551617", Utils.getRational(real8.getRealValue()));
assertEquals("18446744073709551617/1", Utils.getRational(real9.getRealValue()));
assertEquals("23432343/10000", Utils.getRational(real10.getRealValue()));
assertThrows(CVC5ApiException.class, () -> d_tm.mkReal("1/0"));
assertThrows(CVC5ApiException.class, () -> d_tm.mkReal("2/0000"));
}
@Test
void getConstArrayBase()
{
Sort intsort = d_tm.getIntegerSort();
Sort arrsort = d_tm.mkArraySort(intsort, intsort);
Term one = d_tm.mkInteger(1);
Term constarr = d_tm.mkConstArray(arrsort, one);
assertTrue(constarr.isConstArray());
assertEquals(one, constarr.getConstArrayBase());
Term a = d_tm.mkConst(arrsort, "a");
assertThrows(CVC5ApiException.class, () -> a.getConstArrayBase());
assertThrows(CVC5ApiException.class, () -> one.getConstArrayBase());
}
@Test
void getBoolean()
{
Term b1 = d_tm.mkBoolean(true);
Term b2 = d_tm.mkBoolean(false);
assertTrue(b1.isBooleanValue());
assertTrue(b2.isBooleanValue());
assertTrue(b1.getBooleanValue());
assertFalse(b2.getBooleanValue());
}
@Test
void getBitVector() throws CVC5ApiException
{
Term b1 = d_tm.mkBitVector(8, 15);
Term b2 = d_tm.mkBitVector(8, "00001111", 2);
Term b3 = d_tm.mkBitVector(8, "15", 10);
Term b4 = d_tm.mkBitVector(8, "0f", 16);
Term b5 = d_tm.mkBitVector(9, "00001111", 2);
Term b6 = d_tm.mkBitVector(9, "15", 10);
Term b7 = d_tm.mkBitVector(9, "0f", 16);
assertTrue(b1.isBitVectorValue());
assertTrue(b2.isBitVectorValue());
assertTrue(b3.isBitVectorValue());
assertTrue(b4.isBitVectorValue());
assertTrue(b5.isBitVectorValue());
assertTrue(b6.isBitVectorValue());
assertTrue(b7.isBitVectorValue());
assertEquals("00001111", b1.getBitVectorValue(2));
assertEquals("15", b1.getBitVectorValue(10));
assertEquals("f", b1.getBitVectorValue(16));
assertEquals("00001111", b2.getBitVectorValue(2));
assertEquals("15", b2.getBitVectorValue(10));
assertEquals("f", b2.getBitVectorValue(16));
assertEquals("00001111", b3.getBitVectorValue(2));
assertEquals("15", b3.getBitVectorValue(10));
assertEquals("f", b3.getBitVectorValue(16));
assertEquals("00001111", b4.getBitVectorValue(2));
assertEquals("15", b4.getBitVectorValue(10));
assertEquals("f", b4.getBitVectorValue(16));
assertEquals("000001111", b5.getBitVectorValue(2));
assertEquals("15", b5.getBitVectorValue(10));
assertEquals("f", b5.getBitVectorValue(16));
assertEquals("000001111", b6.getBitVectorValue(2));
assertEquals("15", b6.getBitVectorValue(10));
assertEquals("f", b6.getBitVectorValue(16));
assertEquals("000001111", b7.getBitVectorValue(2));
assertEquals("15", b7.getBitVectorValue(10));
assertEquals("f", b7.getBitVectorValue(16));
}
@Test
void getUninterpretedSortValue() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
Sort uSort = d_tm.mkUninterpretedSort("u");
Term x = d_tm.mkConst(uSort, "x");
Term y = d_tm.mkConst(uSort, "y");
d_solver.assertFormula(d_tm.mkTerm(EQUAL, x, y));
assertTrue(d_solver.checkSat().isSat());
Term vx = d_solver.getValue(x);
Term vy = d_solver.getValue(y);
assertEquals(vx.isUninterpretedSortValue(), vy.isUninterpretedSortValue());
assertDoesNotThrow(() -> vx.getUninterpretedSortValue());
assertDoesNotThrow(() -> vy.getUninterpretedSortValue());
}
@Test
void isRoundingModeValue() throws CVC5ApiException
{
assertFalse(d_tm.mkInteger(15).isRoundingModeValue());
assertTrue(d_tm.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).isRoundingModeValue());
assertFalse(d_tm.mkConst(d_tm.getRoundingModeSort()).isRoundingModeValue());
}
@Test
void getRoundingModeValue() throws CVC5ApiException
{
assertThrows(CVC5ApiException.class, () -> d_tm.mkInteger(15).getRoundingModeValue());
assertEquals(
d_tm.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).getRoundingModeValue(),
RoundingMode.ROUND_NEAREST_TIES_TO_EVEN);
assertEquals(d_tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE).getRoundingModeValue(),
RoundingMode.ROUND_TOWARD_POSITIVE);
assertEquals(d_tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE).getRoundingModeValue(),
RoundingMode.ROUND_TOWARD_NEGATIVE);
assertEquals(d_tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO).getRoundingModeValue(),
RoundingMode.ROUND_TOWARD_ZERO);
assertEquals(
d_tm.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY).getRoundingModeValue(),
RoundingMode.ROUND_NEAREST_TIES_TO_AWAY);
}
@Test
void getTuple()
{
Term t1 = d_tm.mkInteger(15);
Term t2 = d_tm.mkReal(17, 25);
Term t3 = d_tm.mkString("abc");
Term tup = d_tm.mkTuple(new Term[] {t1, t2, t3});
assertTrue(tup.isTupleValue());
assertEquals(Arrays.asList((new Term[] {t1, t2, t3})), Arrays.asList(tup.getTupleValue()));
}
@Test
void getFloatingPoint() throws CVC5ApiException
{
Term bvval = d_tm.mkBitVector(16, "0000110000000011", 2);
Term fp = d_tm.mkFloatingPoint(5, 11, bvval);
assertTrue(fp.isFloatingPointValue());
assertFalse(fp.isFloatingPointPosZero());
assertFalse(fp.isFloatingPointNegZero());
assertFalse(fp.isFloatingPointPosInf());
assertFalse(fp.isFloatingPointNegInf());
assertFalse(fp.isFloatingPointNaN());
assertEquals(new Triplet<Long, Long, Term>(5L, 11L, bvval), fp.getFloatingPointValue());
assertTrue(d_tm.mkFloatingPointPosZero(5, 11).isFloatingPointPosZero());
assertTrue(d_tm.mkFloatingPointNegZero(5, 11).isFloatingPointNegZero());
assertTrue(d_tm.mkFloatingPointPosInf(5, 11).isFloatingPointPosInf());
assertTrue(d_tm.mkFloatingPointNegInf(5, 11).isFloatingPointNegInf());
assertTrue(d_tm.mkFloatingPointNaN(5, 11).isFloatingPointNaN());
}
@Test
void getSet()
{
Sort s = d_tm.mkSetSort(d_tm.getIntegerSort());
Term i1 = d_tm.mkInteger(5);
Term i2 = d_tm.mkInteger(7);
Term s1 = d_tm.mkEmptySet(s);
Term s2 = d_tm.mkTerm(Kind.SET_SINGLETON, i1);
Term s3 = d_tm.mkTerm(Kind.SET_SINGLETON, i1);
Term s4 = d_tm.mkTerm(Kind.SET_SINGLETON, i2);
Term s5 = d_tm.mkTerm(Kind.SET_UNION, s2, d_tm.mkTerm(Kind.SET_UNION, s3, s4));
assertTrue(s1.isSetValue());
assertTrue(s2.isSetValue());
assertTrue(s3.isSetValue());
assertTrue(s4.isSetValue());
assertFalse(s5.isSetValue());
s5 = d_solver.simplify(s5);
assertTrue(s5.isSetValue());
assertSetsEquality(new Term[] {}, s1.getSetValue());
assertSetsEquality(new Term[] {i1}, s2.getSetValue());
assertSetsEquality(new Term[] {i1}, s3.getSetValue());
assertSetsEquality(new Term[] {i2}, s4.getSetValue());
assertSetsEquality(new Term[] {i1, i2}, s5.getSetValue());
}
private void assertSetsEquality(Term[] A, Set<Term> B)
{
List<Term> a = Arrays.stream(A).sorted().collect(Collectors.toList());
List<Term> b = B.stream().sorted().collect(Collectors.toList());
assertEquals(a, b);
}
@Test
void getSequence()
{
Sort s = d_tm.mkSequenceSort(d_tm.getIntegerSort());
Term i1 = d_tm.mkInteger(5);
Term i2 = d_tm.mkInteger(7);
Term s1 = d_tm.mkEmptySequence(s);
Term s2 = d_tm.mkTerm(Kind.SEQ_UNIT, i1);
Term s3 = d_tm.mkTerm(Kind.SEQ_UNIT, i1);
Term s4 = d_tm.mkTerm(Kind.SEQ_UNIT, i2);
Term s5 = d_tm.mkTerm(Kind.SEQ_CONCAT, s2, d_tm.mkTerm(Kind.SEQ_CONCAT, s3, s4));
assertTrue(s1.isSequenceValue());
assertTrue(!s2.isSequenceValue());
assertTrue(!s3.isSequenceValue());
assertTrue(!s4.isSequenceValue());
assertTrue(!s5.isSequenceValue());
s2 = d_solver.simplify(s2);
s3 = d_solver.simplify(s3);
s4 = d_solver.simplify(s4);
s5 = d_solver.simplify(s5);
assertEquals(Arrays.asList(new Term[] {}), Arrays.asList(s1.getSequenceValue()));
assertEquals(Arrays.asList(new Term[] {i1}), Arrays.asList(s2.getSequenceValue()));
assertEquals(Arrays.asList(new Term[] {i1}), Arrays.asList(s3.getSequenceValue()));
assertEquals(Arrays.asList(new Term[] {i2}), Arrays.asList(s4.getSequenceValue()));
assertEquals(Arrays.asList(new Term[] {i1, i1, i2}), Arrays.asList(s5.getSequenceValue()));
}
@Test
void getCardinalityConstraint() throws CVC5ApiException
{
Sort su = d_tm.mkUninterpretedSort("u");
Term t = d_tm.mkCardinalityConstraint(su, 3);
assertTrue(t.isCardinalityConstraint());
Pair<Sort, BigInteger> cc = t.getCardinalityConstraint();
assertEquals(cc.first, su);
assertEquals(cc.second, new BigInteger("3"));
Term x = d_tm.mkConst(d_tm.getIntegerSort(), "x");
assertFalse(x.isCardinalityConstraint());
assertThrows(CVC5ApiException.class, () -> x.getCardinalityConstraint());
Term nullt = new Term();
assertThrows(CVC5ApiException.class, () -> nullt.isCardinalityConstraint());
}
@Test
void getRealAlgebraicNumber() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
d_solver.setLogic("QF_NRA");
Sort realsort = d_tm.getRealSort();
Term x = d_tm.mkConst(realsort, "x");
Term x2 = d_tm.mkTerm(MULT, x, x);
Term two = d_tm.mkReal(2, 1);
Term eq = d_tm.mkTerm(EQUAL, x2, two);
d_solver.assertFormula(eq);
// Note that check-sat should only return "sat" if libpoly is enabled.
// Otherwise, we do not test the following functionality.
if (d_solver.checkSat().isSat())
{
// We find a model for (x*x = 2), where x should be a real algebraic number.
// We assert that its defining polynomial is non-null and its lower and
// upper bounds are real.
Term vx = d_solver.getValue(x);
assertTrue(vx.isRealAlgebraicNumber());
Term y = d_tm.mkVar(realsort, "y");
Term poly = vx.getRealAlgebraicNumberDefiningPolynomial(y);
assertTrue(!poly.isNull());
Term lb = vx.getRealAlgebraicNumberLowerBound();
assertTrue(lb.isRealValue());
Term ub = vx.getRealAlgebraicNumberUpperBound();
assertTrue(ub.isRealValue());
// cannot call with non-variable
Term yc = d_tm.mkConst(realsort, "y");
assertThrows(CVC5ApiException.class, () ->vx.getRealAlgebraicNumberDefiningPolynomial(yc));
}
}
@Test
void getSkolem() throws CVC5ApiException
{
// ordinary variables are not skolems
Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
assertFalse(x.isSkolem());
assertThrows(CVC5ApiException.class, () ->x.getSkolemId());
assertThrows(CVC5ApiException.class, () ->x.getSkolemIndices());
}
@Test
void testMkSkolem() throws CVC5ApiException
{
Sort integer = d_solver.getIntegerSort();
Sort arraySort = d_solver.mkArraySort(integer, integer);
Term a = d_solver.mkConst(arraySort, "a");
Term b = d_solver.mkConst(arraySort, "b");
Term sk = d_tm.mkSkolem(SkolemId.ARRAY_DEQ_DIFF, new Term[] {a, b});
Term sk2 = d_tm.mkSkolem(SkolemId.ARRAY_DEQ_DIFF, new Term[] {b, a});
assertTrue(sk.isSkolem());
assertEquals(sk.getSkolemId(), SkolemId.ARRAY_DEQ_DIFF);
assertEquals(Arrays.asList(new Term[] {a, b}), Arrays.asList(sk.getSkolemIndices()));
// ARRAY_DEQ_DIFF is commutative, so the order of the indices is sorted.
assertEquals(Arrays.asList(new Term[] {a, b}), Arrays.asList(sk2.getSkolemIndices()));
}
@Test
void testGetNumIndices() throws CVC5ApiException
{
int numIndices = d_tm.getNumIndicesForSkolemId(SkolemId.ARRAY_DEQ_DIFF);
assertEquals(numIndices, 2);
}
@Test
void substitute()
{
Term x = d_tm.mkConst(d_tm.getIntegerSort(), "x");
Term one = d_tm.mkInteger(1);
Term ttrue = d_tm.mkTrue();
Term xpx = d_tm.mkTerm(ADD, x, x);
Term onepone = d_tm.mkTerm(ADD, one, one);
assertEquals(xpx.substitute(x, one), onepone);
assertEquals(onepone.substitute(one, x), xpx);
// incorrect due to type
assertThrows(CVC5ApiException.class, () -> xpx.substitute(one, ttrue));
// simultaneous substitution
Term y = d_tm.mkConst(d_tm.getIntegerSort(), "y");
Term xpy = d_tm.mkTerm(ADD, x, y);
Term xpone = d_tm.mkTerm(ADD, y, one);
List<Term> es = new ArrayList<>();
List<Term> rs = new ArrayList<>();
es.add(x);
rs.add(y);
es.add(y);
rs.add(one);
assertEquals(xpy.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])), xpone);
// incorrect substitution due to arity
rs.remove(rs.size() - 1);
assertThrows(CVC5ApiException.class,
() -> xpy.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])));
// incorrect substitution due to types
rs.add(ttrue);
assertThrows(CVC5ApiException.class,
() -> xpy.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])));
// null cannot substitute
Term tnull = new Term();
assertThrows(CVC5ApiException.class, () -> tnull.substitute(one, x));
assertThrows(CVC5ApiException.class, () -> xpx.substitute(tnull, x));
assertThrows(CVC5ApiException.class, () -> xpx.substitute(x, tnull));
rs.remove(rs.size() - 1);
rs.add(tnull);
assertThrows(CVC5ApiException.class,
() -> xpy.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])));
es.clear();
rs.clear();
es.add(x);
rs.add(y);
assertThrows(CVC5ApiException.class,
() -> tnull.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])));
es.add(tnull);
rs.add(one);
assertThrows(CVC5ApiException.class,
() -> xpx.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])));
}
@Test
void constArray() throws CVC5ApiException
{
Sort intsort = d_tm.getIntegerSort();
Sort arrsort = d_tm.mkArraySort(intsort, intsort);
Term a = d_tm.mkConst(arrsort, "a");
Term one = d_tm.mkInteger(1);
Term two = d_tm.mkBitVector(2, 2);
Term iconst = d_tm.mkConst(intsort);
Term constarr = d_tm.mkConstArray(arrsort, one);
assertThrows(CVC5ApiException.class, () -> d_tm.mkConstArray(arrsort, two));
assertThrows(CVC5ApiException.class, () -> d_tm.mkConstArray(arrsort, iconst));
assertEquals(constarr.getKind(), CONST_ARRAY);
assertEquals(constarr.getConstArrayBase(), one);
assertThrows(CVC5ApiException.class, () -> a.getConstArrayBase());
Sort arrsort2 = d_tm.mkArraySort(d_tm.getRealSort(), d_tm.getRealSort());
Term zero_array = d_tm.mkConstArray(arrsort2, d_tm.mkReal(0));
Term stores = d_tm.mkTerm(STORE, zero_array, d_tm.mkReal(1), d_tm.mkReal(2));
stores = d_tm.mkTerm(STORE, stores, d_tm.mkReal(2), d_tm.mkReal(3));
stores = d_tm.mkTerm(STORE, stores, d_tm.mkReal(4), d_tm.mkReal(5));
}
@Test
void getSequenceValue() throws CVC5ApiException
{
Sort realsort = d_tm.getRealSort();
Sort seqsort = d_tm.mkSequenceSort(realsort);
Term s = d_tm.mkEmptySequence(seqsort);
assertEquals(s.getKind(), CONST_SEQUENCE);
// empty sequence has zero elements
Term[] cs = s.getSequenceValue();
assertTrue(cs.length == 0);
// A seq.unit app is not a constant sequence (regardless of whether it is
// applied to a constant).
Term su = d_tm.mkTerm(SEQ_UNIT, d_tm.mkReal(1));
assertThrows(CVC5ApiException.class, () -> su.getSequenceValue());
}
@Test
void termScopedToString()
{
Sort intsort = d_tm.getIntegerSort();
Term x = d_tm.mkConst(intsort, "x");
assertEquals(x.toString(), "x");
Solver solver2;
assertEquals(x.toString(), "x");
}
}
Reference in New Issue View Git Blame Copy Permalink