mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
216 lines
7.8 KiB
Java
216 lines
7.8 KiB
Java
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Andres Noetzli, Aina Niemetz, Mudathir Mohamed
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
|
|
* in the top-level source directory and their institutional affiliations.
|
|
* All rights reserved. See the file COPYING in the top-level source
|
|
* directory for licensing information.
|
|
* ****************************************************************************
|
|
*
|
|
* Black box testing of the Op 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.List;
|
|
import org.junit.jupiter.api.AfterEach;
|
|
import org.junit.jupiter.api.BeforeEach;
|
|
import org.junit.jupiter.api.Test;
|
|
|
|
class OpTest
|
|
{
|
|
private TermManager d_tm;
|
|
|
|
@BeforeEach
|
|
void setUp()
|
|
{
|
|
d_tm = new TermManager();
|
|
}
|
|
|
|
@AfterEach
|
|
void tearDown()
|
|
{
|
|
Context.deletePointers();
|
|
}
|
|
|
|
@Test
|
|
void hash() throws CVC5ApiException
|
|
{
|
|
Op ext1 = d_tm.mkOp(BITVECTOR_EXTRACT, 31, 1);
|
|
Op ext2 = d_tm.mkOp(BITVECTOR_EXTRACT, 31, 2);
|
|
assertEquals(ext1.hashCode(), ext1.hashCode());
|
|
assertNotEquals(ext1.hashCode(), ext2.hashCode());
|
|
assertNotEquals(ext1.hashCode(), (new Op()).hashCode());
|
|
}
|
|
|
|
@Test
|
|
void getKind() throws CVC5ApiException
|
|
{
|
|
Op x;
|
|
x = d_tm.mkOp(BITVECTOR_EXTRACT, 31, 1);
|
|
assertDoesNotThrow(() -> x.getKind());
|
|
}
|
|
|
|
@Test
|
|
void isNull() throws CVC5ApiException
|
|
{
|
|
Op x = new Op();
|
|
assertTrue(x.isNull());
|
|
Op y = d_tm.mkOp(BITVECTOR_EXTRACT, 31, 1);
|
|
assertFalse(y.isNull());
|
|
assertTrue(x != y);
|
|
}
|
|
|
|
@Test
|
|
void opFromKind()
|
|
{
|
|
assertDoesNotThrow(() -> d_tm.mkOp(ADD));
|
|
assertThrows(CVC5ApiException.class, () -> d_tm.mkOp(BITVECTOR_EXTRACT));
|
|
}
|
|
|
|
@Test
|
|
void getNumIndices() throws CVC5ApiException
|
|
{
|
|
// Operators with 0 indices
|
|
Op plus = d_tm.mkOp(ADD);
|
|
|
|
assertEquals(0, plus.getNumIndices());
|
|
|
|
// Operators with 1 index
|
|
Op divisible = d_tm.mkOp(DIVISIBLE, 4);
|
|
Op bvRepeat = d_tm.mkOp(BITVECTOR_REPEAT, 5);
|
|
Op bvZeroExtend = d_tm.mkOp(BITVECTOR_ZERO_EXTEND, 6);
|
|
Op bvSignExtend = d_tm.mkOp(BITVECTOR_SIGN_EXTEND, 7);
|
|
Op bvRotateLeft = d_tm.mkOp(BITVECTOR_ROTATE_LEFT, 8);
|
|
Op bvRotateRight = d_tm.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
|
|
Op intToBv = d_tm.mkOp(INT_TO_BITVECTOR, 10);
|
|
Op iand = d_tm.mkOp(IAND, 11);
|
|
Op fpToUbv = d_tm.mkOp(FLOATINGPOINT_TO_UBV, 12);
|
|
Op fpToSbv = d_tm.mkOp(FLOATINGPOINT_TO_SBV, 13);
|
|
|
|
assertEquals(1, divisible.getNumIndices());
|
|
assertEquals(1, bvRepeat.getNumIndices());
|
|
assertEquals(1, bvZeroExtend.getNumIndices());
|
|
assertEquals(1, bvSignExtend.getNumIndices());
|
|
assertEquals(1, bvRotateLeft.getNumIndices());
|
|
assertEquals(1, bvRotateRight.getNumIndices());
|
|
assertEquals(1, intToBv.getNumIndices());
|
|
assertEquals(1, iand.getNumIndices());
|
|
assertEquals(1, fpToUbv.getNumIndices());
|
|
assertEquals(1, fpToSbv.getNumIndices());
|
|
|
|
// Operators with 2 indices
|
|
Op bvExtract = d_tm.mkOp(BITVECTOR_EXTRACT, 1, 0);
|
|
Op toFpFromIeeeBv = d_tm.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 3, 2);
|
|
Op toFpFromFp = d_tm.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 5, 4);
|
|
Op toFpFromReal = d_tm.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
|
|
Op toFpFromSbv = d_tm.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
|
|
Op toFpFromUbv = d_tm.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
|
|
Op regexpLoop = d_tm.mkOp(REGEXP_LOOP, 15, 14);
|
|
|
|
assertEquals(2, bvExtract.getNumIndices());
|
|
assertEquals(2, toFpFromIeeeBv.getNumIndices());
|
|
assertEquals(2, toFpFromFp.getNumIndices());
|
|
assertEquals(2, toFpFromReal.getNumIndices());
|
|
assertEquals(2, toFpFromSbv.getNumIndices());
|
|
assertEquals(2, toFpFromUbv.getNumIndices());
|
|
assertEquals(2, regexpLoop.getNumIndices());
|
|
|
|
// Operators with n indices
|
|
int[] indices = {0, 3, 2, 0, 1, 2};
|
|
Op tupleProject = d_tm.mkOp(TUPLE_PROJECT, indices);
|
|
assertEquals(6, tupleProject.getNumIndices());
|
|
|
|
Op relationProject = d_tm.mkOp(RELATION_PROJECT, indices);
|
|
assertEquals(6, relationProject.getNumIndices());
|
|
|
|
Op tableProject = d_tm.mkOp(TABLE_PROJECT, indices);
|
|
assertEquals(6, tableProject.getNumIndices());
|
|
}
|
|
|
|
@Test
|
|
void opSubscriptOperator() throws CVC5ApiException
|
|
{
|
|
// Operators with 0 indices
|
|
Op plus = d_tm.mkOp(ADD);
|
|
|
|
assertThrows(CVC5ApiException.class, () -> plus.get(0));
|
|
|
|
// Operators with 1 index
|
|
Op divisible = d_tm.mkOp(DIVISIBLE, 4);
|
|
Op bvRepeat = d_tm.mkOp(BITVECTOR_REPEAT, 5);
|
|
Op bvZeroExtend = d_tm.mkOp(BITVECTOR_ZERO_EXTEND, 6);
|
|
Op bvSignExtend = d_tm.mkOp(BITVECTOR_SIGN_EXTEND, 7);
|
|
Op bvRotateLeft = d_tm.mkOp(BITVECTOR_ROTATE_LEFT, 8);
|
|
Op bvRotateRight = d_tm.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
|
|
Op intToBv = d_tm.mkOp(INT_TO_BITVECTOR, 10);
|
|
Op iand = d_tm.mkOp(IAND, 11);
|
|
Op fpToUbv = d_tm.mkOp(FLOATINGPOINT_TO_UBV, 12);
|
|
Op fpToSbv = d_tm.mkOp(FLOATINGPOINT_TO_SBV, 13);
|
|
Op regexpRepeat = d_tm.mkOp(REGEXP_REPEAT, 14);
|
|
|
|
assertEquals(4, divisible.get(0).getIntegerValue().intValue());
|
|
assertEquals(5, bvRepeat.get(0).getIntegerValue().intValue());
|
|
assertEquals(6, bvZeroExtend.get(0).getIntegerValue().intValue());
|
|
assertEquals(7, bvSignExtend.get(0).getIntegerValue().intValue());
|
|
assertEquals(8, bvRotateLeft.get(0).getIntegerValue().intValue());
|
|
assertEquals(9, bvRotateRight.get(0).getIntegerValue().intValue());
|
|
assertEquals(10, intToBv.get(0).getIntegerValue().intValue());
|
|
assertEquals(11, iand.get(0).getIntegerValue().intValue());
|
|
assertEquals(12, fpToUbv.get(0).getIntegerValue().intValue());
|
|
assertEquals(13, fpToSbv.get(0).getIntegerValue().intValue());
|
|
assertEquals(14, regexpRepeat.get(0).getIntegerValue().intValue());
|
|
|
|
// Operators with 2 indices
|
|
Op bvExtract = d_tm.mkOp(BITVECTOR_EXTRACT, 1, 0);
|
|
Op toFpFromIeeeBv = d_tm.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 3, 2);
|
|
Op toFpFromFp = d_tm.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 5, 4);
|
|
Op toFpFromReal = d_tm.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
|
|
Op toFpFromSbv = d_tm.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
|
|
Op toFpFromUbv = d_tm.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
|
|
Op regexpLoop = d_tm.mkOp(REGEXP_LOOP, 15, 14);
|
|
|
|
assertEquals(1, bvExtract.get(0).getIntegerValue().intValue());
|
|
assertEquals(0, bvExtract.get(1).getIntegerValue().intValue());
|
|
assertEquals(3, toFpFromIeeeBv.get(0).getIntegerValue().intValue());
|
|
assertEquals(2, toFpFromIeeeBv.get(1).getIntegerValue().intValue());
|
|
assertEquals(5, toFpFromFp.get(0).getIntegerValue().intValue());
|
|
assertEquals(4, toFpFromFp.get(1).getIntegerValue().intValue());
|
|
assertEquals(7, toFpFromReal.get(0).getIntegerValue().intValue());
|
|
assertEquals(6, toFpFromReal.get(1).getIntegerValue().intValue());
|
|
assertEquals(9, toFpFromSbv.get(0).getIntegerValue().intValue());
|
|
assertEquals(8, toFpFromSbv.get(1).getIntegerValue().intValue());
|
|
assertEquals(11, toFpFromUbv.get(0).getIntegerValue().intValue());
|
|
assertEquals(10, toFpFromUbv.get(1).getIntegerValue().intValue());
|
|
assertEquals(15, regexpLoop.get(0).getIntegerValue().intValue());
|
|
assertEquals(14, regexpLoop.get(1).getIntegerValue().intValue());
|
|
|
|
// Operators with n indices
|
|
int[] indices = {0, 3, 2, 0, 1, 2};
|
|
Op tupleProject = d_tm.mkOp(TUPLE_PROJECT, indices);
|
|
for (int i = 0, size = tupleProject.getNumIndices(); i < size; i++)
|
|
{
|
|
assertEquals(indices[i], tupleProject.get(i).getIntegerValue().intValue());
|
|
}
|
|
}
|
|
|
|
@Test
|
|
void opScopingToString() throws CVC5ApiException
|
|
{
|
|
Op bitvector_repeat_ot = d_tm.mkOp(BITVECTOR_REPEAT, 5);
|
|
String op_repr = bitvector_repeat_ot.toString();
|
|
|
|
Solver solver2;
|
|
assertEquals(bitvector_repeat_ot.toString(), op_repr);
|
|
}
|
|
}
|