test/unit/api/python/test_op.py

   1 ###############################################################################
   2 # Top contributors (to current version):
   3 #   Aina Niemetz, Andres Noetzli, Yoni Zohar
   4 #
   5 # This file is part of the cvc5 project.
   6 #
   7 # Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
   8 # in the top-level source directory and their institutional affiliations.
   9 # All rights reserved.  See the file COPYING in the top-level source
  10 # directory for licensing information.
  11 # #############################################################################
  12 #
  13 # Unit tests for op API.
  14 #
  15 # Obtained by translating test/unit/api/op_black.cpp
  16 ##
  17
  18 import pytest
  19 import cvc5
  20 from cvc5 import Kind
  21 from cvc5 import Sort
  22 from cvc5 import Op
  23
  24
  25 @pytest.fixture
  26 def solver():
  27     return cvc5.Solver()
  28
  29
  30 def test_hash(solver):
  31     hash(solver.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1))
  32
  33 def test_get_kind(solver):
  34     x = solver.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1)
  35     x.getKind()
  36
  37
  38 def test_is_null(solver):
  39     x = Op(solver)
  40     assert x.isNull()
  41     y = solver.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1)
  42     assert not y.isNull()
  43     assert x != y
  44
  45
  46 def test_op_from_kind(solver):
  47     solver.mkOp(Kind.ADD)
  48     with pytest.raises(RuntimeError):
  49         solver.mkOp(Kind.BITVECTOR_EXTRACT)
  50
  51
  52 def test_get_num_indices(solver):
  53     # Operators with 0 indices
  54     plus = solver.mkOp(Kind.ADD)
  55
  56     assert 0 == plus.getNumIndices()
  57
  58     # Operators with 1 index
  59     divisible = solver.mkOp(Kind.DIVISIBLE, 4)
  60     bitvector_repeat = solver.mkOp(Kind.BITVECTOR_REPEAT, 5)
  61     bitvector_zero_extend = solver.mkOp(Kind.BITVECTOR_ZERO_EXTEND, 6)
  62     bitvector_sign_extend = solver.mkOp(Kind.BITVECTOR_SIGN_EXTEND, 7)
  63     bitvector_rotate_left = solver.mkOp(Kind.BITVECTOR_ROTATE_LEFT, 8)
  64     bitvector_rotate_right = solver.mkOp(Kind.BITVECTOR_ROTATE_RIGHT, 9)
  65     int_to_bitvector = solver.mkOp(Kind.INT_TO_BITVECTOR, 10)
  66     iand = solver.mkOp(Kind.IAND, 3)
  67     floatingpoint_to_ubv = solver.mkOp(Kind.FLOATINGPOINT_TO_UBV, 11)
  68     floatingopint_to_sbv = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 13)
  69
  70     assert 1 == divisible.getNumIndices()
  71     assert 1 == bitvector_repeat.getNumIndices()
  72     assert 1 == bitvector_zero_extend.getNumIndices()
  73     assert 1 == bitvector_sign_extend.getNumIndices()
  74     assert 1 == bitvector_rotate_left.getNumIndices()
  75     assert 1 == bitvector_rotate_right.getNumIndices()
  76     assert 1 == int_to_bitvector.getNumIndices()
  77     assert 1 == iand.getNumIndices()
  78     assert 1 == floatingpoint_to_ubv.getNumIndices()
  79     assert 1 == floatingopint_to_sbv.getNumIndices()
  80
  81     # Operators with 2 indices
  82     bitvector_extract = solver.mkOp(Kind.BITVECTOR_EXTRACT, 4, 25)
  83     floatingpoint_to_fp_from_ieee_bv = solver.mkOp(
  84             Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25)
  85     floatingpoint_to_fp_from_fp = solver.mkOp(
  86             Kind.FLOATINGPOINT_TO_FP_FROM_FP, 4, 25)
  87     floatingpoint_to_fp_from_real = solver.mkOp(
  88             Kind.FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25)
  89     floatingpoint_to_fp_from_sbv = solver.mkOp(
  90             Kind.FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25)
  91     floatingpoint_to_fp_from_ubv = solver.mkOp(
  92             Kind.FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25)
  93     regexp_loop = solver.mkOp(Kind.REGEXP_LOOP, 2, 3)
  94
  95     assert 2 == bitvector_extract.getNumIndices()
  96     assert 2 == floatingpoint_to_fp_from_ieee_bv.getNumIndices()
  97     assert 2 == floatingpoint_to_fp_from_fp.getNumIndices()
  98     assert 2 == floatingpoint_to_fp_from_real.getNumIndices()
  99     assert 2 == floatingpoint_to_fp_from_sbv.getNumIndices()
 100     assert 2 == floatingpoint_to_fp_from_ubv.getNumIndices()
 101     assert 2 == regexp_loop.getNumIndices()
 102
 103     # Operators with n indices
 104     indices = [0, 3, 2, 0, 1, 2]
 105     tuple_project_op = solver.mkOp(Kind.TUPLE_PROJECT, *indices)
 106     assert len(indices) == tuple_project_op.getNumIndices()
 107
 108     table_project_op = solver.mkOp(Kind.TABLE_PROJECT, *indices)
 109     assert len(indices) == table_project_op.getNumIndices()
 110
 111
 112 def test_subscript_operator(solver):
 113     # Operators with 0 indices
 114     plus = solver.mkOp(Kind.ADD)
 115
 116     with pytest.raises(RuntimeError):
 117         plus[0]
 118
 119     # Operators with 1 index
 120     divisible = solver.mkOp(Kind.DIVISIBLE, 4)
 121     bitvector_repeat = solver.mkOp(Kind.BITVECTOR_REPEAT, 5)
 122     bitvector_zero_extend = solver.mkOp(Kind.BITVECTOR_ZERO_EXTEND, 6)
 123     bitvector_sign_extend = solver.mkOp(Kind.BITVECTOR_SIGN_EXTEND, 7)
 124     bitvector_rotate_left = solver.mkOp(Kind.BITVECTOR_ROTATE_LEFT, 8)
 125     bitvector_rotate_right = solver.mkOp(Kind.BITVECTOR_ROTATE_RIGHT, 9)
 126     int_to_bitvector = solver.mkOp(Kind.INT_TO_BITVECTOR, 10)
 127     iand = solver.mkOp(Kind.IAND, 11)
 128     floatingpoint_to_ubv = solver.mkOp(Kind.FLOATINGPOINT_TO_UBV, 12)
 129     floatingopint_to_sbv = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 13)
 130     regexp_repeat = solver.mkOp(Kind.REGEXP_REPEAT, 14)
 131
 132     assert 4 == divisible[0].getIntegerValue()
 133     assert 5 == bitvector_repeat[0].getIntegerValue()
 134     assert 6 == bitvector_zero_extend[0].getIntegerValue()
 135     assert 7 == bitvector_sign_extend[0].getIntegerValue()
 136     assert 8 == bitvector_rotate_left[0].getIntegerValue()
 137     assert 9 == bitvector_rotate_right[0].getIntegerValue()
 138     assert 10 == int_to_bitvector[0].getIntegerValue()
 139     assert 11 == iand[0].getIntegerValue()
 140     assert 12 == floatingpoint_to_ubv[0].getIntegerValue()
 141     assert 13 == floatingopint_to_sbv[0].getIntegerValue()
 142     assert 14 == regexp_repeat[0].getIntegerValue()
 143
 144     # Operators with 2 indices
 145     bitvector_extract = solver.mkOp(Kind.BITVECTOR_EXTRACT, 1, 0)
 146     floatingpoint_to_fp_from_ieee_bv = solver.mkOp(
 147             Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 3, 2)
 148     floatingpoint_to_fp_from_fp = solver.mkOp(
 149             Kind.FLOATINGPOINT_TO_FP_FROM_FP, 5, 4)
 150     floatingpoint_to_fp_from_real = solver.mkOp(
 151             Kind.FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6)
 152     floatingpoint_to_fp_from_sbv = solver.mkOp(
 153             Kind.FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8)
 154     floatingpoint_to_fp_from_ubv = solver.mkOp(
 155             Kind.FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10)
 156     regexp_loop = solver.mkOp(Kind.REGEXP_LOOP, 15, 14)
 157
 158     assert 1 == bitvector_extract[0].getIntegerValue()
 159     assert 0 == bitvector_extract[1].getIntegerValue()
 160     assert 3 == floatingpoint_to_fp_from_ieee_bv[0].getIntegerValue()
 161     assert 2 == floatingpoint_to_fp_from_ieee_bv[1].getIntegerValue()
 162     assert 5 == floatingpoint_to_fp_from_fp[0].getIntegerValue()
 163     assert 4 == floatingpoint_to_fp_from_fp[1].getIntegerValue()
 164     assert 7 == floatingpoint_to_fp_from_real[0].getIntegerValue()
 165     assert 6 == floatingpoint_to_fp_from_real[1].getIntegerValue()
 166     assert 9 == floatingpoint_to_fp_from_sbv[0].getIntegerValue()
 167     assert 8 == floatingpoint_to_fp_from_sbv[1].getIntegerValue()
 168     assert 11 == floatingpoint_to_fp_from_ubv[0].getIntegerValue()
 169     assert 10 == floatingpoint_to_fp_from_ubv[1].getIntegerValue()
 170     assert 15 == regexp_loop[0].getIntegerValue()
 171     assert 14 == regexp_loop[1].getIntegerValue()
 172
 173     # Operators with n indices
 174     indices = [0, 3, 2, 0, 1, 2]
 175     tuple_project_op = solver.mkOp(Kind.TUPLE_PROJECT, *indices)
 176     for i in range(len(indices)):
 177         assert indices[i] == tuple_project_op[i].getIntegerValue()
 178
 179
 180 def test_op_scoping_to_string(solver):
 181     bitvector_repeat_ot = solver.mkOp(Kind.BITVECTOR_REPEAT, 5)
 182     op_repr = str(bitvector_repeat_ot)
 183     assert str(bitvector_repeat_ot) == op_repr