mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
6266 commits 23 branches 48 tags 157 MiB
Commit graph

850 commits

Author SHA1 Message Date
Nikolaj Bjorner aedabfff7a disable newer pb encoding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-27 11:24:30 -07:00
Nikolaj Bjorner 41e1b9f3fe gt encoding of pb constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-16 12:07:16 +09:00
Nikolaj Bjorner 05c5b3b07b merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-09 22:45:52 +01:00
Nikolaj Bjorner 5f5819f029 fix xor handling, and defaults for cardinality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-09 22:44:41 +01:00
Nikolaj Bjorner 6f68355fbc Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-08 21:33:43 -08:00
Christoph M. Wintersteiger b57764800c Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-07 18:10:31 +00:00
Christoph M. Wintersteiger 8f14cfadd2 Tabs, whitespace 2017-03-07 18:10:03 +00:00
Murphy Berzish ad0766898c add boolean operators to zstring and fix ostream 2017-03-04 15:20:57 -05:00
Nikolaj Bjorner b0a47ca897 disable pb sorting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-02 08:11:38 -08:00
Nikolaj Bjorner 4792229c2b Merge pull request #922 from mtrberzi/regex-unroll 
add _re.unroll internal operator to seq_decl_plugin
 2017-02-27 18:37:37 -08: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 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
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
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
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
Nikolaj Bjorner 8b7bafbd9f updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 21:23:53 -08: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
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
Nuno Lopes e697d3e810 remove 2 outdated comments 2016-12-01 14:10:31 +00:00
Nikolaj Bjorner 7a4c20698f fix handling of AC operator ++ on regular expressions. Issue #804 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-22 13:02:17 -08:00
Christoph M. Wintersteiger a97358965b Fixed interruption/cancelation issue in rewriter. 2016-11-17 16:28:49 +00:00
Nikolaj Bjorner 1600823435 fix perf bug reported in #790 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-17 05:38:52 +02:00
Christoph M. Wintersteiger 9053e6eba6 Resolved merge conflicts. Added FPA API input validity checks. 2016-11-15 20:19:40 +00:00