mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
5714 commits 23 branches 48 tags 157 MiB
Commit graph

766 commits

Author SHA1 Message Date
Nikolaj Bjorner
58198d7cb6 add consequence finding to inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-16 15:45:39 -04:00
Nikolaj Bjorner
aec59e4ff7 add consequence finding to inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-16 15:43:28 -04:00
Nikolaj Bjorner
487f15f90a better encodings for at-most-1, #755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-10 23:49:45 -07:00
Nikolaj Bjorner
8d2b70a5e2 better encodings for at-most-1, #755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-10 23:46:03 -07:00
Christoph M. Wintersteiger
acdaeca826 Bugfix for ITEs over FP rounding modes. 
Fixes #751.
 2016-10-04 18:04:56 +01:00
Christoph M. Wintersteiger
0bd06930ae whitespace 2016-10-04 18:04:00 +01:00
Nikolaj Bjorner
e3f0aff318 address ubuntu warning and add shortcuts for maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-03 16:22:13 -07:00
Nikolaj Bjorner
ab3b36269e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-28 16:42:14 -07:00
Nikolaj Bjorner
476b06fa14 fix compiler warnings, gcc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-28 16:42:07 -07:00
Nikolaj Bjorner
b758a7a508 disable smt-lib success printing when locally parsing database of common pattern rules. Issue #743 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-22 19:53:48 -07:00
Mikolas Janota
147c0f8152 Removing an unused method from bv_rewriter. 2016-09-16 19:44:37 +01:00
Mikolas Janota
ec47a1df50 Adding bv preprocessing techniques. 2016-09-16 19:44:37 +01:00
Nikolaj Bjorner
5a86815f34 fix regression in seq-replace rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-11 05:43:16 -07:00
Nikolaj Bjorner
0b57829bdd fix heisenbug, unintialized variable, issue #720 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 11:04:29 -07:00
Nikolaj Bjorner
cb140011bc add missing rewrite rule. Issue #731 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 09:42:36 -07:00
Nikolaj Bjorner
e485d1889c update replace semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-08 13:59:13 -07:00
Nikolaj Bjorner
237fde1f76 fix crash during shutdown. Issue #719 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-31 09:57:46 +08:00
Nikolaj Bjorner
882c3bd0cd fix unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 18:18:11 -03:00
Nikolaj Bjorner
b5c521e4b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-23 11:44:48 -03:00
Nikolaj Bjorner
0a09d5ff52 check for non-nullness when handling optional info fields for marking. Fixes issue #719 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 11:33:40 -03:00
Christoph M. Wintersteiger
47e95f8676 Fixed binding substitution in macro_util 2016-08-20 17:56:52 -04:00
Nikolaj Bjorner
879f792125 fix axiomatization of str.replace. Fixes issue #703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 06:13:52 -07:00
Nikolaj Bjorner
439e8e6b04 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-20 03:53:55 -07:00
Nikolaj Bjorner
f2b5c11d1c add option for prettier proof printing, Issue #706 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 03:52:45 -07:00
Christoph M. Wintersteiger
e8141aaa84 debug fixes 2016-08-12 19:52:59 +01:00
Nikolaj Bjorner
bbfe02b25a modulating data-type solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-03 11:16:29 -07:00
Nikolaj Bjorner
4958edeb42 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 19:40:49 -07:00
Loris D'Antoni
73bd4acfc5 added symbolic automata complement for sequences 2016-07-28 13:50:05 -07:00
Nikolaj Bjorner
b7de813c63 set solver on simplify command 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 15:35:44 -07:00
Nikolaj Bjorner
083939ab0e add tactic to eliminate enumeration sorts in favor of bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-23 14:11:21 -07:00
Nikolaj Bjorner
5f39c4371c fix proof generation for unit resolution. Issue #691 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 11:54:39 -07:00
Nikolaj Bjorner
cf48eb5f72 mark also ast in parameters as GC roots. Issue #676 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-17 19:16:15 -04:00
Nikolaj Bjorner
4f5b0667ef fix rounding mode for pseudo-boolean constraint creation, Issue #683 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-14 12:34:18 -07:00
Nikolaj Bjorner
3a83788b97 remove unfinished ite-macro finder, tune ast GC to ensure nodes are roots only once 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-14 09:46:09 -07:00
Nikolaj Bjorner
4720d578a4 add proper garbage collection to ast_manager. Issue #679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-14 09:05:16 -07:00
Nikolaj Bjorner
f30fb7639e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-13 20:32:24 -07:00
Nikolaj Bjorner
3989d238c0 fix bugs exposed in #677. to_int(x) has the semantics that to_int(x) <= x, and to_int(x) is the largest integer satisfying this inequality. The encoding in purify_arith had it the other way x <= to_int(x) contrary to how to_int(x) is handled elsewhere. Another bug in theory_arith for mixed-integer linear case was also exposed. Fractional bounds on expressions of the form to_int(x), and more generally on integer rows were not rounded prior to internalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-13 20:32:18 -07:00
Nikolaj Bjorner
3a70b6aab4 fix model generation, add rewrite rules for sin(acos(x)) reduction to help model validation. Issue #680 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-13 11:12:27 -07:00
Christoph M. Wintersteiger
1e5a87887d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-13 15:36:27 +01:00
Christoph M. Wintersteiger
cfbe16639f Bugfix for fpa2bv translation 2016-07-13 15:35:14 +01:00
Nikolaj Bjorner
63f89f8c45 add sin/cos conversions for #680 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-12 15:12:40 -07:00
Fabian Wolff
6eaab00e83 Fix spelling errors 2016-07-09 11:46:43 +02:00
Nikolaj Bjorner
d5ee7e24bc add simplification for equalities between itos and constant strings, Issue #589 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-08 11:50:39 -07:00
Nikolaj Bjorner
7fc294d329 move arithmetical mbp functionality to model_based_opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-26 14:30:35 -07:00
Nikolaj Bjorner
30cf0d19eb use of mk_bool_val 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-24 09:11:45 -07:00
Nikolaj Bjorner
f72d9c25c6 merge with update to bv rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-24 09:08:01 -07:00
Nikolaj Bjorner
017165c474 fix bug with model completion and remove spurious std::cout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-24 09:02:12 -07:00
Christoph M. Wintersteiger
70301ad3c8 Added bv*mul_no*flow handling in bv_rewriter. 
Fixes #657.
 2016-06-24 16:25:11 +01:00
Nikolaj Bjorner
67ea78a4a5 Add basic MARCO example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-24 08:00:23 -07:00
Nikolaj Bjorner
914bf2ff3b extend constant folding for bit-vector overflow/underflow operators, #657 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-24 07:43:05 -07:00