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

1044 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
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
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
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
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
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
Christoph M. Wintersteiger
14f582eca5 Java API: added automatic detection of jar 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-25 16:03:57 +00:00
Christoph M. Wintersteiger
f5cdc14737 Java API: build system bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-25 15:44:54 +00:00
Christoph M. Wintersteiger
ffb1fc37df Java API: New JDK detection routines. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-25 15:37:33 +00: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
3d4a42c270 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-21 11:02:21 -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
Christoph M. Wintersteiger
2c6c09301f Java API: build system bugfixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-21 16:46:18 +00:00
Christoph M. Wintersteiger
876c6a361e Java API: build system fix for OSX 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-21 16:40:10 +00: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
Christoph M. Wintersteiger
18bae81731 Java Example: build fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-19 22:48:41 +00: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