From a227e2e87dc380993fc7944668dafd2dfab3f4a8 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 12 Feb 2025 09:05:40 -0800 Subject: [PATCH 1/2] ignore most output in pf tests, for test stability --- cvc5_pythonic_api/cvc5_pythonic.py | 43 +++--------------------------- 1 file changed, 4 insertions(+), 39 deletions(-) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index e25a0a2..9086fea 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -6254,28 +6254,9 @@ def proof(self): >>> s.add(a == 0) >>> s.check() unsat - >>> s.proof() + >>> s.proof() #doctest: +ELLIPSIS +NORMALIZE_WHITESPACE (SCOPE: Not(And(a + 2 == 0, a == 0)), - (SCOPE: Not(And(a + 2 == 0, a == 0)), - [a + 2 == 0, a == 0], - (EQ_RESOLVE: False, - (ASSUME: a == 0, [a == 0]), - (TRANS: (a == 0) == False, - (CONG: (a == 0) == (-2 == 0), - [5], - (EQ_RESOLVE: a == -2, - (ASSUME: a + 2 == 0, [a + 2 == 0]), - (TRANS: (a + 2 == 0) == (a == -2), - (CONG: (a + 2 == 0) == (2 + a == 0), - [5], - (TRUST_THEORY_REWRITE: a + 2 == 2 + a, - [a + 2 == 2 + a, 3, 7]), - (REFL: 0 == 0, [0])), - (TRUST_THEORY_REWRITE: (2 + a == 0) == (a == -2), - [(2 + a == 0) == (a == -2), 3, 7]))), - (REFL: 0 == 0, [0])), - (TRUST_THEORY_REWRITE: (-2 == 0) == False, - [(-2 == 0) == False, 3, 7]))))) + ... """ p = self.solver.getProof()[0] return ProofRef(self, p) @@ -6909,25 +6890,9 @@ def getChildren(self): unsat >>> p = s.proof() >>> p = p.getChildren()[0].getChildren()[0] - >>> p + >>> p #doctest: +ELLIPSIS +NORMALIZE_WHITESPACE (EQ_RESOLVE: False, - (ASSUME: a == 0, [a == 0]), - (TRANS: (a == 0) == False, - (CONG: (a == 0) == (-2 == 0), - [5], - (EQ_RESOLVE: a == -2, - (ASSUME: a + 2 == 0, [a + 2 == 0]), - (TRANS: (a + 2 == 0) == (a == -2), - (CONG: (a + 2 == 0) == (2 + a == 0), - [5], - (TRUST_THEORY_REWRITE: a + 2 == 2 + a, - [a + 2 == 2 + a, 3, 7]), - (REFL: 0 == 0, [0])), - (TRUST_THEORY_REWRITE: (2 + a == 0) == (a == -2), - [(2 + a == 0) == (a == -2), 3, 7]))), - (REFL: 0 == 0, [0])), - (TRUST_THEORY_REWRITE: (-2 == 0) == False, - [(-2 == 0) == False, 3, 7]))) + ... """ children = self.proof.getChildren() return [ProofRef(self.solver, cp) for cp in children] From 4f39b207459d7df94e47527a36af2b3970abcef2 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 12 Feb 2025 11:18:51 -0800 Subject: [PATCH 2/2] fix arguments to cvc5 install dependencies action --- .github/workflows/ci.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 14775b9..c022399 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -29,7 +29,6 @@ jobs: uses: ./cvc5/.github/actions/install-dependencies with: with-documentation: false - with-python-bindings: true - name: Setup ccache cache uses: actions/cache@v2