mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
ce64f348d3
This pull requests adds support to get Proofs as proper objects from the API. To do so it adds an object Proof that encapsulates a ProofNode. Furthermore, it adds a function proofsToString to the Solver object that prints (a vector of) proofs. Finally, it modifies the getProof function of the Solver object to return proofs. Proof rules are returned as strings. One thing I don't quite like is that the proof component configuration must be given to both the getProof and proofsToString method and must be the same.
78 lines
2.2 KiB
Python
78 lines
2.2 KiB
Python
###############################################################################
|
|
# Top contributors (to current version):
|
|
# Hans-Jörg Schurr
|
|
#
|
|
# This file is part of the cvc5 project.
|
|
#
|
|
# Copyright (c) 2009-2023 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
|
|
|
|
|
|
@pytest.fixture
|
|
def solver():
|
|
return cvc5.Solver()
|
|
|
|
|
|
def create_proof(solver):
|
|
solver.setOption("produce-proofs", "true");
|
|
|
|
uSort = solver.mkUninterpretedSort("u")
|
|
intSort = solver.getIntegerSort()
|
|
boolSort = solver.getBooleanSort()
|
|
uToIntSort = solver.mkFunctionSort(uSort, intSort)
|
|
intPredSort = solver.mkFunctionSort(intSort, boolSort)
|
|
|
|
x = solver.mkConst(uSort, "x")
|
|
y = solver.mkConst(uSort, "y")
|
|
f = solver.mkConst(uToIntSort, "f")
|
|
p = solver.mkConst(intPredSort, "p")
|
|
zero = solver.mkInteger(0)
|
|
one = solver.mkInteger(1)
|
|
f_x = solver.mkTerm(Kind.APPLY_UF, f, x)
|
|
f_y = solver.mkTerm(Kind.APPLY_UF, f, y)
|
|
summ = solver.mkTerm(Kind.ADD, f_x, f_y)
|
|
p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero)
|
|
p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y)
|
|
solver.assertFormula(solver.mkTerm(Kind.GT, zero, f_x))
|
|
solver.assertFormula(solver.mkTerm(Kind.GT, zero, f_y))
|
|
solver.assertFormula(solver.mkTerm(Kind.GT, summ, one))
|
|
solver.assertFormula(p_0)
|
|
solver.assertFormula(p_f_y.notTerm())
|
|
assert solver.checkSat().isUnsat()
|
|
|
|
return solver.getProof()[0]
|
|
|
|
|
|
def test_get_result(solver):
|
|
proof = create_proof(solver)
|
|
rule = proof.getRule()
|
|
assert rule == "SCOPE"
|
|
|
|
|
|
def test_get_result(solver):
|
|
proof = create_proof(solver)
|
|
proof.getResult()
|
|
|
|
|
|
def test_get_children(solver):
|
|
proof = create_proof(solver)
|
|
children = proof.getChildren()
|
|
assert len(children) > 0
|
|
|
|
|
|
def test_get_arguments(solver):
|
|
proof = create_proof(solver)
|
|
proof.getArguments()
|