Alan Mishchenko
|
81b70c4d20
|
Corner-case bug fix in 'satclp' with conflict limit.
|
2016-03-25 13:51:05 -07:00 |
Alan Mishchenko
|
73cbe319ff
|
Bug fix in &fftest: not outputting test patterns when user test patterns are given.
|
2016-03-09 09:28:31 +09:00 |
Alan Mishchenko
|
67f4f1adae
|
Experiments with SAT-based mapping.
|
2016-02-07 21:13:33 -08:00 |
Alan Mishchenko
|
4ecf43f1f0
|
Adding a way to derive cardinality constraint as a sorting network.
|
2016-01-13 20:32:26 -08:00 |
Alan Mishchenko
|
8dd31fb4a9
|
Integrating new CNF generation into &bmc.
|
2016-01-12 22:07:01 -08:00 |
Alan Mishchenko
|
1bbf239843
|
Experiments with SAT-based mapping.
|
2016-01-10 21:04:17 -08:00 |
Alan Mishchenko
|
d6178631be
|
Adding support of candinality clause to the SAT solver.
|
2016-01-10 10:19:26 -08:00 |
Alan Mishchenko
|
19e4604b1f
|
Improvements to 'satclp'.
|
2015-11-09 09:23:39 -08:00 |
Alan Mishchenko
|
58c2584e2a
|
Improvements to 'satclp'.
|
2015-11-09 08:33:56 -08:00 |
Alan Mishchenko
|
e50fc467fd
|
Improvements to 'satclp' (unfinished).
|
2015-11-06 13:49:23 -08:00 |
Alan Mishchenko
|
dd365cbaf3
|
Improvements to 'satclp' (unfinished).
|
2015-11-06 09:05:17 -08:00 |
Alan Mishchenko
|
9521d1345b
|
Improvements to 'satclp'.
|
2015-10-28 13:44:29 -07:00 |
Alan Mishchenko
|
701565eb7b
|
Set the default cube limit in 'satclp' to be 0.
|
2015-10-23 15:44:53 -07:00 |
Alan Mishchenko
|
ea7b813638
|
Quality improvement in 'satclp'.
|
2015-10-22 16:50:02 -07:00 |
Alan Mishchenko
|
1332dc419f
|
Minor tuning in 'satclp'.
|
2015-10-22 11:45:23 -07:00 |
Alan Mishchenko
|
17718a4c7d
|
Corner case bug in 'satclp'.
|
2015-10-21 20:47:47 -07:00 |
Alan Mishchenko
|
ce232aca4e
|
Code inserts to profile runtime of 'satclp'.
|
2015-10-21 12:26:43 -07:00 |
Alan Mishchenko
|
9faaf802f7
|
Additional improvements in 'satclp'.
|
2015-10-18 15:26:23 -07:00 |
Alan Mishchenko
|
69df5462cb
|
Additional improvements in 'satclp'.
|
2015-10-18 15:24:12 -07:00 |
Alan Mishchenko
|
edf3144543
|
Added approximate SAT-based irredundant procedure to 'satclp'.
|
2015-10-17 12:31:22 -07:00 |
Alan Mishchenko
|
8093611068
|
Added comment how to print binary clauses in procedure Sat_SolverWriteDimacs().
|
2015-10-16 19:54:28 -07:00 |
Alan Mishchenko
|
17cbe3567e
|
Bug fix in 'satclp -r'.
|
2015-10-16 19:45:25 -07:00 |
Alan Mishchenko
|
a2692b70fb
|
New switch 'satclp -r' to reverse variable order.
|
2015-10-07 17:35:36 -07:00 |
Alan Mishchenko
|
f06ca216ab
|
Tuning SAT solver for QBF instances.
|
2015-09-18 09:05:27 -07:00 |
Alan Mishchenko
|
fdf00d8044
|
Tuning SAT solver for QBF instances.
|
2015-09-18 08:38:53 -07:00 |
Alan Mishchenko
|
3b838b953d
|
Tuning SAT solver for QBF instances.
|
2015-09-18 08:10:18 -07:00 |
Alan Mishchenko
|
b11344b454
|
Experiments with SAT-based collapsing.
|
2015-09-04 15:40:53 -07:00 |
Alan Mishchenko
|
a207f6c071
|
Experiments with SAT-based collapsing.
|
2015-09-04 11:52:27 -07:00 |
Alan Mishchenko
|
1ffd9aad76
|
Experiments with SAT-based collapsing.
|
2015-09-03 21:57:21 -07:00 |
Alan Mishchenko
|
5bcde4be2b
|
Experiments with SAT-based collapsing.
|
2015-09-03 21:56:29 -07:00 |
Alan Mishchenko
|
af828a499d
|
Removing unhelpful assertion in CEX minimization.
|
2015-09-01 12:02:44 -07:00 |
Alan Mishchenko
|
f7939ee6b1
|
Merging two threads.
|
2015-05-25 18:23:51 -07:00 |
Alan Mishchenko
|
a39ef30708
|
Procedure for extending care CEX to all objects.
|
2015-05-14 09:34:20 -07:00 |
Alan Mishchenko
|
3e1c831b2d
|
Bug fix in QBF solver.
|
2015-05-04 17:42:19 -07:00 |
Alan Mishchenko
|
bc6c0837a1
|
Adding support for dumping faults not detected by a given test-set in &fftest (switch -n).
|
2015-04-17 17:00:31 +09:00 |
Alan Mishchenko
|
b1aabead5d
|
Bug fix in &satfx.
|
2015-04-17 11:04:14 +09:00 |
Alan Mishchenko
|
cd4807ea04
|
Adding support for cardinality constraints in &fftest (switches -K and -k).
|
2015-04-16 20:58:23 +09:00 |
Alan Mishchenko
|
e85d29663a
|
Adding switch &fftest -e to dump delay-tests in a special format.
|
2015-04-15 08:13:38 +09:00 |
Alan Mishchenko
|
5c840d88f9
|
Adding switch &fftest -e to dump delay-tests in a special format.
|
2015-04-14 19:46:44 +09:00 |
Alan Mishchenko
|
03cd22af6e
|
Typo in hash function.
|
2015-04-02 15:31:48 +07:00 |
Alan Mishchenko
|
57a6f016d2
|
Compiler warning.
|
2015-04-01 15:46:25 +07:00 |
Alan Mishchenko
|
9cee436686
|
Added backward flop order to &icheck (switch -b).
|
2015-04-01 15:36:23 +07:00 |
Alan Mishchenko
|
6f598455bc
|
Updating command &satfx.
|
2015-03-31 16:27:07 +07:00 |
Alan Mishchenko
|
1e757a8567
|
Adding flop-input-only switch -f in &fftest for '-S str'.
|
2015-03-16 10:37:34 +07:00 |
Alan Mishchenko
|
1451e4551c
|
Adding flop-input-only switch -f in &fftest.
|
2015-03-14 16:32:21 +07:00 |
Alan Mishchenko
|
dc92f89278
|
Adding silent mode to &splitprove.
|
2015-03-14 03:13:05 +07:00 |
Alan Mishchenko
|
9e4f8e9fdf
|
Experiments with SAT-based cube enumeration.
|
2015-03-06 11:01:18 -08:00 |
Alan Mishchenko
|
241b042fda
|
Experiments with SAT-based cube enumeration.
|
2015-03-05 23:03:59 -08:00 |
Alan Mishchenko
|
1961f1791d
|
Experiments with SAT-based cube enumeration.
|
2015-03-05 23:02:15 -08:00 |
Alan Mishchenko
|
6da21b8b88
|
Experiments with SAT-based cube enumeration.
|
2015-03-05 23:00:30 -08:00 |