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

6539 commits

Author SHA1 Message Date
Nikolaj Bjorner
aef3de5fca escape ascii above 127, issue #1571 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-12 15:05:35 +08:00
Nikolaj Bjorner
5cff0de844 fix #1567 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-08 11:19:00 -07:00
Nikolaj Bjorner
bab87bfb9b move some methods from header to cpp, format fixing, remove special characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-07 17:34:46 -07:00
Nikolaj Bjorner
2dc92e2b94 merge with pull request #1557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-07 17:22:49 -07:00
Nikolaj Bjorner
b811651673 Merge branch 'master' of https://github.com/z3prover/z3 2018-04-07 16:52:29 -07:00
Nikolaj Bjorner
187ba6a561 fix cast in tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-07 13:31:23 -07:00
Nikolaj Bjorner
65834661a8 disambiguate calls to set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-07 10:53:52 -07:00
Nikolaj Bjorner
4f5133cf72 disambiguate calls to set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-07 10:16:46 -07:00
Simon Cruanes
66b85e000b fix in occurs_check (early exit) 2018-04-07 01:25:19 -05:00
Nikolaj Bjorner
cfd9785025 replace by int64_t and uint64_t 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-06 19:32:01 -07:00
Simon Cruanes
ac881d949d style(datatype): use modern iteration 2018-04-06 17:29:17 -05:00
Simon Cruanes
8fd2d8a636 chore(datatype): small fixes 2018-04-06 17:20:04 -05:00
Simon Cruanes
bf6928fec0 fix(datatypes): additional explanation in occurs_check 2018-04-06 17:20:04 -05:00
Simon Cruanes
d973b08247 fix(datatypes): update following @nikolajbjorner 's review 2018-04-06 17:20:04 -05:00
Simon Cruanes
433f487ff2 fix(datatype): always use root nodes for the parent table 2018-04-06 17:20:04 -05:00
Simon Cruanes
e535cad480 chore(datatype): small improvements 2018-04-06 17:20:04 -05:00
Simon Cruanes
fa10e510bb fix(datatype): only use pointer equality for enode_tbl 2018-04-06 17:20:04 -05:00
Simon Cruanes
9df140343a perf(datatype): whole-graph implementation of occurs_check 2018-04-06 17:20:04 -05:00
Simon Cruanes
2ee1e358b6 chore: add definition for enode_tbl 2018-04-06 17:20:04 -05:00
Simon Cruanes
b5d531f079 perf(datatype): improve caching in occurs_check 2018-04-06 17:20:04 -05:00
Nikolaj Bjorner
3b78bdc8e5 shorthands in enode to access args and partents 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-06 14:01:09 -07:00
Christoph M. Wintersteiger
be4edddd2b Fixed bug in to_fp/to_fp_unsigned. Thanks to Florian Schanda for reporting this bug. 2018-04-06 17:08:29 +01:00
Christoph M. Wintersteiger
287c6f08e1 Resolved merge conflict 2018-04-05 20:31:45 +01:00
Christoph M. Wintersteiger
932ba15261 Merge branch 'master' of https://github.com/Z3Prover/z3 2018-04-05 20:29:01 +01:00
Christoph M. Wintersteiger
b0492659d6 Merge branch 'master' of https://github.com/wintersteiger/z3 2018-04-05 20:28:44 +01:00
Christoph M. Wintersteiger
02bf2530b5 Bugfix for fp.to_sbv. Thanks to Florian Schanda for reporting this bug. 2018-04-05 19:55:41 +01:00
Christoph M. Wintersteiger
724f86d43e Bugfix for unspecified semantics of some fp.* operators. 2018-04-05 19:55:04 +01:00
Christoph M. Wintersteiger
bd00d98398 Fixed overflow bug in fp.to_ubv. Thanks to Florian Schanda for reporting this bug. 2018-04-05 17:21:17 +01:00
Christoph M. Wintersteiger
3de41e5179 Fixed model completion for unspecified cases of floating-point functions. Thanks to Florian Schanda for reporting this bug. 2018-04-05 15:27:02 +01:00
Christoph M. Wintersteiger
328ad248b6 Fixed overflow problem in fp.to_?bv. Thanks to Florian Schanda for reporting this bug. 2018-04-05 15:26:25 +01:00
Christoph M. Wintersteiger
793642f48d Fixed MPF to_sbv. Thanks to Florian Schanda for reporting this bug. 2018-04-05 15:23:16 +01:00
Nikolaj Bjorner
ab43bfafe5 Merge branch 'master' of https://github.com/z3prover/z3 2018-04-03 12:40:26 -07:00
Nikolaj Bjorner
5ba939ad5e add tuple shortcut and example to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-03 12:40:18 -07:00
Moritz Kiefer
6b38edf102 Fix buffering issue in print_success for declare-datatype 2018-04-03 11:57:31 +02:00
Nikolaj Bjorner
21a3b9c8e2 increment version number due to ABI/API breaking change #1556 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-31 05:20:47 -07:00
Bruce Mitchener
2fa304d8de Remove int64, uint64 typedefs in favor of int64_t / uint64_t. 2018-03-31 14:45:04 +07:00
Bruce Mitchener
16a2ad9afd Use stdint.h for int64_t / uint64_t in API. 
Now that we can use stdint.h, we can use it to portably define
64 bit integer types for use in the API.
 2018-03-30 23:06:24 +07:00
Bruce Mitchener
b9f2188fc0 Update Z3_bool doc. 2018-03-30 22:34:07 +07:00
Nikolaj Bjorner
76dec85c93 use stdbool #1526 instead of int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-27 15:41:53 -07:00
Nikolaj Bjorner
78744e589c add stdbool.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-27 12:19:24 -07:00
Nikolaj Bjorner
88e777748a remove stdout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 19:37:19 -07:00
Nikolaj Bjorner
bd2ed196e3 add correct badge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 19:36:21 -07:00
Nikolaj Bjorner
fc719a5ee8 fix diagnostic output #1553 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-24 10:37:05 -07:00
Nikolaj Bjorner
753f2c89ef initialize solvers to ensure that eval mode has a solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-23 18:54:23 -07:00
Nikolaj Bjorner
966a8f73d3 add eval feature #1553 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-23 16:26:20 -07:00
Nikolaj Bjorner
abc274e290 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 14:58:12 -07:00
Nikolaj Bjorner
d99068e412
Merge pull request #1546 from mtrberzi/refactoring 
theory_str determinism refactoring
 2018-03-20 13:38:50 -07:00
Nikolaj Bjorner
931dbd5933 remove python doc test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 13:37:04 -07:00
Murphy Berzish
7759d05efe fix use-after-free 2018-03-19 23:09:07 -04:00
Murphy Berzish
d26eddf776 re-add indexof-contains heuristic 2018-03-19 18:31:26 -04:00