Ken McMillan
f7d589fc49
changed fixedpoint output format for easier parsing in Boogie
2014-04-10 17:53:00 -07:00
Ken McMillan
58ffffe4d4
hack to filter out Boogie axioms with large "distinct" predicates that cause legacy solver death
2014-04-06 13:01:20 -07:00
Ken McMillan
2b492f04f6
merging duality and interpolation changes
2014-04-04 15:50:59 -07:00
Ken McMillan
bdc7bfde87
duality quantifier simplification fix
2014-04-04 13:10:18 -07:00
Christoph M. Wintersteiger
dee21c6656
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
2014-04-04 17:57:57 +01:00
Christoph M. Wintersteiger
9c052f589d
C API bugfix (Stackoverflow #22864146 )
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-04 17:57:50 +01:00
Ken McMillan
43644fc2cb
g++ pedantry
2014-04-04 01:28:09 +01:00
Ken McMillan
588aeff5c3
merged interpolation and duality changes
2014-04-03 17:11:15 -07:00
Ken McMillan
fc62be37b6
getting rid of DOS line endings
2014-04-03 17:09:11 -07:00
Ken McMillan
9a2fe83697
interpolation fix
2014-04-03 13:20:08 -07:00
Christoph M. Wintersteiger
4444eb361c
bugfix
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-03 13:11:39 +01:00
Christoph M. Wintersteiger
944dfee008
.NET and Java API Bugfix (Codeplex issue 101)
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-02 19:25:05 +01:00
Christoph M. Wintersteiger
7bb1469d71
removed debugging code.
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-02 19:10:30 +01:00
Christoph M. Wintersteiger
a833c9ac41
Fixed bug (codeplex issue 102)
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-02 17:56:55 +01:00
Ken McMillan
4671c1be41
duality fix
2014-04-01 17:50:48 -07:00
Ken McMillan
278d619521
set text default to auto to try to avoid crlf disasters
2014-04-01 17:20:37 -07:00
Ken McMillan
6c9483c70a
interpolation fix and improving duality quantifier handling
2014-04-01 17:10:14 -07:00
Nikolaj Bjorner
6f7c9607ea
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
2014-03-28 08:52:04 -07:00
Nikolaj Bjorner
4c95bb4dd9
add 'distinct' to C++ API
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-03-28 08:51:50 -07: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
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
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
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
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
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
