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

1573 commits

Author SHA1 Message Date
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
Murphy Berzish
8c33dfab39 fix escape character overflow print 2016-11-27 20:51:34 -05:00
Murphy Berzish
1fa8129c8f pretty-printing of general escape sequences for string literals 2016-11-25 18:02:24 -05:00
Murphy Berzish
889b6be2c3 fix smt-lib 2.5 double quotes in pp 2016-11-23 19:03:53 -05:00
Murphy Berzish
8e962aa427 escape chars in smt2 printing of string constants 2016-11-22 18:32:03 -05:00
Murphy Berzish
11d8ffc4d4 escape characters in theory_str 2016-11-22 18:21:40 -05: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
Nikolaj Bjorner
e21bd8dacc fix lexicographic combinations for wmax: pb constrsaints were not interpreted in Boolean benchmarks. #782 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-15 15:07:05 +02:00
Murphy Berzish
fbaee080b2 fix performance regression introduced with theory_str str.from-int 
more investigation is required to understand why this works.
 2016-11-11 00:32:50 -05:00
Murphy Berzish
fff1fadf3b add str.from-int in theory_str rewriter 2016-11-09 15:54:22 -05:00
Nikolaj Bjorner
ef9230d8f8 detect quantifiers in model expressions to quiet down failing model validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-07 06:56:36 -08:00
Christoph M. Wintersteiger
75cfd14e5a bugfix for macro finder 2016-11-07 14:14:45 +00:00
Nikolaj Bjorner
152321bce6 fix crash in poly normalizer exposed by qe. Issue #775 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-04 20:29:12 +00:00
Christoph M. Wintersteiger
824ba14977 Disabled some ITE rewrite rules that were applied by default, but too expensive. Added re-computation of subterm occurrences in ctx_simplify_tactic. (Performance fixes for QF_LIA benchmarks). 2016-11-04 13:39:53 +00:00
Christoph M. Wintersteiger
a3e915fbea Whitespace 2016-11-04 13:37:14 +00:00
Nikolaj Bjorner
be9d5c7088 fix evaluator for array store expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-02 21:33:24 +00:00
Nikolaj Bjorner
ff75f88c4f fix memory abuse in internalization in inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-31 22:25:58 +01:00
Murphy Berzish
452eed6626 move get_std_regex_str to str_util 2016-10-29 12:19:24 -04:00
Nikolaj Bjorner
ca309341c3 fixing cancellation code paths for inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 22:07:46 -07:00
Nikolaj Bjorner
41deae52c6 fix enum2bv to handle singleton enumeration types, differentiate disequality conflicts for theories that handle disequalities vs. theories that don't 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 13:35:53 -07:00
Nikolaj Bjorner
24fc19ed58 speed up consequence finding by avoiding local search whenver assumption level is reached during the initial phase 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 08:15:39 -07:00
Christoph M. Wintersteiger
e4f7ff9881 Added Z3_fpa_is_numeral_negative to FPA API 2016-10-27 15:06:24 +01:00
Christoph M. Wintersteiger
bea7bc5e30 Bugfix for bv2fpa_converter. Fixes #767. 2016-10-26 16:32:44 +01:00
Nikolaj Bjorner
da4289fadc fix unit tests for pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-25 20:47:48 -07:00
Christoph M. Wintersteiger
8c5c564d6c fixed initialization order warning in pb2bv_rewriter 2016-10-25 14:31:29 +01:00
Nikolaj Bjorner
fefd00aa49 fix sign of constant in pb constraint 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 20:28:56 -07:00
Nikolaj Bjorner
b82b53dc34 add handling of pseudo-boolean inequalities that use if-expressions over Booleans and arihmetic instead of built-in PB predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 17:41:52 -07:00
Nikolaj Bjorner
6cf54a226e a more efficient encoding for pseudo-Boolean inequality constraints into bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 08:25:02 -07:00
Christoph M. Wintersteiger
89d38385db Added functions to test FP numerals for special values. 2016-10-24 12:50:05 +01:00
Nikolaj Bjorner
b476784f23 add missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:52:44 -07:00