mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
4419 commits 49 branches 53 tags 182 MiB
Commit graph

328 commits

Author SHA1 Message Date
Nikolaj Bjorner
d6de73a2d1 fix model converter in inliner. Bug reported by Sagar Chaki 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-06 18:11:57 +02:00
Nikolaj Bjorner
3533a09010 bit2bool bug reported by Sagar Chaki 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-02 23:48:49 +02:00
Nikolaj Bjorner
7fbe7124f9 bugfixes to hsmax 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-14 17:29:53 -07:00
Nikolaj Bjorner
960e8ea1d5 working on hitting sets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-08 14:12:54 +01:00
Nikolaj Bjorner
4415df3fcf various fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-02 19:10:20 +05:30
Nikolaj Bjorner
aba79802cf fix warning about unused variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-25 21:01:10 -07:00
Ken McMillan
aa35149700 merging duality/interp changes 2014-05-22 11:52:16 -07:00
Ken McMillan
b91cca8db9 fix unbound variables bug in duality_dl_interface 2014-05-20 15:10:16 -07:00
Nikolaj Bjorner
e3098b0ec5 add documentation comment to bind_variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-20 11:20:15 -07:00
Nikolaj Bjorner
2ca14b49fe fix AV in debug assertion, address warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-16 09:45:32 -07:00
Nikolaj Bjorner
3e1b9876db fix bug in model generation for COI filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-15 17:54:54 -07:00
Ken McMillan
a4f3afd70d added fixedpoint.conjecture_file option 2014-05-05 14:29:54 -07:00
Ken McMillan
f7d589fc49 changed fixedpoint output format for easier parsing in Boogie 2014-04-10 17:53:00 -07:00
Nikolaj Bjorner
8d23b2b813 speed up parsing of large Datalog files, remove pinned 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-28 18:26:42 -07:00
Nikolaj Bjorner
3d7f208ce6 add bvsls module as backend to weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-28 13:32:31 -07:00
Christoph M. Wintersteiger
3ab1766588 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt 2014-03-27 13:13:10 +00:00
Ken McMillan
732035bf63 merge interp/duality changes with unstable 2014-03-26 14:48:04 -07:00
Nikolaj Bjorner
88df909a6c merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-20 14:09:18 -07:00
Nikolaj Bjorner
a9e8045071 fix bug reported by Nuno Lopes when query gets sliced 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-19 20:23:54 -07:00
Ken McMillan
bbab6be280 duality: eager deduction and history-based conjectures 2014-03-14 13:40:31 -07:00
Ken McMillan
180f55bbda adding support for non-extensional arrays in duality 2014-03-11 18:20:42 -07:00
Ken McMillan
83a774ac79 duality fix plus mbqi option 2014-03-04 18:38:08 -08:00
Ken McMillan
75bb495585 merging interpolation and duality changes into unstable 2014-02-19 15:36:16 -08:00
Nikolaj Bjorner
c42ee3bb01 Merge branch 'unstable' of https://git01.codeplex.com/z3 into opt 2014-02-11 15:44:12 -08:00
Ken McMillan
f45ad4bdc0 disable silly warnings and add needed header for VS 2014-02-10 12:56:39 -08:00
Ken McMillan
ba193a59b1 some interpolation fixes, plus some options to remove features for testing in duality 2014-02-09 16:04:02 -08:00
Ken McMillan
466c35100d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-01-28 11:28:24 -08:00
Nikolaj Bjorner
23e811d136 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-05 20:44:56 -08:00
Nikolaj Bjorner
084a6f35eb fix bug reported by Nuno Lopes: inlining is unsound for negated predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-02 17:37:35 -08:00
Ken McMillan
9e88691c69 optimizing solver performance in duality 2013-12-22 18:33:40 -08:00
Ken McMillan
48e10a9e2d dealing with incompleteness issues in duality 2013-12-19 11:05:56 -08:00
Ken McMillan
a3462ba6aa working on duality 2013-11-27 17:39:49 -08:00
Nikolaj Bjorner
2ff51e9a60 move model_evaluator from pdr to model, call it model_implicant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-23 21:33:35 +01:00
Nikolaj Bjorner
133ba2d02a fixes to pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-13 13:41:14 -05:00
Ken McMillan
b008d036dd trying to fix proof mode issue 2013-11-05 17:38:50 -08:00
Ken McMillan
a785a5a4b8 Merge branch 'unstable' into interp 2013-11-05 12:28:13 -08:00
Ken McMillan
49c72abb2d new interpolation fixes; re-added fixedpoint-push/pop 2013-11-05 12:17:09 -08:00
Nikolaj Bjorner
89989627d0 add blast method for ite terms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-04 13:33:02 -08:00
Nikolaj Bjorner
c0de1e34ac working on upper bound optimziation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-03 14:54:42 -08:00
Anh-Dung Phan
906bbb4eeb Update Network Simplex implementation 2013-10-28 18:29:14 -07:00
Ken McMillan
3a0947b3ba merged with unstable 2013-10-18 17:26:41 -07:00
Nikolaj Bjorner
eb4c10c037 fixing bugs with validation code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-15 03:53:33 -07:00
Nikolaj Bjorner
9b34350646 test output predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-13 06:25:26 -07:00
Nikolaj Bjorner
1b8d1a1ccc fix bug in ackerman reduction found by Anvesh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-24 10:42:31 +03:00
Nikolaj Bjorner
2d01c4d50f update join planner to take projected columns into account 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-24 06:41:46 +03:00
Nikolaj Bjorner
0a964c324e test for undetermined accessor for PDR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-20 12:32:16 -07:00
Nikolaj Bjorner
41c9e2b1a4 check equalities with unknown evaluations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-20 11:27:52 -07:00
Nikolaj Bjorner
419f99c329 fix bug found by Ethan: fresh values for bit-vectors loops if the domain of bit-vectors is truly small 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-13 15:30:56 -07:00
Nikolaj Bjorner
10e203da43 remove some dependencies on parameter file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-12 20:22:26 -07:00
Nikolaj Bjorner
4af4466821 add qe_arith routine for LW projection on monomomes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-12 12:19:46 -07:00