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

378 commits

Author SHA1 Message Date
Nikolaj Bjorner
498fa87993 seq rewriting fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-22 10:48:49 -08:00
Nikolaj Bjorner
7b2590c026 fix is-unit test in seq rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-21 17:08:33 -08:00
Nikolaj Bjorner
52910fa465 fix #1937 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-14 11:31:39 -08:00
Nikolaj Bjorner
b02c698284 align variable names with dimacs input 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-08 16:52:10 -08:00
Nikolaj Bjorner
3c1c3d5987 fix #1908 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-30 14:15:29 -05:00
Nikolaj Bjorner
1cb3f7c792 fixing #1520 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-28 18:03:13 -07:00
Nikolaj Bjorner
60bb02b709 updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-26 15:31:49 +01:00
trinhmt
54a9482716
Merge pull request #8 from Z3Prover/master 
merge with Z3Prover/z3
 2018-06-27 18:10:54 +08:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:23:04 -07:00
Thai Trinh
aacb7289be merge with Z3Prover/master 2018-06-25 19:44:46 +08:00
Nikolaj Bjorner
c3b27903f8 fix #1677 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 11:22:01 -07:00
Nikolaj Bjorner
74292a48e5 change order of concatentation for empty string, #1595 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-26 09:08:34 +02:00
Nikolaj Bjorner
0b4e54be38 fix #1583 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-23 07:15:04 +02:00
Murphy Berzish
49b810e00f Merge branch 'master' into regex-develop 2018-03-11 23:18:55 -04:00
Nikolaj Bjorner
a4c58ec4c2 fix #1496 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-22 08:05:28 +09:00
Murphy Berzish
54206e3674 Merge branch 'develop' into regex-develop 
Conflicts:
	src/smt/theory_str.h
 2018-02-12 17:25:50 -05:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener
b7d1753843 Use override rather than virtual. 2018-02-09 21:19:27 +07:00
Nikolaj Bjorner
61934d8106 align semantics of re.allchar with string proposal. #1475 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 20:08:15 -08:00
Thai Trinh
c07a63cf8e coalesce seq.unit into string in mk_skolem 2017-12-12 05:00:34 +08:00
Murphy Berzish
fbe8d1577e new regex automata start; add complexity estimation 2017-12-04 18:05:00 -05:00
Nikolaj Bjorner
81ec5bae95 fix #1377 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 11:02:48 -08:00
Nikolaj Bjorner
36e5d4dec9 fix #1377 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 11:01:44 -08:00
Nikolaj Bjorner
a1cc21d77b merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-05 16:03:46 -07:00
Nikolaj Bjorner
a4cf2726fd fix seg-fault from #1244 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-05 07:35:37 -07:00
Nikolaj Bjorner
009e94d188 update to theory_seq following examples from PJLJ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-30 14:00:01 -07:00
Nikolaj Bjorner
276fdd0e97 register auxiliary constants from projection operation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-20 08:51:24 -07:00
Nikolaj Bjorner
07bc19b489 add documentation to string rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-14 07:19:04 -07:00
Nikolaj Bjorner
a39b0b201a another fix to str.to.int/int.to.str semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 17:27:34 -07:00
Nikolaj Bjorner
fb17362dff fix string rewriting according to definition. Relates to examples in #1202 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 17:21:38 -07:00
Nikolaj Bjorner
ead704f52f handle undefined constant cases for int.to.str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 17:13:10 -07:00
Nikolaj Bjorner
c4083c367a update handling of contains constraints taking string literals into account 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 19:14:55 -07:00
Nikolaj Bjorner
50e9b371d9 inc version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 17:52:58 -07:00
Nikolaj Bjorner
85cdfd885f address bug reported in #1196 and include additional ad-hoc rewrites to handle some string cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 17:41:18 -07:00
Nikolaj Bjorner
7b47b0380e update Ackerman reduction for division to make Andre and Nathan happy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-10 23:43:21 +02:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Christoph M. Wintersteiger
a7d5bb7b36 Tabs 2017-05-31 12:18:00 +01:00
Nikolaj Bjorner
79a8e9aab0 fix build break #1029 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-18 12:09:51 -07:00
Nikolaj Bjorner
ceec81de0b simplify code, issue #1028 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-16 08:32:08 -07:00
Nikolaj Bjorner
7fab670719 fix regression, issue #1028 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-16 08:21:32 -07:00
Nikolaj Bjorner
d1cfc53495 fix for #1015 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-10 19:40:00 -07:00
Nikolaj Bjorner
7e1fae418a fix #1005, disable expansion of regular expression range to union as it degrades performance significantly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-05 10:59:47 -04:00
Murphy Berzish
46ac718790 theory_str frontend changes 2017-04-26 17:24:05 -04:00
Nikolaj Bjorner
66e61b8a31 issues #963 #912 2017-04-17 03:06:38 -07:00
Nikolaj Bjorner
48638c6f1e fix for #975, add mask to ensure character encoding is unique within range of bits used for encoding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 09:34:13 +07:00
Nikolaj Bjorner
582880346e add index option to 'eval' command for box objectives. Issue #955 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-31 09:22:56 -07:00
Nikolaj Bjorner
e342b87921 Merge pull request #942 from mtrberzi/str-extract-semantics 
alternate str.extract semantics in seq_rewriter
 2017-03-21 10:48:06 -07:00
Murphy Berzish
6804c88b66 make seq.extract rewrite type-generic 2017-03-21 12:54:06 -04:00
Nikolaj Bjorner
ca4ae171ea remove unsound simplification in prefix #949 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-21 07:40:35 -06:00
Nikolaj Bjorner
05c267b8d8 make seq.at operations generic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-14 15:37:47 -07:00