mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 01:46:39 +00:00
Code Activity
3834 commits 43 branches 51 tags 169 MiB
Commit graph

59 commits

Author SHA1 Message Date
unknown
42c7277ea8 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-23 12:09:51 -07:00
Nikolaj Bjorner
ee458fa601 revising pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-23 12:09:07 -07:00
unknown
b06c4d985e Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-23 10:58:28 -07:00
unknown
2b48092541 local sat solver change 
Signed-off-by: unknown <nbjorner@nikolaj-z.redmond.corp.microsoft.com>
 2015-08-23 10:58:12 -07:00
Nikolaj Bjorner
546a9b8f03 revising pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-23 10:53:39 -07:00
Nikolaj Bjorner
a78fc031bc adding facility to dump wcnf benchmarks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-21 07:26:49 -07:00
Nikolaj Bjorner
954e612188 redoing pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-20 18:09:43 -07:00
Nikolaj Bjorner
a9807878ea reworking pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-20 12:20:30 -07:00
Nikolaj Bjorner
e3cb0e2d8b reworking pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-20 12:06:27 -07:00
Nikolaj Bjorner
64bd62b17e fix gcc compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-16 11:56:04 +01:00
Nikolaj Bjorner
52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
nikolajbjorner
0d9f949ab2 Fix memory smash on double free of clauses 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
 2015-02-23 10:28:32 -08:00
Nikolaj Bjorner
8141dadc89 break on small cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-02-08 10:22:06 +01:00
Nikolaj Bjorner
761c7d9a40 adding annotation to logging to show number of columns and rows, adding dual propagation sketch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-25 04:01:18 -08:00
Nikolaj Bjorner
552cbd840f adding soft-assertions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-23 13:06:11 -08:00
Nikolaj Bjorner
f1d9228b94 fix bug in context push/pop for sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-20 16:30:46 -08:00
Nikolaj Bjorner
c706e91019 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 10:37:55 -07:00
Nikolaj Bjorner
db20b2502d try qx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-04 19:50:42 -07:00
Nikolaj Bjorner
6a3f75822d fix format bug (issue 126) and smaller nits in sat solver (const annotation, disable elimination of external or already elimianted variables) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-04 18:35:18 -07:00
Nikolaj Bjorner
60d7872cc8 adding simple BCE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-29 18:00:34 -07:00
Nikolaj Bjorner
08dcd51594 fix bugs in incremental operation of sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-27 12:04:54 -07:00
Nikolaj Bjorner
e57e5328ce configuration update to SAT solver on creation time. Adding random_seed to sat parameters to enable command-line and module mode to work at the level of sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 16:42:11 -07:00
Nikolaj Bjorner
73070585b8 fix bug in core generation in legacy core: it ignores complementary literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-14 13:06:01 -07:00
Nikolaj Bjorner
18b491eee0 fixes to maxres/mss 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-03 10:03:56 -07:00
Nikolaj Bjorner
b5bbf83847 update core generation to be partial, update maxres to use current model too 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-02 19:05:28 -07:00
Nikolaj Bjorner
83a7d1a658 adding options to maxres for experiments, include option to pretty print module parameters in smt2 style 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-30 11:46:29 -07:00
Nikolaj Bjorner
16bffab8fd add saner Shannon decomposition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-24 14:21:15 -07:00
Nikolaj Bjorner
aa695f6a6c improve incremental use of sat solver: carry over simplification threshold 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-24 12:47:57 -07:00
Nikolaj Bjorner
b596828d23 add DDNF based engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-21 18:04:46 -07:00
Nikolaj Bjorner
78c03ed835 fix crash on delete clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-19 19:36:15 -07:00
Nikolaj Bjorner
a47f3df703 fix bug in unsat core extraction in sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-18 23:43:51 -07:00
Nikolaj Bjorner
f748a03ac7 opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-16 22:31:54 -07:00
Nikolaj Bjorner
ddb9e6e8d4 fix flipper 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-15 18:30:06 -07:00
Nikolaj Bjorner
be1cceba34 fix scope and mus with user-scopes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-15 11:29:08 -07:00
Nikolaj Bjorner
ee1a1b1135 refactor sat/sls interface. Remove wpm2 and bvsls dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-15 10:40:44 -07:00
Nikolaj Bjorner
999db1e280 sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-13 01:22:45 -07:00
Nikolaj Bjorner
180b0d4ec9 add sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-12 19:24:31 -07:00
Nikolaj Bjorner
e832bdd257 fix bug in blocked clause elimination that was enabled for external variables, fix other bugs in maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-10 21:23:05 -07:00
Nikolaj Bjorner
8814ba0629 testing maxres with sat core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-02 12:27:57 -07:00
Nikolaj Bjorner
b928734348 perf improvements, mus 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-01 16:11:52 -07:00
Nikolaj Bjorner
39414d8b8d testing inc_sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-31 22:29:47 -07:00
Nikolaj Bjorner
365f05b41a testing inc-sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-30 17:49:51 -07:00
Nikolaj Bjorner
bfc0af7820 testing inc-sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-30 16:35:46 -07:00
Nikolaj Bjorner
4f0de9a0cf implement user scopes for sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-30 09:27:03 -07:00
Nikolaj Bjorner
2b1af8fd50 updated sat solver for cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-29 14:38:17 -07:00
Nikolaj Bjorner
0e9511b597 unsat core for SAT solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-29 08:39:34 -07:00
Nikolaj Bjorner
66f626b50e local changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-29 07:41:08 -07:00
Nikolaj Bjorner
e98acf4ece working on adding basic cores to efficient SAT solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-29 07:22:59 -07:00
Nikolaj Bjorner
0c750bc714 update sat solver signature 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-28 12:19:46 -07:00
Nikolaj Bjorner
5427964c54 use approximate hitting set implementation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-14 14:08:55 -07:00