Nikolaj Bjorner
|
1a5327e427
|
strengthen quantifier check for PDR (and other engines) that don't handle quantified predicates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-06-24 17:06:05 +01:00 |
|
Nikolaj Bjorner
|
ed7e0e11a8
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-05-28 20:55:13 -07:00 |
|
Nikolaj Bjorner
|
28f6adf79e
|
disable hybrid relations pending overhaul/deletion of product relations
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
|
2015-05-20 09:21:55 -07:00 |
|
Christoph M. Wintersteiger
|
32fb679066
|
tabs
|
2015-05-19 11:01:15 +01:00 |
|
Nikolaj Bjorner
|
52619b9dbb
|
pull unstable
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
|
2015-04-01 14:57:11 -07:00 |
|
Nikolaj Bjorner
|
10cdbb881f
|
enable canceling simplex on interrupt, investigating PDR inconsistency
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-03-25 12:13:57 -07:00 |
|
Christoph M. Wintersteiger
|
b76d588c28
|
Renamed the soft_timeout option to just timeout.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-03-21 16:10:30 +00:00 |
|
Nikolaj Bjorner
|
b8fbc32689
|
fix crash in explanation generation. Codeplex issue 181
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-02-24 17:03:34 -08:00 |
|
Christoph M. Wintersteiger
|
71912830f1
|
Formatting, mostly tabs
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 17:54:44 +00:00 |
|
Christoph M. Wintersteiger
|
0381e4317a
|
Formatting, mostly tabs.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 17:54:04 +00:00 |
|
Nikolaj Bjorner
|
08cb8b8de8
|
address divergence in the case of shared theory symbols. Codeplex issue 147, thanks to George Karpenkov
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-12-09 16:04:25 +01:00 |
|
Ken McMillan
|
d815af9f0f
|
merge duality changes with unstable
|
2014-10-22 10:14:05 -07:00 |
|
Ken McMillan
|
ec48f6d129
|
working on transforms for duality
|
2014-10-04 19:07:14 -07:00 |
|
Nikolaj Bjorner
|
e6725b2344
|
merge unstable into opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-26 12:12:24 -07:00 |
|
Nikolaj Bjorner
|
061a18efcf
|
move some configuration parameters into dl_context, add notes to udoc_relation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-26 08:22:25 -07:00 |
|
Nikolaj Bjorner
|
74053275cf
|
consolidate rule checking in separate class
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-25 19:05:49 -07:00 |
|
Nikolaj Bjorner
|
8e2fedbc2e
|
Merge branch 'opt' of https://git01.codeplex.com/z3 into opt
|
2014-09-25 09:33:20 -07:00 |
|
Nikolaj Bjorner
|
a2d8fd4c4b
|
local opts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-25 09:33:12 -07:00 |
|
Nuno Lopes
|
aaa931e0d5
|
fix build with gcc
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
|
2014-09-25 15:56:01 +01:00 |
|
Nikolaj Bjorner
|
6457654e2e
|
make self-contained bind-variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-24 14:30:30 -07:00 |
|
Nikolaj Bjorner
|
918d52f1b0
|
tune and fix doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-24 09:20:21 -07:00 |
|
Nikolaj Bjorner
|
16f80fce92
|
add check_relation for integrity checking of relational operations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-24 01:06:58 -07:00 |
|
Nikolaj Bjorner
|
22808a039d
|
working on udoc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-21 20:25:11 -07:00 |
|
Nikolaj Bjorner
|
d01ca11001
|
reduce asymptotic overhead of asserting bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-16 17:13:09 -07:00 |
|
Nikolaj Bjorner
|
c09903288f
|
have free variable utility use a class for more efficient re-use
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-15 16:14:22 -07:00 |
|
Ken McMillan
|
13b61d894c
|
adding recursion bounds to duality
|
2014-09-09 14:02:46 -07:00 |
|
Nikolaj Bjorner
|
54c959783d
|
profile, optimize, trying out product-set
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-08-23 20:51:30 -07:00 |
|
Nikolaj Bjorner
|
9b893c625b
|
print output predicates as part of displaying rules
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-08-22 21:17:05 -07:00 |
|
Nikolaj Bjorner
|
b596828d23
|
add DDNF based engine
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-08-21 18:04:46 -07:00 |
|
Nikolaj Bjorner
|
ddbff6f77b
|
revamp configuration parameter names for fixedpoint
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-08-18 01:03:11 -07: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 |
|
Ken McMillan
|
3a0947b3ba
|
merged with unstable
|
2013-10-18 17:26:41 -07: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
|
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
|
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
|
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
|
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
|
e4338f085b
|
re-organization of muz
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-08-28 22:11:33 -07:00 |
|