mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity
3657 commits 49 branches 53 tags 182 MiB
Commit graph

3657 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ken McMillan
01c6fe39ab fix markers aliasing bug in Duality::CheckerForEdgeClone 2014-05-20 15:10:31 -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
6f0155ce94 avoid compiler warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-20 10:14:40 -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
8b5eb08e2d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-05-15 21:12:41 -07:00
Nikolaj Bjorner
3d1ca5ecc9 make eval cache sensitive to model completion. Bug 110 reported by cipher1024 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-15 21:12:16 -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
Nikolaj Bjorner
61dcdcb9d1 separate inc sat solver for now 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-15 11:25:05 -07:00
Nikolaj Bjorner
33e2f2012d inc sat experiment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-15 08:46:20 -07:00
Nikolaj Bjorner
d849b5c637 experiment with sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-14 19:40:58 -07:00
Nikolaj Bjorner
81c2560854 experimenting with inc-sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-14 15:13:26 -07:00
Nikolaj Bjorner
6d6abb4dde experimenting with inc_sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-14 09:27:47 -07:00
Ken McMillan
95146483ea add round-off to farkas resconstruction in interp 2014-05-13 18:15:51 -07:00
Ken McMillan
c9e9b30af6 interp handle mystery arith lemmas 2014-05-13 17:28:22 -07:00
Nikolaj Bjorner
6821d61ac4 working on incremental sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-13 17:19:19 -07:00
Ken McMillan
669fded98a fix for possible problem in Farkas proofs in interp 2014-05-13 14:59:09 -07:00
Ken McMillan
aa35f988fc fix for bad coefficient in AssignBounds 2014-05-13 14:58:32 -07:00
Nikolaj Bjorner
03979fd580 fix up pareto callback mechanism 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-13 12:48:17 -07:00
Nikolaj Bjorner
1ea376e310 edits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-13 10:33:09 -07:00
Nikolaj Bjorner
cad1e5cab3 move to scoped state, change default parameter for sls until bv is debugged 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-11 18:39:36 -07:00
Nikolaj Bjorner
e9a11bd93b fix emptines check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-10 17:43:42 -07:00
Nikolaj Bjorner
d8ad75e3f4 ptr/ref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 22:30:59 -07:00
Nikolaj Bjorner
fb0305d5ec update timeout logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 22:27:35 -07:00
Nikolaj Bjorner
cf55854d22 adding scoped state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 17:21:16 -07:00
Nikolaj Bjorner
252b9e8819 fix lower/upper bound estimate with respect to offset 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 16:32:17 -07:00
Ken McMillan
b3bd9db4a5 merge duality debug code 2014-05-09 13:18:28 -07:00
Ken McMillan
ddd3867beb merged interp hack 2014-05-09 13:12:10 -07:00
Ken McMillan
90ca1b95c0 debugging code in duality 2014-05-09 13:10:03 -07:00
Ken McMillan
2a887a7608 interp localization hack 2014-05-09 13:08:39 -07:00
Nikolaj Bjorner
9c4409a8fe set timout to max 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 11:48:28 -07:00
Nikolaj Bjorner
02b419c939 add logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 11:36:08 -07:00
Nikolaj Bjorner
f1194ffeaa add logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 11:34:15 -07:00
Nikolaj Bjorner
4dc71acde0 add logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 11:31:54 -07:00
Nikolaj Bjorner
a0359c3035 add logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 11:24:36 -07:00
Nikolaj Bjorner
1e235659c7 unreferenced variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 11:05:22 -07:00
Nikolaj Bjorner
9c1f85e564 addressing compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 11:03:11 -07:00
Nikolaj Bjorner
05a39cb2cf fix wrong simplex backtracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 08:51:07 -07:00
Nikolaj Bjorner
d2db8007d8 tuning pb/max 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-06 04:01:10 -07:00
Nikolaj Bjorner
7ade3f2c04 fix sls based on pkb120 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-05 19:22:34 -07:00
Nikolaj Bjorner
f1ebf2002a tuning sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-05 16:40:54 -07:00
Nikolaj Bjorner
25ad9d2ee1 tuning based on benchmarks from Robert White 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-05 14:43:06 -07:00
Ken McMillan
a4f3afd70d added fixedpoint.conjecture_file option 2014-05-05 14:29:54 -07:00
Nikolaj Bjorner
182fea2d7b fix bcd2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-05 10:21:16 -07:00
Christoph M. Wintersteiger
581bbb58fb typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-05-02 18:04:32 +01:00
Christoph M. Wintersteiger
8150bd5617 OSX timeout handling bugfix 2014-05-02 17:58:17 +01:00
Christoph M. Wintersteiger
769b2b585b fixed typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-05-02 16:43:32 +01:00
Christoph M. Wintersteiger
c3b7c738f8 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt 
Conflicts:
	scripts/mk_project.py
	src/duality/duality.h
	src/duality/duality_solver.cpp
	src/duality/duality_wrapper.h
	src/interp/iz3hash.h

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 22:18:41 +01:00
Christoph M. Wintersteiger
fceaf97c95 Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 2014-04-25 22:11:34 +01:00
Christoph M. Wintersteiger
a5ce28d82a bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 22:10:53 +01:00