mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
10838 commits 23 branches 48 tags 157 MiB
Commit graph

10838 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alcides Fonseca
a785ffe0ba Updated deepcopy to the latest Python API 2019-01-25 14:42:22 +00:00
Nikolaj Bjorner
d3d392da41 adding maxlex, delay mk_true() calls in goal2sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 21:36:40 -08:00
Nikolaj Bjorner
b4f4a1f316 adding maxlex, throttle use of asymmetric literal addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 19:47:50 -08:00
Nikolaj Bjorner
ad81fee118 adding maxlex, throttle use of asymmetric literal addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 19:26:44 -08:00
Nikolaj Bjorner
8da1d6070b throttle big-reductions #2101 #2098 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 14:00:56 -08:00
Nikolaj Bjorner
498864c582 adding dump facility for cancelation #2095, easing dimacs in/out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 12:21:23 -08:00
Nikolaj Bjorner
f7746e2284 address perf #2098 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-23 16:58:00 -08:00
Nikolaj Bjorner
9c07167ff8 add new pyg file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-23 16:06:44 -08:00
Nikolaj Bjorner
8e5c1fcfd1 make context_solve configurable and exposed as top-level tactic parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-23 16:06:25 -08:00
Nikolaj Bjorner
412eee0dac throttle number of rounds of ba simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-22 18:12:39 -08:00
Nikolaj Bjorner
f9195c77a7 remove not-handled clause from mod with non-numerals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-22 09:46:04 -08:00
Nikolaj Bjorner
49a51a0757 fix #2096, introduced when fixing #2082 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-22 07:06:40 -08:00
Nikolaj Bjorner
6bd87f837a fix Boolean argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 14:14:26 -08:00
Nikolaj Bjorner
8566d88b99 remove validation assert 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 12:49:04 -08:00
Nikolaj Bjorner
785fe2f6f7 add main remaining updates from #1815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 12:43:05 -08:00
Nikolaj Bjorner
5cdbb1f7be this is still used 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:25:34 -08:00
Nikolaj Bjorner
9dd41ba554 remove offending assert, disable assembly-info for dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:13:03 -08:00
Nikolaj Bjorner
cabe0ee447 integrating additional changes from @yatli pull request #1815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 10:51:44 -08:00
Nikolaj Bjorner
37d9e6d811 incrementally adding files from dotnet core pull request from @yatli 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 10:40:11 -08:00
Nikolaj Bjorner
1efbc25b3b Merge branch 'master' of https://github.com/z3prover/z3 2019-01-18 18:09:22 -08:00
Nikolaj Bjorner
0b7021d2c8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 18:09:19 -08:00
Nikolaj Bjorner
dc5af2d969
Merge pull request #2088 from barik/patch-1 
PYTHON_PATH should say PYTHONPATH.
 2019-01-18 18:07:46 -08:00
Titus Barik
2f0d2ec385
PYTHON_PATH should say PYTHONPATH. 2019-01-18 16:18:16 -08:00
Nikolaj Bjorner
c45ab6efed add setting to dump intermediary models #2087 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 15:12:08 -08:00
Nikolaj Bjorner
4caadc6519 add note about libgomp dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 10:13:04 -08:00
Nikolaj Bjorner
947fe2ff9c fix datatype occurs check bug reported by Gerhard Schellhorn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-17 16:35:07 -08:00
Nikolaj Bjorner
442e47dfce fix datatype occurs check bug reported by Gerhard Schellhorn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-17 16:34:26 -08:00
Nikolaj Bjorner
f2e636c598 record simplified input clauses as lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 16:37:21 -08:00
Nikolaj Bjorner
247980c5a2 don't assign already assigned literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 11:41:32 -08:00
Nikolaj Bjorner
e94aa5bb1d
Merge pull request #2084 from Z3Prover/revert-1815-master 
Revert "api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration."
 2019-01-16 10:22:14 -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
Nikolaj Bjorner
16c15d53a9
Merge pull request #1815 from yatli/master 
api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration.
 2019-01-16 10:16:26 -08:00
Nikolaj Bjorner
e01a668da0 coordinate drat with clause removal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 02:29:33 -08:00
Nikolaj Bjorner
b33f5f879e fix another bug reported by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 17:57:11 -08:00
Nikolaj Bjorner
3298486136 don't reach max conflicts if state is inconsistent 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:40:38 -08:00
Nikolaj Bjorner
5328454c77 const 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:37:23 -08:00
Nikolaj Bjorner
161c83795f remember inconsistent states when cloning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:34:55 -08:00
Nikolaj Bjorner
65bd427e46 neatify statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:48:48 -08:00
Nikolaj Bjorner
f238460597 neatify statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:45:04 -08:00
Nikolaj Bjorner
ed7cac8cc0 neatify logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:42:13 -08:00
nilsbecker
279413412d preventing operations during MBQI search from being logged 2019-01-15 01:09:44 +01:00
Nikolaj Bjorner
b11ec3bfbf merge sat_tactic from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:17:42 -08:00
Nikolaj Bjorner
ee07008fb9 import files from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:04:46 -08:00
Nikolaj Bjorner
54a125063b remove produce interpolants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:00:25 -08:00
Nikolaj Bjorner
e954f59052 ensure that solver objects have timeout/rlimit/ctrl-c exposed as possible parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 13:50:17 -08:00
nilsbecker
bfb554c0b8 logging sorts of quantified variables 
logging proof objects seperately form regular terms
renaming inst-possible -> inst-discovered
 2019-01-14 21:28:06 +01:00
Nikolaj Bjorner
a686aa7f56 produce binary clauses for DRAT for units produced by probing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 10:56:10 -08:00
Yatao Li
43ee345f01 dotnet deps hack for test 2019-01-15 03:06:36 +09:00
Nikolaj Bjorner
0b84c60886 fix another bug uncovered by Dunlop, prepare grounds for equality solving within NNFs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 01:25:25 -08:00
Yatao Li
58e8b2b8d5 Dockerfile: update ubuntu 14.04 image with cmake 3.12 2019-01-14 14:02:58 +08:00