mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
10363 commits 49 branches 53 tags 182 MiB
Commit graph

10363 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
d57bca8f8c fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-10 10:43:55 +08:00
Nikolaj Bjorner
00685ff04f Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2018-04-08 15:46:41 -07:00
Nikolaj Bjorner
f2dfc0dc24 including all touched tautology literals each round 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-08 15:46:21 -07: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
nilsbecker
b3aed5987c Merge branch 'master' of https://github.com/Nils-Becker/z3 2018-04-08 18:27:21 +02:00
Nils Becker
7585f28dec Improved quantifier instantiation logging 2018-04-08 18:18:02 +02: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
Nikolaj Bjorner
21738d9750 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-06 15:59:55 -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
Nikolaj Bjorner
a954ab7d8d flip literals in ATEs produced using RI 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-06 08:38:01 -07: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
528dc8a3f8 disable bdd variable elimination 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-31 17:05:22 -07:00
Nikolaj Bjorner
55eb11d91b fix bug in blocked clause elimination: it was ignoring unit literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-31 13:26:20 -07:00