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.
109 lines
3.1 KiB
Java
109 lines
3.1 KiB
Java
/******************************************************************************
|
|
* 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.
|
|
* ****************************************************************************
|
|
*
|
|
* Black box testing of the guards of the Java API functions.
|
|
*/
|
|
|
|
package tests;
|
|
import static io.github.cvc5.Kind.*;
|
|
import static io.github.cvc5.SortKind.*;
|
|
import static io.github.cvc5.ProofRule.*;
|
|
import static org.junit.jupiter.api.Assertions.*;
|
|
|
|
import io.github.cvc5.*;
|
|
import java.math.BigInteger;
|
|
import java.util.ArrayList;
|
|
import java.util.Arrays;
|
|
import java.util.Iterator;
|
|
import java.util.List;
|
|
import org.junit.jupiter.api.AfterEach;
|
|
import org.junit.jupiter.api.BeforeEach;
|
|
import org.junit.jupiter.api.Test;
|
|
|
|
class ProofTest
|
|
{
|
|
private Solver d_solver;
|
|
|
|
@BeforeEach
|
|
void setUp()
|
|
{
|
|
d_solver = new Solver();
|
|
}
|
|
|
|
@AfterEach
|
|
void tearDown()
|
|
{
|
|
Context.deletePointers();
|
|
}
|
|
|
|
Proof create_proof() throws CVC5ApiException
|
|
{
|
|
d_solver.setOption("produce-proofs", "true");
|
|
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
|
|
Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
|
|
|
|
Term x = d_solver.mkConst(uSort, "x");
|
|
Term y = d_solver.mkConst(uSort, "y");
|
|
Term f = d_solver.mkConst(uToIntSort, "f");
|
|
Term p = d_solver.mkConst(intPredSort, "p");
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term one = d_solver.mkInteger(1);
|
|
Term f_x = d_solver.mkTerm(Kind.APPLY_UF, f, x);
|
|
Term f_y = d_solver.mkTerm(Kind.APPLY_UF, f, y);
|
|
Term sum = d_solver.mkTerm(Kind.ADD, f_x, f_y);
|
|
Term p_0 = d_solver.mkTerm(Kind.APPLY_UF, p, zero);
|
|
Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
|
|
d_solver.assertFormula(d_solver.mkTerm(Kind.GT, zero, f_x));
|
|
d_solver.assertFormula(d_solver.mkTerm(Kind.GT, zero, f_y));
|
|
d_solver.assertFormula(d_solver.mkTerm(Kind.GT, sum, one));
|
|
d_solver.assertFormula(p_0);
|
|
d_solver.assertFormula(p_f_y.notTerm());
|
|
assertTrue(d_solver.checkSat().isUnsat());
|
|
|
|
return d_solver.getProof()[0];
|
|
}
|
|
|
|
@Test
|
|
void getRule() throws CVC5ApiException
|
|
{
|
|
Proof proof = create_proof();
|
|
assertEquals(ProofRule.SCOPE, proof.getRule());
|
|
}
|
|
|
|
@Test
|
|
void getResult() throws CVC5ApiException
|
|
{
|
|
Proof proof = create_proof();
|
|
assertDoesNotThrow(() -> proof.getResult());
|
|
}
|
|
|
|
@Test
|
|
void getChildren() throws CVC5ApiException
|
|
{
|
|
Proof proof = create_proof();
|
|
Proof[] children = proof.getChildren();
|
|
assertNotEquals(0, children.length);
|
|
}
|
|
|
|
@Test
|
|
void getArguments() throws CVC5ApiException
|
|
{
|
|
Proof proof = create_proof();
|
|
assertDoesNotThrow(() -> proof.getArguments());
|
|
}
|
|
|
|
}
|