mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
354fc4147e
This is related to the previous refactor of the C++ API in https://github.com/cvc5/cvc5/pull/10426.
1202 lines
49 KiB
Java
1202 lines
49 KiB
Java
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Mudathir Mohamed, Andrew Reynolds, Aina Niemetz
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2024 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 eq()
|
|
{
|
|
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 == x);
|
|
assertFalse(x != x);
|
|
assertFalse(x == y);
|
|
assertTrue(x != y);
|
|
assertFalse((x == z));
|
|
assertTrue(x != z);
|
|
}
|
|
|
|
@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);
|
|
|
|
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");
|
|
}
|
|
|
|
@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()));
|
|
}
|
|
|
|
@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 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");
|
|
}
|
|
}
|