Nikolaj Bjorner
|
0641c4f694
|
working on pre-processing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-12-26 09:53:33 -08:00 |
|
Nikolaj Bjorner
|
70c4432bb4
|
working on pb pre-processing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-12-23 13:22:21 -08:00 |
|
Nikolaj Bjorner
|
0c2ec6951a
|
working on pre-processing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-12-23 03:25:22 -08:00 |
|
Nikolaj Bjorner
|
24f2fd380c
|
adding pre-processing of BP constraints
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-12-23 01:33:24 -08:00 |
|
Nikolaj Bjorner
|
fe5c42c90f
|
fixes to bugs exposed by regressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-12-15 05:23:47 +02:00 |
|
Nikolaj Bjorner
|
50f18a77af
|
disable 'optimization' that led to wrong model'
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-12-15 02:40:52 +02:00 |
|
Nikolaj Bjorner
|
da348fe1c0
|
first pass on normalization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-12-07 14:38:09 -08:00 |
|
Nikolaj Bjorner
|
97dfb6d521
|
moving to rational coefficients
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-21 15:55:08 -08:00 |
|
Nikolaj Bjorner
|
33895d522b
|
fix and enable learning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-19 20:47:16 -08:00 |
|
Nikolaj Bjorner
|
ee0abfbfe9
|
rename card->pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-18 21:25:02 -08:00 |
|
Nikolaj Bjorner
|
06ae0db116
|
working on pb solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-14 18:04:05 -08:00 |
|
Nikolaj Bjorner
|
d1937b2032
|
add PB operators to C-based API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-13 17:09:10 -08:00 |
|
Nikolaj Bjorner
|
e412d6175d
|
add pb capabilities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-09 16:19:49 -08:00 |
|
Nikolaj Bjorner
|
3e8c7d85aa
|
add vocabulary for arbitrary PB inequalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-09 16:13:26 -08:00 |
|
Nikolaj Bjorner
|
2f04918c39
|
working on cardinality tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-06 12:33:09 -08:00 |
|
Nikolaj Bjorner
|
9467806a5c
|
debugging cardinality theory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-05 09:39:28 -08:00 |
|
Nikolaj Bjorner
|
2853b322ca
|
sketch cardinality plugin module
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-05 01:30:34 -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 |
|
Christoph M. Wintersteiger
|
65a202873f
|
Bugfix for equality rewriting on floats.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2013-10-10 15:38:54 +01:00 |
|
Christoph M. Wintersteiger
|
9a9f8bbb34
|
rewriter and value recognition bugfixes for floats
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2013-10-08 20:01:39 +01: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
|
e4338f085b
|
re-organization of muz
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-08-28 22:11:33 -07:00 |
|
Nikolaj Bjorner
|
5c145dcd4b
|
fix parameter checking on quantifiers (thanks to Esteban Pavese), fix query tracking in rel_context (thanks to Nuno Lopes), fix counter for free variables under quantfiers (thanks to Tomer Weiss)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-08-22 15:00:52 -07:00 |
|
Nikolaj Bjorner
|
8f515ef356
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2013-08-14 17:56:26 -07:00 |
|
Nikolaj Bjorner
|
04678d9628
|
improve error message when sorts are non-numeric
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-08-14 17:56:07 -07:00 |
|
Nikolaj Bjorner
|
f82d055e60
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2013-08-12 08:55:48 -07:00 |
|
Nikolaj Bjorner
|
0f83e7a251
|
fix bug masked by default configuration
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-08-10 12:23:34 -07:00 |
|
Nikolaj Bjorner
|
3b64265c27
|
remove duplicated definition of is_store and is_select
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-08-09 09:15:04 -07:00 |
|
Leonardo de Moura
|
d9941c0ccc
|
Add code for rejecting bitvector constants of size 0
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-06-28 19:21:27 -07:00 |
|
Leonardo de Moura
|
544dfde454
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2013-06-27 09:30:33 -07:00 |
|
Leonardo de Moura
|
f238720b76
|
Cherry-pick goodies from mcsat branch
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-06-27 09:19:23 -07:00 |
|
Nikolaj Bjorner
|
324dc5869d
|
fix substitution bug in qe, working on boogie trace
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-06-25 13:07:28 -05:00 |
|
Leonardo de Moura
|
a60b53bfd8
|
Fix compilation errors/warnings when using GCC
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-06-20 17:52:20 -07:00 |
|
Christoph M. Wintersteiger
|
76c59cb85c
|
MPF conversion bugfix.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2013-06-14 17:22:25 +01:00 |
|
Christoph M. Wintersteiger
|
455618bb2b
|
FPA: added is_nan
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2013-06-07 18:34:31 +01:00 |
|
Christoph M. Wintersteiger
|
d7639557d2
|
FPA: added rewriting and fpa2bv conversion rules for new operations.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2013-06-07 18:03:46 +01:00 |
|
Christoph M. Wintersteiger
|
123d3ec3a7
|
New FPA operators added.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2013-06-07 17:55:29 +01:00 |
|
Christoph M. Wintersteiger
|
e5c720de29
|
FPA: bugfix for abs
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2013-06-07 17:36:34 +01:00 |
|
Leonardo de Moura
|
110fa0b7fb
|
Fix issue http://z3.codeplex.com/workitem/45
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-06-05 13:50:22 -07:00 |
|
Nikolaj Bjorner
|
c0895e5548
|
remove hassel table from unstable: does not compile under other plantforms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-05-31 17:48:19 -07:00 |
|
Leonardo de Moura
|
c6f4cdab0f
|
Fix bug reported at https://z3.codeplex.com/workitem/41
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-05-27 17:49:03 -07:00 |
|
Nikolaj Bjorner
|
e35fd58968
|
add rewriting option to simplify store equalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-05-13 11:43:30 -07:00 |
|
Christoph M. Wintersteiger
|
7053b7636b
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2013-05-01 14:11:21 +01:00 |
|
Christoph M. Wintersteiger
|
65af658fd7
|
FPA: min/max special cases fixed.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2013-05-01 14:08:53 +01:00 |
|
Nikolaj Bjorner
|
8abdefef6d
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2013-04-28 12:48:10 -07:00 |
|
Nikolaj Bjorner
|
8038c719fb
|
optimize rule preprocessing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-04-26 14:40:20 -07:00 |
|
Nikolaj Bjorner
|
b644fb9875
|
optimize rule processing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-04-26 12:02:19 -07:00 |
|
Nikolaj Bjorner
|
c58b4f9a53
|
optimize rule processing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-04-26 11:43:06 -07:00 |
|
Nikolaj Bjorner
|
83add2bd9b
|
fix bugs reported by Filip Konecny <filip.konecny@epfl.ch> in PDR
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-04-25 13:39:11 -07:00 |
|
Nikolaj Bjorner
|
4ceb228583
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2013-04-21 18:17:56 -07:00 |
|