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

• 83e92c2e95 Add several new RARE rules for strings (#11514) Andrew Reynolds 2025-01-27 14:39:50 -06:00
• ed15af848c More preparation for eliminating nested calls to rewriter in strings rewriter (#11556) Andrew Reynolds 2025-01-27 14:05:37 -06:00
• 856c95b6c4 Start post-release for 1.2.1 Aina Niemetz 2025-01-27 11:51:09 -08:00
• dc565d9166 Bump version to 1.2.1 Aina Niemetz 2025-01-27 11:51:09 -08:00
• 4b5fd035ee Update NEWS for release 1.2.1. Aina Niemetz 2025-01-27 11:50:11 -08:00
• 929f2ac4e9 Update the list of build types (#11558) Daniel Larraz 2025-01-24 16:57:19 -06:00
• c009346d81 Disable unstable regression (#11567) Andrew Reynolds 2025-01-24 12:12:17 -06:00
• 027209030b Another fix for LFSC (#11564) Andrew Reynolds 2025-01-24 09:23:20 -06:00
• debd56cfb1 Preparation for 1.2.1 release (#11554) Andrew Reynolds 2025-01-24 08:17:11 -06:00
• 7bb90aeba7 Simplifications and improvements for ARITH_MULT_SIGN (#11476) Andrew Reynolds 2025-01-23 18:51:58 -06:00
• f704d716ed Minor fix to NEWS. (#11563) Mathias Preiner 2025-01-23 14:33:38 -08:00
• d9012b5dfc java: Change search order for native libraries (#11560) Daniel Larraz 2025-01-23 14:00:28 -06:00
• 42a1e0f1f2 Catch cases where list terms are used with illegal kinds in RARE rules (#11477) Andrew Reynolds 2025-01-23 13:40:54 -06:00
• 0647c4c107 Update copyright headers. (#11561) Aina Niemetz 2025-01-23 09:54:20 -08:00
• dbb62bdcce Fix corner case in lfsc node conversion (#11562) Andrew Reynolds 2025-01-23 10:34:34 -06:00
• d7b3320e4b Further restrictions on theory rewriters related to safe options (#11523) Andrew Reynolds 2025-01-22 17:58:45 -06:00
• 459f7207dd [alethe] Remove deleted option from contrib script (#11553) Haniel Barbosa 2025-01-22 20:24:53 -03:00
• 50960651f1 ci: Use GHA-native Linux arm64 runners (#11546) Daniel Larraz 2025-01-22 15:52:43 -06:00
• aa396e1ae8 Update NEWS. (#11557) Aina Niemetz 2025-01-22 12:58:31 -08:00
• 8babd81adb Make constant arrays require array-exp (#11534) Andrew Reynolds 2025-01-22 14:25:39 -06:00
• 77d053a9a4 Ensure lemmas from static learning are rewritten (#11545) Andrew Reynolds 2025-01-22 14:25:23 -06:00
• d10caa9f53 Clarify misleading wording in bug report template (#11551) Daniel Larraz 2025-01-22 14:21:13 -06:00
• 3ba9fcfddd doc: Explain how to use self-contained Java API JAR (#11555) Daniel Larraz 2025-01-22 11:42:49 -06:00
• ec3e7db5cf Add more regressions demonstrating proof holes (#11531) Andrew Reynolds 2025-01-22 11:27:27 -06:00
• 7d2c4ddf05 Reject duplicate variables in define-fun(-rec) (#11507) Andrew Reynolds 2025-01-22 11:15:36 -06:00
• fe6fa214a7 Change syntax for const/var in cpc proofs (#11512) Andrew Reynolds 2025-01-22 10:31:15 -06:00
• 3dedbd0d3a More fixes and improvements for strings infer proof cons (#11552) Andrew Reynolds 2025-01-22 08:25:44 -06:00
• cf0731b72a Add Eunoia definition of QUANT_DT_SPLIT (#11547) Andrew Reynolds 2025-01-22 08:25:36 -06:00
• c72f0d7463 Add more cases of EVALUATE for string operators in Eunoia (#11548) Andrew Reynolds 2025-01-22 08:25:26 -06:00
• 3197845f2d Fix case of collect model info in strings related to cardinality (#11544) Andrew Reynolds 2025-01-22 08:25:16 -06:00
• 5a85c4c3f4 Simplify the behavior of the arithmetic entail utility in strings (#11538) Andrew Reynolds 2025-01-22 08:23:14 -06:00
• 314f57fbaa Do not set dag-thresh to 0 when printing unsat cores (#11549) Andrew Reynolds 2025-01-21 14:49:40 -06:00
• 0eb61b1a8b Add macro rule for capture avoidance in beta redexes and its elaboration (#11513) Andrew Reynolds 2025-01-21 12:32:09 -06:00
• bfe648c1c0 Fix theory mismatch in expand definitions (#11532) Andrew Reynolds 2025-01-21 11:37:40 -06:00
• de69dae26b More updates to safe options (#11539) Andrew Reynolds 2025-01-21 07:49:42 -06:00
• 9acaebc501 Fixes and improvements for datatypes proof constructor (#11533) Andrew Reynolds 2025-01-20 11:30:10 -06:00
• a57cdee6dd Add option to disallow overloading of terms and sorts (#11493) Andrew Reynolds 2025-01-20 11:28:50 -06:00
• 5e0571822d Disable cpc on regression (#11541) Andrew Reynolds 2025-01-20 11:26:31 -06:00
• 6e836339b4 Refactor congruence proof rules (#11501) Andrew Reynolds 2025-01-17 14:11:39 -06:00
• ca078a520e Add three new ad-hoc rewrites for strings (#11429) Andrew Reynolds 2025-01-16 08:16:09 -06:00
• 3de6b613f0 Ensure trust id for solve-int-as-real (#11524) Andrew Reynolds 2025-01-15 16:07:42 -06:00
• 7da71b911f ci: Test Python wheels after build (#11527) Daniel Larraz 2025-01-15 14:21:13 -06:00
• 6e346afbbc proof_node_to_sexpr: Refactor to not use NodeManager::currentNM() (#11528) Daniel Larraz 2025-01-15 13:27:18 -06:00
• 32b5a54391 Eagerly apply-subs + rewrite bodies of define-fun (#11526) Andrew Reynolds 2025-01-15 12:46:51 -06:00
• df72e72ae5 Add new skolem ids for proof rules involving witness terms (#11479) Andrew Reynolds 2025-01-15 11:43:16 -06:00
• c27f5d6fc4 Add elaboration for remaining case of macro-dt-cons-eq (#11521) Andrew Reynolds 2025-01-15 08:27:25 -06:00
• a7d486f750 List theories in check model failures (#11525) Andrew Reynolds 2025-01-15 08:27:07 -06:00
• 8dca52eb78 booleans/builtin: Refactor to not use NodeManager::currentNM() (#11522) Daniel Larraz 2025-01-14 15:51:29 -06:00
• ea7a520f73 Keep platform-dependent python extension filename (#11516) Daniel Larraz 2025-01-14 14:32:53 -06:00
• 95b00b0e32 Add 3 macro theory rewrites and a theory rewrite for sets (#11491) Andrew Reynolds 2025-01-14 08:10:07 -06:00
• a1cb851a5a Add proof rules for extended operators regex evaluation (#11483) Andrew Reynolds 2025-01-14 08:09:44 -06:00
• b037d86343 Add more regressions that demonstrate proof holes (#11515) Andrew Reynolds 2025-01-13 14:56:54 -06:00
• b0bc521149 Define EVALUATE for more string operators in Eunoia (#11518) Andrew Reynolds 2025-01-13 14:47:52 -06:00
• a7e17dc81c Define EVALUATE for more BV operators in Eunoia (#11517) Andrew Reynolds 2025-01-13 14:24:41 -06:00
• 7e35f0be1a Add Eunoia definitions for 3 datatypes proof rules (#11510) Andrew Reynolds 2025-01-12 09:09:03 -06:00
• 8e2a929270 Quick regression tests for structural induction on datatypes (#11473) Kartik Sabharwal 2025-01-12 20:38:49 +05:30
• 6f74a53167 More cases and fixes for strings infer proof constructor (#11508) Andrew Reynolds 2025-01-11 08:22:17 -06:00
• 809af1833f Move several string rewrites to extended rewrites (#11509) Andrew Reynolds 2025-01-11 08:16:09 -06:00
• 53c1300dd1 Eliminate nested call to rewriter for beta reduction, generalize ProofRule::BETA_REDUCE (#11329) Andrew Reynolds 2025-01-10 14:24:58 -06:00
• 4704b1cc4c ci: Provide project description for the PyPI packages (#11506) Daniel Larraz 2025-01-10 13:01:01 -06:00
• 5572abe4ff Setup callbacks to proof logging (#11445) Andrew Reynolds 2025-01-10 11:33:26 -06:00
• a124e79221 Add macro rewrite and RARE rewrite for arrays (#11484) Andrew Reynolds 2025-01-10 10:29:38 -06:00
• 6b59bd4d04 Miscelleanous minor changes related to proofs (#11475) Andrew Reynolds 2025-01-10 09:19:05 -06:00
• 32f56be420 Add trust proof generator utility (#11474) Andrew Reynolds 2025-01-10 09:02:30 -06:00
• 7edc7bb3a1 ci: Update cibuildwheel to v2.22.0 (#11505) Daniel Larraz 2025-01-09 14:23:38 -06:00
• de906bb6d0 Simplifications and fixes for strings infer proof cons (#11452) Andrew Reynolds 2025-01-09 13:12:22 -06:00
• 0e9bd6014d Minor fixes for Eunoia signature and output (#11503) Andrew Reynolds 2025-01-09 10:56:50 -06:00
• 21dea2a435 Make RE derive conflicts an expert option (#11504) Andrew Reynolds 2025-01-09 10:55:48 -06:00
• e7fa55f6f3 Add several regressions that currently generate new kinds of holes in proofs (#11486) Andrew Reynolds 2025-01-09 10:54:32 -06:00
• 5f55821d84 strings: Refactor to not use NodeManager::currentNM() (#11499) Daniel Larraz 2025-01-08 18:46:08 -06:00
• deb28addc7 Remove nested rewrite calls during preRewrite from arrays rewriter (#11402) Andrew Reynolds 2025-01-08 12:55:57 -06:00
• 054632c10a Fix updated re consume (#11500) Andrew Reynolds 2025-01-08 11:47:29 -06:00
• 27b80a17b0 More missing cases of EVALUATE in CPC+Eunoia (#11492) Andrew Reynolds 2025-01-08 10:42:49 -06:00
• ff422314df bags/quantifiers: Refactor to not use NodeManager::currentNM() (#11498) Daniel Larraz 2025-01-07 18:16:38 -06:00
• 9931a9bc4d Fix possible invalid model construction in datatypes (#11426) Andrew Reynolds 2025-01-07 14:39:05 -06:00
• 37d94a45b1 Add a 'safe' build profile that enables safe-options by default (#11434) Daniel Larraz 2025-01-07 13:48:28 -06:00
• 0eb0668694 Simplify interface for ppAssert (#11401) Andrew Reynolds 2025-01-07 11:57:47 -06:00
• a991790c39 Explicitly add nl-cov to regressions that require it (#11482) Andrew Reynolds 2025-01-07 11:08:04 -06:00
• 96737cb19b Make arith static learning compatible with proofs and unsat cores (#11382) Andrew Reynolds 2025-01-07 10:32:11 -06:00
• baf4c8fa56 Fixes for ARITH_MULT_ABS_COMPARISON (#11462) Andrew Reynolds 2025-01-06 16:36:18 -06:00
• d7a5f90822 Initialize the rewriter based on safe-options (#11300) Andrew Reynolds 2025-01-06 15:08:09 -06:00
• e065d981e1 Reorganize final proof callback (#11424) Andrew Reynolds 2025-01-06 14:11:40 -06:00
• f3fc80e362 Fix regex consume for star (#11489) Andrew Reynolds 2025-01-05 09:11:18 -06:00
• bb815cf968 Extend regex consume rewrite to incorporate star (#11480) Andrew Reynolds 2025-01-03 11:51:24 -06:00
• 00c276d729 Fix bug in sygus solver for trivially infeasible conjectures (#11481) Andrew Reynolds 2025-01-02 15:09:43 -06:00
• 0d26ecc489 Disable timeout regression (#11470) Andrew Reynolds 2024-12-23 10:04:11 -06:00
• 53b33b8670 Fix LFSC in nightlies (#11468) Andrew Reynolds 2024-12-21 12:45:40 -06:00
• 14e8532a39 Make TrustId::THEORY_INFERENCE theory specific (#11425) Andrew Reynolds 2024-12-20 14:30:22 -06:00
• 96a35d7cc9 Do not rewrite datatype inferences prior to proof reconstruction (#11465) Andrew Reynolds 2024-12-20 13:34:40 -06:00
• 5ee60a5f28 Do not print BITVECTOR_EAGER_ATOM in cpc proofs (#11377) Andrew Reynolds 2024-12-20 11:37:41 -06:00
• dede2eaf5f Minor fixes for printers (#11430) Andrew Reynolds 2024-12-20 11:36:32 -06:00
• b47cbd4079 Fix issues with shared selectors in proofs (#11415) Andrew Reynolds 2024-12-20 11:04:26 -06:00
• b0382ba12a Add proof support for quantifiers term indexing conflicts (#11454) Andrew Reynolds 2024-12-20 10:12:13 -06:00
• cbbeb5158e Only try to use basic rewriter to automatically reconstruct trust steps (#11388) Andrew Reynolds 2024-12-20 08:32:02 -06:00
• b76c2b5f1d Disable lfsc tester on t3_rw903 (#11464) Daniel Larraz 2024-12-19 13:54:23 -06:00
• da255fd537 preprocessing/proof: Refactor to not use NodeManager::currentNM() (#11459) Daniel Larraz 2024-12-18 11:58:21 -06:00
• d9249b35a6 Make DT_CONS_EQ macro, elaborate to simpler version (#11420) Andrew Reynolds 2024-12-18 11:02:13 -06:00
• f102069ee7 Several fixes for quantifiers rewrite proofs (#11456) Andrew Reynolds 2024-12-18 10:09:32 -06:00
• 6c1b9d26ca Disable unsat-core tester on t3_rw903 (#11458) Daniel Larraz 2024-12-18 10:08:00 -06:00
• 13c3d2c456 Eliminate more calls to NodeManager::{currentNM,getSkolemManager} (#11457) Daniel Larraz 2024-12-18 08:45:27 -06:00