mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
2106 commits 23 branches 48 tags 157 MiB
Commit graph

65 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
0aaa67fa7d check for uninterpreted functions in tail for PDR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-10 22:45:37 -07:00
Nikolaj Bjorner
f4e048c1e8 partition inequalities into conjuncts determined by equivalence classes of shared variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-10 22:23:09 -07:00
Nikolaj Bjorner
f4aae5e56a fix C(R) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-09 23:12:55 -07:00
Nikolaj Bjorner
ab5894412d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-09-09 23:05:34 -07:00
Nikolaj Bjorner
c87ae1e99b add transformation to reduce overhead of negation for predicates with free variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-09 23:05:18 -07:00
Nikolaj Bjorner
1496333e5b fix mint64 build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-09 09:22:45 -07:00
Nikolaj Bjorner
861a31f458 fix build warning from tptp example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-08 13:30:03 -07:00
Nikolaj Bjorner
93fd36b5da revert wrong optimization for single-occurrence negative columns 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-08 11:52:00 -07:00
Nikolaj Bjorner
716663b04a avoid creating full tables when negated variables are unitary, add lazy table infrastructure, fix coi_filter for relations, reduce dependencies on fixedpoing_parameters.hpp header file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-08 05:52:18 -07:00
Nikolaj Bjorner
0f9160a738 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-09-06 21:49:14 -07:00
Nikolaj Bjorner
457b22b00e add TPTP example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-06 21:49:00 -07:00
Nikolaj Bjorner
7c4b2b04a7 fix coi-filter to not ignore relational tables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-04 08:54:02 -07:00
Nikolaj Bjorner
1cf2b7c2d3 remove unused reference to rm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-02 21:22:44 -07:00