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

2055 commits

Author SHA1 Message Date
Murphy Berzish
725352234d refactoring theory_str 2017-02-27 13:22:56 -05:00
Nikolaj Bjorner
e9b49644b2 Merge branch 'master' of https://github.com/z3prover/z3 into opt 2017-02-25 16:20:33 -08:00
Nikolaj Bjorner
996c0f0666 fix type on exception message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-25 16:14:50 -08:00
Nikolaj Bjorner
8437cb7132 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-02-24 07:54:25 -08:00
Murphy Berzish
0ebd93c8b5 add _re.unroll internal operator to seq_decl_plugin 2017-02-23 20:57:19 -05:00
Murphy Berzish
7e3e434147 Merge branch 'upstream-master' into release-1.0 2017-02-23 19:18:58 -05:00
Murphy Berzish
eb0ba26f90 C-style octal escapes, including 1- and 2-digit escapes 2017-02-23 18:33:10 -05:00
Murphy Berzish
61bbf8ba7e add octal escape to seq_decl_plugin 2017-02-23 18:24:08 -05:00
Murphy Berzish
5107e5cafc refactor: remove t_str_refcount_hack traces 2017-02-23 15:01:55 -05:00
Murphy Berzish
179b0f7630 clean up todos theory_str 2017-02-21 19:52:27 -05:00
Murphy Berzish
15e3d3ec3c octal escape theory_str 2017-02-21 15:51:08 -05:00
Nikolaj Bjorner
122a12c980 fix build on downlevel compilers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-21 09:12:10 -08:00
Nikolaj Bjorner
98c5a779b4 add xor parity solver feature 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-20 16:55:00 -08:00
Nikolaj Bjorner
0cf5af121a Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-02-19 11:32:18 -08:00
Nikolaj Bjorner
dc588b54f7 add sorting-based pb encoding in the style of minisat+ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-19 11:31:34 -08:00
Murphy Berzish
235ea79043 Merge branch 'upstream-master' into release-1.0 
Conflicts:
	src/cmd_context/check_logic.cpp
	src/cmd_context/cmd_context.cpp
	src/cmd_context/cmd_context.h
	src/smt/params/smt_params_helper.pyg
	src/smt/smt_context.cpp
 2017-02-18 15:04:44 -05:00
Nikolaj Bjorner
b0dd3f3238 add recursive function graphs to model, adapt rewriter to bypass branches whose evaluation is redundant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-16 13:58:12 -08:00
Nikolaj Bjorner
7e391a8a57 add option to disable cardinality solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-16 08:38:38 -08:00
Nikolaj Bjorner
2bcb875559 add option to disable cardinality solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-16 08:36:16 -08:00
Murphy Berzish
3670fa64e6 add hex escape support theory_str 2017-02-11 16:59:06 -05:00
Nikolaj Bjorner
4220432ac3 Merge branch 'master' of https://github.com/z3prover/z3 into opt 2017-02-11 11:57:47 -05:00
Nikolaj Bjorner
b6b6035cfb tuning and fixing drat checker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-07 16:50:39 -08:00
Christoph M. Wintersteiger
c56edc63d2 Merge pull request #882 from dwoos/sine-filter 
Add basic Sine Qua Non filtering
 2017-02-04 20:24:09 +00:00
Nikolaj Bjorner
e9e0293d1a local updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-02 10:19:51 -08:00
Doug Woos
d6fbfe401e add and use new is_pattern recognizer 2017-02-01 16:21:15 -08:00
Nikolaj Bjorner
7faa35ebdb fixing card 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-31 18:47:30 -08:00
Murphy Berzish
19779f1a9b fix string operators in theory_str, this breaks theory_seq temporarily 2017-01-31 11:49:10 -05:00
Nikolaj Bjorner
8b7bafbd9f updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 21:23:53 -08:00
Murphy Berzish
fa1ec0b80f smtlib25 draft standard in theory_str 2017-01-27 16:49:40 -05:00
Murphy Berzish
a879b24011 add str.prefixof, str.suffixof in theory_str 2017-01-27 16:26:30 -05:00
Murphy Berzish
50e2273dbd substr bugfix 2017-01-20 17:39:32 -05:00
Nikolaj Bjorner
13099b1590 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-19 17:56:43 -08:00
Christoph M. Wintersteiger
6d34899c46 Bugfix for macro finder. Fixes #832. 2017-01-17 15:44:03 +00:00
Nikolaj Bjorner
dc543a7ee7 update macro_util logging to uniform format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 21:13:22 -08:00
Nikolaj Bjorner
24eae3f6e0 fix crash with unary xor #870 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 12:06:56 -08:00
Nikolaj Bjorner
cb6c6332b3 update conflict resolution for cardinality case 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-28 12:44:30 -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
Nikolaj Bjorner
5cb21924ad ensure that FD logic understands pb from command context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-17 16:02:54 -08:00
Murphy Berzish
dd8cd8199b theory_str refcount debug messages and beginning theory case split 2016-12-16 14:37:34 -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
7cc093eee0 Add rewrite rule for property encoded in #812 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 11:05:12 +01:00
Nikolaj Bjorner
0765eea486 add suggestions from #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 05:45:40 +01:00
Nikolaj Bjorner
32c63ce4cd address other warnings per input from delcypher 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 17:23:59 +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
Nikolaj Bjorner
8e6600c6be add python API for newly exposed regex constructors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 09:09:03 +01:00
Murphy Berzish
be9cb8db82 regex tracing theory_str 2016-12-05 20:17:43 -05:00
Nuno Lopes
e697d3e810 remove 2 outdated comments 2016-12-01 14:10:31 +00:00
Murphy Berzish
947d443726 improved regex concat rewrite 2016-11-29 19:46:37 -05:00