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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
###############################################################################
# Top contributors (to current version):
# Abdalrhman Mohamed, Aina Niemetz, Hans-Joerg Schurr
#
# 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.
# #############################################################################
#
# Unit tests for proof API.
#
# Obtained by translating test/unit/api/sort_black.cpp
##
import pytest
import cvc5
from cvc5 import Kind, ProofRule
@pytest.fixture
def tm():
return cvc5.TermManager()
@pytest.fixture
def solver(tm):
return cvc5.Solver(tm)
def create_proof(tm, solver):
solver.setOption("produce-proofs", "true")
uSort = tm.mkUninterpretedSort("u")
intSort = tm.getIntegerSort()
boolSort = tm.getBooleanSort()
uToIntSort = tm.mkFunctionSort(uSort, intSort)
intPredSort = tm.mkFunctionSort(intSort, boolSort)
x = tm.mkConst(uSort, "x")
y = tm.mkConst(uSort, "y")
f = tm.mkConst(uToIntSort, "f")
p = tm.mkConst(intPredSort, "p")
zero = tm.mkInteger(0)
one = tm.mkInteger(1)
f_x = tm.mkTerm(Kind.APPLY_UF, f, x)
f_y = tm.mkTerm(Kind.APPLY_UF, f, y)
summ = tm.mkTerm(Kind.ADD, f_x, f_y)
p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero)
p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y)
solver.assertFormula(tm.mkTerm(Kind.GT, zero, f_x))
solver.assertFormula(tm.mkTerm(Kind.GT, zero, f_y))
solver.assertFormula(tm.mkTerm(Kind.GT, summ, one))
solver.assertFormula(p_0)
solver.assertFormula(p_f_y.notTerm())
assert solver.checkSat().isUnsat()
return solver.getProof()[0]
def create_rewrite_proof(tm, solver):
solver.setOption("produce-proofs", "true")
solver.setOption("proof-granularity", "dsl-rewrite")
int_sort = tm.getIntegerSort()
x = tm.mkConst(int_sort, "x")
zero = tm.mkInteger(0)
geq = tm.mkTerm(Kind.GEQ, x, zero)
leq = tm.mkTerm(Kind.LEQ, zero, x)
solver.assertFormula(tm.mkTerm(Kind.DISTINCT, geq, leq))
solver.checkSat()
return solver.getProof()[0]
def test_null_proof(solver):
proof = cvc5.Proof()
assert proof.getRule() == ProofRule.UNKNOWN
assert hash(ProofRule.UNKNOWN) == hash(ProofRule.UNKNOWN)
assert proof.getResult().isNull()
assert len(proof.getChildren()) == 0
assert len(proof.getArguments()) == 0
def test_get_rule(tm, solver):
proof = create_proof(tm, solver)
rule = proof.getRule()
assert rule == ProofRule.SCOPE
def test_get_rewrite_rule(tm, solver):
proof = create_rewrite_proof(tm, solver)
with pytest.raises(RuntimeError):
proof.getRewriteRule()
rule = None
stack = [proof]
while rule != ProofRule.DSL_REWRITE:
proof = stack.pop()
rule = proof.getRule()
children = proof.getChildren()
stack.extend(children)
assert proof.getRewriteRule() is not None
def test_get_result(tm, solver):
proof = create_proof(tm, solver)
proof.getResult()
def test_get_children(tm, solver):
proof = create_proof(tm, solver)
children = proof.getChildren()
assert len(children) > 0
def test_get_arguments(tm, solver):
proof = create_proof(tm, solver)
proof.getArguments()
def test_eq(tm, solver):
x = create_proof(tm, solver)
y = x.getChildren()[0]
z = cvc5.Proof()
assert x == x
assert not x != x
assert not x == y
assert x != y
assert not (x == z)
assert x != z
assert hash(x) == hash(x)
|
