Commit Graph

Select branches

Hide Pull Requests

17

18-sustained

18.0

18.1

18.2

19-sustained

19.0

19.1

19.2

20-sustained

20.0

20.1

20.2

21-sustained

21.0

21.1

21.2

22.0

22.1

22.2

23-sustained

23-sustained-cvc4

23.0

23.0-cvc4

23.1

23.1-cvc4

23.2

24-sustained

24-sustained-cvc4

24.0

24.0-cvc4

24.1

24.1-cvc4

24.2

24.2-cvc4

25.0

25.1

OA16-011

a2c2-2020

gpl-2015

gpl-2016

gpl-2017

gpl-2018

lts-18

lts-19

lts-20

lts-21

master

master-cvc4

master-cvc5

nyu-1.7.x

nyu-cvc5-0.0.7

nyu-cvc5-1.0.0

nyu-cvc5-1.0.3

nyu-gcc6

nyu-main

nyu-master

spark-15.0

spark-16.0

Mono Color

• 3c3e4c8f43 Merge branch 'topic/kanig-2326-python' into '24-sustained' 24-sustained Liaiss Merzougue 2026-01-25 23:35:27 +01:00
• 97e0c193c0 Reenable support for all versions of python (#9844) Vinícius Camillo 2023-06-22 16:25:16 -03:00
• f2f9a40c37 Merge branch 'topic/kanig-1152-cvc5-132' into 'master' master Johannes Kanig 2026-01-07 09:27:23 +00:00
• fdf148cc47 fix location of cadical files Johannes Kanig 2026-01-05 18:26:56 +09:00
• 7be139c659 Remove cadical which has now its own repo Johannes Kanig 2026-01-05 10:43:59 +09:00
• d0cf79c932 Merge cvc5 1.3.2 into AdaCore master Johannes Kanig 2026-01-05 10:43:25 +09:00
• 86cecd83b6 Bump version to 1.3.2 Mathias Preiner 2025-12-12 10:58:38 -08:00
• 0ca1f0b9e1 Update version in NEWS file. Mathias Preiner 2025-12-12 10:58:14 -08:00
• 1f5c50e323 ci: Remove ubuntu:production-clang CI job (#12300) Daniel Larraz 2025-12-11 13:08:27 -06:00
• b886b61030 Disable regression (#12302) Andrew Reynolds 2025-12-10 14:11:53 -06:00
• 417810e66e ci: Pin MSYS2 installation to use Clang 19.1.4 (#12301) Daniel Larraz 2025-12-10 06:17:51 -06:00
• a137ead681 Preparation for 1.3.2 release (#12297) Andrew Reynolds 2025-12-09 15:27:33 -06:00
• 6dd08fb064 Move shadow elimination to post-rewrite, guard variable elimination (#12288) Andrew Reynolds 2025-12-09 14:31:32 -06:00
• 05a9433b25 Fix issue with substitution context in strings extended function inference (#12292) Andrew Reynolds 2025-12-09 14:15:32 -06:00
• e622d77107 Ensure integer constants are converted to rationals in numerator of division terms (#12294) Andrew Reynolds 2025-12-09 13:29:22 -06:00
• ec1104194a ci: Move cross-compilation jobs to a new workflow (#12299) Daniel Larraz 2025-12-09 11:29:51 -06:00
• a83019d9fb ci: Build and release Linux artifacts compiled with libc++ (#12293) Daniel Larraz 2025-12-08 19:47:51 -06:00
• 4e7922ee32 Use MSYS2 CLANG64 to compile on Windows x86_64 (#12291) Daniel Larraz 2025-12-08 18:18:23 -06:00
• b7542cfa74 Piand pr4 (#12295) BergerZvika 2025-12-08 08:14:02 -08:00
• 22ecb335c5 smt: ModelBlocker: Fix refcount issues of TNode vs Node handling. (#12287) Mathias Preiner 2025-12-04 10:17:02 -08:00
• f6a97feed8 ci: Bump GitHub Actions versions (#12290) Daniel Larraz 2025-12-04 10:03:36 -06:00
• 74554ef170 Fix subtype elimination for ARITH_MULT_SIGN (#12275) Andrew Reynolds 2025-12-03 14:26:36 -06:00
• 5ddd4f098e Fix double negation handling in NNF proofs (#12276) Andrew Reynolds 2025-12-03 13:18:21 -06:00
• f825b36f13 Fix issue with subtypes in NL comparison proofs (#12277) Andrew Reynolds 2025-12-03 12:03:32 -06:00
• b19989f56a Fix issue with duplicate proof steps in theory rewrite reconstruction (#12278) Andrew Reynolds 2025-12-03 10:50:54 -06:00
• c74436736e Assign function values lazily in theory model (#12267) Andrew Reynolds 2025-12-03 09:57:13 -06:00
• 2547e66f7e Fix two RARE proof rules for strings (#12259) Andrew Reynolds 2025-12-03 09:16:41 -06:00
• 686e31842b prop: cadical: Reorganize CaDiCaL wrapper code. (#12286) Mathias Preiner 2025-12-03 07:14:51 -08:00
• af48ba32fe Update Eunoia+CPC to ensure substitutions have no variable capture (#12274) Andrew Reynolds 2025-12-02 11:24:30 -06:00
• ece7e2f3e0 Remove unused method (#12270) Bruno Andreotti 2025-12-02 13:11:54 -03:00
• 0a48398ee2 Normalization algorithm implementation (FMCAD 2025 paper) (#12206) Daneshvar Amrollahi 2025-12-02 07:00:58 -08:00
• b1d6b3f1c8 piand pr3 - piand solver (#12245) BergerZvika 2025-12-02 07:00:41 -08:00
• e933b7c554 Move arithmetic utility to context where types for numerals are defined (#12262) Andrew Reynolds 2025-12-02 08:58:19 -06:00
• e603425598 Bump Pythonic API version (#12280) Daniel Larraz 2025-12-02 06:16:19 -06:00
• 67312dcd41 doc: Add instructions for using Java bindings with Maven (#12271) Daniel Larraz 2025-12-01 18:35:54 -06:00
• 107be4fd49 ci: Only publish to Maven Central when running on the cvc5 repo (#12273) Daniel Larraz 2025-12-01 11:56:55 -06:00
• a4ca250306 Add timing stat to justify heuristic (#12269) Andrew Reynolds 2025-12-01 09:24:34 -06:00
• 911d9b4b6a Apply extensionality eagerly to functions with HO arguments (#12265) Andrew Reynolds 2025-12-01 09:23:59 -06:00
• 84c7e4829e ci: Publish cvc5 Java API to Maven Central (#12268) Daniel Larraz 2025-11-26 09:29:21 -06:00
• 3410dd348b Remove test when libpoly is not present. (#12250) Thomas Hader 2025-11-25 14:46:04 -08:00
• c6cc9c93db Build native JAR and add POM file for Maven Central publication (#12249) Daniel Larraz 2025-11-25 15:41:09 -06:00
• 076d065ea4 [proofs] Fix cyclic proof issue in EqProof conversion (#12266) Haniel Barbosa 2025-11-25 17:21:44 -03:00
• 2b3d85f6c8 Add proof support for lazy distinct extension of UF (#12220) Andrew Reynolds 2025-11-25 13:21:49 -06:00
• dbbd3aff6a Copy utility methods to theory model for delayed function models (#12230) Andrew Reynolds 2025-11-25 13:20:07 -06:00
• e0ee808eee Fix cyclic arithmetic proof (#12264) Andrew Reynolds 2025-11-25 13:19:11 -06:00
• 3da5981987 More fixes for proof subtype elimination (#12228) Andrew Reynolds 2025-11-25 12:05:51 -06:00
• ff09969f7f Fix proof reconstruction for nctn rewrite with str.from_code (#12263) Andrew Reynolds 2025-11-25 11:00:54 -06:00
• 2397a0e2b4 Fix proofs of nl comparison with arithmetic subtyping (#12261) Andrew Reynolds 2025-11-25 10:46:11 -06:00
• 37609cb737 Eliminate shadowing at prerewrite (#12258) Andrew Reynolds 2025-11-24 17:23:56 -06:00
• 8c4803232f Fix ARITH_MULT_SIGN for mixed arithmetic (#12243) Andrew Reynolds 2025-11-24 16:38:40 -06:00
• 90ea47f5e1 Fix proofs in arithmetic congruence manager (#12260) Andrew Reynolds 2025-11-24 15:17:59 -06:00
• f365b8d30b Fix fairness issue with inst-when mode (#12222) Andrew Reynolds 2025-11-24 15:14:13 -06:00
• a7676d7fd6 Fix inference ids for E-matching (#12232) Andrew Reynolds 2025-11-24 14:52:02 -06:00
• 6980d6ac7f Fix issue with proofs of length intro on non-ACI normalized strings (#12242) Andrew Reynolds 2025-11-24 14:29:20 -06:00
• 74e4727a3a Add missing :signature annotation (#12251) Andrew Reynolds 2025-11-24 10:25:13 -06:00
• 17f380674b java: Store JNI library by OS and CPU architecture (#12237) Daniel Larraz 2025-11-17 10:17:04 -06:00
• 67c2c201ff Build Javadoc and sources JARs for IDE docs and navigation (#12236) Daniel Larraz 2025-11-17 10:09:54 -06:00
• c1f829cfca Use Maven versioning scheme for cvc5 Java bindings (#12235) Daniel Larraz 2025-11-17 10:06:35 -06:00
• ef828478cf Improvement to get-ethos-checker script (#12225) yoni206 2025-11-13 18:48:57 +02:00
• 21cdd7ccf7 Piand: add piand kind (#12221) BergerZvika 2025-11-13 18:21:51 +02:00
• 443bfee282 cpc proofs for log2 (#12233) yoni206 2025-11-13 17:41:12 +02:00
• c07c580542 Allow MBQI by terms with constant arrays when arraysExp is enabled (#12205) Andrew Reynolds 2025-11-12 10:00:36 -06:00
• 941a5c94fb Fix LFSC regressions with log2 (#12231) Andrew Reynolds 2025-11-12 09:54:46 -06:00
• 310f487e6a Basic Support for Logarithm with Base 2 (#12224) yoni206 2025-11-11 19:52:25 +02:00
• f70c183c0f Fix proofs for linear arithmetic conflicts that involve non-linear (#12227) Andrew Reynolds 2025-11-11 10:54:21 -06:00
• 724682fa53 Enable proof subtype elimination by default (#12198) Andrew Reynolds 2025-11-07 08:44:25 -06:00
• f8b78ade4a Use Brzozowski derivatives for evaluating regexes in Eunoia (#12210) ofecisrael 2025-11-07 16:17:28 +02:00
• 536a6a5c18 Do not split on infinite datatypes based on fmf option (#12218) Andrew Reynolds 2025-11-06 16:49:58 -06:00
• 7209879a53 Add distinct extension to UF (#12164) Andrew Reynolds 2025-11-06 10:38:57 -06:00
• 1875b33ad3 Add two temporary bit-vector rules to the alethe translation (#12217) Lachnitt 2025-11-06 08:36:45 -08:00
• 7f13a963c7 Consolidate comments about proof_rule.h (#12213) Lachnitt 2025-11-06 08:34:36 -08:00
• 1120e3df17 Adapt CMake files to run Java tests on Windows (#12203) Daniel Larraz 2025-11-05 15:25:56 -06:00
• dc8ad24031 Add Piand Solver Header (#12211) BergerZvika 2025-11-05 16:51:00 +02:00
• c2effa38fd Fix issue with duplicate lemma in datatypes split (#12209) Andrew Reynolds 2025-11-04 14:56:52 -06:00
• 4213d540bf Added normalization utlity for Sort nodes (#12190) Daneshvar Amrollahi 2025-10-31 10:21:22 -07:00
• 887e171610 Added header file for normalization pre-pass (#12191) Daneshvar Amrollahi 2025-10-31 10:05:40 -07:00
• 61fdd49941 Add flatten monomials lemma schema (#12204) Andrew Reynolds 2025-10-31 11:03:39 -05:00
• 1e8ffb3f29 Do not check if qid is a declared symbol (#12201) Andrew Reynolds 2025-10-30 14:11:11 -05:00
• aeb554775b Use builtin singleton elimination method in Eunoia (#12199) Andrew Reynolds 2025-10-29 11:54:15 -05:00
• 478876f4d8 Add missing Java and Python API tests (#12186) Daniel Larraz 2025-10-28 06:29:03 -05:00
• 18d0c5e070 Avoid evaluation in premises of two RE RARE rules (#12175) Andrew Reynolds 2025-10-24 09:34:55 -05:00
• ba84f7c96d More fixes for proof-elim-subtypes (#12197) Andrew Reynolds 2025-10-23 15:29:40 -05:00
• ecde653542 ci: Upgrade macOS runners to macOS 15 (#12169) Daniel Larraz 2025-10-22 14:00:30 -05:00
• 4a31e001ac cmake: Use correct source directory for GMP install (#12168) Daniel Larraz 2025-10-22 13:23:01 -05:00
• feb784748d Add the no-supports field in the output of --help-option-categories (#12171) Andrew Reynolds 2025-10-22 13:03:34 -05:00
• 1d37b4970e cmake: Check for Pip after creating venv (#12167) Daniel Larraz 2025-10-22 13:03:17 -05:00
• 4b68b2cd7b More fixes for proof subtype elimination (#12182) Andrew Reynolds 2025-10-21 13:16:20 -05:00
• 679b9f702d Fix soundness of 5 RARE BV proof rules (#12184) Andrew Reynolds 2025-10-20 11:53:08 -05:00
• 90ba85d0f9 Add side conditions to make alpha equivalence rule sound in Eunoia (#12187) Andrew Reynolds 2025-10-20 09:39:31 -05:00
• 221f108b10 Moved beta reduction infra to correct directory (#12188) Daneshvar Amrollahi 2025-10-20 07:39:20 -07:00
• 95879aeeb7 Disable timeout regression (bv_to_int_bvmul2) (#12193) Daniel Larraz 2025-10-20 09:25:31 -05:00
• f56d15750c Disable unsat core on regression (bv_to_int_bvmul2) (#12189) Daniel Larraz 2025-10-18 11:02:37 -05:00
• 2526624021 Treat nonlinear monomials as variables in the DIO solver (#12178) Daniel Larraz 2025-10-16 14:29:54 -05:00
• 0a8689fd5d Enable proof-chain-m-res by default (#12181) Andrew Reynolds 2025-10-16 12:17:35 -05:00
• 8730c328b2 Add beta reduction infra (#12177) Daneshvar Amrollahi 2025-10-16 07:22:17 -07:00
• cbcaf6e783 Implement general lemma schema for context-dependent rewriting in strings (#12174) Andrew Reynolds 2025-10-16 08:42:00 -05:00
• 05697494fe [proof log] Fix (again) when to start the proof logger in the PropEngine (#12185) Haniel Barbosa 2025-10-15 17:09:30 -03:00
• c23612bb98 Renable class of quantifiers rewrites when not in safe mode (#12179) Andrew Reynolds 2025-10-15 10:13:22 -05:00
• 8e01b70a8f Minor improvements to handling corner cases of RE (#12108) Andrew Reynolds 2025-10-15 09:56:17 -05:00
• 393d249ba9 Building GMP in source directory (#12180) Thomas Hader 2025-10-14 10:39:54 -07:00