mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 02:41:52 +00:00
Code Activity
9703 commits 23 branches 48 tags 156 MiB
Commit graph

9703 commits

This branch
This branch
All branches
Author SHA1 Message Date
Yatao Li 461c32e11e ... 2018-09-12 16:07:45 +08:00
Yatao Li aae28bd0eb CI: update dotnet example to coreclr 2.0 2018-09-12 14:26:21 +08:00
Yatao Li 20c128d3fa replace LIST FILTER with handrolled implementation to cancel cmake v3.6+ dependency 2018-09-12 01:28:42 +08:00
Yatao Li 5474e1675a CI: Dockerfile: install curl before dotnet 2018-09-12 00:53:10 +08:00
Yatao Li 5fdf3ff799 CI: Dockerfile: use curl instead of wget 2018-09-12 00:37:06 +08:00
Yatao Li 5bc7a5d673 CI: configure dotnet via docker 2018-09-12 00:29:58 +08:00
Yatao Li 44e21d9948 CI: 3rd attempt: trying to incorporate .net sdk into travis build 2018-09-11 23:37:26 +08:00
Yatao Li 538272d2d5 CI: 2nd attempt: trying to incorporate .net sdk into travis build 2018-09-11 23:32:29 +08:00
Yatao Li a162a60d9c CI: trying to incorporate .net sdk into travis build 2018-09-11 23:16:45 +08:00
Yatao Li e787c01d41 ... 2018-09-10 16:40:22 +08:00
Yatao Li 5c81559f71 api: dotnet: copy native binary to output folder only for non-netstandard, non-netcoreapp TFMs. 2018-09-10 16:02:09 +08:00
Yatao Li 534de98ff3 fine-tune native assembly packing 2018-09-10 15:05:22 +08:00
Yatao Li 969a922145 api: dotnet: install nuget package and register local repo; xplat native assembly detection 2018-09-10 13:19:48 +08:00
Yatao Li 90890e46a9 api: dotnet: FindDotnet.cmake now handles 'REQUIRED' option. 2018-09-10 09:34:28 +08:00
Yatao Li 232a88101b
api: dotnet: ADD_DOTNET should be uppercased. 2018-09-10 08:57:28 +08:00
Yatao Li c77af6b75f api: dotnet: switch to multi-targeting project and modern cmake-dotnet 
integration.
 2018-09-10 02:49:22 +08:00
Nikolaj Bjorner 1e11b62bc6
Merge pull request #1809 from agurfinkel/deep_space 
Fix performance regression
 2018-09-04 20:35:46 -07:00
Arie Gurfinkel f67346d16e Fix is_infty_level to treat 2^16-1 as infinity 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 5d2f682f7a Enable proof mode in add_cover 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 7bff74dec0 Minor pass on synchronize transform 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 24044429a7 Rename cache to m_cache 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 0516e6f21f Integrating synchronize pass 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 8400122596 mk_synchronize rule transformation 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 3a01fd791b Replace rule API 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 0035d9b8cb Background external invariants 
Background external invariants are constraints that are assumed to be
true of the system. This commit introduces a mode in which
background invariants are used only duing inductive generalization
and lemma pushing, but not during predecessor computation.

It is believed that this will be more efficient used of background
external invariants since they will not be able to disturb how
predecessors are generalized and computed.

Based on a patch by Jorge Navas
 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 533e9c5837 Expand equality literals when eq_prop is disabled 
When equality propagation is disabled for arithmetic,
equality atoms are expanded into inequality for potentially
better generalization with interpolation
 2018-09-04 21:49:59 -04:00
Nikolaj Bjorner e8a78ec696 remove std::max for #1752 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-03 10:24:01 -07:00
Nikolaj Bjorner 85e7b18451 fix name to divisible, guard under smtlib2_compliant as sugguested in #1757 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-01 18:22:10 -07: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
Nikolaj Bjorner d6298b089d
Merge pull request #1799 from c-cube/fix-union-find 
fix(union-find): keep values and representative in consistent order
 2018-08-18 05:51:01 -07:00
Simon Cruanes 5141f05e6d fix(union-find): keep values and representative in consistent order 
the merge handlers should be called with r1,r2,v1,v2 or r2,r1,v2,v1
but not a mix
 2018-08-17 14:58:44 -05:00
Nikolaj Bjorner 12f9336fec disable unused macros 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-15 22:44:07 -07:00
Nikolaj Bjorner 056ec2d5c4 remove inc file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-15 22:27:07 -07:00
Nikolaj Bjorner 2b2f193f2b remove dependency on ARRAYSIZE for issue #1616 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-15 22:26:14 -07:00
Nikolaj Bjorner 95963f71f4 fix bug introduced in fix of #1798 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-11 17:18:11 -07:00
Nikolaj Bjorner d270df67f7 Merge branch 'master' of https://github.com/z3prover/z3 2018-08-11 13:33:35 -07:00
Nikolaj Bjorner 96d3b98a44 fix #1783, wronge clausification of negated pb inequalities. Signs were ignored 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-11 13:33:09 -07:00
Nikolaj Bjorner 8de8c4cade fix #1798 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-11 11:41:06 -07:00
Nikolaj Bjorner a13b6a99d6
Merge pull request #1797 from c-cube/conf-dt-lazy-split 
expose the configuration param for datatype case splits
 2018-08-10 16:09:13 -07:00
Simon Cruanes 0aca1ad4c1 feat(smt/dt): expose the configuration param for datatype case splits 2018-08-10 17:37:23 -05:00
Nikolaj Bjorner d5b2059fdb
Merge pull request #1796 from mtrberzi/issue1726-2 
fix contains/indexof heuristic precondition and re.loop handling
 2018-08-07 16:03:13 -07:00
Murphy Berzish c65dbaea90 z3str3: fix contains-indexof precondition 2018-08-07 15:12:37 -04:00
Murphy Berzish 7a84486df2 Merge branch 'master' into develop 2018-08-07 12:57:02 -04:00
Nikolaj Bjorner 8b4e1c1209 fix #1793 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-06 18:13:26 -07:00
Nikolaj Bjorner 84c7df75d6 record statistics setting in config_params so that fp engine can access them, fix serialization bug when check-assumptions returns unsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-06 16:21:27 -07:00
Nikolaj Bjorner 24b6ff90cd Merge branch 'master' of https://github.com/z3prover/z3 2018-08-05 13:49:42 -07:00
Nikolaj Bjorner a3c692c05f fix include paths 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 13:49:26 -07:00
Nikolaj Bjorner a33a1ab92b
Merge pull request #1790 from NikolajBjorner/master 
bmc improvements, move fd_solver to self-contained directory
 2018-08-05 10:35:39 -07:00
Nikolaj Bjorner 60110bb289 reduce dependencies in CMakeLists file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:34:13 -07:00
Nikolaj Bjorner 6400da63ab missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:10:52 -07:00