mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 10:19:23 +00:00
Code Activity
9694 commits 46 branches 52 tags 178 MiB
Commit graph

9694 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
74efe253a0 fix header files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:09:23 -07:00
Nikolaj Bjorner
d47e06732c bmc improvements, move fd_solver to self-contained directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:02:15 -07:00
Nikolaj Bjorner
e041ebbe80 bmc improvements, move fd_solver to self-contained directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:00:49 -07:00
Nikolaj Bjorner
fd09b1a7d0 Merge branch 'master' of https://github.com/z3prover/z3 2018-08-03 22:14:28 -07:00
Nikolaj Bjorner
c247abfc65 prepare js output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-03 22:13:25 -07:00
Nikolaj Bjorner
f306f75e36 harness internalization and API for #1776 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-02 20:18:27 -07:00
Nikolaj Bjorner
51610842b9 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-02 10:41:53 -07:00
Nikolaj Bjorner
7bd4a313dd expr utilities for pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-02 10:41:07 -07:00
Nikolaj Bjorner
fed977b492 fix #1782 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-02 10:08:16 -07:00