Nuno Lopes
1917c909d8
delete garbage
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-23 11:28:09 -07:00
Nuno Lopes
12b092c45f
[datalog] restore the old (linear) cycle breaker
...
force the compiler to use all preds as global deltas for correctness. This is a temporary fix.
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-23 11:27:27 -07:00
Nuno Lopes
08eb85fe3d
minor cleanup
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-23 10:02:44 -07:00
Nikolaj Bjorner
d849dbf21f
remove pointer comparisons/hash
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-23 09:58:30 -07:00
Nuno Lopes
db653a6e68
[datalog] merge changes from the hassel branch
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-22 09:05:27 -07:00
Nuno Lopes
7ce88d4da9
fix a few compilation warnings
...
- remove unused variables and class fields
- add support for gcc 4.5 & clang's __builtin_unreachable
- fix 2 bugs related to strict aliasing
- remove a few unused function parameters
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-21 14:36:39 -07:00
Nuno Lopes
63ece8278d
[datalog] improve compilation to reuse total tables, and to reduce cloning/deallocs.
...
this gives up to 40% in memory reduction and 10% speedup in test cases with many rules
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-18 11:23:21 -07:00
Nuno Lopes
51d3db8105
[dl] remove 2 uneeded fields from sparse_table::rename_fn
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-16 10:48:57 -07:00
Nuno Lopes
38823d6c79
[PDR] fix expansion of BV literals
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-16 08:16:02 -07:00
Nuno Lopes
1f5097cdaa
[datalog] fix stratum cycle break for rules with multiple looping dependecies
...
e.g.
a -> b
b-> a
a -> a
this change makes the cycle breaker quadratic on the number of predicates. This should be revisited later
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-15 16:53:25 -07:00
Nikolaj Bjorner
a054b099c1
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
2013-04-11 13:44:30 -07:00
Nikolaj Bjorner
18ea547cea
compiler optimization and fixes to unit tests
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-11 13:44:23 -07:00
Nuno Lopes
cb31a294c8
use unsigned_vector where appropriate
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-11 08:50:04 -07:00
Nuno Lopes
2685c605e5
[datalog] fix a few bugs related with output predicates
...
(by me & Nikolaj)
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-10 16:37:47 -07:00
Nuno Lopes
14172d3fae
fix crash in dl_interp_tail_simplifier when no transformation is performed
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-10 14:49:07 -07:00
Nikolaj Bjorner
6a36116b5c
stash
2013-04-09 10:16:37 -07:00
Nikolaj Bjorner
9456f16a4c
overhaul urle_set
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-09 10:15:20 -07:00
Nuno Lopes
90c808bde9
[datalog] fix memory leak in union instructions
...
the source operand was never cleaned up
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-08 17:14:43 -07:00
Nikolaj Bjorner
8f46179def
reorganization of rule_set structure
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-08 13:50:56 -07:00
Nuno Lopes
1ef17cbe67
add dl_context::has_facts(pred)
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-05 18:12:58 -07:00
Nuno Lopes
5f298b6965
spread some static love
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-05 18:02:41 -07:00
Nikolaj Bjorner
5ef0fdc9c8
dealing with build warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-04 21:39:20 -07:00
Nikolaj Bjorner
65dff93e93
fix more compiler warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-03 17:11:33 -07:00
Nikolaj Bjorner
282173773f
Merge branch 'dl_transforms' into unstable
2013-04-03 17:06:47 -07:00
Nikolaj Bjorner
359d2326f8
stash
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-03 17:06:45 -07:00
Nikolaj Bjorner
afd83f41b8
fix compiler warnings and errors
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-03 17:03:07 -07:00
Nikolaj Bjorner
0b7a270883
debug quantifier transforms
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-03 16:53:09 -07:00
Nikolaj Bjorner
2a745d5224
adding model convertion to quantifier transformation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-03 14:46:58 -07:00
Nikolaj Bjorner
477e8cc46a
debugging quantifier instantiation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-02 20:33:22 -07:00
Nikolaj Bjorner
cda29bc03b
add abstraction and instantiation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-02 15:29:52 -07:00
Nikolaj Bjorner
3d486c4c98
add abstraction and instantiation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-02 15:28:45 -07:00
Nikolaj Bjorner
155f629d96
Merge branch 'dl_transforms' of https://git01.codeplex.com/z3 into unstable
2013-04-02 15:27:00 -07:00
Nikolaj Bjorner
cbb4c12191
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
...
Conflicts:
src/muz_qe/dl_mk_karr_invariants.cpp
2013-04-01 14:57:15 -07:00
Nikolaj Bjorner
65e64d1006
loop counting
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-01 09:54:32 -07:00
Nikolaj Bjorner
2e0c5f5042
loop counting
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-01 09:15:23 -07:00
Nikolaj Bjorner
fbb59453c3
add loop counter v1
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-04-01 09:10:34 -07:00
Nikolaj Bjorner
a2207bc35c
stash
2013-04-01 07:52:55 -07:00
Nikolaj Bjorner
4138e17b3f
extract karr invariants as a Datalog relation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-03-31 16:40:10 -07:00
Nikolaj Bjorner
cd48a5164e
fix bug in hilbert_basis reset method. Missing reset of m_iseq
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-03-29 17:05:17 -07:00
Nikolaj Bjorner
0590101e6f
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
2013-03-29 08:53:50 -07:00
Nikolaj Bjorner
6ed266e4de
debugging karr invariants
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-03-29 08:53:46 -07:00
Nikolaj Bjorner
06e3b6cfb8
remove model converter from transformer operators. Rely on reference in context
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-03-29 08:13:07 -07:00
Nikolaj Bjorner
ce7d6a16d0
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
2013-03-27 15:55:44 -07:00
Nuno Lopes
1cece1c1fb
Datalog improvements:
...
- add cancel status
- display statistics on cancel
(by me & Nikolaj)
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-03-27 10:38:50 -07:00
Nikolaj Bjorner
c9109132da
test hilbert-basis with fdds and checked integers
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-03-26 17:33:44 -07:00
Nikolaj Bjorner
5c4003b4e5
test hilbert-basis with fdds and checked integers
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-03-26 17:31:59 -07:00
Nikolaj Bjorner
00e79e6b6b
test hilbert-basis with fdds and checked integers
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-03-26 17:31:11 -07:00
Nuno Lopes
da83a6b28c
dl_bit_blasting: run simplifier before bit-blasting, in order to comply with its precondition
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-03-25 14:48:22 -07:00
Nuno Lopes
df35da1acf
rule_manager::mk(): default initialization of m_proof to null
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-03-25 10:48:48 -07:00
Nuno Lopes
b427958b9e
qe_lite> fix crash in is_var_eq()
...
(by me & Nikolaj)
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-03-25 09:53:11 -07:00