mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity
1099 commits 23 branches 48 tags 157 MiB
Commit graph

1099 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner b1fc6a5cac Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-24 18:26:48 -07:00
Nikolaj Bjorner bbe93ef610 fix build warning, make context simplifier traverse subterms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-24 18:26:22 -07:00
Leonardo de Moura def69e2521 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-24 14:59:38 -07:00
Leonardo de Moura a71bb549c6 Add option :bv-sort-ac true 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-24 14:59:29 -07:00
Nikolaj Bjorner e61fa50dc3 fix build breaks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-24 11:26:46 -07:00
Nikolaj Bjorner ee5d61bd60 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-24 11:26:07 -07:00
Nikolaj Bjorner 6084cbd065 fix build breaks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-24 11:25:43 -07:00
Leonardo de Moura 9d0b0df985 Fix gcc compilation errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-24 09:07:51 -07:00
Leonardo de Moura 5aa84c28a6 Remove trace msg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-24 09:00:19 -07:00
Leonardo de Moura 2633dc56ab Fix non ASCII character 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-24 08:59:43 -07:00
Nikolaj Bjorner 7c3ca302f0 missing hnf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-23 16:56:47 -07:00
Nikolaj Bjorner fb5d2cae17 local changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-23 16:44:07 -07:00
Nikolaj Bjorner 26f4d3be20 significant update to Horn routines: add module hnf to extract Horn normal form (removed from rule_manager). Associate proof objects with rules to track (all) rewrites, so that proof traces can be tracked back to original rules after transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-23 14:11:54 -07:00
Nikolaj Bjorner e73c06a8b0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 
73aee81bfa8e0edccd25066d755ce2.
 2013-03-23 13:57:12 -07:00
Nuno Lopes 7e0723e42b add unit test for previous commit 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-03-22 11:51:28 -07:00
Nuno Lopes c824178e7e bit_vector: fix operator==() for the case that num_bits is a multiple of 32 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-03-22 11:50:41 -07:00
unknown 54d9fb5c4b Revert "fix crash in qe_lite::is_var_eq" 
This reverts commit b2d4aa0859.
 2013-03-22 01:25:22 +01:00
Nikolaj Bjorner 7b148a73a2 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-21 17:15:36 -07:00