1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
###############################################################################
# Top contributors (to current version):
# Alex Ozdemir
#
# 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.
# #############################################################################
#
# A simple demonstration of the solving capabilities of the cvc5
# bit-vector and array solvers.
##
from cvc5.pythonic import *
if __name__ == '__main__':
# Consider the following (where k is some previously defined constant):
#
#
# Assert (current_array[0] > 0);
# for (unsigned i = 1; i < k; ++i) {
# current_array[i] = 2 * current_array[i - 1];
# Assert (current_array[i-1] < current_array[i]);
# }
#
# We want to check whether the assertion in the body of the for loop holds
# throughout the loop.
k = 4
idx_bits = int(math.ceil(math.log(k, 2)))
init_array = Array('init_arr', BitVecSort(idx_bits), BitVecSort(32))
array = init_array
assertions = []
for i in range(1, k):
array = Store(array, i, 2 * Select(array, i - 1))
assertions.append(Select(array, i - 1) < Select(array, i))
# Does *not* hold.
# If the first element is large enough, the multiplication overflows.
prove(Implies(Select(init_array, 0) > 0, And(*assertions)))
|
