mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
6129 commits 49 branches 53 tags 182 MiB
Commit graph

4949 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
5598f334d4 optimizations to Hilbert basis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-26 17:01:49 -08:00
Leonardo de Moura
e8140f5c1f Fix compilation problems when using Visual Studio 32 bit compiler 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-26 12:34:52 -08:00
Christoph M. Wintersteiger
5fe58c2f2d Java API: renamed assert_(...) to add(...) 
.NET API: added alias Add(...) for Assert(...)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-26 19:13:48 +00:00
Leonardo de Moura
b2810592e6 Add enumeration_sort method to C++ API. Add as_expr method to goal class in C++ API. Add enum_sort_example to C++ examples/c++/example.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-26 08:29:01 -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
Leonardo de Moura
4922d62311 Fix bug reported at http://z3.codeplex.com/workitem/23 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-21 11:02:13 -08:00
Leonardo de Moura
70192b66e9 Remove dead files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-20 17:17:11 -08:00
Leonardo de Moura
fa298fc7f6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-20 13:41:16 -08:00
Leonardo de Moura
97bf9418f7 Add new probes for arithmetic. Check for LIA and LRA (and activate qe if applicable). Modify echo tactic to send results to the regular stream. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-20 13:41:08 -08:00
Christoph M. Wintersteiger
6075ae28fc ML/Java: Proper use of Datatype API for List/Enum/Constructor 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-20 19:40:48 +00:00
Leonardo de Moura
b4d57e0ab1 Merge branch 'unstable' into contrib 2013-02-19 15:35:05 -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
Leonardo de Moura
4a97e6daea Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-15 16:32:30 -08:00
Leonardo de Moura
0af4384882 Fix more issues unintepreted sort tests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-15 16:31:49 -08:00
Leonardo de Moura
943e142bfa Fix bug in ast_smt_pp.cpp. After user_sort_plugin was introduced, it is not that case that if a sort is uninterpreted, then sort->get_family_id() == null_family_id. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-15 16:27:55 -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
784307fc30 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-14 15:06:25 -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
Leonardo de Moura
030aef5d5a Fix bug reported by Andrey Kupriyanov 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-14 09:55:42 -08:00
Leonardo de Moura
d2651f1afc Keep consistent error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-13 18:53:37 -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
Christoph M. Wintersteiger
f161f455df Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-13 17:21:29 +00:00
Christoph M. Wintersteiger
92e7384bf5 Java API: final adjustments 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-13 17:21:08 +00:00
Leonardo de Moura
60ce2a84cd Fix build hashcode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-13 09:16:38 -08:00
Leonardo de Moura
5790115e40 Include git hash in the binary 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-13 08:39:26 -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
0879c6f052 updating tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-12 18:13:02 -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
a14f29a4eb add hilbert basis utility for extracting auxiliary invariants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-12 14:58:04 -08:00
Leonardo de Moura
3a15db5244 Fix uninterpreted sort definition. There was a mismatch in the behavior of the API and SMT front-ends. The SMT front-ends were using user_sorts to be able to support parametric uninterpreted sorts. After this fix, the API also creates user_sorts. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-12 14:34:31 -08:00