3907 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Alan Mishchenko	db36c65bce	Small changes in the usage message for &gla.	2017-02-23 14:12:56 -08:00
Alan Mishchenko	dd8cc7e9a2	Removing unused procedure.	2017-02-22 13:03:53 -08:00
Alan Mishchenko	53b1d46b8d	Remapping flops in '%pdra.	2017-02-21 22:20:03 -08:00
Alan Mishchenko	96ccd24e6e	Changes to Visual Studio project file to support 'pdra'.	2017-02-21 20:39:52 -08:00
Alan Mishchenko	0e9f8093c3	Merged in ysho/abc (pull request #59) ... added a new abstraction	2017-02-22 04:31:10 +00:00
Yen-Sheng Ho	fb2fbd70bd	clean up	2017-02-21 20:10:11 -08:00
Yen-Sheng Ho	01e6beea8e	clean up	2017-02-21 20:06:13 -08:00
Bruno Schmitt	9d46d84b27	Small tweak to rollback behavior.	2017-02-21 18:37:06 -03:00
Yen-Sheng Ho	c5e9506f5d	small tweaks in %pdra -p	2017-02-20 12:58:20 -08:00
Yen-Sheng Ho	9f43c84501	added options of checking and pushing to %pdra	2017-02-20 12:51:04 -08:00
Alan Mishchenko	ac1eb60db9	Experiments with SAT sweeping.	2017-02-20 12:32:32 -08:00
Yen-Sheng Ho	19510bd38e	added datastructure for %pdra options	2017-02-20 11:07:12 -08:00
Yen-Sheng Ho	222b3741a4	fixed time profiling in pdr	2017-02-20 10:13:18 -08:00
Yen-Sheng Ho	25ecc3d429	fixed a tricky bug: property should not be assumed true in the last frame	2017-02-19 19:57:44 -08:00
Yen-Sheng Ho	1a66a5823a	working on pdr with wla	2017-02-19 16:09:59 -08:00
Yen-Sheng Ho	2d1792040a	working on pdr with wla	2017-02-19 15:57:13 -08:00
Bruno Schmitt	68dd780635	Adding new command to reset Satoko. ... Small fixes in watching list data structure.	2017-02-19 15:34:21 -08:00
Alan Mishchenko	99fe7dfe29	Experiments with SAT sweeping.	2017-02-19 12:51:38 -08:00
Yen-Sheng Ho	2732cbc1ee	working on pdr with wla	2017-02-19 12:31:28 -08:00
Yen-Sheng Ho	840f5d1ca8	working on pdr with wla	2017-02-19 10:22:15 -08:00
Yen-Sheng Ho	6cf289dadd	working on pdr with wla	2017-02-19 09:55:58 -08:00
Yen-Sheng Ho	24fdcecb2d	started %pdra	2017-02-19 09:20:44 -08:00
Yen-Sheng Ho	fc0f3b8d0d	working on incremental pdr	2017-02-18 21:22:26 -08:00
Alan Mishchenko	27caed8dc8	Experiments with SAT sweeping.	2017-02-18 20:20:50 -08:00
Bruno Schmitt	3f0cb6318b	New function to retrieve polarity value of a variable.	2017-02-18 17:08:54 -08:00
Bruno Schmitt	ac409b3152	Bug fix in analyze_final method.	2017-02-18 15:24:56 -08:00
Yen-Sheng Ho	fdc0b471e5	working on incremental pdr	2017-02-18 14:38:08 -08:00
Alan Mishchenko	131c1613a4	Compiler warnings.	2017-02-18 14:29:04 -08:00
Alan Mishchenko	316238d484	Compiler warnings.	2017-02-18 14:26:31 -08:00
Alan Mishchenko	429f52ce15	Experiments with SAT sweeping.	2017-02-18 14:20:10 -08:00
Yen-Sheng Ho	b93a805129	copied some functions from pdr	2017-02-18 12:43:03 -08:00
Yen-Sheng Ho	91a0a0fc3b	copied pdr_mansolve	2017-02-18 10:28:16 -08:00
Yen-Sheng Ho	196b359183	started pdrIncr.c	2017-02-18 09:51:54 -08:00
Yen-Sheng Ho	16fda0bd24	added a simple example; edited hgignore	2017-02-18 09:10:45 -08:00
Yen-Sheng Ho	1d3ff5338a	added ipdr	2017-02-17 18:55:00 -08:00
Alan Mishchenko	bc010af4be	Promising modification of the generalization procedure in 'pdr'.	2017-02-17 14:10:32 -08:00
Alan Mishchenko	378af9d94f	Experiment with graph constuction using ZDDs.	2017-02-17 14:09:58 -08:00
Alan Mishchenko	6d6bf8740d	Fixing missing sat_solver APIs in 'iprove'.	2017-02-16 13:57:36 -08:00
Alan Mishchenko	632ca7ed11	Promising alternative of CEX minimization in 'pdr'.	2017-02-16 13:37:46 -08:00
Alan Mishchenko	61b665ac8d	Experiment with graph constuction using ZDDs.	2017-02-16 11:38:06 -08:00
Alan Mishchenko	408ce46815	Fixing memory leak in 'pdr'.	2017-02-16 10:28:39 -08:00
Alan Mishchenko	c7b68c5e3f	Promising modification of the generalization procedure in 'pdr'.	2017-02-16 10:03:34 -08:00
Alan Mishchenko	bcc6d2686f	Fixing missing sat_solver APIs in 'iprove'.	2017-02-15 19:12:47 -08:00
Bruno Schmitt	7811f1bb07	Merged alanmi/abc into default	2017-02-15 17:19:52 -08:00
Alan Mishchenko	ab387953ab	Word-level abstraction engine.	2017-02-15 17:16:19 -08:00
Bruno Schmitt	088aabc102	- Small changes to the watch lists behavior. ... - Implementation of bookmark, unbookmark and rollback procedures. - Minor changes.	2017-02-15 17:02:32 -08:00
Alan Mishchenko	cb1ab7030f	Experiments with simulation.	2017-02-14 20:26:43 -08:00
Bruno Schmitt	30037e0653	- Small bug fix in var activity (improve performance) ... - New implementation of watcher lists.	2017-02-14 14:43:44 -08:00
Alan Mishchenko	f4853496d7	Adding PDR with abstraction.	2017-02-13 01:02:03 -08:00
Alan Mishchenko	3fb058a355	Adding PDR with abstraction.	2017-02-11 22:48:20 -08:00