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

8101 commits

Author SHA1 Message Date
Simon Cruanes 5141f05e6d fix(union-find): keep values and representative in consistent order 
the merge handlers should be called with r1,r2,v1,v2 or r2,r1,v2,v1
but not a mix
 2018-08-17 14:58:44 -05:00
Nikolaj Bjorner 12f9336fec disable unused macros 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-15 22:44:07 -07:00
Nikolaj Bjorner 056ec2d5c4 remove inc file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-15 22:27:07 -07:00
Nikolaj Bjorner 2b2f193f2b remove dependency on ARRAYSIZE for issue #1616 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-15 22:26:14 -07:00
Nikolaj Bjorner 95963f71f4 fix bug introduced in fix of #1798 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-11 17:18:11 -07:00
Nikolaj Bjorner d270df67f7 Merge branch 'master' of https://github.com/z3prover/z3 2018-08-11 13:33:35 -07:00
Nikolaj Bjorner 96d3b98a44 fix #1783, wronge clausification of negated pb inequalities. Signs were ignored 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-11 13:33:09 -07:00
Nikolaj Bjorner 8de8c4cade fix #1798 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-11 11:41:06 -07:00
Nikolaj Bjorner a13b6a99d6
Merge pull request #1797 from c-cube/conf-dt-lazy-split 
expose the configuration param for datatype case splits
 2018-08-10 16:09:13 -07:00
Simon Cruanes 0aca1ad4c1 feat(smt/dt): expose the configuration param for datatype case splits 2018-08-10 17:37:23 -05:00
Murphy Berzish c65dbaea90 z3str3: fix contains-indexof precondition 2018-08-07 15:12:37 -04:00
Murphy Berzish 7a84486df2 Merge branch 'master' into develop 2018-08-07 12:57:02 -04:00
Nikolaj Bjorner 8b4e1c1209 fix #1793 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-06 18:13:26 -07:00
Nikolaj Bjorner 84c7df75d6 record statistics setting in config_params so that fp engine can access them, fix serialization bug when check-assumptions returns unsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-06 16:21:27 -07:00
Nikolaj Bjorner a3c692c05f fix include paths 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 13:49:26 -07:00
Nikolaj Bjorner 60110bb289 reduce dependencies in CMakeLists file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:34:13 -07:00
Nikolaj Bjorner 6400da63ab missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:10:52 -07:00
Nikolaj Bjorner 74efe253a0 fix header files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:09:23 -07:00
Nikolaj Bjorner d47e06732c bmc improvements, move fd_solver to self-contained directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:02:15 -07:00
Nikolaj Bjorner e041ebbe80 bmc improvements, move fd_solver to self-contained directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:00:49 -07:00
Nikolaj Bjorner fd09b1a7d0 Merge branch 'master' of https://github.com/z3prover/z3 2018-08-03 22:14:28 -07:00
Nikolaj Bjorner f306f75e36 harness internalization and API for #1776 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-02 20:18:27 -07:00
Nikolaj Bjorner 51610842b9 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-02 10:41:53 -07:00
Nikolaj Bjorner 7bd4a313dd expr utilities for pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-02 10:41:07 -07:00
Nikolaj Bjorner fed977b492 fix #1782 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-02 10:08:16 -07:00
Nikolaj Bjorner 39333273a5 Merge branch 'master' of https://github.com/z3prover/z3 2018-08-01 17:31:20 -07:00
Nikolaj Bjorner 8b08821112 fix #1784, fix #1783 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-01 17:31:14 -07:00
Lev Nachmanson ed44ffd54d
Merge pull request #1781 from levnach/master 
unroll static_matrix to avoid dead cells
 2018-08-01 15:03:39 -07:00
Lev Nachmanson adfbc2d001 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-08-01 10:26:39 -07:00
Lev Nachmanson 075cf106aa fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-08-01 08:46:03 -07:00
Nikolaj Bjorner 77d68409c2 handle null declarations for kind 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-01 08:43:32 -07:00
Lev Nachmanson 7370396c30 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-08-01 08:06:56 -07:00
Lev Nachmanson 0a51417804 unroll static_matrix to avoid dead cells 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-31 22:57:10 -07:00
Nikolaj Bjorner 124e963b10 revert bit-resize issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-31 16:26:41 -07:00
Nikolaj Bjorner 4b00d6aef2 move mk-bits to mk-var 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-31 16:13:25 -07:00
Nikolaj Bjorner 22a5687e16 supply bits on demand 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-31 15:52:21 -07:00
Nikolaj Bjorner 114f31c16a do not update assertions within scopes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-31 15:12:46 -07:00
Nikolaj Bjorner c7898b1977 trace push/pop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-31 14:22:57 -07:00
Nikolaj Bjorner 98d42421bc harness more pop uses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-31 08:42:19 -07:00
Nikolaj Bjorner 42d30e3edd remove availability of divides as it clashes with user-defined functions in benchmarks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-31 08:20:14 -07:00
Sosuke MORIGUCHI 22fc5ad771 Modify javadoc directive and mis-capitalization of method name 2018-07-31 21:39:02 +09:00
Lev Nachmanson de9023a928
Merge pull request #1777 from levnach/master 
use dead cells in static_matrix
 2018-07-30 20:25:49 -07:00
Lev 3d274c2e6f use CASSERT for hnf 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-30 15:55:06 -07:00
Lev Nachmanson 0ee68220e1 use CASSERT instead of lp_assert for static_matrix 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-30 14:34:03 -07:00
Lev 181bb60e36 remove some lp_asserts 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-30 12:54:53 -07:00
Lev Nachmanson 9cb713879e fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-30 09:56:39 -07:00
Nikolaj Bjorner 6d36e4277a Merge branch 'master' of https://github.com/z3prover/z3 2018-07-30 09:56:30 -07:00
Nikolaj Bjorner fdcedee887 hardening pop abuse and exception safety for #1776 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-30 09:56:16 -07:00
Lev Nachmanson 2de27ae3af uniform choice of a beneficial column 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-29 22:33:19 -07:00
Lev e9595eb283 merge with z3prover 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-29 21:15:42 -07:00
Lev Nachmanson 16b71fe911 work on static_matrix's cells 
Signed-off-by: Lev <levnach@hotmail.com>

trying the new scheme in static_matrix : in progress

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

in the middle of changes in static_matrix

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

more fixes in static_matrix.h

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

debug

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fixes in static_matrix

Signed-off-by: Lev <levnach@hotmail.com>

fixes in static_matrix, column_strip

Signed-off-by: Lev <levnach@hotmail.com>

fixes in static_matrix

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fixes for static_matrix

Signed-off-by: Lev <levnach@hotmail.com>

work on static_matrix

Signed-off-by: Lev <levnach@hotmail.com>

work on static_matrix

Signed-off-by: Lev <levnach@hotmail.com>

progress in static_matrix

Signed-off-by: Lev <levnach@hotmail.com>

fix a bug in swap_with_head_cell

Signed-off-by: Lev <levnach@hotmail.com>

progress in static_matrix

Signed-off-by: Lev <levnach@hotmail.com>

compress rows and columns if needed

Signed-off-by: Lev <levnach@hotmail.com>

fix in compression of cells

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-29 20:45:13 -07:00
Nikolaj Bjorner 95845bbb01
Merge pull request #1775 from NikolajBjorner/master 
fix #681, unsound propagation of binary equalities. Clean up memory l…
 2018-07-29 17:33:22 -07:00
Nikolaj Bjorner 13390e2c3a fix #681, unsound propagation of binary equalities. Clean up memory leaks on exit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-29 12:08:59 -07:00
Nikolaj Bjorner 6bacf09447
Merge pull request #1773 from NikolajBjorner/master 
bug fixes
 2018-07-29 08:09:35 -07:00
Nikolaj Bjorner 5509bf248a coallesce lambda/quant tracing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-29 08:02:56 -07:00
Nikolaj Bjorner 64e570f159 fix #1766 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-29 02:22:28 -07:00
Nikolaj Bjorner 5380b01fd1 bool -> string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-29 00:44:40 -07:00
Nikolaj Bjorner 879e217fe6 limits -> climits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-28 20:28:53 -07:00
Audrey Dutcher 310de49d2b Update link to reference high-compatibility build script 2018-07-28 18:56:40 -07:00
Audrey Dutcher d74edbcb2b Add environment variable for controlling version suffixes 2018-07-28 18:11:58 -07:00
Audrey Dutcher a7f7872f45 Update maintainer info 2018-07-28 18:05:58 -07:00
Nikolaj Bjorner 1cb3f7c792 fixing #1520 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-28 18:03:13 -07:00
Audrey Dutcher 42af36563e Autogenerate list of header files 2018-07-28 17:55:16 -07:00
Audrey Dutcher 64eaf6cb01 Add bdist_wheel tag renaming blurb 2018-07-28 17:55:02 -07:00
Audrey Dutcher a91531c04c Stub z3test.py for pydistrib 2018-07-28 17:54:32 -07:00
Lev ef2cdc226a a fix in maximize_term 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-26 22:46:28 -07:00
Nikolaj Bjorner d74978c277 fix #1762, #1764, #1768 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-26 20:29:26 +01:00
Nikolaj Bjorner 259d4c4e43 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-26 15:32:02 +01:00
Nikolaj Bjorner 60bb02b709 updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-26 15:31:49 +01:00
Lev Nachmanson b71fe0b3b7 speed up find_cube 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-16 16:17:49 -07:00
Lev Nachmanson 35f7f1f62e fix in cube heuristic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-16 12:29:42 -07:00
Nikolaj Bjorner 8744c62fca fix #1755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-16 10:55:25 +01:00
Nikolaj Bjorner 49141c7813 remove left-over break assert 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-16 08:33:41 +01:00
Nikolaj Bjorner 30330c79a1 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-15 22:36:02 -07:00
Nikolaj Bjorner d00ffdda82 strengthen filter for specialized tactic conditions, add flag to disable hnf to lp_params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-15 22:35:47 -07:00
Lev Nachmanson f7ac096696 avoid a vector copy 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-15 15:29:13 -07:00
Nuno Lopes dfa8c4432f add parameter(rational&&) 2018-07-14 20:50:49 +01:00
Nuno Lopes b88596283f don't use mp[zq] synchronized mode if OpenMP mode is disabled 2018-07-14 20:44:35 +01:00
Nuno Lopes 7d20fbb280 do not cooperate if OMP mode is disabled (i.e. it's single threaded only) 2018-07-14 12:21:43 +01:00
Nikolaj Bjorner bdd8685146 use params for arguments to Fixedpoint methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-13 18:09:30 -07:00
Nikolaj Bjorner 88f4ce68fd fix model generation regression exposed in nightly builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-13 13:51:07 -07:00
Nikolaj Bjorner 774fa33bfe fix parameter lookup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-13 08:49:46 -07:00
Nikolaj Bjorner 1d408c1955 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-13 07:52:40 -07:00
Nikolaj Bjorner 167969d6c2 remove debug/non-debug difference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-13 07:52:36 -07:00
Nikolaj Bjorner ca12a8482f fix to closure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-12 22:50:24 -07:00
Nikolaj Bjorner 4915fb080b fix #1749 by rejecting non-well-founded use of datatype in array 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-12 22:45:52 -07:00
Nuno Lopes b7ea90c12b bv_decl_plugin: remove some mem allocs of parameters 2018-07-12 18:36:09 +01:00
Lev Nachmanson e0e893b791 fix in hnf for the lower bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 12:29:09 -07:00
Lev Nachmanson 2dfb8f53b6 do not add term to hnf if one of the vars has v.y value 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Lev Nachmanson 5cfc3591d2 create hnf cuts too, when gomory_cut_period is 2 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Lev Nachmanson 3c230727bb rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Lev Nachmanson adf0d745c1 rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Lev Nachmanson bc17b18ed0 setting smt.arith.solver=6 by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Nikolaj Bjorner f09f1a7524 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-11 08:53:00 -07:00
Nikolaj Bjorner 3a5aebd1d3 tidy model generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-11 08:52:57 -07:00
Nikolaj Bjorner 9f2bafbf10 tidy model generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-11 08:52:13 -07:00
Nikolaj Bjorner e39107c682 turn lemma-id into an attribute on the cotext 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 21:26:51 -07:00
Nikolaj Bjorner 5e5f46f0f8 handle cancelation from nra_solver gracefully 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 17:34:45 -07:00
Nikolaj Bjorner 0170a9772a expose methods for dumping T-lemmas from theory_lra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 16:44:48 -07:00
Lev a4a468660d remove an assert 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-10 12:05:23 -07:00