Skip to content

Commit 17517b5

Browse files
mudathirmahgoubmudathirmahgoub
authored
Merge branch 'main' into noLiftLambda
2 parents b5dc76f + 053f65c commit 17517b5

214 files changed

Lines changed: 9179 additions & 3357 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎NEWS.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,17 @@
11
This file contains a summary of important user-visible changes.
22

3+
cvc5 1.4.2 prerelease
4+
=====================
5+
6+
- Adds techniques for returning "sat" when the returned candidate model
7+
happens to satisfy the set of input assertions (`--model-verify`).
8+
9+
- `set.insert` is now a binary operator, where applications with more than two
10+
arguments are constructed as nested binary applications, e.g.
11+
`(set.insert a b S)` is constructed as `(set.insert a (set.insert b S))`.
12+
This impacts the children of such terms when inspected via the API, as well
13+
as how they are printed.
14+
315
cvc5 1.4.1
416
==========
517

‎README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
[![License: BSD](
22
https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)](
33
https://opensource.org/licenses/BSD-3-Clause)
4-
![CI](https://github.com/cvc5/cvc5/workflows/CI/badge.svg)
4+
![CI](https://github.com/cvc5/cvc5/actions/workflows/ci.yml/badge.svg?branch=main)
55
[![Coverage](
66
https://img.shields.io/endpoint?url=https://cvc5.stanford.edu/downloads/builds/coverage/nightly-coverage.json)](
77
https://cvc5.stanford.edu/downloads/builds/coverage)

‎cmake/FindCoCoA.cmake‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,6 @@ if(CoCoA_INCLUDE_DIR AND CoCoA_LIBRARIES)
3333
try_compile(CoCoA_USABLE "${DEPS_BASE}/try_compile/CoCoA-EP"
3434
"${CMAKE_CURRENT_LIST_DIR}/deps-utils/cocoa-test.cpp"
3535
CMAKE_FLAGS
36-
"-DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE}"
3736
"-DINCLUDE_DIRECTORIES=${CoCoA_INCLUDE_DIR}"
3837
LINK_LIBRARIES ${CoCoA_LIBRARIES} ${GMP_LIBRARIES} ${GMPXX_LIBRARIES}
3938
)

‎cmake/FindGMP.cmake‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,6 @@ if(GMP_INCLUDE_DIR AND GMPXX_INCLUDE_DIR AND GMP_LIBRARIES AND GMPXX_LIBRARIES)
5151
try_compile(GMP_USABLE "${DEPS_BASE}/try_compile/GMP-EP"
5252
"${CMAKE_CURRENT_LIST_DIR}/deps-utils/gmp-test.cpp"
5353
CMAKE_FLAGS
54-
"-DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE}"
5554
"-DINCLUDE_DIRECTORIES=${GMP_INCLUDE_DIR}"
5655
LINK_LIBRARIES ${GMP_LIBRARIES} ${GMPXX_LIBRARIES}
5756
)

‎contrib/get-logos-checker‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ set -e -o pipefail
1414
# place that pin lives: contrib/check-logos-compilation reads it from here, so
1515
# the checker that is installed and the checker that proofs/eo/cpc is checked
1616
# against are the same one by construction. Moving this line moves both.
17-
LOGOS_VERSION="49f4fd1f256f5504f1a21c61c1808ffc56eeb6b8"
17+
LOGOS_VERSION="9c4834bb91bc311cc502005a12c95992eb1edabe"
1818

1919
while [ $# -gt 0 ]; do
2020
case "$1" in

‎docs/CMakeLists.txt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
# The build system configuration.
1111
##
1212
find_package(Sphinx REQUIRED)
13-
check_python_module(breathe "breathe<5")
13+
check_python_module(breathe "breathe!=5.0.0")
1414
check_python_module(sphinxcontrib.bibtex sphinxcontrib-bibtex)
1515
check_python_module(sphinx_tabs.tabs sphinx-tabs)
1616
check_python_module(sphinxcontrib.programoutput sphinxcontrib-programoutput)

‎include/cvc5/cvc5_kind.h‎

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3467,9 +3467,9 @@ enum ENUM(Kind)
34673467
*/
34683468
EVALUE(SET_SINGLETON),
34693469
/**
3470-
* The set obtained by inserting elements;
3470+
* The set obtained by inserting elements, right associative.
34713471
*
3472-
* - Arity: ``n > 0``
3472+
* - Arity: ``n > 1``
34733473
*
34743474
* - ``1..n-1:`` Terms of any Sort (must match the element sort of the given set Term)
34753475
* - ``n:`` Term of set Sort
@@ -3482,6 +3482,15 @@ enum ENUM(Kind)
34823482
* - Create Op of this kind with:
34833483
*
34843484
* - TermManager::mkOp(Kind, const std::vector<uint32_t>&)
3485+
*
3486+
* \rst
3487+
* .. note::
3488+
*
3489+
* Similar to :cpp:enumerator:`IMPLIES`, terms of this kind with more
3490+
* than two arguments are constructed as nested binary applications,
3491+
* e.g. ``(set.insert a b S)`` is constructed as
3492+
* ``(set.insert a (set.insert b S))``.
3493+
* \endrst
34853494
*/
34863495
EVALUE(SET_INSERT),
34873496
/**

‎include/cvc5/cvc5_proof_rule.h‎

Lines changed: 2 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -4185,17 +4185,6 @@ enum ENUM(ProofRewriteRule)
41854185
* \endverbatim
41864186
*/
41874187
EVALUE(SETS_EVAL_OP),
4188-
/**
4189-
* \verbatim embed:rst:leading-asterisk
4190-
* **Sets -- sets insert elimination**
4191-
*
4192-
* .. math::
4193-
*
4194-
* \mathit{set.insert}(t_1, \ldots, t_n, S) = \texttt{set.union}(\texttt{sets.singleton}(t_1), \ldots, \texttt{sets.singleton}(t_n), S)
4195-
*
4196-
* \endverbatim
4197-
*/
4198-
EVALUE(SETS_INSERT_ELIM),
41994188
// RARE rules
42004189
// ${rules}$
42014190
/** Auto-generated from RARE rule arith-div-total-zero-real */
@@ -4656,6 +4645,8 @@ enum ENUM(ProofRewriteRule)
46564645
EVALUE(SETS_MEMBER_EMP),
46574646
/** Auto-generated from RARE rule sets-subset-elim */
46584647
EVALUE(SETS_SUBSET_ELIM),
4648+
/** Auto-generated from RARE rule sets-insert-elim */
4649+
EVALUE(SETS_INSERT_ELIM),
46594650
/** Auto-generated from RARE rule sets-union-comm */
46604651
EVALUE(SETS_UNION_COMM),
46614652
/** Auto-generated from RARE rule sets-inter-comm */

‎proofs/eo/cpc/Cpc.eo‎

Lines changed: 353 additions & 290 deletions
Large diffs are not rendered by default.

‎proofs/eo/cpc/programs/AciNorm.eo‎

Lines changed: 44 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -2,43 +2,54 @@
22

33
; program: $get_ai_norm_rec
44
; args:
5-
; - f (-> S S S): The function we are considering, which is assumed to be associative+idempotent and has the given identity.
5+
; - f (-> S S S): The function we are considering, which is assumed to be
6+
; associative+idempotent and has the given identity.
67
; - id S: The nil terminator of f.
78
; - s S: The term to process.
8-
; return: the result of normalizing s based on associative+idempotent+identity reasoning.
9-
(program $get_ai_norm_rec ((T Type) (S Type) (f (-> S S S)) (id T) (x T) (x1 T) (x2 T))
9+
; return: the result of normalizing s based on associative+idempotent+identity
10+
; reasoning.
11+
(program $get_ai_norm_rec
12+
((T Type) (S Type) (f (-> S S S)) (id T) (x T) (x1 T) (x2 T))
1013
:signature ((-> S S S) T T) T
1114
(
12-
(($get_ai_norm_rec f id (f x1 x2)) (eo::list_setof f (eo::list_concat f ($get_ai_norm_rec f id x1) ($get_ai_norm_rec f id x2))))
13-
(($get_ai_norm_rec f id id) id)
14-
(($get_ai_norm_rec f id x) (_ f x id))
15+
(($get_ai_norm_rec f id (f x1 x2))
16+
(eo::list_setof f
17+
(eo::list_concat f ($get_ai_norm_rec f id x1) ($get_ai_norm_rec f id x2)))
18+
)
19+
(($get_ai_norm_rec f id id) id)
20+
(($get_ai_norm_rec f id x) (_ f x id))
1521
)
1622
)
1723

1824
; program: $get_ai_norm
1925
; args:
2026
; - t U: The term to process.
21-
; return: the result of normalizing t based on associative+idempotent+identity reasoning.
27+
; return: the result of normalizing t based on associative+idempotent+identity
28+
; reasoning.
2229
(program $get_ai_norm ((S Type) (U Type) (f (-> S S S)) (x U) (y U))
2330
:signature (U) U
2431
(
25-
(($get_ai_norm (f x y)) (eo::define ((id (eo::nil f (eo::typeof (f x y)))))
26-
(eo::list_singleton_elim f ($get_ai_norm_rec f id (f x y)))))
32+
(($get_ai_norm (f x y))
33+
(eo::define ((id (eo::nil f (eo::typeof (f x y)))))
34+
(eo::list_singleton_elim f ($get_ai_norm_rec f id (f x y)))))
2735
)
2836
)
2937

3038
; program: $get_a_norm_rec
3139
; args:
32-
; - f (-> S S S): The function we are considering, which is assumed to be associative and has the given identity.
40+
; - f (-> S S S): The function we are considering, which is assumed to be
41+
; associative and has the given identity.
3342
; - id S: The nil terminator of f.
3443
; - s S: The term to process.
3544
; return: the result of normalizing s based on associative+identity reasoning.
36-
(program $get_a_norm_rec ((T Type) (S Type) (f (-> S S S)) (id T) (x T) (x1 T) (x2 T))
45+
(program $get_a_norm_rec
46+
((T Type) (S Type) (f (-> S S S)) (id T) (x T) (x1 T) (x2 T))
3747
:signature ((-> S S S) T T) T
3848
(
39-
(($get_a_norm_rec f id (f x1 x2)) (eo::list_concat f ($get_a_norm_rec f id x1) ($get_a_norm_rec f id x2)))
40-
(($get_a_norm_rec f id id) id)
41-
(($get_a_norm_rec f id x) (_ f x id))
49+
(($get_a_norm_rec f id (f x1 x2))
50+
(eo::list_concat f ($get_a_norm_rec f id x1) ($get_a_norm_rec f id x2)))
51+
(($get_a_norm_rec f id id) id)
52+
(($get_a_norm_rec f id x) (_ f x id))
4253
)
4354
)
4455

@@ -49,16 +60,22 @@
4960
(program $get_a_norm ((S Type) (U Type) (f (-> S S S)) (x U) (y U))
5061
:signature (U) U
5162
(
52-
(($get_a_norm (f x y)) (eo::define ((id (eo::nil f (eo::typeof (f x y)))))
53-
(eo::list_singleton_elim f ($get_a_norm_rec f id (f x y)))))
63+
(($get_a_norm (f x y))
64+
(eo::define ((id (eo::nil f (eo::typeof (f x y)))))
65+
(eo::list_singleton_elim f ($get_a_norm_rec f id (f x y)))))
5466
)
5567
)
5668

5769
; A placeholder that indicates that the given list can be sorted with respect
58-
; to operator f. For example, (@aci.sorted f t) indicates that t is an application
59-
; of a commutative operator f. We show the equivalence of two applications marked
70+
; to operator f. For example, (@aci.sorted f t) indicates that t is an
71+
; application
72+
; of a commutative operator f. We show the equivalence of two applications
73+
; marked
6074
; in this way using the operator for multiset equality below.
61-
(declare-parameterized-const @@aci_sorted ((U Type :implicit) (T Type :implicit)) (-> U T T))
75+
(declare-parameterized-const @@aci_sorted
76+
((U Type :implicit) (T Type :implicit))
77+
(-> U T T))
78+
6279
(define @aci.sorted () @@aci_sorted)
6380

6481
; program: $aci_norm_eq
@@ -69,10 +86,10 @@
6986
(program $aci_norm_eq ((S Type) (U Type) (t U) (s U) (f (-> S S S)))
7087
:signature (U U) Bool
7188
(
72-
(($aci_norm_eq t t) true)
73-
(($aci_norm_eq (@aci.sorted f t) t) true)
89+
(($aci_norm_eq t t) true)
90+
(($aci_norm_eq (@aci.sorted f t) t) true)
7491
(($aci_norm_eq (@aci.sorted f t) (@aci.sorted f s)) (eo::list_meq f t s))
75-
(($aci_norm_eq t s) false)
92+
(($aci_norm_eq t s) false)
7693
)
7794
)
7895

@@ -84,6 +101,8 @@
84101
; - bn S: The normalized form of the second term.
85102
; return: whether a can be shown equal to b by ACI_NORM
86103
(define $is_aci_norm ((S Type :implicit) (a S) (b S) (an S) (bn S))
87-
(eo::ite ($aci_norm_eq an b) true ; first check if we are singleton case
88-
(eo::ite ($aci_norm_eq bn a) true ; vice versa
89-
($aci_norm_eq an bn)))) ; otherwise check equivalence by above
104+
(eo::ite ($aci_norm_eq an b)
105+
true ; first check if we are singleton case
106+
(eo::ite ($aci_norm_eq bn a)
107+
true ; vice versa
108+
($aci_norm_eq an bn)))) ; otherwise check equivalence by above

0 commit comments

Comments
 (0)