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

3641 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
70d765df5c Merge pull request #23 from wintersteiger/unstable 
Made GetInterpolant and ComputeInterpolant public in Java and .NET.
 2015-04-02 17:53:34 +02:00
Christoph M. Wintersteiger
b47851d7da Made GetInterpolant and ComputeInterpolant public in Java and .NET. 
Fixes Codeplex discussion #616450
 2015-04-02 16:51:30 +01:00
Nikolaj Bjorner
6b995c4077 disable wrong fix for simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-02 02:56:40 -07:00
Nikolaj Bjorner
e944f89505 fix bug introduced when clearing state between calls to Pareto/Box 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-02 02:36:01 -07:00
Nikolaj Bjorner
fc36d861a7 update default to maxres for MaxSAT, reset pareto and box state on every constraint update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-01 19:32:50 -07:00
Nikolaj Bjorner
9978cba5a8 Codeplex issue 191: inconsistent results from PDR engine. The report exposed bugs in the implementation of the priority queue leaving unexplored leaves durin search. The priority queue has now been revised to address the exposed bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 16:27:15 -07:00
Nikolaj Bjorner
f8d04118d8 switch models for multiple box objectives. Feature request at codeplex issue 194, George Karpenov. Usage model is same as Pareto fronts you call check-sat multiple times until retrieving unsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 16:21:56 -07:00
Nikolaj Bjorner
52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Nikolaj Bjorner
9c55be14fb change print parameters to use hyphen instead of namespace dots 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 10:56:40 -07:00
Christoph M. Wintersteiger
7fe337daef Merge pull request #21 from wintersteiger/unstable 
Made the InterpolationContext public.
 2015-03-31 19:53:10 +02:00
Christoph M. Wintersteiger
1d9c9bcf7a Made the InterpolationContext public. 
Fixes #20
 2015-03-31 19:51:42 +02:00
Christoph M. Wintersteiger
637554dcf5 Merge pull request #18 from wintersteiger/unstable 
Bugfix for mpf is_normal.
 2015-03-30 10:29:54 +01:00
Christoph M. Wintersteiger
99ea0a8c19 Bugfix for mpf is_normal. 
Fixes #17
 2015-03-30 08:02:57 +01:00
Christoph M. Wintersteiger
5540d738ab Merge pull request #16 from wintersteiger/unstable 
Enabled test for OpenMP in Windows (for old and express versions of visu...
 2015-03-29 15:56:50 +01:00
Christoph M. Wintersteiger
0f03cd2ae0 Enabled test for OpenMP in Windows (for old and express versions of visual studio). 
Fixes #8
 2015-03-29 15:49:03 +01:00
Christoph M. Wintersteiger
4a0eb93f87 Merge pull request #15 from wintersteiger/unstable 
Integrating fixes for #10, #13, #14
 2015-03-29 14:44:21 +01:00
Christoph M. Wintersteiger
5911f788c3 Improved translation from reals to floats (fp.to_real). 
Fixes #14
 2015-03-29 14:39:47 +01:00
Christoph M. Wintersteiger
0ed16c09f9 Bugfix for fp.isNegative. 
Fixes #13
 2015-03-29 13:57:11 +01:00
Christoph M. Wintersteiger
690eb8eaca Bugfix for fp.isSubnormal. 
Fixes #10
 2015-03-29 13:31:44 +01:00
Nikolaj Bjorner
4bfe20647b remove tab in mk_util.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-27 02:43:21 -07:00
Nikolaj Bjorner
e456af142e fix complex.py example with power prompted by suggestion of smilliken 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-27 02:42:08 -07:00
NikolajBjorner
437a69b258 Update README 
change reference to license
 2015-03-26 11:44:52 -07:00
Leonardo de Moura
ae74b97c77 Move to MIT License 2015-03-26 11:44:49 -07:00
NikolajBjorner
3b16cfbd44 Update README 
change reference to license
 2015-03-26 11:43:51 -07:00
Leonardo de Moura
274f2b7a5d Move to MIT License 2015-03-26 11:43:41 -07:00
Christoph M. Wintersteiger
fc84461e31 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-03-26 14:49:45 +00:00
Christoph M. Wintersteiger
9cbf45f689 Added int to float conversion. 2015-03-26 14:48:55 +00:00
Nikolaj Bjorner
10cdbb881f enable canceling simplex on interrupt, investigating PDR inconsistency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-25 12:13:57 -07:00
Nikolaj Bjorner
0482e7fe72 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:46:28 -07:00
Nikolaj Bjorner
39892aae10 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:46:17 -07:00
Nikolaj Bjorner
8059a5a0b7 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:36:01 -07:00
Nikolaj Bjorner
86ac20faf6 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:35:44 -07:00
Nikolaj Bjorner
3c5897eea0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-03-25 11:25:12 -07:00
Nikolaj Bjorner
2aa91eee70 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:24:47 -07:00
Christoph M. Wintersteiger
a792790882 Fixed performance problems with enumeration sorts (Codeplex #190). 2015-03-25 18:08:56 +00:00
Christoph M. Wintersteiger
1c77ad00c3 Added accessors to enumeration sorts. Thanks to codeplex user steimann for suggesting this. 
(http://z3.codeplex.com/workitem/195)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-24 21:42:05 +00:00
Christoph M. Wintersteiger
b76d588c28 Renamed the soft_timeout option to just timeout. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-21 16:10:30 +00:00
Ken McMillan
be709802cd merging interpolation fix (issue 182) 2015-03-20 17:46:01 -07:00
Ken McMillan
47d33452c6 interpolation fix (issue 182) 2015-03-20 17:39:45 -07:00
Christoph M. Wintersteiger
ed81e3b9d8 Bugfix for BV-SLS initialization 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-20 17:07:32 +00:00
Nikolaj Bjorner
4145b92136 use of regions for AUX lemmas from pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-11 11:52:07 -07:00
Nikolaj Bjorner
f47cc70236 use of regions for AUX lemmas from pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-11 11:48:52 -07:00
Nuno Lopes
4ed062d54a fix missing memset in my previous commit 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-03-11 11:04:33 +00:00
Nikolaj Bjorner
695ce643f5 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-03-11 00:45:09 -07:00
Nikolaj Bjorner
755a259ea0 fix codeplex issue 188 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-11 00:44:56 -07:00
Nikolaj Bjorner
51267f3aba take into account that bound from optimization may create atom that clashes with inequality bound from term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-11 00:26:49 -07:00
nikolajbjorner
fe6af38d97 debugging assertion violation 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
 2015-03-10 20:57:01 -07:00
Nuno Lopes
44e647e72b add reallocate() function and use it in bit_vector and vector containers 
give a speedup of 1-4%

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-03-10 16:53:47 +00:00
Christoph M. Wintersteiger
55ca6ce44b Resurrected the dack* options. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 19:15:22 +00:00
Christoph M. Wintersteiger
6630994a3d + bug reporter 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 18:31:08 +00:00