mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
13947 commits 49 branches 53 tags 182 MiB
Commit graph

3302 commits

Author SHA1 Message Date
Nikolaj Bjorner
2749e547cf fix c example, remove more smtlib1 printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 18:14:24 -08:00
Nikolaj Bjorner
d7042c234f fix #1371 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 09:34:44 -08:00
Nikolaj Bjorner
2b3ee995ff fix #1375 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 09:03:52 -08:00
Nikolaj Bjorner
bfe6260c58 fix #1376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 08:39:20 -08:00
Nikolaj Bjorner
4520fafa8c fix #1368 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-26 19:13:35 -08:00
Nikolaj Bjorner
7d693a5f9f fix different bug reported on #1366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 20:01:14 -08:00
Nikolaj Bjorner
841c48e04d fix break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 18:24:45 -08:00
Nikolaj Bjorner
77b74ddb88 fix #1366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 17:55:20 -08:00
Nikolaj Bjorner
441c0de3c8 Merge branch 'master' of https://github.com/z3prover/z3 2017-11-23 11:17:58 -08:00
Nikolaj Bjorner
357b4b20fd fix #1365. Filter MBQI instantiations for as-array terms that lead the array theory to return unknown and therefore block further instantiations. as-array terms are at this point almost always created from internal model values so quantifier instantiations with these have little value, other than instantiations of other paraameters that may indepdendently help 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-23 11:17:41 -08:00
Nikolaj Bjorner
107bfb1438 print model-add in display method 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 21:26:07 -08:00
Nikolaj Bjorner
d520557ad9 fix #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 11:52:15 -08:00
Nikolaj Bjorner
c5f231acdf debugging #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 08:16:41 -08:00
Nikolaj Bjorner
33e8113c9e adding instrumentation to debug #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-20 16:51:17 -08:00
Nikolaj Bjorner
2f218b0bdc remove also cores as arguments to tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-19 12:18:50 -08:00
Nikolaj Bjorner
4bbece6616 re-organize proof and model converters to be associated with goals instead of external 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-18 16:33:54 -08:00
Nikolaj Bjorner
df6b1a707e remove proof_converter from tactic application, removing nlsat_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 23:32:29 -08:00
Nikolaj Bjorner
0d15b6abb7 add stubs for converting assertions, consolidate filter_model_converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 14:51:13 -08:00
Nikolaj Bjorner
2e6ae8cfd2 fix crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 23:06:05 -08:00
Nikolaj Bjorner
c3364f17fa fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 21:19:22 -08:00
Nikolaj Bjorner
c3f67f3b5f fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 21:17:00 -08:00
Nikolaj Bjorner
454e12fc49 update to vector format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-10 15:28:16 -08:00
Nikolaj Bjorner
75b8d10f48 add backtrack level to cuber interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 21:44:21 -08:00
Nikolaj Bjorner
9d3518736b fix #889 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 15:25:10 -08:00
Nikolaj Bjorner
53ed1bb862 fix segfault reported as part of #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 02:05:00 -08:00
Nikolaj Bjorner
fd49a0c89c added facility to persist model transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 00:05:52 -05:00
Murphy Berzish
2d25355611 Merge remote-tracking branch 'upstream/master' into issue1274-crash 2017-10-31 17:07:54 -04:00
Nikolaj Bjorner
24a44a0b29
Merge pull request #1336 from mtrberzi/clean-rewriter-patch 
fix rewriter in theory_str
 2017-10-31 08:45:14 -07:00
Nikolaj Bjorner
3de8c193ea implementing model updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-30 16:11:51 -05:00
Nikolaj Bjorner
29d643cc23
Merge pull request #1337 from mtrberzi/fix-length-testing 
Optimizations for length testing in theory_str
 2017-10-30 12:00:47 -07:00
Nikolaj Bjorner
34f24aee72 fix order of instantiation for recursive functions, #1274 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-30 13:50:31 -05:00
Murphy Berzish
6e31d9c3f5 internalize free var before iterating eqc in theory_str 2017-10-30 14:34:27 -04:00
Murphy Berzish
2ffffa9bed Merge remote-tracking branch 'upstream/master' into fix-length-testing 2017-10-30 14:04:10 -04:00
Murphy Berzish
a8d025f5b4 Merge remote-tracking branch 'upstream/master' into HEAD 2017-10-30 13:55:31 -04:00
Nikolaj Bjorner
b556f3ca42 fix stack overflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:41:29 -07:00
Nikolaj Bjorner
e4b595d490 add solver pool abstraction for Spacer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:10:20 -07:00
Nikolaj Bjorner
371f0b193c move min_cut, fix #1321 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 02:59:04 -07:00
Nikolaj Bjorner
637a0fa139 unused warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 08:49:25 -07:00
Nikolaj Bjorner
d67f3c1466 create proofs folder, move proof-post-order utility to proofs directory, fix regression with proofs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 03:08:56 -07:00
Nikolaj Bjorner
72c9134424 fixing regressions introduced when reducing astm proof dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 02:26:39 -07:00
Nikolaj Bjorner
f63439603d streamlining proof generation (initial step of removing ast-manager dependency). Detect error in model creation when declaring constant with non-zero arity. See #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-23 21:16:46 -07:00
Murphy Berzish
5e19e905fa Merge remote-tracking branch 'upstream/master' into fix-length-testing 2017-10-23 17:59:54 -04:00
Nikolaj Bjorner
1a859d4591 Merge branch 'master' of https://github.com/z3prover/z3 2017-10-21 18:56:50 -04:00
Nikolaj Bjorner
42fbe19814 fix #1316, segmentation fault when numeric value is not internalized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-21 18:56:36 -04:00
Nikolaj Bjorner
183bad69c8 Merge pull request #1315 from mtrberzi/str-equals-str-bug 
Add special case handling for theory_str constant backpropagation
 2017-10-21 15:47:14 -07:00
Murphy Berzish
ce1c8f7be2 remove debug code 2017-10-19 17:01:10 -04:00
Nikolaj Bjorner
c9f540b066 additional array functions exposed over API, ping #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-19 11:08:48 -07:00
Murphy Berzish
abdb41c5df add special case handling for string constant backpropagation in theory_str 
avoid a crash when asserting that a constant string is equal to itself
by not generating this assert in the first place
 2017-10-18 16:09:10 -04:00
Christoph M. Wintersteiger
0169417c64 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-16 16:40:39 +01:00
Nuno Lopes
82b25a0608 add move constructor to watch_list 2017-10-16 00:54:31 +01:00