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

334 commits

Author SHA1 Message Date
Titus Barik
2f0d2ec385
PYTHON_PATH should say PYTHONPATH. 2019-01-18 16:18:16 -08:00
Nikolaj Bjorner
038971c029
Revert "api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration." 2019-01-16 10:21:56 -08:00
Yatao Li
43ee345f01 dotnet deps hack for test 2019-01-15 03:06:36 +09:00
Yatao Li
209ebecb86 cmake: dotnet: example: dotnet.csproj is NETCOREAPP 2019-01-14 00:51:44 +08:00
Yatao Li
f0f9a16f85 cmake: dotnet: example: program -> Program 2019-01-14 00:22:51 +08:00
Yatao Li
08adc1bf97 ... 2019-01-13 23:15:40 +08:00
Yatao Li
8ebde41f35 dotnet: example: copy to binary dir before build 2019-01-13 22:45:05 +08:00
Yatao Li
5e79dba3d6 dotnet: move example project build to cmake 2019-01-13 00:03:37 +08:00
Yatao Li
17596fcc17 Merge remote-tracking branch 'upstream/master' 2019-01-12 15:01:28 +08:00
Huanyi Chen
19471f9fa3 Implement mini_quip 2019-01-04 18:30:02 -05:00
Huanyi Chen
83e3a79bd1 Remove testcase that takes long time to finish 2019-01-04 17:31:47 -05:00
Yatao Li
f5b874e0a3 Merge branch 'master' of https://github.com/Z3Prover/z3 2018-12-29 16:27:00 +08:00
Huanyi Chen
4b29b208ad Add few more testcases 2018-12-28 13:28:15 -05:00
Huanyi Chen
300e99b67a Make sure init is included when generalize 2018-12-28 13:21:40 -05:00
Huanyi Chen
b083c7546e Substitue Vars in queries 
Replace Vars that are representing primary inputs as "i#" when query
solvers.
 2018-12-28 13:21:35 -05:00
Bruce Mitchener
44bc00f13d Fix typos. 2018-12-23 21:58:57 -05:00
Nikolaj Bjorner
f591e0948a fix #1841 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-22 15:28:33 -08:00
Nikolaj Bjorner
498fa87993 seq rewriting fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-22 10:48:49 -08:00
Nikolaj Bjorner
2cc654081c
Merge pull request #1955 from waywardmonkeys/Z3_bool_to_bool 
Switch from using Z3_bool to using bool.
 2018-11-20 20:29:28 -08:00
Nikolaj Bjorner
37ef3cbeb2 add rc2 sample 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-20 14:32:01 -08:00
Bruce Mitchener
edf8ba44d1 Switch from using Z3_bool to using bool. 
This is a continuation of the work started by using stdbool and
continued by switching from Z3_TRUE|FALSE to true|false.
 2018-11-20 11:27:09 +07:00
Bruce Mitchener
56bbed173e Remove usages of Z3_TRUE / Z3_FALSE. 
Now that this is all using stdbool.h, we can just use true/false.

For now, we leave the aliases in place in z3_api.h.
 2018-11-20 00:25:37 +07:00
Nikolaj Bjorner
a85a612bae use old-fashined C for test_capi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-15 10:03:43 -08:00
Nikolaj Bjorner
51a0022450 add recfun to API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-27 11:41:18 -05:00
Nikolaj Bjorner
c802a0ac96 fix crash exposed by examples/dotnet/Program.cs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-20 14:32:59 -07:00
Nikolaj Bjorner
3ba2aa2672 regressions in examples/dotnet/Program.cs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-20 14:01:43 -07:00
Florian Pigorsch
326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Nikolaj Bjorner
7cc6d84e6f merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-19 21:02:15 -07:00
Nikolaj Bjorner
694a6a26c9 bump version, add double access 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-19 20:20:08 -07:00
Bruce Mitchener
372cab2c5b Fix some typos. 2018-10-17 22:49:39 +07:00
Bruce Mitchener
a76397d3b8 Refer to macOS rather than Mac OS / OSX. 2018-10-02 17:38:09 +07:00
Nikolaj Bjorner
2b35f1a924 quip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-16 13:14:41 -07:00
Nikolaj Bjorner
98dfd82765 adding quipie 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-15 21:55:49 -07:00
Nikolaj Bjorner
0232383191 mini IC3 sample 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-15 16:59:06 -07:00
Yatao Li
aae28bd0eb CI: update dotnet example to coreclr 2.0 2018-09-12 14:26:21 +08:00
Nikolaj Bjorner
94ffa3963e fix #1800 by converting large integers to strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-24 16:54:22 +02:00
rainoftime
bb534f6103 Add example of using z3's model construction C++ API 2018-07-10 11:16:20 +08:00
Nikolaj Bjorner
adb9a1c797 fix c 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-04 17:31:26 -07:00
Nikolaj Bjorner
03ed33ac02 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 15:31:26 -07:00
Nikolaj Bjorner
648a531950 update java example to bypass bit-rot 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 09:50:29 -07:00
Nikolaj Bjorner
46ea054784 merge get_value and get_ivalue that produced different results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 03:55:40 -07:00
Nikolaj Bjorner
9f3da32a77 remove interpolation from test_capi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-24 16:28:23 -07:00
Nikolaj Bjorner
50c93d1ad4 merge with 4.7.1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-22 17:10:36 -07:00
Joran Honig
e32dfad81e Add comments 2018-05-19 11:16:20 +02:00
Joran Honig
7d51353b8b Implement parallel python example 2018-05-19 11:13:53 +02:00
Nikolaj Bjorner
2aedaf315a fix removal bug, tune all-interval usage 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-09 16:32:38 +01:00
Nikolaj Bjorner
3736c0ae8b touch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-03 08:52:25 -07:00
Nikolaj Bjorner
8ecff9e5ee fix java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-03 08:04:10 -07:00
Nikolaj Bjorner
e98c808f47 fixing compilation errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-03 03:18:29 -07:00
Nikolaj Bjorner
bb041495e3 fix java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-02 14:00:37 -07:00