mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
17861 commits 49 branches 53 tags 182 MiB
Commit graph

4108 commits

Author SHA1 Message Date
Nikolaj Bjorner
e36eba1168 added cardinality solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-27 09:58:23 -08:00
Nikolaj Bjorner
cb10a618a1 Merge branch 'master' of https://github.com/z3prover/z3 into opt 2016-12-26 10:19:51 -08:00
Nikolaj Bjorner
7210f6e912 local changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-26 10:19:48 -08:00
Nikolaj Bjorner
8dde60f634 initialize watch in assign_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-26 10:18:55 -08:00
Nikolaj Bjorner
2bd29548da improve parser error message over API, streamline names of statistics for arithmetic solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-25 17:27:56 -08:00
Nikolaj Bjorner
46df31babf Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-22 20:54:14 -08:00
Nikolaj Bjorner
1787fa8296 remove redundant disjunction in compilation of at-most-1 constraints, log mutexes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 20:54:09 -08:00
Nikolaj Bjorner
a444a33c30 updated encodings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 17:45:21 -08:00
Murphy Berzish
0a6c23148f fix empty vector edge case in binary search 2016-12-22 19:33:38 -05:00
Murphy Berzish
2dc9b486d3 theory_str binary search heuristic WIP 2016-12-22 19:17:42 -05:00
Nikolaj Bjorner
f52baf1e17 fix build again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:48:43 -08:00
Nikolaj Bjorner
4bcf1bf2f6 fix debug build, unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:44:49 -08:00
Nikolaj Bjorner
df492e200f merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:04:02 -08:00
Nikolaj Bjorner
8d18fd075e remove sources for unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 09:54:45 -08:00
Murphy Berzish
df63b62763 fix vector manip bug in theory case split 2016-12-20 17:32:51 -05:00
Murphy Berzish
ab0fcc42f9 theory case split heuristic 2016-12-20 16:21:07 -05:00
Murphy Berzish
a04bc9974b theory case split WIP 2016-12-20 11:14:42 -05:00
Murphy Berzish
94762d276d add string constant cache to theory_str and associated param 2016-12-18 18:47:38 -05:00
Murphy Berzish
e5d3e425f1 theory_str caching of all string constants 2016-12-18 15:23:05 -05:00
Murphy Berzish
e85f9d33c4 add "legacy" support for theory case splits 
this replicates what was done in theory_str to add axioms excluding each
pair of literals from being assigned True at the same time;
no new heuristics are being used in smt_context (yet)
 2016-12-16 15:50:03 -05:00
Murphy Berzish
dd8cd8199b theory_str refcount debug messages and beginning theory case split 2016-12-16 14:37:34 -05:00
Murphy Berzish
67e7307777 add cut var debug info, wip 2016-12-14 15:00:17 -05:00
Murphy Berzish
27a2c20c1c add more parameters for theory_str 2016-12-13 19:38:40 -05:00
Murphy Berzish
bced5828f7 theory_str parameters 2016-12-13 17:20:58 -05:00
Murphy Berzish
f5bc17b864 theory_str params module, WIP 2016-12-13 16:12:57 -05:00
Nikolaj Bjorner
c1480b4389 handle model generation from issue #748. Deal with warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-12 00:40:52 +01:00
Nikolaj Bjorner
dea3b8ddf7 address warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 13:14:36 +01:00
Nikolaj Bjorner
fe10f2d244 address #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 07:51:16 +01:00
Murphy Berzish
09053b831d enforce nonempty string constraint on refreshed nonempty string vars 2016-12-09 17:23:39 -05:00
Murphy Berzish
e9411e5b8c explicitly re-introduce string axioms on refreshed string theory vars 
this fixes at least one case (kaluza/unsat/big/9650.smt2) where a string
could have a negative length value due to a constraint that went out of scope
 2016-12-09 17:12:29 -05:00
Murphy Berzish
737565180f disable stronger arrangements in theory_str for now 2016-12-09 16:55:34 -05:00
Christoph M. Wintersteiger
4c664f1c05 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-09 15:03:36 +00:00
Christoph M. Wintersteiger
16b32ecf12 Bugfix for special-case handling in fp.fma. 
Thanks to Florian Schanda for reporting this bug.

(+reversed accidental debug code commit).
 2016-12-09 15:03:31 +00:00
Nikolaj Bjorner
a17e957362 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-09 15:32:26 +01:00
Nikolaj Bjorner
acba529bce fix bug in encoding of axioms for indexof. Issue #806 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 15:32:15 +01:00
Christoph M. Wintersteiger
56b1a8b086 Bugfix for special-case handling in fp.fma. 
Thanks to Florian Schanda for reporting this bug.
 2016-12-09 13:43:05 +00:00
Murphy Berzish
515cd4a3f3 add boolean case split in theory_str::solve_concat_eq_str 2016-12-08 14:49:38 -05:00
Murphy Berzish
7b0aaf8745 boolean case split theory_str concat_eq remaining cases 2016-12-06 16:22:42 -05:00
Murphy Berzish
225b527d58 boolean case split theory_str process_concat_eq_type2 2016-12-06 16:09:38 -05:00
Murphy Berzish
b57f04e2d2 optimize generate_mutual_exclusion in theory_str to make only half as many subterms 2016-12-06 12:59:40 -05:00
Murphy Berzish
da61c99f9e experimental boolean case split in theory_str process_concat_eq_type1 WIP 2016-12-06 12:52:48 -05:00
Murphy Berzish
938dcaa669 Merge branch 'develop' of github.com:/mtrberzi/z3 into develop 2016-12-05 20:17:44 -05:00
Murphy Berzish
be9cb8db82 regex tracing theory_str 2016-12-05 20:17:43 -05:00
Murphy Berzish
35ad68d9b5 assert stronger arrangements theory_str 2016-12-05 15:13:48 -05:00
Murphy Berzish
406b622f59 Revert "testing term generation refactor in theory_str::check_length_const_string" 
This reverts commit edf151c9a0.
 2016-12-01 15:19:51 -05:00
Murphy Berzish
b020c71f8a Revert "ref_vector refactoring in theory_str::check_length_concat_concat" 
This reverts commit 599cc1e75d.
 2016-12-01 15:19:51 -05:00
Murphy Berzish
548f635f7e Revert "experimental non-reuse of XOR vars in theory_str" 
This reverts commit fd1bf65b64.
 2016-12-01 15:19:50 -05:00
Murphy Berzish
10c0d94cf2 Revert "refactor theory_str::check_length_concat_var" 
This reverts commit 170e2b4e2a.
 2016-12-01 15:19:50 -05:00
Nuno Lopes
42b26c63e5 make a few functions static 2016-12-01 14:01:20 +00:00
Murphy Berzish
170e2b4e2a refactor theory_str::check_length_concat_var 2016-11-30 19:41:00 -05:00