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

  • 823d92702c Add Alethe Translation for Miniscope Rules (#12166) Lachnitt 2025-10-13 12:49:13 -07:00
  • b7ecabe17a Include Exist in QUANT_UNUSED_VARS Documentation (#11848) Lachnitt 2025-10-13 11:08:13 -07:00
  • 272e08074d Reorganize BV RARE rules to avoid computation in premises (#12153) Andrew Reynolds 2025-10-13 12:29:12 -05:00
  • da72534d68 Add missing include for rewrites.eo (#12176) Andrew Reynolds 2025-10-12 12:26:39 -05:00
  • 61f194aa83 Avoid computation in premises of string RARE rules (#12152) Andrew Reynolds 2025-10-10 08:38:32 -05:00
  • 2c0a181b99 Remove proof rule MACRO_RESOLUTION(_TRUST) (#12157) Andrew Reynolds 2025-10-09 12:31:48 -05:00
  • 0173534e69 Avoid mixed arithmetic in ARITH_REDUCTION (#12162) Andrew Reynolds 2025-10-08 13:42:25 -05:00
  • 63a88fb44e Fixes warnings in GMP build (#12165) Thomas Hader 2025-10-06 16:37:57 -07:00
  • 3e000e645a Add --inst-local option (#12121) Andrew Reynolds 2025-10-06 13:29:36 -05:00
  • 6a098fab88 ci: Remove option to choose release version (#12148) Daniel Larraz 2025-10-06 13:29:12 -05:00
  • 5eb4046f4d Introduce 3 new proof rules for handling distinct (#12124) Andrew Reynolds 2025-10-06 11:21:55 -05:00
  • 9115280669 Added --std=c99 to the GLPK build (#12160) Thomas Hader 2025-10-03 14:33:42 -07:00
  • 29ca6e63b0 python: Define explicit __init__ constructors for Cython classes (#12159) Daniel Larraz 2025-10-02 09:41:03 -05:00
  • b5bd2ca6a9 python: Allow None for tm argument in _term function (#12158) Daniel Larraz 2025-10-02 09:39:29 -05:00
  • c435239224 Minor simplifications to CPC+Eunoia (#12156) Andrew Reynolds 2025-10-01 11:21:51 -05:00
  • 1bfb5d467f setDefault: Use decision=internal only with bitblast-internal for QF_BV. (#12154) Mathias Preiner 2025-10-01 08:53:20 -07:00
  • 1bcf293081 Add an encapsulation of the optimization query result (#12138) ntsis 2025-09-30 11:53:16 -07:00
  • b4b886fe21 Add translation of EXISTS_ELIM (#12151) Lachnitt 2025-09-30 08:34:21 -07:00
  • 734c22114f new lemmas for pow2 (#12139) BergerZvika 2025-09-26 00:32:34 +03:00
  • 36ebc172d5 [alethe] Update names of proof-specific BV operators (#12150) Haniel Barbosa 2025-09-24 19:30:13 -03:00
  • a507dfdf11 cmake: Reintroduce variable CVC5_WHEEL_VERSION (#12149) Daniel Larraz 2025-09-24 14:46:35 -07:00
  • 967bdac410 ci: Add option to choose release version to build (#12146) Daniel Larraz 2025-09-24 11:05:26 -07:00
  • 1583578e8c Start post-release for 1.3.1 Mathias Preiner 2025-09-24 07:43:04 -07:00
  • ea1b484fa5 Bump version to 1.3.1 Mathias Preiner 2025-09-24 07:43:04 -07:00
  • 79ad3d0e49 Update version in NEWS file. Mathias Preiner 2025-09-24 07:42:49 -07:00
  • 1b34e4c887 java: Make CVC5ApiException a subclass of RuntimeException (#12141) Daniel Larraz 2025-09-22 15:36:26 -05:00
  • ba161bd3f0 Set default value for stable_mode in configure.sh (#12142) Daniel Larraz 2025-09-22 14:01:34 -05:00
  • 2c3da39208 Minor updates for printing CPC proofs (#12132) Andrew Reynolds 2025-09-22 11:34:25 -05:00
  • fd7e6d0620 cmake: Update targets to build and run API tests (#12127) Daniel Larraz 2025-09-22 10:33:06 -05:00
  • 201b968859 ci: Update cibuildwheel to v3.1.4 (#12125) Daniel Larraz 2025-09-22 10:29:25 -05:00
  • 5bb8d67ad6 Bump Pythonic API version (#12135) Daniel Larraz 2025-09-22 10:26:37 -05:00
  • 82f7bd50c1 Document missing change from 1.3.0 in NEWS (#12134) Daniel Larraz 2025-09-19 16:01:50 -05:00
  • 8ad1b3f772 Disable LFSC on regression (#12133) Andrew Reynolds 2025-09-19 08:45:55 -05:00
  • b056bd2446 Add stable as a build type (#12128) Andrew Reynolds 2025-09-18 13:36:59 -05:00
  • d75627373f setDefaults: Use decision=internal for QF_BV. (#12131) Mathias Preiner 2025-09-18 08:19:10 -07:00
  • 6a7dd160a4 Fix nightly failure. (#12130) Abdalrhman Mohamed 2025-09-18 07:47:23 -07:00
  • 5cf969ab01 Fix sort reps printing bug in get-model command. (#12129) Abdalrhman Mohamed 2025-09-18 06:42:02 -07:00
  • ed459990fd Fix type in macro elaboration of var-elim-ineq (#12126) Andrew Reynolds 2025-09-17 14:01:10 -05:00
  • 0f0ae82ce0 Optimizations for caching evaluation in RARE reconstruction (#12109) Andrew Reynolds 2025-09-17 08:18:28 -05:00
  • 8cd1274161 Add SMT-LIB command to print model domain elements. (#12088) Abdalrhman Mohamed 2025-09-16 10:20:03 -07:00
  • d264ea2100 Move distinct to theory UF (#12118) Andrew Reynolds 2025-09-16 11:47:24 -05:00
  • 79e1c14e5e Implement chain multiset resolution in Eunoia (#12080) Andrew Reynolds 2025-09-16 11:12:03 -05:00
  • 67975ea890 ci: Treat all Sphinx warnings as errors (#12112) Daniel Larraz 2025-09-16 09:33:19 -05:00
  • 416f8d6198 ci: Add Windows ARM64 build job (#12119) Daniel Larraz 2025-09-16 09:25:36 -05:00
  • 10b5de9eec More minor simplifications to declarations in Eunoia+CPC (#12028) Andrew Reynolds 2025-09-16 08:36:26 -05:00
  • 387a19d80a cmake: Use valid version id as specified in PEP 440 (#12120) Daniel Larraz 2025-09-11 14:43:50 -05:00
  • 5a7a3d2da2 cmake: Update versioning scheme (#12116) Daniel Larraz 2025-09-10 10:48:33 -05:00
  • e0ec61e050 Add support for compilation on Windows ARM64 (#12111) Daniel Larraz 2025-09-10 10:44:59 -05:00
  • e063876f5d ci: Use single job to set up release pages (#12104) Daniel Larraz 2025-09-10 10:39:06 -05:00
  • d509acd588 Ensure secant planes for exp don't cross zero (#12115) Andrew Reynolds 2025-09-09 14:58:36 -05:00
  • f4b081e82f Disable timeout regression (#12114) Andrew Reynolds 2025-09-09 13:08:20 -05:00
  • 543d2ed2fc Improvements to mbqi from mbqi enum choice branch (#12105) Andrew Reynolds 2025-09-08 12:01:52 -05:00
  • 2d240c467a Fix duplicate C++ declarations in Sphinx documentation (#12069) Daniel Larraz 2025-09-08 10:08:58 -05:00
  • f30f3a00e3 doc: Avoid duplicate indexing of cvc5.pythonic.Length (#12097) Daniel Larraz 2025-09-08 10:07:48 -05:00
  • 867cdf6271 Category option info for Python and Java APIs (#12100) José Neto 2025-09-08 10:47:59 -03:00
  • 58a8fad806 Minor improvement to sygus grammar, option to include partial apps in HO (#12106) Andrew Reynolds 2025-09-08 08:45:15 -05:00
  • ae2d768ec2 Minor improvements to higher-order solver from mbqi enum choice branch (#12107) Andrew Reynolds 2025-09-05 11:58:33 -05:00
  • aa93cb3041 Fix to transcendental rule, doc (#12110) Andrew Reynolds 2025-09-05 10:11:35 -05:00
  • be28db6c58 Do not do congruence over ordinary kinds in the model equality engine (#12093) Andrew Reynolds 2025-09-05 09:30:06 -05:00
  • f7db8faac6 Do not introduce mixed arithmetic in transcendental proof rules (#12101) Andrew Reynolds 2025-09-02 20:26:50 -05:00
  • 0ee7dca383 ci: Change the GH job that builds the documentation (#12076) Daniel Larraz 2025-09-02 11:59:16 -05:00
  • d552b2fa93 ci: Update code to clean up artifacts from latest (#12096) Daniel Larraz 2025-09-02 09:52:07 -05:00
  • 8ec24e5956 [proofs] [alethe] Do not name partial applications in Alethe printer (#12098) Haniel Barbosa 2025-08-28 16:39:17 -03:00
  • c680fe2481 Also send ensured atom equalities to THEORY_BUILTIN with ee central (#11921) Andrew Reynolds 2025-08-28 14:13:14 -05:00
  • aca99089d0 Fix error checking for UF type rule (#12064) Andrew Reynolds 2025-08-28 08:07:19 -05:00
  • ae1be1abfe Minor fixes to model construction for theory of datatypes (#12094) Andrew Reynolds 2025-08-27 09:21:00 -05:00
  • 2ae4ede42a Make NL more careful wrt theory combination (#11962) Andrew Reynolds 2025-08-25 10:22:20 -05:00
  • 36da0af5c6 Fix LFSC for regexp repeat (#12091) Andrew Reynolds 2025-08-25 09:42:19 -05:00
  • ec9cbcb6ce doc: Fix toctree consistency issues (#12090) Daniel Larraz 2025-08-23 17:10:09 -05:00
  • 5b85cad4ee doc: Add missing references to c examples (#12089) Daniel Larraz 2025-08-23 17:09:10 -05:00
  • 41576236b4 Add C++ version of the 'exceptions' example (#12085) Daniel Larraz 2025-08-23 17:08:09 -05:00
  • 90644be997 doc: Copy references.bib to build directory (#12073) Daniel Larraz 2025-08-23 17:06:36 -05:00
  • 04bfb2c31f doc: Address all warnings reported by docutils (#12071) Daniel Larraz 2025-08-23 17:06:09 -05:00
  • 651f196032 ci: Treat all Doxygen warnings as errors (#12068) Daniel Larraz 2025-08-23 17:01:43 -05:00
  • 6c2dc6e78f Add option to make regular expressions first class (#12049) Andrew Reynolds 2025-08-23 11:48:07 -05:00
  • ef4d013bdb Fix documentation for str.indexof_re (#12082) Andrew Reynolds 2025-08-23 11:47:54 -05:00
  • 31f513e64e Catch more cases of failure in HO model construction (#12087) Andrew Reynolds 2025-08-23 10:28:56 -05:00
  • efee026444 Add missing mapping for BITVECTOR_NEGO from internal to external (#12086) Daniel Larraz 2025-08-22 14:36:22 -05:00
  • a2eac27ab5 Add re.^ to CPC (#12081) Andrew Reynolds 2025-08-22 13:56:22 -05:00
  • 4cab88c762 Update wasm build (#11956) José Neto 2025-08-21 18:48:49 -03:00
  • 83a1549e98 Track has term incrementally for term db relevant (#12072) Andrew Reynolds 2025-08-20 10:57:51 -05:00
  • 13e624a1f5 Add ProofRule::CHAIN_M_RESOLUTION, disabled by default (#11984) Andrew Reynolds 2025-08-20 10:10:58 -05:00
  • 92d3ebfa40 Demote arithmetic POW to expert (#12070) Andrew Reynolds 2025-08-20 09:25:13 -05:00
  • 7c5c3f7d9d Do not mention safe mode in exception message if safe mode is not enabled (#12057) Andrew Reynolds 2025-08-20 09:24:37 -05:00
  • 8d8afd991c Infer recursive function definitions with sygus, permit declare-fun (#12050) Andrew Reynolds 2025-08-18 16:15:41 -05:00
  • a7a277211c Simplify and document several skolems (#12044) Andrew Reynolds 2025-08-18 09:57:30 -05:00
  • 383ed49a85 Add naive handling of re equalities, pf rule RE_EQ_ELIM (#12001) Andrew Reynolds 2025-08-15 12:39:09 -05:00
  • 89968ad88c Fix assertion related to printing lemma count (#12075) Andrew Reynolds 2025-08-14 15:36:45 -05:00
  • b1fe582ece Fix unsound proof rule str-indexof-find-emp (#12060) Andrew Reynolds 2025-08-13 12:22:31 -05:00
  • a6048282c3 cadical: Update to fixed CaDiCaL version. (#12055) Aina Niemetz 2025-08-13 03:40:20 -07:00
  • 259f435d4d Update Doxyfile from 1.9.1 to 1.9.8 (#12063) Daniel Larraz 2025-08-13 04:54:32 -05:00
  • 00c54de893 doc: Fix invalid escape sequences in Sphinx config files (#12066) Daniel Larraz 2025-08-13 04:53:37 -05:00
  • ae3b44eca1 ci: Continue if setup-cmake fails (#12065) Daniel Larraz 2025-08-12 10:25:51 -05:00
  • e52530cba7 ci: Treat all Javadoc warnings as errors (#12053) Daniel Larraz 2025-08-12 06:11:03 -05:00
  • eb9619bd54 Fix possible non-idempotency in rewriter (#12059) Andrew Reynolds 2025-08-11 17:03:04 -05:00
  • be7318d25a java: Make Proof a subclass of AbstractPointer (#12043) Daniel Larraz 2025-08-06 18:34:29 +02:00
  • 81eb5db515 Add missing Java API docs for Datatype* classes (#12041) Daniel Larraz 2025-08-06 18:18:43 +02:00
  • f455984f75 Add Java API docs for enumeration types (#12037) Daniel Larraz 2025-08-06 17:32:51 +02:00
  • 60254d553c Add missing Java API docs for the Op, Sort, and Term classes (#12035) Daniel Larraz 2025-08-06 17:30:02 +02:00
  • cb7677f6a7 Add Java API docs for the AbstractPointer and Context classes (#12034) Daniel Larraz 2025-08-06 13:02:15 +02:00