Solutions to Exercises
Solution to Exercise 1
1(set-logic QF_LIA)
2
3(declare-const a Int)
4(declare-const b Int)
5
6(assert (= (+ a 10) (* 2 b)))
7(assert (= (+ b 20) (* 2 a)))
8
9(check-sat)
1from cvc5.pythonic import *
2a, b = Ints('a b')
3solve(a + 10 == 2 * b, b + 20 == 2 * a)
The output is as follows.
1unsat
1no solution
The SMT solver says unsat (or “no solution” for the Python version)
because there are no integer values that satisfy the constraints.
Solution to Exercise 2
1(set-logic QF_BV)
2(set-option :produce-models true)
3
4(declare-const x (_ BitVec 8))
5
6(assert (= (bvmul x (_ bv5 8)) (_ bv1 8)))
7
8(check-sat)
9(get-model)
1from cvc5.pythonic import *
2
3x = BitVec('x', 8)
4s = SolverFor('QF_BV')
5
6s.add(x * 5 == 1)
7
8result = s.check()
9print("result: ", result)
10if result == sat:
11 m = s.model()
12 print("\n".join([str(k) + " : " + str(m[k]) for k in m]))
The output is as follows.
1sat
2(
3(define-fun x () (_ BitVec 8) #b11001101)
4)
1result: sat
2x : 205
The SMT solver gives a binary value of x as #b11001101. This
equals 205 in decimal. And, indeed, \(5 \times 205 = 1025\), and
\(1025 \equiv 1\ \mathsf{mod}\ 256\).
Solution to Exercise 3
One way to modify Example 4 to make it satisfiable is to change the
hypothesis so that f is applied 2 and 4 times instead of 3 and 5 times.
In fact, any two number of applications that are not relatively prime will work.
1(set-logic QF_UF)
2(set-option :produce-models true)
3
4(declare-sort U 0)
5
6(declare-fun f (U) U)
7(declare-const x U)
8
9(assert (and (= (f (f x)) x) (= (f (f (f (f x)))) x)))
10(assert (distinct (f x) x))
11
12(check-sat)
13(get-model)
1from cvc5.pythonic import *
2U = DeclareSort("U")
3f = Function("f", U, U)
4x = Const("x", U)
5
6s = SolverFor('QF_UF')
7s.add(And((f(f(x)) == x), (f(f(f(f(x))))) == x))
8s.add(Distinct(f(x), x)) # negation of f(x) = x
9
10result = s.check()
11print(result)
12if result == sat:
13 m = s.model()
14 print("\n".join([str(k) + " : " + str(m[k]) for k in m]))
15
The output from cvc5 is as follows.
1sat
2(
3; cardinality of U is 2
4; rep: (as @U_0 U)
5; rep: (as @U_1 U)
6(define-fun f ((_arg_1 U)) U (ite (= (as @U_1 U) _arg_1) (as @U_0 U) (as @U_1 U)))
7(define-fun x () U (as @U_1 U))
8)
1sat
2f : Lambda(_arg_1,
3 If((as @U_1 U) == _arg_1, (as @U_0 U), (as @U_1 U)))
4x : (as @U_1 U)
Notice that for the SMT-LIB example, cvc5 uses a custom output format to describe how it has
interpreted the sort U: as a set with two elements, @U_0 and
@U_1. Furthermore, cvc5 uses the define-fun command to
describe the value assigned to f. In this case, the interpretation of
f maps @U_1 to @U_0 and everything else (i.e.,
@U_0) to @U_1. Then, interpreting x as @U_1
satisfies the constraints. The Python output gives the same model, but it uses
Lambda to define the function.
We next consider how to modify Example 5. One way to do
this is to additionally require that y and z: are equal.
1(set-logic QF_UF)
2
3(declare-sort U 0)
4
5(declare-const b Bool)
6(declare-const x U)
7(declare-const y U)
8(declare-const z U)
9(declare-const w U)
10
11(assert (= x (ite b y z)))
12(assert (or (= w y) (= w z)))
13(assert (= y z))
14(assert (distinct x w))
15
16(check-sat)
1from cvc5.pythonic import *
2U = DeclareSort("U")
3b = Const("b", BoolSort())
4x, y, z, w = Consts("x y z w", U)
5
6s = SolverFor('QF_UF')
7s.add(x == (If(b, y, z)))
8s.add(Or((w == y), (w == z)))
9s.add(y == z)
10s.add(x != w)
11
12if s.check() == sat:
13 m = s.model()
14 print("\n".join([str(k) + " : " + str(m[k]) for k in m]))
15else:
16 print("no solution")
The output from cvc5 is as follows.
1no solution
Solution to Exercise 4
In the SMT-LIB solution, we make use of the incremental option, which
enables the commands push and pop. These commands allow us to
temporarily add one or more assertions, check for satisfiability, and then
return to the previous state. The Python example demonstrates the power of
having the solver embedded in a general-purpose programming language: we can
use a loop to iterate until no better solution is found. We first show that
for the original problem, 30 minutes is the best possible time.
1(set-logic QF_IDL)
2(set-option :produce-models true)
3(set-option :incremental true)
4
5(declare-const j11 Int)
6(declare-const j12 Int)
7(declare-const j21 Int)
8(declare-const j22 Int)
9(declare-const j31 Int)
10(declare-const j32 Int)
11
12(assert (and (>= j11 0) (>= j12 0) (>= j21 0) (>= j22 0) (>= j31 0) (>= j32 0)))
13(assert (and (>= (- j12 j11) 10) (>= (- j22 j21) 20) (>= (- j32 j31) 5)))
14(assert (and (or (>= (- j22 j11) 10) (>= (- j11 j22) 5))
15 (or (>= (- j31 j11) 10) (>= (- j11 j31) 5))
16 (or (>= (- j31 j22) 5) (>= (- j22 j31) 5))))
17(assert (and (or (>= (- j21 j12) 5) (>= (- j12 j21) 20))
18 (or (>= (- j32 j12) 5) (>= (- j12 j32) 5))
19 (or (>= (- j32 j21) 20) (>= (- j21 j32) 5))))
20
21(define-fun max3 ((i Int) (j Int) (k Int)) Int
22 (ite (< i j) (ite (< j k) k j) (ite (< i k) k i)))
23
24(push)
25(assert (<= (max3 j12 j22 j32) 25))
26(check-sat)
27(get-model)
28(pop)
29
30(assert (<= (max3 j12 j22 j32) 24))
31(check-sat)
1def max2(i, j):
2 if i < j:
3 return j
4 else:
5 return i
6
7def max3(i, j, k):
8 return max2(max2(i,j),k)
9
10from cvc5.pythonic import *
11
12j11,j12,j21,j22,j31,j32 = Ints("j11 j12 j21 j22 j31 j32")
13
14s = SolverFor('QF_IDL')
15s.add(And([x >= 0 for x in [j11, j12, j21, j22, j31, j32]]))
16s.add(And(j12 - j11 >= 10, j22 - j21 >= 20, j32 - j31 >= 5))
17s.add(And(Or(j22 - j11 >= 10, j11 - j22 >= 5),
18 Or(j31 - j11 >= 10, j11 - j31 >= 5),
19 Or(j31 - j22 >= 5, j22 - j31 >= 5)))
20s.add(And(Or(j21 - j12 >= 5, j12 - j21 >= 20),
21 Or(j32 - j12 >= 5, j12 - j32 >= 5),
22 Or(j32 - j21 >= 20, j21 - j32 >= 5)))
23s.add(And(j12 <= 25, j22 <= 25, j32 <= 25))
24
25s.push()
26result = s.check()
27while result == sat:
28 m = s.model()
29 a = m.eval(j12).as_long()
30 b = m.eval(j22).as_long()
31 c = m.eval(j32).as_long()
32 s.pop()
33 best = max3(a, b, c) + 5
34 print("Best solution so far:", best, "minutes")
35 new_threshold = best - 5
36 s.push()
37 s.add(And(j12 < new_threshold, j22 < new_threshold, j32 < new_threshold))
38 result = s.check()
39
40s.pop()
41print(best, "is the best solution")
The output from cvc5 is as follows.
1sat
2(
3(define-fun j11 () Int 0)
4(define-fun j12 () Int 25)
5(define-fun j21 () Int 0)
6(define-fun j22 () Int 21)
7(define-fun j31 () Int 15)
8(define-fun j32 () Int 20)
9)
10unsat
1Best solution so far: 30 minutes
230 is the best solution
We now modify the example so that Job 2 only uses machine 2 for 15 minutes. The best solution is now 25 minutes.
1(set-logic QF_IDL)
2(set-option :produce-models true)
3(set-option :incremental true)
4
5(declare-const j11 Int)
6(declare-const j12 Int)
7(declare-const j21 Int)
8(declare-const j22 Int)
9(declare-const j31 Int)
10(declare-const j32 Int)
11
12(assert (and (>= j11 0) (>= j12 0) (>= j21 0) (>= j22 0) (>= j31 0) (>= j32 0)))
13(assert (and (>= (- j12 j11) 10) (>= (- j22 j21) 15) (>= (- j32 j31) 5)))
14(assert (and (or (>= (- j22 j11) 10) (>= (- j11 j22) 5))
15 (or (>= (- j31 j11) 10) (>= (- j11 j31) 5))
16 (or (>= (- j31 j22) 5) (>= (- j22 j31) 5))))
17(assert (and (or (>= (- j21 j12) 5) (>= (- j12 j21) 15))
18 (or (>= (- j32 j12) 5) (>= (- j12 j32) 5))
19 (or (>= (- j32 j21) 15) (>= (- j21 j32) 5))))
20
21(define-fun max3 ((i Int) (j Int) (k Int)) Int
22 (ite (< i j) (ite (< j k) k j) (ite (< i k) k i)))
23
24(push)
25(assert (<= (max3 j12 j22 j32) 25))
26(check-sat)
27(pop)
28
29(push)
30(assert (<= (max3 j12 j22 j32) 24))
31(check-sat)
32(pop)
33
34(push)
35(assert (<= (max3 j12 j22 j32) 23))
36(check-sat)
37(pop)
38
39(push)
40(assert (<= (max3 j12 j22 j32) 23))
41(check-sat)
42(pop)
43
44(push)
45(assert (<= (max3 j12 j22 j32) 21))
46(check-sat)
47(pop)
48
49(push)
50(assert (<= (max3 j12 j22 j32) 20))
51(check-sat)
52(get-model)
53(pop)
54
55(assert (< (max3 j12 j22 j32) 20))
56(check-sat)
1def max2(i, j):
2 if i < j:
3 return j
4 else:
5 return i
6
7def max3(i, j, k):
8 return max2(max2(i,j),k)
9
10from cvc5.pythonic import *
11
12j11,j12,j21,j22,j31,j32 = Ints("j11 j12 j21 j22 j31 j32")
13
14s = SolverFor('QF_IDL')
15s.add(And([x >= 0 for x in [j11, j12, j21, j22, j31, j32]]))
16s.add(And(j12 - j11 >= 10, j22 - j21 >= 15, j32 - j31 >= 5))
17s.add(And(Or(j22 - j11 >= 10, j11 - j22 >= 5),
18 Or(j31 - j11 >= 10, j11 - j31 >= 5),
19 Or(j31 - j22 >= 5, j22 - j31 >= 5)))
20s.add(And(Or(j21 - j12 >= 5, j12 - j21 >= 15),
21 Or(j32 - j12 >= 5, j12 - j32 >= 5),
22 Or(j32 - j21 >= 15, j21 - j32 >= 5)))
23s.add(And(j12 <= 25, j22 <= 25, j32 <= 25))
24
25s.push()
26result = s.check()
27while result == sat:
28 m = s.model()
29 a = m.eval(j12).as_long()
30 b = m.eval(j22).as_long()
31 c = m.eval(j32).as_long()
32 s.pop()
33 best = max3(a, b, c) + 5
34 print("Best solution so far:", best, "minutes")
35 new_threshold = best - 5
36 s.push()
37 s.add(And(j12 < new_threshold, j22 < new_threshold, j32 < new_threshold))
38 result = s.check()
39
40s.pop()
41print(best, "is the best solution")
The output from cvc5 is as follows.
1sat
2sat
3sat
4sat
5sat
6sat
7(
8(define-fun j11 () Int 10)
9(define-fun j12 () Int 20)
10(define-fun j21 () Int 0)
11(define-fun j22 () Int 20)
12(define-fun j31 () Int 5)
13(define-fun j32 () Int 15)
14)
15unsat
1Best solution so far: 30 minutes
2Best solution so far: 29 minutes
3Best solution so far: 28 minutes
4Best solution so far: 27 minutes
5Best solution so far: 26 minutes
6Best solution so far: 25 minutes
725 is the best solution
Solution to Exercise 5
1(set-logic QF_LRA)
2(set-option :produce-models true)
3
4(declare-const a Real)
5(declare-const b Real)
6
7(assert (= (+ a 10.0) (* 2.0 b)))
8(assert (= (+ b 20.0) (* 2.0 a)))
9
10(check-sat)
11(get-model)
1from cvc5.pythonic import *
2a, b = Reals('a b')
3solve(a + 10.0 == 2.0 * b, b + 20.0 == 2.0 * a)
The output is as follows.
1sat
2(
3(define-fun a () Real (/ 50 3))
4(define-fun b () Real (/ 40 3))
5)
1[a = 50/3, b = 40/3]
Solution to Exercise 6
The changes are pretty simple.
In Example 4, we proved
that if the elements in indexes i and j
are the same, then the arrays are the same.
The way to do that was to assert that the elements are the same
while the arrays are different, and expect to get an unsat
answer, which indeed we got.
Now, we want to show that if the elements are different, then so are the arrays. Hence, we would like to assert that the elements are different while the arrays are the same. Hence, we interchange the equality and dis-equality in the last two assertions.
1(set-logic QF_AX)
2(declare-sort I 0)
3(declare-sort E 0)
4(declare-fun i () I)
5(declare-fun j () I)
6(declare-fun tmp () E)
7(declare-fun a_in () (Array I E))
8(declare-fun a_out () (Array I E))
9
10(assert (= tmp (select a_in i)))
11(assert (= a_out (store (store a_in i (select a_in j)) j tmp)))
12(assert (distinct (select a_in i) (select a_in j)))
13(assert (= a_in a_out))
14
15(check-sat)
1from cvc5.pythonic import *
2I = DeclareSort("I")
3E = DeclareSort("E")
4i, j = Consts("i j", I)
5tmp = Const("tmp", E)
6array = ArraySort(I, E)
7a_in, a_out = Consts("a_in, a_out", array)
8
9s = SolverFor('QF_AX')
10
11s.add(tmp == a_in[i])
12s.add(a_out == Store(Store(a_in, i, a_in[j]),
13 j, tmp))
14s.add(a_in[i] != a_in[j])
15s.add(a_in == a_out)
16
17print(s.check())
The output is as follows.
1unsat
1unsat
Solution to Exercise 7
1(set-logic QF_BV)
2(set-option :incremental true)
3
4(declare-const x (_ BitVec 32))
5
6; orignal abs(x) version
7(define-fun abs ((x (_ BitVec 32))) (_ BitVec 32) (ite (bvslt x (_ bv0 32)) (bvneg x) x))
8
9; encode branchless abs(x) alternatives
10(define-fun xrs () (_ BitVec 32) (bvashr x (_ bv31 32)))
11(define-fun abs1 ((x (_ BitVec 32))) (_ BitVec 32) (bvsub (bvxor x xrs) xrs))
12(define-fun abs2 ((x (_ BitVec 32))) (_ BitVec 32) (bvxor (bvadd x xrs) xrs))
13(define-fun abs3 ((x (_ BitVec 32))) (_ BitVec 32) (bvsub x (bvand (bvshl x (_ bv1 32)) xrs)))
14
15; check if abs() and abs1() are equivalent
16(push 1)
17(assert (distinct (abs x) (abs1 x)))
18(check-sat)
19(pop 1)
20
21; check if abs() and abs2() are equivalent
22(push 1)
23(assert (distinct (abs x) (abs2 x)))
24(check-sat)
25(pop 1)
26
27; check if abs() and abs3() are equivalent
28(push 1)
29(assert (distinct (abs x) (abs3 x)))
30(check-sat)
31(pop 1)
1from cvc5.pythonic import *
2x = Const("x", BitVecSort(32))
3xrs = x >> 31
4abs_ref = If(x < 0, -x, x) # abs() reference implementation
5abs1 = (x ^ xrs) - xrs
6abs2 = (x + xrs) ^ xrs
7abs3 = x - ((x << 1) & xrs)
8
9prove(abs_ref == abs1)
10prove(abs_ref == abs2)
11prove(abs_ref == abs3)
The output is as follows.
1unsat
2unsat
3unsat
1proved
2proved
3proved
Solution to Exercise 8
1(set-logic QF_DTLIA)
2(set-option :produce-models true)
3
4(declare-datatypes ((Tree 0)) (((node (data Int) (left Tree) (right Tree)) (nil))))
5
6(declare-fun x () Tree)
7
8(assert ((_ is node) x))
9(assert (= (left x) x))
10
11(check-sat)
1from cvc5.pythonic import *
2decl = Datatype("tree")
3decl.declare("node", ("data", IntSort()), ("left", decl), ("right", decl))
4decl.declare("nil")
5Tree = decl.create()
6
7x = Const("x", Tree)
8
9s = SolverFor('ALL')
10s.add(Tree.is_node(x))
11s.add(Tree.left(x) == x)
12
13print(s.model() if s.check() == sat else "unsat")
14
The output is as follows.
1unsat
1unsat
Solution to Exercise 9
1(set-logic QF_FP)
2(set-option :produce-models true)
3(declare-const a Float32)
4(declare-const b Float32)
5(declare-const c Float32)
6(declare-const rm RoundingMode)
7(assert (distinct (fp.add rm a (fp.add rm b c)) (fp.add rm (fp.add rm a b) c)))
8(check-sat)
9(get-model)
10(get-value ((fp.add rm a (fp.add rm b c))))
11(get-value ((fp.add rm (fp.add rm a b) c)))
1from cvc5.pythonic import *
2
3a, b, c = FPs("a b c", Float32())
4rm = Const("rm", RNE().sort())
5
6s = SolverFor('QF_FP')
7s.add(Distinct(fpAdd(rm, a, fpAdd(rm, b, c)), fpAdd(rm, fpAdd(rm, a, b), c)))
8result = s.check()
9m = s.model()
10print(m)
11print(f'fpAdd(rm, a, fpAdd(rm, b, c)) = {m.eval(fpAdd(rm, a, fpAdd(rm, b, c)))}')
12print(f'fpAdd(rm, fpAdd(rm, a, b), c) = {m.eval(fpAdd(rm, fpAdd(rm, a, b), c))}')
The output is as follows.
1sat
2(
3(define-fun a () (_ FloatingPoint 8 24) (fp #b1 #b11000111 #b00011111111111111111111))
4(define-fun b () (_ FloatingPoint 8 24) (fp #b0 #b11000111 #b00000000000000000000000))
5(define-fun c () (_ FloatingPoint 8 24) (fp #b1 #b10001101 #b11111111000000000000000))
6(define-fun rm () RoundingMode roundTowardNegative)
7)
8(((fp.add rm a (fp.add rm b c)) (fp #b1 #b11000011 #b11111111111111111111000)))
9(((fp.add rm (fp.add rm a b) c) (fp #b1 #b11000011 #b11111111111111111110001)))
1[a = -1.1249998807907104*(2**72), b = 1*(2**72), c = -1.99609375*(2**14), rm = RTN()]
2fpAdd(rm, a, fpAdd(rm, b, c)) = -1.9999990463256836*(2**68)
3fpAdd(rm, fpAdd(rm, a, b), c) = -1.9999982118606567*(2**68)
Solution to Exercise 10
We can change the solution to Example 12 to enforce that x1 and
x2 have length 1. With this change, the problem becomes unsatisfiable.
Thus, to obtain the solution, we add one more layer of concatenations, as shown
below.
1(set-logic QF_SLIA)
2(set-option :produce-models true)
3
4(declare-const p1 Bool)
5(declare-const p2 Bool)
6(declare-const p3 Bool)
7(declare-const p4 Bool)
8(declare-const p5 Bool)
9(declare-const p6 Bool)
10(declare-const p7 Bool)
11(declare-const p8 Bool)
12(declare-const p9 Bool)
13(declare-const p10 Bool)
14(declare-const p11 Bool)
15(declare-const p12 Bool)
16(declare-const p13 Bool)
17(declare-const p14 Bool)
18(declare-const p15 Bool)
19(declare-const p16 Bool)
20(declare-const p17 Bool)
21(declare-const p18 Bool)
22(declare-const p19 Bool)
23(declare-const p20 Bool)
24
25(declare-const x1 String)
26(declare-const x2 String)
27(declare-const x3 String)
28(declare-const x4 String)
29(declare-const x5 String)
30(declare-const x6 String)
31
32(declare-const i1 String)
33(declare-const i2 String)
34(declare-const i3 String)
35(declare-const i4 String)
36(declare-const i5 String)
37(declare-const i6 String)
38(declare-const i7 String)
39(declare-const i8 String)
40
41(define-const result String "abbaabb")
42
43(assert (and (<= (str.len x1) 1) (<= (str.len x2) 1)))
44
45(assert (= i1 (ite p1 x1 x2)))
46(assert (= i2 (ite p2 x1 x2)))
47(assert (= x3 (str.++ i1 i2)))
48
49(assert (= i3 (ite p3 x1 (ite p4 x2 x3))))
50(assert (= i4 (ite p5 x1 (ite p6 x2 x3))))
51(assert (= x4 (str.++ i3 i4)))
52
53(assert (= i5 (ite p7 x1 (ite p8 x2 (ite p9 x3 x4)))))
54(assert (= i6 (ite p10 x1 (ite p11 x2 (ite p12 x3 x4)))))
55(assert (= x5 (str.++ i5 i6)))
56
57(assert (= i7 (ite p13 x1 (ite p14 x2 (ite p15 x3 (ite p16 x4 x5))))))
58(assert (= i8 (ite p17 x1 (ite p18 x2 (ite p19 x3 (ite p20 x4 x5))))))
59(assert (= x6 (str.++ i7 i8)))
60
61(assert (= x6 result))
62
63(check-sat)
64(get-model)
1from cvc5.pythonic import *
2p, x, i = {}, {}, {}
3for k in range(1, 21): p[k] = Bool("p" + str(k))
4for k in range(1, 7): x[k] = String("x" + str(k))
5for k in range(1, 9): i[k] = String("i" + str(k))
6
7result = StringVal("abbaabb")
8
9s = SolverFor('QF_SLIA')
10s.add(And(Length(x[1]) <= 2, Length(x[2]) <= 2))
11
12s.add(i[1] == If(p[1], x[1], x[2]))
13s.add(i[2] == If(p[2], x[1], x[2]))
14s.add(x[3] == Concat(i[1], i[2]))
15
16s.add(i[3] == If(p[3], x[1], If(p[4], x[2], x[3])))
17s.add(i[4] == If(p[5], x[1], If(p[6], x[2], x[3])))
18s.add(x[4] == Concat(i[3], i[4]))
19
20s.add(i[5] == If(p[7], x[1], If(p[8], x[2], If(p[9], x[3], x[4]))))
21s.add(i[6] == If(p[10], x[1], If(p[11], x[2], If(p[12], x[3], x[4]))))
22s.add(x[5] == Concat(i[5], i[6]))
23
24s.add(i[7] == If(p[13], x[1], If(p[14], x[2], If(p[15], x[3], If(p[16], x[4], x[5])))))
25s.add(i[8] == If(p[17], x[1], If(p[18], x[2], If(p[19], x[3], If(p[20], x[4], x[5])))))
26s.add(x[6] == Concat(i[7], i[8]))
27
28s.add(x[6] == result)
29
30print(s.model() if s.check() == sat else "unsat")
The output is as follows.
1sat
2(
3(define-fun p1 () Bool true)
4(define-fun p2 () Bool true)
5(define-fun p3 () Bool false)
6(define-fun p4 () Bool true)
7(define-fun p5 () Bool false)
8(define-fun p6 () Bool false)
9(define-fun p7 () Bool false)
10(define-fun p8 () Bool true)
11(define-fun p9 () Bool true)
12(define-fun p10 () Bool false)
13(define-fun p11 () Bool false)
14(define-fun p12 () Bool false)
15(define-fun p13 () Bool false)
16(define-fun p14 () Bool false)
17(define-fun p15 () Bool false)
18(define-fun p16 () Bool true)
19(define-fun p17 () Bool false)
20(define-fun p18 () Bool false)
21(define-fun p19 () Bool false)
22(define-fun p20 () Bool false)
23(define-fun x1 () String "b")
24(define-fun x2 () String "a")
25(define-fun x3 () String "bb")
26(define-fun x4 () String "abb")
27(define-fun x5 () String "aabb")
28(define-fun x6 () String "abbaabb")
29(define-fun i1 () String "b")
30(define-fun i2 () String "b")
31(define-fun i3 () String "a")
32(define-fun i4 () String "bb")
33(define-fun i5 () String "a")
34(define-fun i6 () String "abb")
35(define-fun i7 () String "abb")
36(define-fun i8 () String "aabb")
37)
1[i1 = "a", i2 = "a", i3 = "aa", i4 = "bb", i5 = "bb", i6 = "aabb", i7 = "a", i8 = "bbaabb", p1 = True, p10 = False, p11 = False, p12 = False, p13 = True, p14 = True, p15 = True, p16 = True, p17 = False, p18 = False, p19 = False, p2 = True, p20 = False, p3 = False, p4 = False, p5 = False, p6 = True, p7 = False, p8 = True, p9 = True, x1 = "a", x2 = "bb", x3 = "aa", x4 = "aabb", x5 = "bbaabb", x6 = "abbaabb"]
Thus, the answer is that four concatentations are required.
Solution to Exercise 11
The most natural solution to this exercise seems to be to use the seq.prefixof operator in SMT-LIB
(PrefixOf in python).
However, this operator only enforces the property of being a prefix,
not a proper prefix.
Hence, we also need to add for each pair of variables
that they are distinct.
The result is indeed unsat as expected.
1(set-logic QF_SLIA)
2
3(declare-const x (Seq Int))
4(declare-const y (Seq Int))
5(declare-const z (Seq Int))
6
7(assert (and (seq.prefixof x y) (distinct x y)))
8(assert (and (seq.prefixof y z) (distinct y z)))
9(assert (and (seq.prefixof z x) (distinct z x)))
10
11(check-sat)
1from cvc5.pythonic import *
2x, y, z = Consts("x y z", SeqSort(IntSort()))
3
4s = SolverFor('QF_SLIA')
5
6s.add(And(PrefixOf(x, y), x != y))
7s.add(And(PrefixOf(y, z), y != z))
8s.add(And(PrefixOf(z, x), z != x))
9
10
11print(s.model() if s.check() == sat else "unsat")
12
The output is as follows.
1unsat
Solution to Exercise 12
1(set-logic QF_FF)
2(set-option :produce-models true)
3
4(define-sort F () (_ FiniteField 13)) ; F is an alias of sort (_ FiniteField 13)
5
6(declare-const x F)
7(declare-const y F)
8
9(assert (= (ff.mul x x) y))
10(assert (= (ff.mul y y) (as ff1 F)))
11
12(check-sat)
13(get-model)
1from cvc5.pythonic import *
2x, y = FiniteFieldElems("x y", 13)
3s = SolverFor("QF_FF")
4s.add(x * x == y)
5s.add(y * y == 1)
6print(s.model() if s.check() == sat else "unsat")
The output is as follows.
1sat
2(
3(define-fun x () (_ FiniteField 13) #f12m13)
4(define-fun y () (_ FiniteField 13) #f1m13)
5)
1[x = -1, y = 1]
Solution to Exercise 13
Set difference does not distribute over intersection. The solver is able to find a counterexample for this property.
1(set-logic QF_FS)
2(set-option :produce-models true)
3
4(declare-sort U 0)
5
6(declare-const A (Set U))
7(declare-const B (Set U))
8(declare-const C (Set U))
9
10(assert (not (= (set.minus A (set.inter B C)) (set.inter (set.minus A B) (set.minus A C)))))
11
12(check-sat)
13(get-model)
1from cvc5.pythonic import *
2S = DeclareSort("S")
3A, B, C = [Set(i, S) for i in ["A","B","C"]]
4s = SolverFor('QF_FS')
5s.add(Not(SetMinus(A, (B & C)) == ((SetMinus(A, B)) & (SetMinus(A, C)))))
6print(s.check())
7print(s.model())
8
The output is as follows.
1sat
2(
3; cardinality of U is 1
4; rep: (as @U_0 U)
5(define-fun A () (Set U) (set.singleton (as @U_0 U)))
6(define-fun B () (Set U) (set.singleton (as @U_0 U)))
7(define-fun C () (Set U) (as set.empty (Set U)))
8)
1sat
2[A = Singleton((as @S_0 S)), B = Singleton((as @S_0 S)), C = Empty(Set(S))]