mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
1117 commits 23 branches 48 tags 157 MiB
Commit graph

1117 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Leonardo de Moura
75ad174567 Initialize int64_min constant when using GMP 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-08 15:02:51 -07:00
Leonardo de Moura
3d34aa7f01 Fix is_int64 bug in mpz when compiling with GMP 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-08 14:50:17 -07:00
Leonardo de Moura
03c1b24dea Fix get_int64 and is_int64 methods in mpz. Fix INT64_MAX constant definition. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-08 14:25:25 -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
Christoph M. Wintersteiger
5915533170 FPA: bugfix for corner-case sign of division 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-04-05 15:27:05 +01:00
Christoph M. Wintersteiger
26efb3c7f1 FPA bugfixes for denormal numbers. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-04-05 12:45:28 +01: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
f8476a1c87 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-03 17:03:29 -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
Leonardo de Moura
1c96a7d52f Add option smt.bv.enable_int2bv in the new parameter setting framework. This is the new name for the old parameter :bv-enable-int2bv-propagation. This modification addresses an issue reported at http://stackoverflow.com/questions/15798984/bv-enable-int2bv-propagation-option. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-03 15:51: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
Nuno Lopes
67e9d74653 constify a few functions 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-03 09:44:31 -07:00
Nikolaj Bjorner
99cdf3d742 Merge branch 'unstable' of https://git01.codeplex.com/z3 into dl_transforms 2013-04-02 20:34:02 -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
Christoph M. Wintersteiger
4c353ec720 FPA: bugfix for model completion. Thanks to Levent Erkok. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-04-02 13:45:42 +01: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
435c6dd365 convert mega-bytes to bytes in env_params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-29 09:05:36 -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
96f4606a7f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-27 10:39:15 -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
Leonardo de Moura
b417ca657d Fix set_interruptable usage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-25 16:52:08 -07:00
Leonardo de Moura
7e9715f3e6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-25 15:43:04 -07:00
Nuno Lopes
25a41d48dc speedup bit_vector::num_words() 
Proof of equivalence w.r.t. previous code: http://rise4fun.com/Z3/aiLV

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-03-25 15:41:52 -07:00
Leonardo de Moura
4385b51c84 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-25 15:41:02 -07:00
Leonardo de Moura
f32eaee62e Replace std::sort with std::stable_sort when the given relation is just a partial order. This change avoids discrepancies when using different implmentations of std::sort. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-25 15:40:52 -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
Leonardo de Moura
9abcde9a35 Fix typos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-25 14:42:18 -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