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

• c4e55cc959 Introduce MACRO_QUANT_DT_VAR_EXPAND and its elaboration (#11604) Andrew Reynolds 2025-02-26 12:55:07 -06:00
• 9826a0eb9f Add RARE rule for divisible (#11677) Andrew Reynolds 2025-02-26 09:39:00 -06:00
• 67595f8f24 Add macro and elaboration for MACRO_STR_COMPONENT_CTN (#11681) Andrew Reynolds 2025-02-26 09:07:32 -06:00
• 3b7111d98e Add getGeneralizedConstRegExp utility in RegExp entail (#11608) Andrew Reynolds 2025-02-25 08:57:56 -06:00
• 1596859935 Fix corner case of elaboration of quantifiers merge prenex (#11661) Andrew Reynolds 2025-02-25 07:29:03 -06:00
• 934876f9f2 Add regressions for fixed issues (#11671) Andrew Reynolds 2025-02-25 07:28:08 -06:00
• c67d35bb9a Add bitvector concat and xor to ACI_NORM (#11674) Andrew Reynolds 2025-02-25 07:27:56 -06:00
• ae3442bd5a ci: Use separate GitHub Action to set up CMake (#11673) Daniel Larraz 2025-02-24 14:08:43 -06:00
• 116c288082 Minor fix for quantifiers preprocessing pass (#11672) Andrew Reynolds 2025-02-24 13:06:48 -06:00
• 2e06222ce6 Miscellaneous changes from proof dev branch (#11668) Andrew Reynolds 2025-02-24 13:06:25 -06:00
• 9dbba0f1f6 Do not use array constants in sygus grammars unless arraysExp is true (#11655) Andrew Reynolds 2025-02-24 13:06:11 -06:00
• b936ead441 Add support for datatypes updater elimination rules in Eunoia (#11625) Andrew Reynolds 2025-02-24 10:35:19 -06:00
• 76b59f02cf separate function for debugging irrelevant eqc computation (#11669) Kartik Sabharwal 2025-02-24 08:57:13 -06:00
• e2d2cfd027 Small Cosmetic Changes to RARE rules (#11666) Lachnitt 2025-02-24 06:56:35 -08:00
• a69fba766a Do not purify ground Boolean subterms in quantifier bodies (#11654) Andrew Reynolds 2025-02-20 17:39:42 -06:00
• 0ab0f2de41 Add elaboration for MACRO_STR_EQ_LEN_UNIFY_PREFIX (#11658) Andrew Reynolds 2025-02-20 07:16:47 -06:00
• 348845e3f4 Documentation for OpArgIndex in conjecture generator (#11665) Kartik Sabharwal 2025-02-20 07:10:08 -06:00
• cecff59b21 Add proof rewrite rule SEQ_EVAL_OP (#11657) Andrew Reynolds 2025-02-20 06:52:46 -06:00
• a09cf821a0 Add elaboration for MACRO_STR_EQ_LEN_UNIFY (#11659) Andrew Reynolds 2025-02-20 06:14:22 -06:00
• 2dcbe617a3 Improvements and optimizations for Eunoia quantifiers signature (#11603) Andrew Reynolds 2025-02-19 20:41:50 -06:00
• d0e7209cba Fixes for BV RARE rules (#11642) Andrew Reynolds 2025-02-19 14:26:14 -06:00
• 228f749173 Add proof elaboration for string overlap macro rules (#11650) Andrew Reynolds 2025-02-19 13:34:48 -06:00
• 69ba034479 Simplifications to the core rules of the strings calculus (#11594) Andrew Reynolds 2025-02-19 07:42:36 -06:00
• 6eaadbc457 Add helper functions to proof elaborator (#11652) Andrew Reynolds 2025-02-19 07:38:46 -06:00
• 3759dab950 Simplify internal proof checker for strings to not splice constants (#11628) Andrew Reynolds 2025-02-18 14:01:28 -06:00
• 9de62f6490 Do not include expert Eunoia signature from main signature (#11653) Andrew Reynolds 2025-02-18 13:35:18 -06:00
• bb7099f532 Add distinct values to RARE reconstruction strategy (#11636) Andrew Reynolds 2025-02-18 13:04:01 -06:00
• 3e88ebd292 Move BV ppAssert to its own utility, add proofs (#11427) Andrew Reynolds 2025-02-18 11:37:03 -06:00
• 6983538ca4 arith: Refactor to not use NodeManager::currentNM() (#11496) Daniel Larraz 2025-02-18 10:53:16 -06:00
• ac2b8b8cae Fix several Eunoia rules for sequences (#11649) Andrew Reynolds 2025-02-18 06:59:04 -06:00
• 16d644be1a Add -o rare-db-expert, partition eo rewrite signatures (#11648) Andrew Reynolds 2025-02-18 06:58:49 -06:00
• 339a3047e7 Add macros for string contains split overlap rule (#11591) Andrew Reynolds 2025-02-18 06:58:25 -06:00
• 5efa79f7b9 Add Eunoia definition for ProofRewriteRule::DISTINCT_CARD_CONFLICT (#11638) Andrew Reynolds 2025-02-17 15:08:51 -06:00
• 72be5c8d2a Add macros for (non-splitting) string overlap rules (#11618) Andrew Reynolds 2025-02-17 10:17:37 -06:00
• 92e99e724d Add Eunoia signature defining translation from sequences to strings (#11612) Andrew Reynolds 2025-02-17 07:41:56 -06:00
• 10cc6d5a1c Add rewrite level (normal/expert for rewrite rules) (#11646) Leni Aniva 2025-02-17 05:39:28 -08:00
• 368a34f6f5 Moved computation of irrelevant equivalence classes to separate function (#11643) Kartik Sabharwal 2025-02-14 16:43:33 -06:00
• 9dbabd2939 fix type errors in proofs/eo/programs/Nary.eo (#11640) Ciarán Dunne 2025-02-14 20:57:45 +01:00
• 3ff8ea3332 Ensure only canonized terms are added to theorem index (#11635) Kartik Sabharwal 2025-02-14 10:26:19 -06:00
• 0311e55a5e Add macro rewrite MACRO_BV_EQ_SOLVE (#11466) Andrew Reynolds 2025-02-14 08:10:25 -06:00
• 9fc7fa51b6 Add regressions for proofs (#11634) Andrew Reynolds 2025-02-13 13:27:13 -06:00
• b4356ffab3 Add regressions for fixed issues (#11627) Andrew Reynolds 2025-02-13 11:28:54 -06:00
• af8e321d57 Miscellaneous refactoring of arithmetic RARE rewrites (#11478) Andrew Reynolds 2025-02-13 08:04:56 -06:00
• 25ab3e0b32 Generalize BV poly norm eq to odd coefficients (#11632) Andrew Reynolds 2025-02-13 06:38:58 -06:00
• ed4a464dc8 Simplify quantifiers variable elimination inequality rewrite (#11605) Andrew Reynolds 2025-02-13 06:15:43 -06:00
• 8cda341d39 Add unused variables to RARE preprocess tactic (#11467) Andrew Reynolds 2025-02-12 16:59:09 -06:00
• 8e2d145a34 Add remaining cases of STRING_REDUCTION in Eunoia (#11630) Andrew Reynolds 2025-02-12 13:18:09 -06:00
• 2f076ba049 Add ProofRule::DISTINCT_VALUES (#11596) Andrew Reynolds 2025-02-12 12:52:37 -06:00
• 584111c94f Split proof rules ARITH_POLY_NORM(_REL) to BV_POLY_NORM(_EQ) (#11609) Andrew Reynolds 2025-02-12 10:56:07 -06:00
• 669004e965 Add proof elaboration for diamonds preprocessing (#11447) Andrew Reynolds 2025-02-12 09:20:46 -06:00
• 53560b9d5a Fix documentation for transcendentals, make proof checker more pedantic (#11615) Andrew Reynolds 2025-02-12 09:04:37 -06:00
• 13f7a91cf3 Splice constants in strings infer proof cons (#11593) Andrew Reynolds 2025-02-12 08:21:02 -06:00
• 056ada583c Adding all Mbqi-Enum options and renaming the method from Mbqi-Fast-Sygus to Mbqi-Enum (#11592) Lydia Kondylidou 2025-02-12 14:20:35 +01:00
• 24b2d5a88a Split RARE rewrites for expert extensions to own files (#11619) Andrew Reynolds 2025-02-11 16:40:34 -06:00
• 9880318285 Add ProofRule::RE_CONCAT (#11600) Andrew Reynolds 2025-02-11 16:24:40 -06:00
• ed3f78c4cf NodeBuilder: Assert that NodeManagers match. (#11620) Aina Niemetz 2025-02-11 10:24:45 -08:00
• 1d83f8c62e Update policy on options exceptions (#11566) Andrew Reynolds 2025-02-11 10:32:48 -06:00
• 2ffe9f35f8 ci: Use the minimum required CMake version on Linux runners (#11595) Daniel Larraz 2025-02-11 10:28:32 -06:00
• fbf4750bf9 Guard more cases of constant arrays in assertions (#11602) Andrew Reynolds 2025-02-11 10:20:20 -06:00
• 2b3a4be025 Minor modifications to expert signature (#11611) Andrew Reynolds 2025-02-11 08:15:09 -06:00
• 637d166573 Handle more cases in arith string pred entail (#11610) Andrew Reynolds 2025-02-11 08:15:01 -06:00
• c5fd700538 Updates for string entail utility (#11607) Andrew Reynolds 2025-02-11 08:14:54 -06:00
• cbc0bd0391 Fix printer for user patterns and annotations (#11598) Andrew Reynolds 2025-02-11 08:14:44 -06:00
• b0cff1823e Add Eunoia definition for more cases of STRING_REDUCTION (#11587) Andrew Reynolds 2025-02-11 08:14:34 -06:00
• dbb3c25b73 bitblast_utils: Refactor to not use NodeManager::currentNM() (#11529) Daniel Larraz 2025-02-10 16:47:40 -06:00
• e067b5261b Make unit tests for proofs more robust wrt rewrite rules (#11601) Andrew Reynolds 2025-02-10 16:35:29 -06:00
• fb0b8e84d2 Update CPC signature and output to fully support parametric datatypes (#11577) Andrew Reynolds 2025-02-10 16:05:50 -06:00
• e59c1e4b49 [proofs] Remove eager check for SAT proof closedness (#11613) Haniel Barbosa 2025-02-10 17:09:24 -03:00
• b38c29b502 Add macros and elaboration for arithmetic integer relation rewrites (#11441) Andrew Reynolds 2025-02-10 11:00:58 -06:00
• 4fbf9edb04 Add more regressions demonstrating tricky proof cases (#11574) Andrew Reynolds 2025-02-10 10:13:39 -06:00
• c79e20ebf9 Add missing consts to iterator members (#11575) Eric Wieser 2025-02-10 15:29:28 +00:00
• f7d323c8ac Refactor proof post processor DSL to avoid subgoal tracking (#11442) Andrew Reynolds 2025-02-08 05:52:17 -06:00
• 4f3d959166 Add Eunoia definitions of ARITH_MULT_SIGN and ARITH_MULT_ABS_COMPARISION (#11497) Andrew Reynolds 2025-02-07 16:34:15 -06:00
• 87fd92a17f Two fixes for quantifiers prenex proofs (#11487) Andrew Reynolds 2025-02-07 16:13:14 -06:00
• 68363982f9 More updates to classifications of options (#11576) Andrew Reynolds 2025-02-06 11:12:17 -06:00
• 30bc237196 Make RE_INTER_UNION_INCLUSION a macro, elaborate to simpler version (#11590) Andrew Reynolds 2025-02-06 07:15:59 -06:00
• acd6995731 Add proof elaboration for MACRO_ARRAYS_NORMALIZE_OP (#11530) Andrew Reynolds 2025-02-05 14:17:36 -06:00
• f784f982f9 Simplify CPC and Eunoia definition of ARITH_POLY_NORM_REL (#11578) Andrew Reynolds 2025-02-05 13:49:09 -06:00
• 4953ad307f ci: Update Ubuntu runners to 22.04 (#11573) Daniel Larraz 2025-02-05 13:32:32 -06:00
• 70229a12a2 Add CPC and Eunoia definitions for string theory rewrites involving overlap reasoning (#11580) Andrew Reynolds 2025-02-05 07:26:35 -06:00
• fb422d0b28 Fix corner case in Eo signature for replace_re_all (#11585) Andrew Reynolds 2025-02-04 08:49:01 -06:00
• 89e01fcf4a Add more cases of STRING_REDUCTION in Eunoia (#11586) Andrew Reynolds 2025-02-04 08:11:06 -06:00
• 470bfc75a7 moved conjecture generator eqc collection code into new function (#11582) Kartik Sabharwal 2025-02-03 15:08:08 -06:00
• 93a6469ee1 Eunoia definition of arith BV conversions (#11584) Andrew Reynolds 2025-02-03 13:57:49 -06:00
• cbb647bdaa resolve dependency issues in rules/Uf.eo and programs/Nary.eo (#11543) Ciarán Dunne 2025-02-03 19:53:42 +01:00
• c1ad0f4fee Split expert portions of Cpc.eo to own subdirectory (#11583) Andrew Reynolds 2025-02-03 12:52:52 -06:00
• c638460810 Add proof support for arithmetic static learning (#11494) Andrew Reynolds 2025-02-03 09:55:07 -06:00
• 4180a07295 Add support for str.replace_all in evaluator (#11334) Andrew Reynolds 2025-02-03 09:12:31 -06:00
• a352c69d09 Add Eunoia definitions of extended RE evaluation (#11581) Andrew Reynolds 2025-02-03 08:33:36 -06:00
• 2469f18187 Merge branch 'topic/sync_upstream' into 'master' Piotr Trojanek 2025-02-03 00:14:29 +00:00
• 68bf6fb828 Add default proof logger to log cpc proofs (#11511) Andrew Reynolds 2025-01-31 08:24:20 -06:00
• eb6ccba668 Introduce a primative string utility Word::hasOverlap (#11579) Andrew Reynolds 2025-01-31 08:23:32 -06:00
• 4e155a029b Update references from CVC4 to CVC5 Piotr Trojanek 2025-01-31 11:02:31 +01:00
• 06150eba6c Remove old license file that is not present in CVC5 repository Piotr Trojanek 2025-01-31 11:01:56 +01:00
• 8cb6f1db8f Remove AdaCore build artefacts Piotr Trojanek 2025-01-31 11:01:24 +01:00
• 503cadf2ae Regression tests for the conjecture generator (#11519) Kartik Sabharwal 2025-01-30 13:50:46 -06:00
• 27e184d182 Demote more string rewrites to the extended rewriter (#11570) Andrew Reynolds 2025-01-28 15:31:36 -06:00
• fbed8f82c4 Use Cython's definition of libcpp.optional. (#11572) Robert Bradshaw 2025-01-28 09:29:20 -08:00
• c251365665 ci: Add option to choose the Python versions to build (#11571) Daniel Larraz 2025-01-28 10:41:52 -06:00
• 4007720dd4 ci: Add manual trigger for wheel publication (#11568) Daniel Larraz 2025-01-27 16:18:49 -06:00