mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity
1822 commits 24 branches 48 tags 158 MiB
Commit graph

1822 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
d91a114b80 Java API: removed Z3_get_param_value as in other APIs. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-22 16:29:13 +01:00
Nuno Lopes
ae6121525a Z3Py: improve readability of Z3 exceptions 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-22 13:57:07 +01:00
Nikolaj Bjorner
1059d226e4 add default statement instead of incomplete cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 13:25:19 -07:00
Nikolaj Bjorner
d77d6c6648 update parameter checking for doubles, and fix error reporting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 13:24:31 -07:00
Nikolaj Bjorner
f3a04734d9 add pretty printing to SMT2 from solver, add get_id to Ast objects 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 12:48:49 -07:00
Nikolaj Bjorner
3ecffaa1e5 remove unused and always failing get_param_value function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 11:12:50 -07:00
Nikolaj Bjorner
340f765983 make sure that parameters are appended such that multiple paramters are not ignored on the solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 09:35:32 -07:00
Nikolaj Bjorner
983f9abf15 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-21 09:11:53 -07:00
Nikolaj Bjorner
7f04529080 validate types of parameter values that get set globally 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 09:11:38 -07:00
Christoph M. Wintersteiger
de9f6d3e11 FPA name clash fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-21 16:52:16 +01:00
Christoph M. Wintersteiger
f4a015602c Disable FPA-min/max because of name clashes with user-defined functions. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-18 13:43:13 +01:00
Nikolaj Bjorner
fe4a8b44a5 revert some changes to how 'out' parameters are annotated on API calls. Retain the 'out' annotation for so-called managed out parameters. The data-type examples in managed API fail with the out parameter annotation as no memory is allocated on instances of out parameters, other than the interpolation APIs that are new 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-16 22:40:52 -07:00
Nikolaj Bjorner
7767a23626 improve error messages on incorrect parameter passing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-15 21:37:37 -07:00
Nikolaj Bjorner
097f4c3a34 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-15 18:35:55 -07:00
Nikolaj Bjorner
c739d803ab include model/proof/unsat_core as part of model parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-15 13:42:56 -07:00
Nikolaj Bjorner
136b172b5a move parameter validation for when solver object is actually crated 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-15 09:58:54 -07:00
Nikolaj Bjorner
92166eb5cb deal with warning for unused parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-14 13:12:40 -07:00
Nikolaj Bjorner
10c5ed6344 add parameter validation in two remaining local cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-14 11:29:05 -07:00
Christoph M. Wintersteiger
0e4e72b1bc Added new params.Add functions to the .NET and Java APIs. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-14 13:22:12 +01:00
Nikolaj Bjorner
4d1f3ca087 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-11 09:46:14 -07:00
Nikolaj Bjorner
e8b04790cf fix build by disabling removed API call from interpolation sample 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-11 09:43:55 -07:00
Christoph M. Wintersteiger
0451a605f4 Interpolation example bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-10 13:05:11 +01:00
Christoph M. Wintersteiger
342a23cfcb C++ API bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-10 13:00:41 +01:00
Christoph M. Wintersteiger
3e7c95db6b Interpolation API bugfixes 
Added Interpolation to the Java API

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-10 12:34:17 +01:00
Christoph M. Wintersteiger
490e931f39 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-10 11:41:28 +01:00
Christoph M. Wintersteiger
9b8406c717 Resolved interpolation API issues. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-10 11:41:21 +01:00
Nikolaj Bjorner
25ef1db874 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-09 10:19:01 -07:00
Nikolaj Bjorner
bcd2d935a9 enable modular parameters from the parser 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-09 10:18:46 -07:00
Christoph M. Wintersteiger
1c1351a064 Interpolation .NET API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-09 18:11:42 +01:00
Christoph M. Wintersteiger
503ad78bf3 Interpolation API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-09 18:08:07 +01:00
Nikolaj Bjorner
25b974306d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-08 18:44:54 -07:00
Nikolaj Bjorner
f0c63e56f3 make module parameter validation and adjustment more flexible: you can use both module qualifiers and unqualified parameters from the API at local scope 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 16:27:40 -07:00
Nikolaj Bjorner
8cf21dc242 fix tactic parameter checking to API, deal with compiler warnings in api_interp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 13:47:55 -07:00
Nikolaj Bjorner
11740dfcee Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-08 13:21:48 -07:00
Nikolaj Bjorner
b8b5c4d5b4 disable blanket validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 13:21:34 -07:00
Christoph M. Wintersteiger
ca83f47be6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-08 21:03:01 +01:00
Christoph M. Wintersteiger
b03a9d3f0a Interpolation API: infrastructure fixes and .NET API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-08 21:01:27 +01:00
Nikolaj Bjorner
335f9a9be1 add parameter validation to tactic parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 10:55:24 -07:00
Christoph M. Wintersteiger
4370d40dd8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-08 10:56:20 +01:00
Nikolaj Bjorner
1bb4d52cb8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-07 15:38:57 -07:00
Nikolaj Bjorner
d6964226c7 indentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-07 15:38:44 -07:00
Nikolaj Bjorner
4ea3ed7e27 ensure parameters are updated and ensure that global use of auto-config is not obscured by smt.auto-config scoping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-07 11:00:45 -07:00
Christoph M. Wintersteiger
7fc95aff3c Minor cleanliness fix. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-07 14:24:28 +01:00
Nikolaj Bjorner
c7e27fb2d9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-06 15:43:38 -07:00
Nikolaj Bjorner
8438ac6e21 fix internalization bug when bit2bool is applied to numeral 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-06 15:43:24 -07:00
Christoph M. Wintersteiger
a77694d9a8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-06 18:10:13 +01:00
Christoph M. Wintersteiger
3222ecd992 tabs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-06 18:09:40 +01:00
Christoph M. Wintersteiger
30b72809c5 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-06 18:07:07 +01:00
Christoph M. Wintersteiger
929880e4fd Fix for bogus runtime reports on Linux. Thanks to Vladimir Klebanov for reporting this one. 2014-10-06 18:06:36 +01:00
Nikolaj Bjorner
6d8daacdec fix check for satisfiability before calling final_check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-06 08:35:05 -07:00