mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 09:24:36 +00:00
Code Activity
1963 commits 45 branches 52 tags 177 MiB
Commit graph

1963 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
unknown
b2d4aa0859 fix crash in qe_lite::is_var_eq 
Signed-off-by: unknown <nbjorner@NIKOLAJ-Z420.redmond.corp.microsoft.com>
 2013-03-22 01:14:08 +01:00
Nuno Lopes
39d7246251 fix overloading of complement from base_table 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-03-20 15:47:56 -07:00
Nuno Lopes
ab761c4c32 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-20 10:41:06 -07:00
Nuno Lopes
ea2b17d83b remove debug code 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-03-20 10:40:52 -07:00
Nikolaj Bjorner
babfc701a6 make model and proof converters a reference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-20 10:36:36 -07:00
Nikolaj Bjorner
5455704af2 move quantifier hoist routines to quant_hoist 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-19 15:00:23 -07:00
Nikolaj Bjorner
b0787024c7 Move ast_counter to location for common utilities. It depends on get_free_vars, so is in rewriter directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-19 09:47:52 -07:00
Nikolaj Bjorner
b8b73077a9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-18 21:46:48 -07:00
Nikolaj Bjorner
7e9f4e264d working on separating horn simplificaiton 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-18 21:46:42 -07:00
Nikolaj Bjorner
d4d3ba104e fix compiler warning for unused variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-18 21:41:00 -07:00
Nikolaj Bjorner
d1ffeb36b0 fix warning messages for unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-18 21:37:44 -07:00
Nuno Lopes
b8598225bf fix definition of bit_vector::empty() 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-03-18 09:20:25 -07:00
Leonardo de Moura
fed2ad2300 Fix nontermination bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-18 08:23:33 -07:00
Leonardo de Moura
39b9da7118 Fix bug in smt_model_finder, it was producing the incorrect instantiation set. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-13 19:02:48 -07:00
Christoph M. Wintersteiger
21f69c2b3a Java API build bugfix. Thanks to Fabian Emmes for reporting this. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-12 12:27:08 +00:00
Christoph M. Wintersteiger
4b973e115f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-11 14:31:33 +00:00
Nikolaj Bjorner
ab73c20757 add Karr linear invariants as transformer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-10 17:53:18 -07:00
Christoph M. Wintersteiger
a9c7517275 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-08 13:22:06 +00:00
Ken McMillan
2b93537366 debugging interpolation 2013-03-06 18:26:46 -08:00
Nikolaj Bjorner
3810374cdd LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-06 15:20:11 -08:00
Nikolaj Bjorner
37a75622a9 LRA tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-06 08:32:21 -08:00
Nikolaj Bjorner
f9aeeeef36 LRA tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-06 08:29:29 -08:00
Christoph M. Wintersteiger
e5307300de FPA: bugfixes in mul() and abs() 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-06 15:04:58 +00:00
Ken McMillan
ae9276ad9b more work on interpolation 2013-03-05 21:56:09 -08:00
Leonardo de Moura
bdc675b1df Fix bug reported at http://stackoverflow.com/questions/15226944/segmentation-fault-in-z3 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-05 09:04:03 -08:00
Christoph M. Wintersteiger
9a4331995e FPA: bugfix for bitblaster. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-05 14:11:50 +00:00
Christoph M. Wintersteiger
35906889b6 FPA: compilation bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-05 13:49:42 +00:00
Kenneth McMillan
d66211c007 working on interpolation API 2013-03-04 23:48:01 -08:00
Kenneth McMillan
bc6b20d557 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-03-04 19:53:53 -08:00
Kenneth McMillan
12d2d3beef minor fixes for OSX 2013-03-04 19:53:46 -08:00
Ken McMillan
9792f6dd33 more work on incorporating iz3 2013-03-04 18:41:30 -08:00
Christoph M. Wintersteiger
e5f03f999a FPA: Added conversion operator float -> float. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-04 20:21:14 +00:00
Kenneth McMillan
e5f5e008aa fixing file heads to match z3 2013-03-03 21:22:50 -08:00
Ken McMillan
68fb01c206 initial commit for interpolation 2013-03-03 20:45:58 -08:00
Nikolaj Bjorner
197b2e8ddb fix bugs reported by Arie Gurfinkel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-03 13:55:41 -08:00
Nikolaj Bjorner
523dc0fb36 add slicing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-02 21:24:21 -08:00
Nikolaj Bjorner
352912c6b5 add default simplifications as tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-02 21:06:13 -08:00
Nikolaj Bjorner
ed846a9ff3 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-02 21:03:15 -08:00
Nikolaj Bjorner
6c3e2e6764 add default simplifications as tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-02 21:03:08 -08:00
Christoph M. Wintersteiger
7822b86b53 FPA: multiple bugfixes for HWF, MPF and a bugfix for FPA2BV (many thanks to Gabriele Paganelli) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-01 19:06:01 +00:00
Christoph M. Wintersteiger
6f3850bfbc FPA bug and leak fixes (thanks to Gabriele Paganelli) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-28 18:46:29 +00:00
Nikolaj Bjorner
75eca46d93 added Karr test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-27 17:32:27 -08:00
Nikolaj Bjorner
5d2d89a85c Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-26 19:15:04 -08:00
Nikolaj Bjorner
2a75f1d71e update logging for hilbert 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-26 19:14:52 -08:00