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
f2fb0be98861642e0e33ff3c5dc763e8aa5fe769
cvc5/test/unit/api/java/TermTest.java
Aina Niemetz f2fb0be988 sets: Rename kinds with a more consistent naming scheme. (#7595) 
This prefixes sets kinds with SET_ and relation kinds with
RELATION_. It also prefixes the corresponding SMT-LIB operators with
'set.' and relation operators with 'rel.'.
2021-11-08 12:49:14 -08:00

1065 lines
46 KiB
Java
Raw Blame History

/******************************************************************************
* Top contributors (to current version):
* Aina Niemetz, Makai Mann, Andrew Reynolds, Mudathir Mohamed
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* Black box testing of the Term class.
*/
package tests;
import static io.github.cvc5.api.Kind.*;
import static org.junit.jupiter.api.Assertions.*;
import io.github.cvc5.api.*;
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 Solver d_solver;
@BeforeEach void setUp()
{
d_solver = new Solver();
}
@AfterEach void tearDown()
{
d_solver.close();
}
@Test void eq()
{
Sort uSort = d_solver.mkUninterpretedSort("u");
Term x = d_solver.mkVar(uSort, "x");
Term y = d_solver.mkVar(uSort, "y");
Term z = d_solver.getNullTerm();
assertTrue(x == x);
assertFalse(x != x);
assertFalse(x == y);
assertTrue(x != y);
assertFalse((x == z));
assertTrue(x != z);
}
@Test void getId()
{
Term n = d_solver.getNullTerm();
assertThrows(CVC5ApiException.class, () -> n.getId());
Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
assertDoesNotThrow(() -> x.getId());
Term y = x;
assertEquals(x.getId(), y.getId());
Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z");
assertNotEquals(x.getId(), z.getId());
}
@Test void getKind() throws CVC5ApiException
{
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
Term n = d_solver.getNullTerm();
assertThrows(CVC5ApiException.class, () -> n.getKind());
Term x = d_solver.mkVar(uSort, "x");
assertDoesNotThrow(() -> x.getKind());
Term y = d_solver.mkVar(uSort, "y");
assertDoesNotThrow(() -> y.getKind());
Term f = d_solver.mkVar(funSort1, "f");
assertDoesNotThrow(() -> f.getKind());
Term p = d_solver.mkVar(funSort2, "p");
assertDoesNotThrow(() -> p.getKind());
Term zero = d_solver.mkInteger(0);
assertDoesNotThrow(() -> zero.getKind());
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
assertDoesNotThrow(() -> f_x.getKind());
Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
assertDoesNotThrow(() -> f_y.getKind());
Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
assertDoesNotThrow(() -> sum.getKind());
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.getKind());
Term p_f_y = d_solver.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_solver.mkSequenceSort(intSort);
Term s = d_solver.mkConst(seqSort, "s");
Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s);
assertEquals(ss.getKind(), SEQ_CONCAT);
}
@Test void getSort() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
Term n = d_solver.getNullTerm();
assertThrows(CVC5ApiException.class, () -> n.getSort());
Term x = d_solver.mkVar(bvSort, "x");
assertDoesNotThrow(() -> x.getSort());
assertEquals(x.getSort(), bvSort);
Term y = d_solver.mkVar(bvSort, "y");
assertDoesNotThrow(() -> y.getSort());
assertEquals(y.getSort(), bvSort);
Term f = d_solver.mkVar(funSort1, "f");
assertDoesNotThrow(() -> f.getSort());
assertEquals(f.getSort(), funSort1);
Term p = d_solver.mkVar(funSort2, "p");
assertDoesNotThrow(() -> p.getSort());
assertEquals(p.getSort(), funSort2);
Term zero = d_solver.mkInteger(0);
assertDoesNotThrow(() -> zero.getSort());
assertEquals(zero.getSort(), intSort);
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
assertDoesNotThrow(() -> f_x.getSort());
assertEquals(f_x.getSort(), intSort);
Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
assertDoesNotThrow(() -> f_y.getSort());
assertEquals(f_y.getSort(), intSort);
Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
assertDoesNotThrow(() -> sum.getSort());
assertEquals(sum.getSort(), intSort);
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.getSort());
assertEquals(p_0.getSort(), boolSort);
Term p_f_y = d_solver.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_solver.getIntegerSort();
Sort bvsort = d_solver.mkBitVectorSort(8);
Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
Term x = d_solver.mkConst(intsort, "x");
Term a = d_solver.mkConst(arrsort, "a");
Term b = d_solver.mkConst(bvsort, "b");
assertFalse(x.hasOp());
assertThrows(CVC5ApiException.class, () -> x.getOp());
Term ab = d_solver.mkTerm(SELECT, a, b);
Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
Term extb = d_solver.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_solver.mkConst(funsort, "f");
Term fx = d_solver.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_solver.mkTerm(fx.getOp(), children));
// Test Datatypes Ops
Sort sort = d_solver.mkParamSort("T");
DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
cons.addSelector("head", sort);
cons.addSelectorSelf("tail");
listDecl.addConstructor(cons);
listDecl.addConstructor(nil);
Sort listSort = d_solver.mkDatatypeSort(listDecl);
Sort intListSort = listSort.instantiate(new Sort[] {d_solver.getIntegerSort()});
Term c = d_solver.mkConst(intListSort, "c");
Datatype list = listSort.getDatatype();
// list datatype constructor and selector operator terms
Term consOpTerm = list.getConstructorTerm("cons");
Term nilOpTerm = list.getConstructorTerm("nil");
}
@Test void isNull() throws CVC5ApiException
{
Term x = d_solver.getNullTerm();
assertTrue(x.isNull());
x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
assertFalse(x.isNull());
}
@Test void notTerm() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().notTerm());
Term b = d_solver.mkTrue();
assertDoesNotThrow(() -> b.notTerm());
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.notTerm());
Term f = d_solver.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.notTerm());
Term p = d_solver.mkVar(funSort2, "p");
assertThrows(CVC5ApiException.class, () -> p.notTerm());
Term zero = d_solver.mkInteger(0);
assertThrows(CVC5ApiException.class, () -> zero.notTerm());
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.notTerm());
Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.notTerm());
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
assertDoesNotThrow(() -> p_0.notTerm());
Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
assertDoesNotThrow(() -> p_f_x.notTerm());
}
@Test void andTerm() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
Term b = d_solver.mkTrue();
assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().andTerm(b));
assertThrows(CVC5ApiException.class, () -> b.andTerm(d_solver.getNullTerm()));
assertDoesNotThrow(() -> b.andTerm(b));
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.andTerm(b));
assertThrows(CVC5ApiException.class, () -> x.andTerm(x));
Term f = d_solver.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.andTerm(b));
assertThrows(CVC5ApiException.class, () -> f.andTerm(x));
assertThrows(CVC5ApiException.class, () -> f.andTerm(f));
Term p = d_solver.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_solver.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_solver.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_solver.mkTerm(PLUS, 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_solver.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_solver.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_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
Term b = d_solver.mkTrue();
assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().orTerm(b));
assertThrows(CVC5ApiException.class, () -> b.orTerm(d_solver.getNullTerm()));
assertDoesNotThrow(() -> b.orTerm(b));
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.orTerm(b));
assertThrows(CVC5ApiException.class, () -> x.orTerm(x));
Term f = d_solver.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.orTerm(b));
assertThrows(CVC5ApiException.class, () -> f.orTerm(x));
assertThrows(CVC5ApiException.class, () -> f.orTerm(f));
Term p = d_solver.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_solver.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_solver.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_solver.mkTerm(PLUS, 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_solver.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_solver.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_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
Term b = d_solver.mkTrue();
assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().xorTerm(b));
assertThrows(CVC5ApiException.class, () -> b.xorTerm(d_solver.getNullTerm()));
assertDoesNotThrow(() -> b.xorTerm(b));
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> x.xorTerm(x));
Term f = d_solver.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.xorTerm(b));
assertThrows(CVC5ApiException.class, () -> f.xorTerm(x));
assertThrows(CVC5ApiException.class, () -> f.xorTerm(f));
Term p = d_solver.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_solver.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_solver.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_solver.mkTerm(PLUS, 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_solver.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_solver.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_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
Term b = d_solver.mkTrue();
assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().eqTerm(b));
assertThrows(CVC5ApiException.class, () -> b.eqTerm(d_solver.getNullTerm()));
assertDoesNotThrow(() -> b.eqTerm(b));
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.eqTerm(b));
assertDoesNotThrow(() -> x.eqTerm(x));
Term f = d_solver.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.eqTerm(b));
assertThrows(CVC5ApiException.class, () -> f.eqTerm(x));
assertDoesNotThrow(() -> f.eqTerm(f));
Term p = d_solver.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_solver.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_solver.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_solver.mkTerm(PLUS, 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_solver.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_solver.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_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
Term b = d_solver.mkTrue();
assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().impTerm(b));
assertThrows(CVC5ApiException.class, () -> b.impTerm(d_solver.getNullTerm()));
assertDoesNotThrow(() -> b.impTerm(b));
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
assertThrows(CVC5ApiException.class, () -> x.impTerm(b));
assertThrows(CVC5ApiException.class, () -> x.impTerm(x));
Term f = d_solver.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.impTerm(b));
assertThrows(CVC5ApiException.class, () -> f.impTerm(x));
assertThrows(CVC5ApiException.class, () -> f.impTerm(f));
Term p = d_solver.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_solver.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_solver.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_solver.mkTerm(PLUS, 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_solver.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_solver.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_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
Term b = d_solver.mkTrue();
assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().iteTerm(b, b));
assertThrows(CVC5ApiException.class, () -> b.iteTerm(d_solver.getNullTerm(), b));
assertThrows(CVC5ApiException.class, () -> b.iteTerm(b, d_solver.getNullTerm()));
assertDoesNotThrow(() -> b.iteTerm(b, b));
Term x = d_solver.mkVar(d_solver.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_solver.mkVar(funSort1, "f");
assertThrows(CVC5ApiException.class, () -> f.iteTerm(b, b));
assertThrows(CVC5ApiException.class, () -> x.iteTerm(b, x));
Term p = d_solver.mkVar(funSort2, "p");
assertThrows(CVC5ApiException.class, () -> p.iteTerm(b, b));
assertThrows(CVC5ApiException.class, () -> p.iteTerm(x, b));
Term zero = d_solver.mkInteger(0);
assertThrows(CVC5ApiException.class, () -> zero.iteTerm(x, x));
assertThrows(CVC5ApiException.class, () -> zero.iteTerm(x, b));
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, b));
assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, x));
Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
assertThrows(CVC5ApiException.class, () -> sum.iteTerm(x, x));
assertThrows(CVC5ApiException.class, () -> sum.iteTerm(b, x));
Term p_0 = d_solver.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_solver.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_solver.mkInteger(1);
Term t2 = t1;
t2 = d_solver.mkInteger(2);
assertEquals(t1, d_solver.mkInteger(1));
}
@Test void termCompare()
{
Term t1 = d_solver.mkInteger(1);
Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.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_solver.mkInteger(2);
Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
assertEquals(t1.getChild(0), two);
assertEquals(t1.getNumChildren(), 2);
Term tnull = d_solver.getNullTerm();
assertThrows(CVC5ApiException.class, () -> tnull.getNumChildren());
// apply term f(2)
Sort intSort = d_solver.getIntegerSort();
Sort fsort = d_solver.mkFunctionSort(intSort, intSort);
Term f = d_solver.mkConst(fsort, "f");
Term t2 = d_solver.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_solver.mkInteger("-18446744073709551616");
Term int2 = d_solver.mkInteger("-18446744073709551615");
Term int3 = d_solver.mkInteger("-4294967296");
Term int4 = d_solver.mkInteger("-4294967295");
Term int5 = d_solver.mkInteger("-10");
Term int6 = d_solver.mkInteger("0");
Term int7 = d_solver.mkInteger("10");
Term int8 = d_solver.mkInteger("4294967295");
Term int9 = d_solver.mkInteger("4294967296");
Term int10 = d_solver.mkInteger("18446744073709551615");
Term int11 = d_solver.mkInteger("18446744073709551616");
Term int12 = d_solver.mkInteger("-0");
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(""));
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-"));
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-1-"));
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("0.0"));
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-0.1"));
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("012"));
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("0000"));
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-01"));
assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-00"));
assertTrue(int1.isIntegerValue());
assertEquals(int1.getIntegerValue().toString(), "-18446744073709551616");
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");
assertTrue(int7.isIntegerValue());
assertEquals(int7.getIntegerValue().intValue(), 10);
assertEquals(int7.getIntegerValue().intValue(), 10);
assertEquals(int7.getIntegerValue().toString(), "10");
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_solver.mkString("abcde");
assertTrue(s1.isStringValue());
assertEquals(s1.getStringValue(), "abcde");
}
@Test void getReal() throws CVC5ApiException
{
Term real1 = d_solver.mkReal("0");
Term real2 = d_solver.mkReal(".0");
Term real3 = d_solver.mkReal("-17");
Term real4 = d_solver.mkReal("-3/5");
Term real5 = d_solver.mkReal("12.7");
Term real6 = d_solver.mkReal("1/4294967297");
Term real7 = d_solver.mkReal("4294967297");
Term real8 = d_solver.mkReal("1/18446744073709551617");
Term real9 = d_solver.mkReal("18446744073709551617");
Term real10 = d_solver.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_solver.getIntegerSort();
Sort arrsort = d_solver.mkArraySort(intsort, intsort);
Term one = d_solver.mkInteger(1);
Term constarr = d_solver.mkConstArray(arrsort, one);
assertTrue(constarr.isConstArray());
assertEquals(one, constarr.getConstArrayBase());
}
@Test void getBoolean()
{
Term b1 = d_solver.mkBoolean(true);
Term b2 = d_solver.mkBoolean(false);
assertTrue(b1.isBooleanValue());
assertTrue(b2.isBooleanValue());
assertTrue(b1.getBooleanValue());
assertFalse(b2.getBooleanValue());
}
@Test void getBitVector() throws CVC5ApiException
{
Term b1 = d_solver.mkBitVector(8, 15);
Term b2 = d_solver.mkBitVector(8, "00001111", 2);
Term b3 = d_solver.mkBitVector(8, "15", 10);
Term b4 = d_solver.mkBitVector(8, "0f", 16);
Term b5 = d_solver.mkBitVector(9, "00001111", 2);
Term b6 = d_solver.mkBitVector(9, "15", 10);
Term b7 = d_solver.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 getAbstractValue() throws CVC5ApiException
{
Term v1 = d_solver.mkAbstractValue(1);
Term v2 = d_solver.mkAbstractValue("15");
Term v3 = d_solver.mkAbstractValue("18446744073709551617");
assertTrue(v1.isAbstractValue());
assertTrue(v2.isAbstractValue());
assertTrue(v3.isAbstractValue());
assertEquals("1", v1.getAbstractValue());
assertEquals("15", v2.getAbstractValue());
assertEquals("18446744073709551617", v3.getAbstractValue());
}
@Test void getTuple()
{
Sort s1 = d_solver.getIntegerSort();
Sort s2 = d_solver.getRealSort();
Sort s3 = d_solver.getStringSort();
Term t1 = d_solver.mkInteger(15);
Term t2 = d_solver.mkReal(17, 25);
Term t3 = d_solver.mkString("abc");
Term tup = d_solver.mkTuple(new Sort[] {s1, s2, s3}, 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_solver.mkBitVector(16, "0000110000000011", 2);
Term fp = d_solver.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_solver.mkPosZero(5, 11).isFloatingPointPosZero());
assertTrue(d_solver.mkNegZero(5, 11).isFloatingPointNegZero());
assertTrue(d_solver.mkPosInf(5, 11).isFloatingPointPosInf());
assertTrue(d_solver.mkNegInf(5, 11).isFloatingPointNegInf());
assertTrue(d_solver.mkNaN(5, 11).isFloatingPointNaN());
}
@Test void getSet()
{
Sort s = d_solver.mkSetSort(d_solver.getIntegerSort());
Term i1 = d_solver.mkInteger(5);
Term i2 = d_solver.mkInteger(7);
Term s1 = d_solver.mkEmptySet(s);
Term s2 = d_solver.mkTerm(Kind.SET_SINGLETON, i1);
Term s3 = d_solver.mkTerm(Kind.SET_SINGLETON, i1);
Term s4 = d_solver.mkTerm(Kind.SET_SINGLETON, i2);
Term s5 = d_solver.mkTerm(Kind.SET_UNION, s2, d_solver.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_solver.mkSequenceSort(d_solver.getIntegerSort());
Term i1 = d_solver.mkInteger(5);
Term i2 = d_solver.mkInteger(7);
Term s1 = d_solver.mkEmptySequence(s);
Term s2 = d_solver.mkTerm(Kind.SEQ_UNIT, i1);
Term s3 = d_solver.mkTerm(Kind.SEQ_UNIT, i1);
Term s4 = d_solver.mkTerm(Kind.SEQ_UNIT, i2);
Term s5 = d_solver.mkTerm(Kind.SEQ_CONCAT, s2, d_solver.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 getUninterpretedConst() throws CVC5ApiException
{
Sort s = d_solver.mkUninterpretedSort("test");
Term t1 = d_solver.mkUninterpretedConst(s, 3);
Term t2 = d_solver.mkUninterpretedConst(s, 5);
assertTrue(t1.isUninterpretedValue());
assertTrue(t2.isUninterpretedValue());
assertEquals(new Pair<Sort, Integer>(s, 3), t1.getUninterpretedValue());
assertEquals(new Pair<Sort, Integer>(s, 5), t2.getUninterpretedValue());
}
@Test void substitute()
{
Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
Term one = d_solver.mkInteger(1);
Term ttrue = d_solver.mkTrue();
Term xpx = d_solver.mkTerm(PLUS, x, x);
Term onepone = d_solver.mkTerm(PLUS, 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_solver.mkConst(d_solver.getIntegerSort(), "y");
Term xpy = d_solver.mkTerm(PLUS, x, y);
Term xpone = d_solver.mkTerm(PLUS, 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, rs), xpone);
// incorrect substitution due to arity
rs.remove(rs.size() - 1);
assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs));
// incorrect substitution due to types
rs.add(ttrue);
assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs));
// null cannot substitute
Term tnull = d_solver.getNullTerm();
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, rs));
es.clear();
rs.clear();
es.add(x);
rs.add(y);
assertThrows(CVC5ApiException.class, () -> tnull.substitute(es, rs));
es.add(tnull);
rs.add(one);
assertThrows(CVC5ApiException.class, () -> xpx.substitute(es, rs));
}
@Test void constArray() throws CVC5ApiException
{
Sort intsort = d_solver.getIntegerSort();
Sort arrsort = d_solver.mkArraySort(intsort, intsort);
Term a = d_solver.mkConst(arrsort, "a");
Term one = d_solver.mkInteger(1);
Term constarr = d_solver.mkConstArray(arrsort, one);
assertEquals(constarr.getKind(), CONST_ARRAY);
assertEquals(constarr.getConstArrayBase(), one);
assertThrows(CVC5ApiException.class, () -> a.getConstArrayBase());
arrsort = d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0));
Term stores = d_solver.mkTerm(STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2));
stores = d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3));
stores = d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
}
@Test void getSequenceValue() throws CVC5ApiException
{
Sort realsort = d_solver.getRealSort();
Sort seqsort = d_solver.mkSequenceSort(realsort);
Term s = d_solver.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_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1));
assertThrows(CVC5ApiException.class, () -> su.getSequenceValue());
}
@Test void termScopedToString()
{
Sort intsort = d_solver.getIntegerSort();
Term x = d_solver.mkConst(intsort, "x");
assertEquals(x.toString(), "x");
Solver solver2;
assertEquals(x.toString(), "x");
}
}
Reference in New Issue View Git Blame Copy Permalink