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

8148 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
Murphy Berzish 6a3ce301b7 fix collection error 2018-04-03 12:51:03 -04:00
Nikolaj Bjorner 852f1b87dc
Merge pull request #1559 from cocreature/print-success-declare-datatype 
Fix buffering issue in print_success for declare-datatype
 2018-04-03 09:45:31 -07:00
Murphy Berzish 41703a4254 Merge branch 'develop' into regex-develop 2018-04-03 12:31:27 -04: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