ada/cvc5
0
0
Fork 0
mirror of https://github.com/AdaCore/cvc5.git synced 2026-02-12 12:32:16 -08:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • c164a6aa0a Add missing Java API docs for the Pair, Triplet, and Utils classes (#12032) Daniel Larraz 2025-08-06 12:58:38 +02:00
  • 5fcdb48eb2 Fix another naming convention issue in CPC (#12048) Andrew Reynolds 2025-08-05 09:16:15 -05:00
  • 2e79a8a8d2 Fix unsound proof rule strings_decompose (#12047) Andrew Reynolds 2025-08-05 08:42:04 -05:00
  • d6b64007d3 Fix unsound proof rule str-contains-repl-char (#12045) Andrew Reynolds 2025-08-05 08:05:44 -05:00
  • b78e7ed233 Fix unsound proof rule str-indexof-eq-irr (#12046) Andrew Reynolds 2025-08-01 15:36:58 -05:00
  • 6dacfa50e1 Fix resource limit setup in get-value (#12039) Andrew Reynolds 2025-07-29 11:06:14 -05:00
  • 42ecde4d82 Fix (unused) incorrect bound inference in strings arith entail (#12036) Andrew Reynolds 2025-07-29 03:35:23 -05:00
  • c5fb98b48c Introduce naming convention in CPC for internal data declarations (#12033) Andrew Reynolds 2025-07-28 13:55:10 -05:00
  • bc009afd43 Java bindings: fix for performance bottleneck in Context (#12030) am 2025-07-25 02:16:21 +10:00
  • da72dc1bea Use subsolver in get-value when necessary (#12002) Andrew Reynolds 2025-07-24 10:22:22 -05:00
  • 6a4791bf51 Add missing #includes (#11355) Eric Wieser 2025-07-21 13:07:01 +01:00
  • 6372a39525 Use new NFA regular expression test whenever possible in CPC rules (#12025) Andrew Reynolds 2025-07-18 12:26:13 -05:00
  • fcdd9f78bc Minor simplifications to Eunoia CPC signature (#12018) Andrew Reynolds 2025-07-18 10:31:48 -05:00
  • e997816864 Add NFA-based regular expression utility in CPC (#12024) ofecisrael 2025-07-18 17:25:06 +03:00
  • 9c754d4585 cmake: Enforce C11 standard (#12019) Daniel Larraz 2025-07-15 17:06:08 +02:00
  • 057c141d74 doc: Update steps for testing cvc5 (#12022) Daniel Larraz 2025-07-15 17:05:25 +02:00
  • 77d024a386 Remove 'friend' declaration from Grammar class (#12021) Daniel Larraz 2025-07-15 17:02:49 +02:00
  • db2da02ee5 cmake: Install Sphinx if not available (#12020) Daniel Larraz 2025-07-15 17:02:19 +02:00
  • f38e07df08 prop: cadical: Add support for getProof via CaDiCaL's proof tracer. (#11709) Mathias Preiner 2025-07-08 17:18:51 -07:00
  • 5b8eb7fff0 cmake: Download GMP from cvc5-deps (#12017) Daniel Larraz 2025-07-08 20:17:54 +02:00
  • e4b1fb5934 Catch illegal code points in u32string mkString API function (#11937) Andrew Reynolds 2025-07-08 09:55:50 -05:00
  • 510315c260 Use u32string to represent Unicode strings encoded in UTF-32 (#11994) Daniel Larraz 2025-07-08 10:12:52 +02:00
  • e900af3059 docs: Add docs for OptionCategory. (#12016) Aina Niemetz 2025-07-03 15:23:04 -07:00
  • e2a2b30ab6 doc: Update references to deprecated Solver methods (#12014) Daniel Larraz 2025-07-04 00:19:04 +02:00
  • aca1eb3e94 Remove old references and add missing one in COPYING file (#12015) Daniel Larraz 2025-07-03 19:21:14 +02:00
  • 9a65c178cf Move declarations out of loop when checking cycles in datatypes (#12013) Tomer Hakak 2025-06-29 16:17:26 +03:00
  • 58cda4cdc9 Do not filter output for the model-validation and unsat-cores tracks (#12012) Daniel Larraz 2025-06-25 23:34:11 +02:00
  • b3f4de3472 OptionCategory: Add missing implementations, uncovered tests. (#12011) Aina Niemetz 2025-06-24 23:59:46 -07:00
  • 5372270b5e python: Suppress deprecation warnings related to OptionInfo (#12009) Daniel Larraz 2025-06-24 18:04:35 +02:00
  • fa9f9cdd3e OptionInfo: Revert change to field name. (#12008) José Neto 2025-06-24 12:58:13 -03:00
  • ed897d4c91 Add Editline setup steps in INSTALL.rst (#12004) Daniel Larraz 2025-06-24 08:04:56 +02:00
  • fe5d4fed98 api: Refactor OptionInfo struct to provide option category. (#11931) José Neto 2025-06-23 13:54:00 -03:00
  • adc84c243b Simplify usage of list_concat in Eunoia+CPC (#12006) Andrew Reynolds 2025-06-23 10:26:08 -05:00
  • 557253155e cadical: Do not notifySatLiteral on renotify_fixed. (#11998) Aina Niemetz 2025-06-20 13:41:51 -07:00
  • b7e85d77ac ci: Tag latest as prerelease. (#11999) Aina Niemetz 2025-06-19 13:45:51 -07:00
  • cdbe05279c Add pre-simplify routine for proof node updater (#11950) Andrew Reynolds 2025-06-19 09:08:14 -05:00
  • 304409c52b Take into account component types to compute well foundedness of dt constructors (#11992) Andrew Reynolds 2025-06-19 08:15:58 -05:00
  • 15c808f86d Start post-release for 1.3.0 Aina Niemetz 2025-06-18 17:27:32 -07:00
  • 02c4e43d19 Bump version to 1.3.0 Aina Niemetz 2025-06-18 17:27:32 -07:00
  • af68265e2d Update NEWS for release 1.3.0. Aina Niemetz 2025-06-18 17:26:17 -07:00
  • 13df737104 ci: Fix auto-population of release message. (#11995) Aina Niemetz 2025-06-18 15:59:44 -07:00
  • 7d234f53f2 ci: Auto-populate release message. (#11993) Aina Niemetz 2025-06-18 13:20:55 -07:00
  • f19f42f377 Update copyright headers, add missing header documentation. (#11990) Mathias Preiner 2025-06-18 12:41:07 -07:00
  • c6160f5068 News for release (#11976) Andrew Reynolds 2025-06-18 10:08:30 -05:00
  • 1089af8511 Merge branch 'topic/aarch64_aborted' into 'master' Piotr Trojanek 2025-06-18 10:02:18 +02:00
  • da344db063 Fix "Aborted" message being printed on aarch64 Daniel Larraz 2025-06-18 00:08:59 +02:00
  • 440e4eee24 Minor fix for check proofs configuration (#11989) Andrew Reynolds 2025-06-17 14:39:35 -05:00
  • 21ba5e87dd More miscellaneous changes to Eunoia+CPC to ensure terms can be type checked (#11979) Andrew Reynolds 2025-06-17 13:11:46 -05:00
  • 7b2fe68c95 Add CoCoALib to the GPL section in the COPYING file (#11987) Daniel Larraz 2025-06-17 17:57:32 +02:00
  • 91201c459e Fix docs in preparation for upcoming release. (#11983) Aina Niemetz 2025-06-17 06:22:02 -07:00
  • 403162b510 Do not merge relevant domains of different type (#11985) Andrew Reynolds 2025-06-17 08:21:48 -05:00
  • 85663b2a91 Fix soundness bug with injective map down rule (#11986) mudathirmahgoub 2025-06-17 08:21:30 -05:00
  • 02113d2e05 Update CPC+Eunoia bitblast signature to avoid eo::match, use type checkable terms (#11980) Andrew Reynolds 2025-06-16 10:06:56 -05:00
  • 336d2f3d61 Minor simplification of BV rewriter for xor simplification (#11981) Andrew Reynolds 2025-06-13 20:06:05 -05:00
  • a5cee7a410 More refactoring of the CPC signature of strings (#11964) Andrew Reynolds 2025-06-12 11:30:36 -05:00
  • 4ddcbcb691 Eagerly eliminate duplicates in CPC+Eunoia definition of ACI_NORM (#11978) Andrew Reynolds 2025-06-11 18:07:31 -05:00
  • 97d323e053 Add portfolio-dry-run option (#11977) Daniel Larraz 2025-06-11 23:17:58 +02:00
  • e3bc51080f Convert mk scripts to Python (#11810) José Neto 2025-06-11 13:36:43 -03:00
  • 7b6771fbb1 Fix performance bug in RARE fixed point rules (#11954) Andrew Reynolds 2025-06-11 09:56:48 -05:00
  • d9a6495d62 Rewrite CPC+Eunoia definition of SEQ_EVAL_OP (#11975) Andrew Reynolds 2025-06-11 08:04:40 -05:00
  • e41f3ee071 ff: fix bitsum rewriter (#11972) Alex Ozdemir 2025-06-10 09:18:33 -07:00
  • 0c69ec4015 Pin Cython to versions < 3.1.2 (#11973) Daniel Larraz 2025-06-10 10:45:11 -05:00
  • a5f64f2188 Update portfolio options to ensure last strategy is compatible with models/unsat cores (#11960) Andrew Reynolds 2025-06-07 15:27:42 -05:00
  • 4ccf7277be Modify CPC definition of quantifiers rules to avoid eo::match (#11963) Andrew Reynolds 2025-06-06 04:08:03 -05:00
  • ca5c10931c Miscellaneous refactoring of CPC (#11965) Andrew Reynolds 2025-06-06 02:29:49 -05:00
  • befcee5dd1 Clean miscellaneous minor issues in CPC with types and eo::match (#11948) Andrew Reynolds 2025-06-05 09:28:47 -05:00
  • 1e7433d29a Refactor CPC signature for string rules to avoid eo::match (#11949) Andrew Reynolds 2025-06-05 02:44:54 -05:00
  • 4d6788e43e Fix issue in HO solver with finite types (#11955) Andrew Reynolds 2025-06-04 02:12:56 -05:00
  • bd5b89f49c Remove spurious assertion for HO models (#11959) Andrew Reynolds 2025-06-03 12:42:13 -05:00
  • 52dad31ff7 Modify regression (#11957) Andrew Reynolds 2025-06-03 12:14:37 -05:00
  • ae75a101d6 Handle SMT-LIB 2.7 as an input case (#11939) Andrew Reynolds 2025-06-03 11:26:07 -05:00
  • ec22154a34 Fix GPL arm64 macOS builds (#11958) Daniel Larraz 2025-06-03 11:25:50 -05:00
  • 27b2af6ebe ci: Use the lowest supported Java version for each platform (#11925) Daniel Larraz 2025-06-02 15:54:09 -05:00
  • b8a8d89941 Ensure constant folding on BV overflow predicates (#11929) Andrew Reynolds 2025-06-02 15:53:10 -05:00
  • 65bcc8aa6a cmake: Always set --build option when building GMP, CLN, and GLPK (#11953) Daniel Larraz 2025-06-02 12:08:24 -05:00
  • 5a238734d6 Remove deprecated table-based license key from pyproject.toml (#11952) Daniel Larraz 2025-06-02 11:57:22 -05:00
  • a255e1cef0 Refactor CPC arithmetic signature to avoid eo::match, fix types (#11947) Andrew Reynolds 2025-05-31 16:27:53 -05:00
  • 49c49a0c77 Bump Pythonic API version and add Pythonic tests (#11951) Daniel Larraz 2025-05-30 10:16:33 -05:00
  • 5172e8e717 Refactor CPC definition of string RE consume to avoid eo::match (#11945) Andrew Reynolds 2025-05-29 21:21:15 -05:00
  • 67982c836f Refactor CPC utilities to avoid programs that cannot be type checked (#11944) Andrew Reynolds 2025-05-29 20:54:15 -05:00
  • 4e6faee30c Refactor CPC ACI_NORM and ABSORB to have proper types (#11942) Andrew Reynolds 2025-05-29 19:04:01 -05:00
  • 32c5f698c4 Refactor CPC Booleans and UF to avoid eo::match (#11943) Andrew Reynolds 2025-05-29 18:15:35 -05:00
  • 9c08f7e6bc Annotate signatures of programs in CPC using :signature (#11946) Andrew Reynolds 2025-05-29 18:03:19 -05:00
  • 8f0fed3a43 Fix 11932 (#11940) Alex Ozdemir 2025-05-29 10:06:27 -07:00
  • 9a0bbd94aa Update CPC signature to use new list primitives (#11914) Andrew Reynolds 2025-05-28 16:13:20 -05:00
  • a0a6334acb Update usages of eo::nil to new syntax (#11938) Andrew Reynolds 2025-05-28 14:07:12 -05:00
  • be095feecc Further type fixes for CPC signature (#11913) Andrew Reynolds 2025-05-28 13:20:23 -05:00
  • bb321e300e More type fixes for CPC signature (#11894) Andrew Reynolds 2025-05-28 12:17:31 -05:00
  • 6a5959d9d1 Purification for nested sequence constants (#11865) Andrew Reynolds 2025-05-28 08:42:09 -05:00
  • 761ae2309a Use model directly for arithmetic values in strings (#11891) Andrew Reynolds 2025-05-28 08:24:58 -05:00
  • f0a1364a86 Print statistics on timeout (#11922) Amalee Wilson 2025-05-27 09:12:15 -07:00
  • a7fef69901 Do not evaluate semi-evaluated operators applied to unevaluated terms (#11930) Andrew Reynolds 2025-05-25 11:27:16 -05:00
  • d9d5ad1b42 Refactor arithmetic signature to simplify types for Eunoia programs (#11896) Andrew Reynolds 2025-05-22 14:04:04 -05:00
  • 581f774544 Disable another timeout regression (#11927) Andrew Reynolds 2025-05-22 13:44:28 -05:00
  • 448f5c10f6 Refactor distinct values program for datatypes and definition of DT_CONS_EQ_CLASH (#11897) Andrew Reynolds 2025-05-22 13:04:05 -05:00
  • 7c014ee90a More updates to options categories (#11920) Andrew Reynolds 2025-05-22 12:01:48 -05:00
  • de5bd39eb5 Add --help-option-categories (#11919) Andrew Reynolds 2025-05-22 12:01:37 -05:00
  • 9a3cc4f132 Eliminate term attributes from the CPC signature (#11874) Andrew Reynolds 2025-05-22 11:50:34 -05:00
  • 64ce392d2d Update CPC to use eo::eq instead of eo::is_eq when applicable (#11892) Andrew Reynolds 2025-05-22 10:46:02 -05:00
  • c167cfb2e5 Print portfolio config string even when strategy is a single config (#11918) Daniel Larraz 2025-05-21 11:11:33 -05:00