mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 07:53:15 +00:00
Code Activity
7180 commits 44 branches 51 tags 170 MiB
Commit graph

1015 commits

Author SHA1 Message Date
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
f99048f3e7 rewrite to address some cases like #1203, updates to division handling in NRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 13:24:54 -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
082936bca6 enable overloading resolution on define-fun declarations, fix #1199 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-08 09:21:06 +02:00
Nikolaj Bjorner
2f466b6585 Merge branch 'master' of https://github.com/z3prover/z3 2017-08-03 13:56:04 -07:00
Nikolaj Bjorner
91ee52e549 fix #1195 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 13:53:38 -07:00
Nikolaj Bjorner
ffaaa1ff34 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-03 08:50:17 -07:00
Nikolaj Bjorner
8844112418 update header include generation to use relative paths #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 08:50:04 -07:00
Nikolaj Bjorner
ce3fd22f3b use common idioms for factor-equivalence code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 21:07:20 -07:00
Arie Gurfinkel
88a35119b9 moved obj_equiv_class to ast 2017-08-01 19:24:50 -04:00
Nikolaj Bjorner
2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Christoph M. Wintersteiger
e8cdc34219 Debug fix in fpa2bv converter. Relates to #872. 2017-07-31 22:34:58 +01:00
Christoph M. Wintersteiger
6a2fa91818 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 22:12:37 +01:00
Christoph M. Wintersteiger
9601761a6f Added missing float conversion in fpa2bv converter. Relates to #1178. 2017-07-31 22:12:15 +01:00
Nikolaj Bjorner
013127e947 fix build break based on ambiguous path resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 14:01:39 -07:00
Nikolaj Bjorner
063b6e9ea5 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 13:24:57 -07: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
bbf0ebcb74 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 20:18:53 +01:00
Christoph M. Wintersteiger
507356c7bf Fixed bug in fpa2bv converter. Fixes #1178. 2017-07-31 20:18:39 +01:00
Christoph M. Wintersteiger
52cf80d637 Simplified bit-vector bounds in fp.rem. Relates to #872. 2017-07-31 19:53:55 +01:00
Christoph M. Wintersteiger
ecfd241e19 Injected 3 missing bits of precision into fp.rem. Relates to #872. 2017-07-31 19:53:44 +01:00
Arie Gurfinkel
7670b49ada mark mk_true() and mk_false() const 2017-07-31 14:14:35 -04:00
Arie Gurfinkel
15451ae858 extra flags to control quant_hoist 2017-07-31 14:13:45 -04:00
Arie Gurfinkel
be1df279ec make proof_checker less verbose 2017-07-31 14:11:07 -04:00
Christoph M. Wintersteiger
a59907170d Fixed renormalization in fp.mul. Relates to #872. 2017-07-31 18:34:46 +01:00
Christoph M. Wintersteiger
175f042db8 Fixed renormalization in fp.fma. Relates to #872. 2017-07-28 23:01:01 +01:00
Christoph M. Wintersteiger
a30c343d7a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-28 20:24:35 +01:00
Christoph M. Wintersteiger
0610392a05 Bugfix for fp.fma. Fixes #872. 2017-07-28 20:16:13 +01:00
Nikolaj Bjorner
31d6abcfe8 remove arity check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:55:41 -07:00
Nikolaj Bjorner
e9b9a29339 revert first fix for #1173, replace by handling single arity chainables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:44:19 -07:00
Nikolaj Bjorner
64233034cc fix #1173 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:26:52 -07:00
Christoph M. Wintersteiger
33ebdc8adc Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872. 2017-07-27 23:08:35 +01:00
Christoph M. Wintersteiger
f1c0ac72e7 Fix for fp.fma encoding. Relates to #872. 2017-07-25 20:29:10 +01:00
Nikolaj Bjorner
9d6be286d0 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-25 10:18:43 -07:00
Nikolaj Bjorner
70f6280bf1 fix regression reported in #1159 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-25 10:18:21 -07:00
Nikolaj Bjorner
741f940119 Merge pull request #1158 from facanferff/master 
pretty printer: fix typo with ReSort sort name
 2017-07-24 21:19:18 -07:00
Nikolaj Bjorner
ae5e39a8b8 Merge branch 'master' of https://github.com/z3prover/z3 2017-07-24 09:18:27 -07:00
Nikolaj Bjorner
a0a8bc2a62 fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-24 09:12:43 -07:00
Fábio Ferreira
2e2782577b pretty printer: fix typo with ReSort sort name 2017-07-23 02:32:35 +01:00
Christoph M. Wintersteiger
0f1583309d Bugfix for fp.fma. One piece of puzzle #872. 2017-07-21 21:12:45 +01:00
Dan Liew
89c8f1722f Fix typo that prevented uses of bvsmod_i being parsed. 2017-07-12 12:53:10 +01:00
Nikolaj Bjorner
2af08a378d avoid complaining about division by 0 as unhandled in theory-lra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-08 18:21:47 -07:00
Nikolaj Bjorner
d66db280a8 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 13:43:32 -07:00
Nikolaj Bjorner
08524a2d90 cleanup for warning message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 11:47:17 -07:00
Nikolaj Bjorner
244cbc2638 ensure that auxiliary PB booleans are recognized during rewriting. Fixes segementation fault #1113, but does not address performance issues with quantifiers and optimization combinations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-26 10:04:50 -07:00