Claire Wolf
65a3ff69bd
Improve ezsat onehot encoding scheme
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-04-02 12:22:28 +02:00
Claire Wolf
f72b65b2a5
Using LFSR counter for ezSAT::manyhot()
...
The only user of this API right now is the puzzle3d benchmark and
it sees a slight reduction in CNF size from this, but the performance
difference is within the noise of measurement on my system.
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-04-02 11:37:12 +02:00
Clifford Wolf
0d7fd2585e
Added "int ceil_log2(int)" function
2016-02-13 16:52:16 +01:00
Clifford Wolf
6c84341f22
Fixed trailing whitespaces
2015-07-02 11:14:30 +02:00
Clifford Wolf
2a9ad48eb6
Added ENABLE_NDEBUG makefile options
2015-01-24 12:16:46 +01:00
Clifford Wolf
29a555ec7e
Added statehash to ezSAT
2014-12-29 17:10:37 +01:00
Clifford Wolf
84ffe04075
Fixed various VS warnings
2014-10-18 15:20:38 +02:00
Clifford Wolf
b3a6f8f530
More win32 (mxe and vs) build fixes
2014-10-17 16:04:59 +02:00
Clifford Wolf
7df8cbe2a9
Not using std::to_string in ezsat (problems with mingw)
2014-10-11 10:46:50 +02:00
Clifford Wolf
7cb0d3aa1a
Renamed TRUE/FALSE to CONST_TRUE/CONST_FALSE because of name collision on Win32
2014-10-10 17:07:24 +02:00
Clifford Wolf
9b566a7efa
Added native support for shift operations to ezSAT
2014-07-30 18:37:17 +02:00
Clifford Wolf
b1d520949b
Added ezSAT::keep_cnf() and ezSAT::non_incremental()
2014-07-21 02:01:32 +02:00
Clifford Wolf
91704a7853
Merged a few fixes for non-posix systems from github.com/Siesh1oo/yosys
...
(see https://github.com/cliffordwolf/yosys/pull/28 )
2014-03-11 14:24:24 +01:00
Clifford Wolf
d5bd93997c
ezSAT: Added frozen_literal() API
2014-03-03 02:13:17 +01:00
Clifford Wolf
895e9fc70c
ezSAT: Fixed handling of eliminated Literals, added auto-freeze for expressions
2014-03-03 02:12:45 +01:00
Clifford Wolf
d500bd749f
Added ezSAT::eliminated API to help the SAT solver remember eliminated variables
2014-03-01 21:00:34 +01:00
Clifford Wolf
23f0a12c72
ezSAT bugfix: don't call virtual methods in base class constructor
2014-03-01 20:59:00 +01:00
Clifford Wolf
edc2146056
Removed ezSAT::assumed() API
2014-03-01 20:55:06 +01:00
Clifford Wolf
e3debea4e6
Removed ezSAT built-in brute-froce solver
2014-03-01 20:53:09 +01:00
Clifford Wolf
dab1612f81
Added support for Minisat::SimpSolver + ezSAT frezze() API
2014-02-23 01:35:59 +01:00
Clifford Wolf
61a2bf57b4
Improved non-verbose ezSAT::printDIMACS() format
2014-02-18 09:25:41 +01:00
Clifford Wolf
11e8118589
Added ezsat vec_const() api
2013-11-25 15:10:32 +01:00
Clifford Wolf
457dc09cdc
Added ezsat api for creation of anonymous vectors
2013-08-15 14:40:26 +02:00
Clifford Wolf
ccf36cb7d8
Added SAT support for $div and $mod cells
2013-08-11 16:27:15 +02:00
Clifford Wolf
8fbb5b6240
Added timout functionality to SAT solver
2013-06-20 12:49:10 +02:00
Clifford Wolf
1bee82ae2d
Fixed gcc build (c++11 stuff in ezSAT)
2013-06-12 10:18:01 +02:00
Clifford Wolf
25ae2d4df0
Fixes and improvements in ezSAT library
2013-06-08 12:14:20 +02:00
Clifford Wolf
56b593b91c
Improved sat generator and sat_solve pass
2013-06-07 14:37:33 +02:00
Clifford Wolf
3371563f2f
Added ezSAT library
2013-06-07 10:38:35 +02:00