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

  • 2ff1e17d62 More updates to safe options (#11761) Andrew Reynolds 2025-04-07 16:32:39 -05:00
  • 1dd45a4857 Refactor and minor improvements to MBQI (#11722) Andrew Reynolds 2025-04-07 16:32:00 -05:00
  • de09de59a0 Infrastructure and proof rules involving witness terms (#11536) Andrew Reynolds 2025-04-07 12:27:46 -05:00
  • 0310120e1d Add Eunoia signature for (forthcoming) rule exists string length (#11788) Andrew Reynolds 2025-04-07 10:19:45 -05:00
  • 6dbf4a123b Finish Eunoia bitblasting signature and enable (#11785) Andrew Reynolds 2025-04-04 07:38:00 -05:00
  • 9b8ccc59b7 Extend evaluator for applications of symbolic indexed operators (#11641) Andrew Reynolds 2025-04-04 07:16:41 -05:00
  • ee76c367ef Add Eunoia signature for bitblasting shifts (#11783) Andrew Reynolds 2025-04-03 10:53:21 -05:00
  • 9d99200333 Miscellaneous changes to string rewriter (#11779) Andrew Reynolds 2025-04-03 08:32:14 -05:00
  • 0c31f7b803 Pass NodeManager pointer to getNullTerminator (#11781) Daniel Larraz 2025-04-03 08:18:23 -05:00
  • 1267afadce preprocessing/printer/proof: Refactor to not use NodeManager::currentNM() (#11780) Daniel Larraz 2025-04-02 17:30:52 -05:00
  • 8bee87b942 Minor changes and fixes to RARE rules (#11776) Andrew Reynolds 2025-04-02 16:42:20 -05:00
  • 19d1c1d104 Add Eunoia bitblast signature for bvite, refactor constant (#11774) Andrew Reynolds 2025-04-02 15:36:41 -05:00
  • 210436e143 Add Eunoia definitions for BV multiplication overflow predicates (#11675) Andrew Reynolds 2025-04-02 15:35:40 -05:00
  • f086362342 rewriter: Refactor to not use NodeManager::currentNM() (#11778) Daniel Larraz 2025-04-02 14:45:06 -05:00
  • 0e4aaa4a34 Add fine grained proof support for quantifiers variable eliminations (#11698) Andrew Reynolds 2025-04-02 14:00:57 -05:00
  • 268f4fd142 expr: Refactor to not use NodeManager::currentNM() (#11777) Daniel Larraz 2025-04-02 12:55:39 -05:00
  • 6ec5fb7633 [proof log] Make sure we log lemmas from presolve() (#11631) Haniel Barbosa 2025-04-02 14:51:44 -03:00
  • 6826042ced Add NodeManager pointer to SkolemManager (#11773) Daniel Larraz 2025-04-02 11:24:07 -05:00
  • 6ec69ca856 bags/sets/datatypes: Eliminate calls to NodeManager::currentNM() (#11771) Daniel Larraz 2025-04-02 09:43:43 -05:00
  • 3f84ac1a1b Disable unsat core on regression (#11775) Andrew Reynolds 2025-04-02 09:40:07 -05:00
  • fe6d0cc836 Add remaining RARE rewrites for strings (#11569) Andrew Reynolds 2025-04-01 19:27:46 -05:00
  • 38875008cd [proofs] [alethe] Fix handling of Alethe skolem definitions (#11753) Haniel Barbosa 2025-04-01 20:52:32 -03:00
  • ff8459d834 Add Eunoia definitions for bitblasting udiv/urem (#11770) Andrew Reynolds 2025-04-01 16:07:56 -05:00
  • 05b01735a3 moved code that prints theorem index to a separate function (#11767) Kartik Sabharwal 2025-04-01 12:36:27 -05:00
  • 3e9d3f2924 Add Eunoia side conditions for bitblasting multiplication (#11765) Andrew Reynolds 2025-04-01 11:50:13 -05:00
  • f82d1403b6 Set CMAKE_POLICY_VERSION_MINIMUM for libpoly (#11768) Daniel Larraz 2025-04-01 11:20:35 -05:00
  • 34518c3100 arith: Refactor to not use NodeManager::currentNM() (#11748) Daniel Larraz 2025-03-31 13:04:43 -05:00
  • 3cb56d402b Treat higher-order equality as define-fun in non-incremental (#11766) Daniel Larraz 2025-03-31 11:22:02 -05:00
  • 54148e583a Add side conditions for bitblasting addition and bitwise operators (#11763) Andrew Reynolds 2025-03-31 08:53:08 -05:00
  • a4f1c9128c Miscellaneous remaining changes to strings signature (#11762) Andrew Reynolds 2025-03-28 08:31:39 -05:00
  • ba649b731f Add bv (un)signed inequality to bitblasting signature (#11759) Andrew Reynolds 2025-03-27 09:32:31 -05:00
  • 8594a8e4dc Include MinGW-w64 libraries in static JNI library (#11757) Daniel Larraz 2025-03-26 13:19:12 -05:00
  • 93e3ce3cb3 More minor changes to BV rewriter for proofs (#11704) Andrew Reynolds 2025-03-26 13:00:36 -05:00
  • 81eb2b281b Add bitblasting utils to Eunoia signature (#11754) Andrew Reynolds 2025-03-26 08:44:56 -05:00
  • 5b954dffb8 Fix prenex quant norm (#11755) Andrew Reynolds 2025-03-26 08:44:43 -05:00
  • 760e6953a5 moved code that prints unproven conjectures to a separate function (#11737) Kartik Sabharwal 2025-03-24 16:19:53 -05:00
  • 46d49e43b2 Add macro elaboration for MACRO_BV_AND_OR_XOR_CONCAT_PULLUP (#11676) Andrew Reynolds 2025-03-24 13:14:56 -05:00
  • 7bf5d3e457 cadical: Add more stats. (#11747) Aina Niemetz 2025-03-21 13:31:18 -07:00
  • 4384596826 cadical: Add more trace messages. (#11746) Aina Niemetz 2025-03-21 12:44:27 -07:00
  • ab64642fc9 Improve documentation of SatSolver interface. (#11745) Aina Niemetz 2025-03-18 13:41:48 -07:00
  • 82ff0f2f3e cmake: Compute absolute path to toolchain files (#11743) Daniel Larraz 2025-03-18 10:29:22 -05:00
  • b949f81fbf Add a static build option for the JNI library (#11730) Daniel Larraz 2025-03-17 14:58:03 -05:00
  • b50dd17a1d Add more regressions from proof branch (#11739) Andrew Reynolds 2025-03-17 11:11:49 -05:00
  • 497e9847e8 Allow quoted symbols in indexed operators (#11738) Andrew Reynolds 2025-03-17 10:35:16 -05:00
  • c1bdfd37e7 Disable proof tester for regression. (#11741) Aina Niemetz 2025-03-14 09:37:44 -07:00
  • 8cbd5801a2 Refactor bound variable manager to use identifiers instead of attributes (#11588) Andrew Reynolds 2025-03-13 09:25:45 -05:00
  • 743eaf6a26 Fix type rule for nested lambda, add regression (#11735) Andrew Reynolds 2025-03-13 09:01:09 -05:00
  • 4c64a77188 Add proof elaboration for MultSltMult BV rewrite (#11732) Andrew Reynolds 2025-03-13 09:00:57 -05:00
  • dc24c31d19 moved code that builds the theorem index to a separate function (#11731) Kartik Sabharwal 2025-03-13 07:03:40 -05:00
  • 1f2237a388 cmake: Add JNI_HOME variable to specify the path to JNI libraries (#11733) Daniel Larraz 2025-03-13 07:03:01 -05:00
  • d79b39e1d9 Bump CaDiCaL to version 2.1.3. (#11716) Aina Niemetz 2025-03-12 16:19:35 -07:00
  • 057f782470 Use arith substitution context for case of congruence manager conflicts (#11708) Andrew Reynolds 2025-03-12 16:36:54 -05:00
  • 5ab6ba0146 Do not throw an assertion failure when arithmetic model construction fails and a lemma has been sent. (#11565) Andrew Reynolds 2025-03-12 15:42:27 -05:00
  • aba5d87156 Add proof elaboration for BV concat extract rule (#11728) Andrew Reynolds 2025-03-12 08:34:26 -05:00
  • 74e6fa46e5 Move bitblasting to its own file in Eunoia signature (#11729) Andrew Reynolds 2025-03-12 08:34:17 -05:00
  • 576182a814 strings: Refactor to not use NodeManager::currentNM() (#11717) Daniel Larraz 2025-03-11 10:40:47 -05:00
  • ea756fba69 Moved computation of relevant equivalence classes into a separate function (#11725) Kartik Sabharwal 2025-03-11 10:36:28 -05:00
  • eccd3138e8 Add elaboration for BV concat merge rules (#11727) Andrew Reynolds 2025-03-11 10:09:40 -05:00
  • fdce0c10f8 More updates to safe options (#11664) Andrew Reynolds 2025-03-10 15:01:48 -05:00
  • 4b5a5228c9 Minor fixes and improvements for CPC Eunoia signature (#11719) Andrew Reynolds 2025-03-10 14:52:28 -05:00
  • 8f8c70b813 Avoid deadlock in HO model construction (#11723) Andrew Reynolds 2025-03-10 14:52:18 -05:00
  • 94950d9ffb Add proof elaboration for And/Or/Xor simplify rules (#11720) Andrew Reynolds 2025-03-10 14:52:08 -05:00
  • 1cb2845027 Remove DT_CLASH proof rule (#11629) Andrew Reynolds 2025-03-07 15:15:29 -06:00
  • 3a8a70f1a7 Fix numeric overflow case in strings rewriter (#11713) Andrew Reynolds 2025-03-07 14:54:43 -06:00
  • 3f110c01e3 bv: Eliminate calls to NodeManager::currentNM() (#11712) Daniel Larraz 2025-03-07 14:40:00 -06:00
  • ff31255a0a Consolidate sets evaluation rules, implement in Eunoia (#11614) Andrew Reynolds 2025-03-06 21:00:28 -06:00
  • f97ed6871c Simple fixes for projects issues (#11714) Andrew Reynolds 2025-03-06 18:50:40 -06:00
  • c7d2d3cd7e Remove CONCAT_CONFLICT(_DEQ) rules (#11660) Andrew Reynolds 2025-03-06 18:36:52 -06:00
  • acff956c75 quantifiers: Eliminate calls to NodeManager::currentNM() (#11711) Daniel Larraz 2025-03-06 13:42:40 -06:00
  • de91651570 Add necessary BV rewrites (#11662) Andrew Reynolds 2025-03-06 12:31:46 -06:00
  • cb8ccdd850 Fix check for whether a regular expression is constant, guard cases of RegLan in constraints (#11705) Andrew Reynolds 2025-03-05 11:39:27 -06:00
  • 263e43431b Setup infrastructure for necessary BV macro rewrites (#11707) Andrew Reynolds 2025-03-05 09:44:56 -06:00
  • 704bd37d4c Add more regressions for proof holes (#11706) Andrew Reynolds 2025-03-05 09:42:58 -06:00
  • 03370423ce Fix JNI string conversion to handle Unicode surrogate pairs (#11693) Daniel Larraz 2025-03-04 14:29:35 -06:00
  • 0d835cc792 Print the result to the most recent solver's output stream (#11702) Daniel Larraz 2025-03-04 13:23:56 -06:00
  • 802460d5c4 Add proof elaboration for MACRO_BOOL_BV_INVERT_SOLVE (#11701) Andrew Reynolds 2025-03-04 09:38:50 -06:00
  • 8288af5a7a Address nondeterminism in quantifiers rewriter (#11700) Andrew Reynolds 2025-03-04 08:27:14 -06:00
  • 1539ae5777 Add proof rule ABSORB (#11637) Andrew Reynolds 2025-03-03 16:18:10 -06:00
  • 28c14d639e Improve warnings and errors for sygus-inference (#11690) Andrew Reynolds 2025-03-03 13:39:10 -06:00
  • 017310217a Improve recursion limit heuristic in RARE (#11683) Andrew Reynolds 2025-03-03 09:14:40 -06:00
  • ac0619882a Add regressions for more proof holes (#11663) Andrew Reynolds 2025-03-01 08:41:41 -06:00
  • 335a4e42fb Fix elaboration of MACRO_SR_PRED_TRANSFORM (#11688) Andrew Reynolds 2025-03-01 07:51:30 -06:00
  • f00cb40677 Add regressions for fixed issues. (#11697) Andrew Reynolds 2025-03-01 07:27:40 -06:00
  • 44b9ba8923 Add proof elaboration for MACRO_RE_INTER_UNION_CONST_ELIM (#11685) Andrew Reynolds 2025-03-01 07:27:28 -06:00
  • d287860e16 Add proof rewrite rule MACRO_BOOL_BV_INVERT_SOLVE (#11687) Andrew Reynolds 2025-03-01 07:26:45 -06:00
  • 0232cd8b9b Guard another case of expert extensions of arithmetic (#11686) Andrew Reynolds 2025-03-01 07:26:23 -06:00
  • 2f92bbac2c Take remaining minor changes to strings rewriter from proof branch (#11696) Andrew Reynolds 2025-03-01 07:21:09 -06:00
  • bbf701cf5b java: Remove reference to non-existent API function. (#11694) Aina Niemetz 2025-02-28 15:08:57 -08:00
  • 2668938bc8 cadical: Make modelValue more robust. (#11695) Aina Niemetz 2025-02-28 15:05:24 -08:00
  • 5e6dae4967 Guard another case where variable elimination is not equivalence preserving (#11633) Andrew Reynolds 2025-02-28 16:58:30 -06:00
  • 3ba0cf3947 cmake: Remove workaround that got addressed on CMS side. (#11692) Aina Niemetz 2025-02-28 14:38:39 -08:00
  • e1aecfbaa1 cmake: Introduce max version check for CaDiCaL. (#11691) Aina Niemetz 2025-02-27 17:06:54 -08:00
  • 06d065a604 theory_bv_utils: Refactor to not use NodeManager::currentNM() (#11617) Daniel Larraz 2025-02-27 16:12:25 -06:00
  • 685fa7d879 Only support datatype match if datatypesExp is true (#11444) Andrew Reynolds 2025-02-27 15:02:17 -06:00
  • 84d755c24b Eliminate use of LinearRewriteStrategy in cases where proofs can not be elaborated (#11656) Andrew Reynolds 2025-02-27 11:21:55 -06:00
  • d9d228f28e More fixes for LFSC + nightlies (#11684) Andrew Reynolds 2025-02-27 09:34:19 -06:00
  • fb7e904c5f Add proof elaboration for MACRO_STR_IN_RE_INCLUSION (#11680) Andrew Reynolds 2025-02-26 15:30:01 -06:00
  • ec4c6787a3 Disable LFSC on regression (#11682) Andrew Reynolds 2025-02-26 14:19:29 -06:00
  • e9704d4786 Add proof elaboration for MACRO_STR_CONST_NCTN_CONCAT (#11679) Andrew Reynolds 2025-02-26 12:58:04 -06:00
  • 3cf3f1ca0f Refactor RE inter/union rewriter, add macro rewrite for RE inter/union constant elimination (#11678) Andrew Reynolds 2025-02-26 12:57:54 -06:00