Commit Graph

807 Commits

Author SHA1 Message Date
MyskYko 6e130c15a3 fix setnvars 2025-06-20 15:28:27 -07:00
MyskYko 9ea1aaa3cf fix comments 2025-06-20 14:45:50 -07:00
MyskYko a5156f257e fix cadical 2025-06-20 13:40:04 -07:00
Alan Mishchenko 692b0c6908 Printout of column multiplicity statistics. 2025-05-02 08:13:20 -07:00
Alan Mishchenko 1c2b935a77 Adding new feature to "lutexact". 2025-05-01 21:08:46 -07:00
Alan Mishchenko 6a031620fe Supporting random seed in "lutexact". 2025-04-30 12:10:22 -07:00
Alan Mishchenko e320888191 Adding structural guidance. 2025-03-19 12:14:28 -07:00
Alan Mishchenko e7dd9151b1 Adding structural guidance. 2025-03-18 17:51:40 -07:00
Alan Mishchenko 2078b3945b Adding support for the random seed to the recent experiments. 2025-03-18 07:55:28 -07:00
Alan Mishchenko 59a7cc5c9c Removing intermediate files in exact synthesis. 2025-03-17 17:12:01 -07:00
Alan Mishchenko 0ebc9dbbae Experiments with exact synthesis. 2025-03-16 09:39:04 -07:00
alanminko f058e15f87
Merge pull request #382 from MyskYko/cadical
CaDiCaL
2025-03-07 23:17:57 +07:00
alanminko 383c16b690
Merge pull request #380 from MyskYko/kissat
support debug mode
2025-03-07 23:17:44 +07:00
MyskYko 14b451b52f patch 2025-03-07 00:25:11 -08:00
MyskYko f544165a88 cadical original 2025-03-05 21:25:31 -08:00
MyskYko 8fb9fc5d0f add version 2025-03-05 21:19:39 -08:00
MyskYko f168f2f286 support debug mode 2025-03-05 20:25:40 -08:00
Alan Mishchenko 2126cb3ca1 Fixing a typo in Kissat integration. 2025-03-05 10:30:16 -08:00
Alan Mishchenko b9b8ff47e3 Adding programmable call to Kissat in command &kissat. 2025-03-05 08:26:28 -08:00
MyskYko 3f6171127a add license 2025-03-05 04:21:18 -08:00
MyskYko 664d285fcb patch 2025-03-05 04:10:49 -08:00
MyskYko a7476c65d8 kissat original 2025-03-04 17:39:59 -08:00
Alan Mishchenko f2e4ceb0e3 Update to "lutexact". 2024-11-10 19:12:40 -08:00
Alan Mishchenko c787e32f86 Adding postiive minterm count for random functions generated by "lutexact". 2024-11-05 22:01:07 -08:00
Alan Mishchenko 091ff4e7a9 Adding generation of random functions to "lutexact" 2024-11-05 19:23:04 -08:00
alanminko a239dd8c0b
Merge pull request #328 from heshpdx/master
Perf improvement in satsolver
2024-10-21 01:38:40 -07:00
Alan Mishchenko 2e3384390a Updating "lutexact" to run on symmetric functions. 2024-10-07 14:10:02 +07:00
Mahesh Madhav ad8f8a2aab Convert the other divide to a multiply 2024-09-03 04:48:07 +00:00
Mahesh Madhav cd711089d7 Perf improvement in satsolver
Switch one FP divide to an FP multiply (variable is constant).
Calculate ratio inside of verbosity clause, since that is where it is used.
2024-09-03 04:30:14 +00:00
Alan Mishchenko c2391686ea Adding BLIF dumping to "lutexact". 2024-08-13 20:03:18 -07:00
Alan Mishchenko 81fcf8494e Updating "lutexact" to support single-rail LUT cascade. 2024-08-12 16:26:55 -07:00
alanminko 0129b4c60a
Merge pull request #316 from YosysHQ/povik/yosyshq-commands
Pull command changes from YosysHQ fork
2024-08-08 14:59:31 -07:00
Martin Povišer 1383c76464 Pull YosysHQ read_cex/write_cex changes
See

 - YosysHQ/abc#19
 - YosysHQ/abc#16
 - commit 6234e18d
 - YosysHQ/abc#14
 - YosysHQ/abc#12
 - YosysHQ/abc#11

Co-authored-by: Jannis Harder <me@jix.one>
Co-authored-by: Claire Xenia Wolf <claire@clairexen.net>
Co-authored-by: Miodrag Milanovic <mmicko@gmail.com>
2024-08-07 15:46:43 +02:00
Martin Povišer 57c3bd36f2 Patch to support WASI builds
Co-authored-by: whitequark <whitequark@whitequark.org>
2024-08-07 14:49:13 +02:00
Robert O'Callahan e0a9c29e5a Instead of throwing C++ exceptions, just print an error message and abort
Many C++ projects forbid the use of exceptions. These are not recoverable
errors anyway, so just abort.
2024-08-06 17:51:15 +00:00
Robert O'Callahan 6c6260465e Make `lbool` explicitly signed
This avoids issues due to some platforms making `char` signed and others
unsigned. For example, currently the result of promoting `(lbool)-1` to `int`
can differ on different platforms. See
50ffa10848/lib/bill/bill/sat/interface/abc_bsat2.hpp (L156)
for an example of that.
2024-06-28 01:07:10 +00:00
Alan Mishchenko 8ec95e85c6 Bug fix. 2024-05-19 15:03:12 -07:00
Alan Mishchenko c64f927828 Various changes and bug fixes. 2024-05-19 14:47:18 -07:00
Alan Mishchenko 2c02ae89a0 Updating the previous commit. 2024-05-15 09:41:14 -07:00
Alan Mishchenko c906dfb748 Upgrading "twoexact" to read relations in an updated format. 2024-05-15 09:33:57 -07:00
Alan Mishchenko bc725b85de Bug fix in CNF generation for &glucose (three more places). 2024-04-15 20:29:38 -07:00
Alan Mishchenko 2d6b5c9adc Bug fix in CNF generation for &glucose. 2024-04-15 20:25:43 -07:00
Alan Mishchenko b0d2ff1c63 Exact synthesis using NAND-gates. 2024-03-24 00:10:08 +09:00
Allen Ho d87b1cd543 fixed some warnings in bsat2 2024-03-04 10:16:14 +08:00
Alan Mishchenko eb24d29777 More changes. 2024-03-02 17:10:30 -08:00
Alan Mishchenko b73f1030a6 More changes. 2024-03-02 17:03:42 -08:00
Alan Mishchenko b627aa7cb5 More changes. 2024-03-02 16:57:00 -08:00
Alan Mishchenko ce44eda85a More changes. 2024-03-02 16:46:09 -08:00
Alan Mishchenko f6f542c873 More changes to compile with namespaces. 2024-03-02 16:38:16 -08:00
Alan Mishchenko 4de4605836 More changees to compile new code with namespaces. 2024-03-02 16:31:41 -08:00