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

1249 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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