3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Commit graph

10372 commits

Author SHA1 Message Date
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 0a6a76734a docker: ubuntu 14.04 dotnet source fix 2019-01-13 00:08:32 +08:00
Yatao Li 5e79dba3d6 dotnet: move example project build to cmake 2019-01-13 00:03:37 +08:00
Yatao Li 55f92f3658 dotnet: remove stale packages before pack; relay cmake config generator expression into msbuild property.. 2019-01-12 21:33:09 +08:00
Yatao Li 4b3189f3e2 dotnet: identifies arch-specific native libraries 2019-01-12 20:04:44 +08:00
Yatao Li 3767c311aa FindDotnet: generator expression IF is not available for older cmake versions 2019-01-12 19:35:08 +08:00
Yatao Li e5f65263bb dotnet: reigster local repo for nupkg 2019-01-12 19:22:38 +08:00
Yatao Li 53eaab4709 dotnet: update build scripts 2019-01-12 17:38:24 +08:00
Yatao Li 17596fcc17 Merge remote-tracking branch 'upstream/master' 2019-01-12 15:01:28 +08:00
Yatao Li ffd26e5a56 .net: remove net35 related build props; drop src/api/dotnet/core 2019-01-12 15:01:05 +08:00
Nikolaj Bjorner 63d480fd92 fix cnf check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-11 21:17:39 -08:00
Nikolaj Bjorner b8d18c6c6d speed-up handling of cnf input to inc_sat_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-11 20:52:19 -08:00
Nikolaj Bjorner 9bd4050e0c use ref-vector for shared occurrences to avoid hash-table overhead
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-11 13:43:39 -08:00
Nikolaj Bjorner f8f3549c1c Merge branch 'master' of https://github.com/z3prover/z3 2019-01-11 10:13:14 -08:00
Nikolaj Bjorner 1a4636518c Merge branch 'master' of https://github.com/z3prover/z3 2019-01-11 04:58:47 -08:00
Nikolaj Bjorner f1c3e1aa77 fix #2077
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-11 04:58:40 -08:00
Nikolaj Bjorner 434eb25004 add useful div lemma for case #2079
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-10 17:20:01 -08:00
Nikolaj Bjorner 6e60926cc3 fix drat output for elim_eqs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-10 15:25:10 -08:00
Nikolaj Bjorner b12c1b1cba set a throttle on ala
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-10 13:38:45 -08:00
Nikolaj Bjorner 7fc349b622 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-10 12:08:44 -08:00
Nikolaj Bjorner 59b0b56b42 add checkpoints to blocked clause elimination to handle timeouts, #2080
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-10 12:08:38 -08:00
Nikolaj Bjorner 1e4662e0bc
Merge pull request #2073 from waywardmonkeys/emscripten-no-debug
Define NO_Z3_DEBUGGER for emscripten builds.
2019-01-10 11:39:19 -08:00
Nikolaj Bjorner efaab6d8fd have sat cleaner use a fixed-point
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-10 11:38:35 -08:00
Nikolaj Bjorner 9c318ed304 fix #2076, add option to handle .cnf files into dimacs parser
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-09 15:43:45 -08:00
Nikolaj Bjorner b63a0e31d3 fix regression from #2061 breaking #2074
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-07 16:30:04 -08:00
Nikolaj Bjorner 14f3ff0b63 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-07 09:00:21 -08:00
Nikolaj Bjorner cec34c745a defer blocking propagation until all properties of literal have been axiomatized. Deals with seq part of #2071
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-07 09:00:11 -08:00
Bruce Mitchener d757c342d5 Define NO_Z3_DEBUGGER for emscripten builds. 2019-01-07 23:13:09 +07:00
Nikolaj Bjorner bde4ddd861 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-06 20:20:55 -08:00
Nikolaj Bjorner 6113149138 fix #2060. Code comment was right, code wasn't. Code comment and code could also be tuned
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-06 20:20:34 -08:00
Nikolaj Bjorner dc94d83c2e
Merge pull request #2051 from waywardmonkeys/wasm-builds
Allow emscripten builds.
2019-01-06 18:56:32 -08:00
Nikolaj Bjorner 2486971094
Merge pull request #2065 from waywardmonkeys/improve-ios-support
Define NO_Z3_DEBUGGER for iOS builds.
2019-01-06 18:56:03 -08:00
Nikolaj Bjorner 8ad2f70aaa
Merge pull request #2066 from waywardmonkeys/const-str-hashtable
Let str_hashtable store `const char*`.
2019-01-06 18:55:32 -08:00
Nikolaj Bjorner ea48d0a95a add set method to iterator, #2068, a set method to the vector template was also added
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-06 18:55:00 -08:00
Nikolaj Bjorner a87f7a14d3 ever so gentle slap over the fingers for not using real regular expressions, #2058
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-06 13:46:04 -08:00
Nikolaj Bjorner 6f6880812b Merge branch 'master' of https://github.com/z3prover/z3 2019-01-06 13:01:19 -08:00
Nikolaj Bjorner 71e239c08e fix #2061
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-06 11:49:47 -08:00
Bruce Mitchener 7e1ce2a16c Define NO_Z3_DEBUGGER for iOS builds.
This is defined because we can't call `system` (via `invoke_gdb`)
on iOS and related platforms.
2019-01-06 12:16:33 +07:00
Bruce Mitchener a06bc49710 Let str_hashtable store const char*.
This removes some boilerplate const casting.
2019-01-06 12:15:31 +07:00
Nikolaj Bjorner ed4223af94
Merge pull request #2064 from varming/cv/utf8
Specify UTF-8 encoding in python scripts
2019-01-06 12:58:37 +08:00
Carsten Varming e1a9154555 Specify UTF-8 encoding in python build scripts 2019-01-05 13:48:15 -05:00
Nikolaj Bjorner e770f37f52
Merge pull request #2062 from Chen-Huanyi/master
Implement QUIP variant in mini_quip
2019-01-05 08:05:42 +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
Nikolaj Bjorner fb397cbe25 remove incorrect assertion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-04 08:18:40 -08:00
Nikolaj Bjorner 425c47bc81 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-04 07:47:00 -08:00
Nikolaj Bjorner 0d400a5ad6 fix bit2bool bug reported by Jianying Li
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-04 07:46:53 -08:00