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

2677 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
466ac0237f Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 2014-03-27 13:11:29 +00:00
Ken McMillan
732035bf63 merge interp/duality changes with unstable 2014-03-26 14:48:04 -07:00
Ken McMillan
fcada914d5 duality fix 2014-03-26 14:10:21 -07:00
Christoph M. Wintersteiger
6f9a348f63 removed dependency of bvsls on goal_refs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-26 17:26:06 +00:00
Ken McMillan
c9fcf7ee96 interpolation fix (add simplify_cong) 2014-03-24 17:21:29 -07:00
Ken McMillan
e3c1cdfe8c interpolation fix 2014-03-24 11:33:09 -07:00
Christoph M. Wintersteiger
d1376343c7 Compilation fix. 
gcc 4.3.2 (on debian 5) did not like the definitions of gcd and abs in class rational, so I moved them outside of the class.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-22 16:42:11 +00:00
Ken McMillan
fb2caf99e6 duality fix 2014-03-21 10:35:33 -07:00
Christoph M. Wintersteiger
83f88917a8 bugfix for python 2.6 2014-03-20 17:47:41 +00:00
Christoph M. Wintersteiger
5f040e7480 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into bvsls 2014-03-20 17:20:12 +00:00
Christoph M. Wintersteiger
041427b530 Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 2014-03-20 17:19:51 +00:00
Andreas Froehlich
202eb7b0ef Merge branch 'bvsls' of https://git01.codeplex.com/z3 into bvsls 
Conflicts:
	src/tactic/sls/sls_tactic.cpp
 2014-03-20 16:32:24 +00:00
Andreas Froehlich
c615bc0c34 uct forget and minisat restarts added 2014-03-20 15:58:53 +00:00
Nikolaj Bjorner
3e0e9c7f3c parse also bit-vector constants with set-info. Reported by David Cok 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-19 20:30:58 -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
Nikolaj Bjorner
a8fb15ce2c patch bounds normalization bug found by dvitek 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-19 18:02:05 -07:00
Ken McMillan
3e91037a4d duality fixes 2014-03-19 12:37:05 -07:00
Christoph M. Wintersteiger
e3ae0ba0bd SLS refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-19 17:26:05 +00:00
Christoph M. Wintersteiger
3d6f8840c6 SLS refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-19 17:04:38 +00:00
Andreas Froehlich
eabebedabf Merge branch 'bvsls' of https://git01.codeplex.com/z3 into bvsls 
Conflicts:
	src/tactic/sls/sls_evaluator.h
	src/tactic/sls/sls_tactic.cpp
	src/tactic/sls/sls_tracker.h
 2014-03-19 12:09:29 +00:00
Andreas Froehlich
90245021b2 Current version for relocating. 2014-03-19 11:49:44 +00:00
Christoph M. Wintersteiger
5aa352fd16 removed tabs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-19 09:40:01 +00:00
Ken McMillan
2417b75d8d duality: added restarts 2014-03-16 15:37:19 -07:00
Ken McMillan
663d110b72 interpolation fix 2014-03-16 12:09:53 -07:00
Ken McMillan
675820ff67 merged changes from linux 2014-03-14 14:51:39 -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
Andreas Froehlich
853ce522cc plenty of new stuff 2014-03-09 15:42:51 +00:00
Nikolaj Bjorner
4732e03259 filter fresh constants from models 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-07 08:59:27 -08:00
Ken McMillan
83a774ac79 duality fix plus mbqi option 2014-03-04 18:38:08 -08:00
Nikolaj Bjorner
601cb43f78 fix quotation bug reported by Arie Gurfinkel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-04 17:18:49 -08:00
Nikolaj Bjorner
b1b349f496 modify offset check to accept linear expressions over numerals. Codeplex issue 81 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-02 17:50:29 -08:00
Nikolaj Bjorner
23313e5bdc remove unsound simplification for rem. Codeplex Issue 76 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-02 17:24:40 -08:00
Nikolaj Bjorner
4f20216677 fix documnetation to say milli-seconds. Issue 84 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-02 17:14:26 -08:00
Nikolaj Bjorner
a00a9fbdfd generate error on duplicated data-type accessors. Issue 85 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-02 17:10:48 -08:00
Nikolaj Bjorner
e27b7e3038 use size_t for return values from strlen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-01 11:09:57 -08:00
Nikolaj Bjorner
f2ecd70e65 fix ctx solver simplify, remove horn inequalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-01 11:02:18 -08:00
Ken McMillan
19dbd02e13 interpolation fix 2014-02-28 10:38:35 -08:00
Ken McMillan
acf4ad0ab6 use new hashtable implementation in windows 2014-02-27 17:23:19 -08:00
Ken McMillan
08d892bbdb interpolation fixes 2014-02-27 17:21:47 -08:00
Nikolaj Bjorner
891d0d07f8 removig unsound simplification in ctx-solver-simplify tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-02-27 13:42:40 -08:00
Christoph M. Wintersteiger
d1d038da35 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2014-02-27 18:06:13 +00:00
Ken McMillan
4f06b347b3 new hastable implementation for interp/duality 2014-02-25 18:21:06 -08:00
Ken McMillan
ee9907a700 two interpolation fixes 2014-02-25 18:19:50 -08:00
Christoph M. Wintersteiger
4c8bbad8d6 FPA probe bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-25 18:16:28 +00:00
Christoph M. Wintersteiger
b968eb2b8c FPA probe bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-25 18:13:16 +00:00
Ken McMillan
7fc011dbb8 interpolation fixes 2014-02-24 11:59:02 -08:00
Christoph M. Wintersteiger
efd0cdc740 bugfix for FPA 2014-02-24 14:01:51 +00:00
Christoph M. Wintersteiger
4a9f12dd34 bugfix for FPA 2014-02-24 13:57:15 +00:00
Christoph M. Wintersteiger
07d56bdc70 Java API bugfixes for cygwin compilation 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-21 13:44:39 +00:00