mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 19:47:52 +00:00
Code Activity
8238 commits 61 branches 52 tags 177 MiB
Commit graph

1737 commits

Author SHA1 Message Date
Nikolaj Bjorner
fa0c75e76e rename to core2 to avoid overloaded virtual 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 15:13:13 -08:00
Nikolaj Bjorner
a74d18a695 prepare for variable scoping and autarkies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-13 20:11:16 -08:00
Nikolaj Bjorner
7afbf8165e snapshot 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-12 01:36:44 -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
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
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
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
Nuno Lopes
9b54b4e784 fix vector<> to support non-POD types 
adjust code to std::move and avoid unnecessary/illegal
 2017-10-16 00:54:29 +01:00
Nikolaj Bjorner
4d1acadabb fix leaks reported in #1309 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-15 09:56:21 -07:00
Murphy Berzish
7b536e910e take shortcuts during binary search length testing when length is known from integer theory 2017-10-13 11:39:33 -04:00
Nikolaj Bjorner
1a6f8c2fad working on parallel solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 16:35:05 -07:00
Nikolaj Bjorner
cae414e575 fixes for #1296, removing COMPILE_TIME_ASSERT 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-09 13:59:44 -07:00
Christoph M. Wintersteiger
800fa3d246 Added bv_sort_ac=true to asserted_formulas::m_rewriter 2017-10-09 19:18:41 +01:00
Christoph M. Wintersteiger
5819e38606 whitespace 2017-10-09 19:17:44 +01:00
Nikolaj Bjorner
356835533a clean up debug output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 10:47:15 -07:00
Nikolaj Bjorner
c1b243a8e3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 19:24:30 +01:00
Nikolaj Bjorner
6df628edc7 pin elements in expr2depth 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 11:45:29 +01:00
Nikolaj Bjorner
eac659f748 deal with empty set of post-orders 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 11:34:14 +01:00
Nikolaj Bjorner
e0e2397566 missing setup datatypes for QF_DT 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-01 19:40:30 -07:00
Nikolaj Bjorner
05428314be fix #1276 related crashes for re-sumption after cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-01 15:13:43 -07:00
Nikolaj Bjorner
8ff8c6433b fix #1277 fix #1278 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-30 10:15:27 -07:00
Nikolaj Bjorner
e507a6ccd1 adding incremental cubing from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-28 09:06:17 -07:00