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

7698 commits

Author SHA1 Message Date
Nikolaj Bjorner
19e2f8c9d5 fix #1694 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-20 17:35:41 -07:00
Nikolaj Bjorner
8241ba784d Merge branch 'master' of https://github.com/z3prover/z3 2018-06-19 16:33:34 -07:00
Nikolaj Bjorner
341f7ceb17 remove quantified lemmas for idiv/mod 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 13:19:48 -07:00
Nikolaj Bjorner
eeba30a277 fix #1677 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 10:56:45 -07:00
Nikolaj Bjorner
2456513053 sometimes comments are worth reading 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 10:43:51 -07:00
Nikolaj Bjorner
9b6a99794b add default method for fresh fp value, try to address OsX build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 10:02:31 -07:00
Nikolaj Bjorner
8a29c2803c improvements to arithmetic preprocessing simplificaiton and axiom generation for #1683 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 07:04:39 -07:00
Nikolaj Bjorner
86c39c971d fix #1681 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 21:53:45 -07:00
Nikolaj Bjorner
b4aac1ab55 revert fix to #1677 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 21:23:13 -07:00
Nikolaj Bjorner
c15eca66d6 fix #1685 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 20:53:33 -07:00
Nikolaj Bjorner
6a0b70ee5c selective expansion of strings for canonizer to fix #1690 regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 20:42:53 -07:00
Nikolaj Bjorner
4634d1daed selective expansion of strings for canonizer to fix #1690 regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 20:37:39 -07:00
Nikolaj Bjorner
8040eddf65 fix #1658 fix #1689 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 16:41:04 -07:00
Nikolaj Bjorner
c3b27903f8 fix #1677 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 11:22:01 -07:00
Nikolaj Bjorner
55ebf69648 move comment to fix #1682 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 09:42:05 -07:00
Nikolaj Bjorner
cd890bd993 fix bug in order for model conversion in normalize_bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 09:34:53 -07:00
Nikolaj Bjorner
c81f25a1c8 fix build issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-17 09:59:03 -07:00
Nikolaj Bjorner
035baf7cb9 align use of spaces before for/if/while 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-17 09:43:40 -07:00
Nikolaj Bjorner
190428ab3f Merge branch 'master' of https://github.com/z3prover/z3 2018-06-17 09:40:40 -07:00
Nikolaj Bjorner
6bc14afa5e
Merge pull request #1686 from agurfinkel/deep_space 
switching spacer to new model api
 2018-06-17 09:40:13 -07:00
Wojciech Nawrocki
0adf66dc0a
python: fix usage of fpa_get_numeral_significand_uint64 2018-06-17 13:20:01 +02:00
Arie Gurfinkel
4204b6ede2 Switch rest of spacer to new model API and remove mev_util 2018-06-16 14:40:17 -07:00
Arie Gurfinkel
a222b6d41f Switch reach_fact to new model API 2018-06-16 14:17:33 -07:00
Arie Gurfinkel
f226c6682b Switched derivation to new model API 2018-06-16 14:09:24 -07:00
Arie Gurfinkel
5e65b37f25 Switch spacer::qe_project to new model API 2018-06-16 13:58:58 -07:00
Arie Gurfinkel
fffc8489bf Switched compute_implicant_literals to use new model API 2018-06-16 13:43:30 -07:00
Arie Gurfinkel
60888a93eb Minor fixes to model 2018-06-16 13:42:26 -07:00
Nikolaj Bjorner
66e6dc78a3 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-16 11:23:03 -07:00
Nikolaj Bjorner
c64321c2e4 debugging maxres bug report 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-16 11:22:58 -07:00
Nikolaj Bjorner
450da5ea0c moving model_evaluator to model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 17:40:54 -07:00
Nikolaj Bjorner
9149048f34 use quotes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:53:47 -07:00
Nikolaj Bjorner
c0e378b045 remove { 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:44:33 -07:00
Nikolaj Bjorner
e350bf8a27 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-15 15:28:26 -07:00
Nikolaj Bjorner
caca07c85f fix path to moved header file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:28:18 -07:00
Nikolaj Bjorner
d7ba178d53
Merge pull request #1684 from agurfinkel/deep_space 
Remove spurious quote
 2018-06-15 15:16:52 -07:00
Nikolaj Bjorner
b6c43f6143 move files for build script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:13:55 -07:00
Arie Gurfinkel
3ad1446597 Remove spurious quote 2018-06-15 15:09:25 -07:00
Nikolaj Bjorner
6fc08e9c9f Merge branch 'master' of https://github.com/z3prover/z3 2018-06-15 14:58:10 -07:00
Nikolaj Bjorner
a51d6cbcbc debug model evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 14:58:02 -07:00
Arie Gurfinkel
f936c92efc Improve distinct constraint generation 
still many more optimizations possible
 2018-06-14 22:27:57 -07:00
Nikolaj Bjorner
baa96909cc mb-skolem for arithmetic with model repair 
The contract is that users of mb-skolem ensure that
interface equalities are preserved (by adding a
sufficient set of disequalities, such as a chain
x1 < x2 < x3 .., to force that solutions for
x_i does not clash).

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 17:26:04 -07:00
Nikolaj Bjorner
a0af3383db fixes to bdd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 17:25:18 -07:00
Arie Gurfinkel
05abf19009 comment 2018-06-14 16:38:27 -07:00
Arie Gurfinkel
a3de478c93 typo 2018-06-14 16:13:53 -07:00
Arie Gurfinkel
83cee9e81f Comments 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
87715620d9 Fix mk_distict in term_graph 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
2a6b7e5482 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
bc8ddedc54 fix a few build regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
e355123e37 Change declaration of projector 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
bbd917a0e6 Remove dead comment 2018-06-14 16:08:52 -07:00