mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 10:51:50 +00:00
Code Activity
8104 commits 23 branches 48 tags 156 MiB
Commit graph

8104 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner b79440a21d add web assembly link 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-18 21:13:24 -07:00
Nikolaj Bjorner 393d25f661 add web assembly link 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-18 21:12:43 -07:00
Nikolaj Bjorner 97cee7d0a4 fix #1576, hopefully 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-18 07:30:26 -07:00
Nikolaj Bjorner bf6fd1e682 Merge branch 'master' of https://github.com/z3prover/z3 2018-04-18 07:18:56 -07:00
Nikolaj Bjorner 6224db71f3 fix #1579 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-18 07:18:33 -07:00
Christoph M. Wintersteiger dab8e49e22 Fixed corner-case in fp.to_ubv. 2018-04-16 18:28:13 +01:00
Nikolaj Bjorner 098bce0f46 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-14 08:44:20 -07:00
Nikolaj Bjorner d939c05e72 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-14 08:27:40 -07:00
Nikolaj Bjorner 56827d5725 adding the orphaned shorthand #1574 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-13 23:10:21 -07:00
Nikolaj Bjorner 3b7520729e Merge branch 'master' of https://github.com/z3prover/z3 2018-04-13 23:08:19 -07:00
Nikolaj Bjorner 6078d24016 adding orphaned function declaration #1574 2018-04-13 23:07:14 -07:00
Nikolaj Bjorner f1c51982f8
Merge pull request #1562 from mtrberzi/regex-develop 
automata-based regex engine for Z3str3
 2018-04-13 16:33:45 +08:00
Murphy Berzish 3cfb32cd2d fix regex automata leaked memory 2018-04-12 14:35:29 -04:00
Murphy Berzish 47007d3f04 Merge remote-tracking branch 'upstream/master' into regex-develop 2018-04-12 12:13:30 -04:00
Nikolaj Bjorner 28fbcd7687 fix #1571 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-12 15:59:06 +08:00
Nikolaj Bjorner f77cfc1487 Merge branch 'master' of https://github.com/z3prover/z3 2018-04-12 15:06:02 +08:00
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
Christoph M. Wintersteiger 2abc759d0e Merge branch 'master' of https://github.com/Z3Prover/z3 2018-04-08 21:58:39 +01:00
Christoph M. Wintersteiger b373bf4252 Bugfixes for fpa2bv_converter. Fixes #1564. 2018-04-08 21:51:27 +01: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 9e8192e448
Merge pull request #1560 from c-cube/perf-occurs-check 
improve performance of occurs check for datatypes
 2018-04-07 10:29:11 -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
Murphy Berzish 27f2b542df remove comment 2018-04-06 12:13:53 -04: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
Murphy Berzish 45f48123e7 add re.plus length enumeration; fix reordering warning 2018-04-06 11:39:08 -04: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