mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity
1058 commits 24 branches 48 tags 158 MiB
Commit graph

200 commits

Author SHA1 Message Date
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
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
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
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
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
6c3e2e6764 add default simplifications as tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-02 21:03:08 -08: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
Nikolaj Bjorner
5598f334d4 optimizations to Hilbert basis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-26 17:01:49 -08:00
Nikolaj Bjorner
e0c73d9bc1 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-24 21:52:38 -08:00
Nikolaj Bjorner
562ae7bec5 faster saturation without backwards subsumption and using SOS-style set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-24 21:52:10 -08:00
Christoph M. Wintersteiger
0f9f01a321 Fix for G++. 
Avoids this error:
../src/muz_qe/heap_trie.h: In member function ‘virtual unsigned int heap_trie<Key, KeyLE, Value>::leaf::num_leaves() const’:
../src/muz_qe/heap_trie.h:91:64: error: there are no arguments to ‘ref_count’ that depend on a template parameter, so a declaration of ‘ref_count’ must be available [-fpermissive]
../src/muz_qe/heap_trie.h:91:64: note: (if you use ‘-fpermissive’, G++ will accept your code, but allowing the use of an undeclared name is deprecated)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-19 22:08:44 +00:00
Nikolaj Bjorner
0aa8df98a1 optimizing hilbert basis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-18 18:58:43 -08:00
Nikolaj Bjorner
306855ba55 fix hilbert_basis tests and add heap_trie index 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-16 22:45:37 -08:00
Nikolaj Bjorner
47342e5d0c move validation code to unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-15 17:46:22 -08:00
Leonardo de Moura
f46c7f9bd9 Fix the build on g++, Fix g++ warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-15 16:36:57 -08:00
Nikolaj Bjorner
a242ac46b6 hilbert validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-15 15:05:39 -08:00
Nikolaj Bjorner
aaf0c16e08 working on hilbert basis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-15 09:09:58 -08:00
Nikolaj Bjorner
3a68affb1b cal modifications 2013-02-14 15:10:52 -08:00
Nikolaj Bjorner
6e7d04f94e working on hilbert basis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-14 15:06:17 -08:00
Nikolaj Bjorner
0c641cdf95 hilbert basis experiment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-13 16:53:56 -08:00
Nikolaj Bjorner
1317a71a1a Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-13 09:42:12 -08:00
Nikolaj Bjorner
706cbd3872 hilbert basis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-12 21:45:20 -08:00
Nikolaj Bjorner
ff03da9e67 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-12 15:44:32 -08:00
Nikolaj Bjorner
0fc44a43e1 add hilbert basis utility for extracting auxiliary invariants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-12 14:58:44 -08:00
Nikolaj Bjorner
ce9a098f16 local changes to pdr_generalizer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-09 10:58:37 -08:00
Nikolaj Bjorner
3ad43c60a9 working on pdr gen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-08 16:54:05 -08:00
Nikolaj Bjorner
9e868cdef3 fix pretty printer bug found by ken 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-08 16:04:46 -08:00
Nikolaj Bjorner
2e2fa84d40 experiment with arithmetic core generalizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-07 19:21:52 -08:00
Nikolaj Bjorner
0fd1c00053 fix reference counting bug in qe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-06 09:40:16 -08:00
Nikolaj Bjorner
8354c2dfb1 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-06 08:10:32 -08:00