mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
15613 commits 49 branches 53 tags 182 MiB
Commit graph

15613 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
dea7c92730 updated nightly 2021-06-04 10:54:32 -07:00
Nikolaj Bjorner
5da4b29136 turn on parity test 2021-06-04 10:18:24 -07:00
Nikolaj Bjorner
c194441824 #5324 2021-06-04 10:18:24 -07:00
Nikolaj Bjorner
73118012c5 #5324 2021-06-04 09:40:31 -07:00
Nikolaj Bjorner
7c86134e85 #5324 2021-06-03 18:36:44 -07:00
Nikolaj Bjorner
0182187296 fix regression in arithmetic resource bound 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-03 11:41:42 -07:00
Nikolaj Bjorner
d2330055e7 disable travis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-02 18:27:57 -07:00
Nikolaj Bjorner
8a02167e30 get-universe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 21:08:08 -07:00
Nikolaj Bjorner
3e773fba5e get-universe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 21:07:48 -07:00
Nikolaj Bjorner
6a5cdd48e7 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 20:43:45 -07:00
Nikolaj Bjorner
ab3b387076 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 20:37:43 -07:00
Nikolaj Bjorner
45adfc6a66 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 20:31:05 -07:00
Nikolaj Bjorner
0e6d530518 std::cout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 18:49:37 -07:00
Nikolaj Bjorner
2156c74d51 #4702 
initial gcd test implementation for accumulated parity constraints
 2021-06-01 15:26:36 -07:00
Nikolaj Bjorner
5127014f18 track cuts 2021-06-01 15:26:36 -07:00
Jakob Rath
9cc78ef98e
Polysat: unit testing minor changes (#5326) 
* Use check instead of check_sat in tests

* First steps at standalone entry point
 2021-06-01 10:12:51 -07:00
Nikolaj Bjorner
ba56bfa656 spelling 2021-05-31 19:04:38 -07:00
Nikolaj Bjorner
e2c5e2e39c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-31 12:32:33 -07:00
Nikolaj Bjorner
8d1dfb9f32 #5223 2021-05-31 12:30:05 -07:00
Nikolaj Bjorner
fe0727d889 #5223 2021-05-31 12:29:31 -07:00
Nikolaj Bjorner
fb75dac63f #5223 2021-05-31 12:01:33 -07:00
Jakob Rath
46f8b15c14
ref/ref_vector minor convenience changes (#5322) 
* Add ref_vector_core::push_back(ref<T>&&)

* Make operator bool() explicit
 2021-05-31 10:27:46 -07:00
Nikolaj Bjorner
50cf321171 fix #5320 2021-05-31 10:18:27 -07:00
Nikolaj Bjorner
83e2e7200c fix #5316 2021-05-30 11:28:31 -07:00
Nikolaj Bjorner
4d75281841 fix #5315 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-30 10:38:04 -07:00
Nikolaj Bjorner
b1606487f0 fix #5289 2021-05-30 10:32:30 -07:00
Nikolaj Bjorner
4d41db2920 #5223 
unreachable code in dual solver
 2021-05-29 09:49:47 -07:00
Nikolaj Bjorner
3024fe7baf fix #5312 2021-05-29 08:17:33 -07:00
Nikolaj Bjorner
56b47fa956 fix #5304 2021-05-29 08:06:06 -07:00
Nikolaj Bjorner
15916091d1 fix #5307 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-28 14:38:41 -07:00
Nikolaj Bjorner
ce6fc21bef fix #5300 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-28 14:17:13 -07:00
Nikolaj Bjorner
c5d4ff9b6f fix #5300 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-28 14:16:43 -07:00
Nikolaj Bjorner
f42d4a58e3 fix #5308 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-28 14:10:32 -07:00
Iain Scott
48beb814f5
Use more generic linux-x64 for NuGet rid instead of specific ubuntu, debian, etc. (#5310) 2021-05-28 13:53:52 -07:00
Jakob Rath
8757f04d20
Polysat: disjunctive lemmas (#5311) 
* Add macro to disable linear solver for development

* Move new_* and add_* to header

* Add ref_vector_core::push_back(ref<T>&&)

* Attempt to simplify lifetime handling

* Make operator bool() explicit

* clause improvements

* display boolean assignment

* clause::resolve

* bug fixes

* more fixes

* final case of backtrack
 2021-05-28 13:53:08 -07:00
Nuno Lopes
5a66dfad2a change parameter::hash so that the least significant bits arent overriden 
the 3rd bit was being stuck by the parameter kind, leading to increased number of hash collisions
 2021-05-27 09:38:21 +01:00
Nikolaj Bjorner
322531e95c fix #5303 2021-05-25 10:20:20 -07:00
Nuno Lopes
36ca98cbbe ast: remove 2 default constructors 2021-05-24 14:59:03 +01:00
Nikolaj Bjorner
5fd3ef6580 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-23 16:50:47 -07:00
Nikolaj Bjorner
2ebab021f2 fix #5297 2021-05-23 13:42:15 -07:00
Nikolaj Bjorner
8919fa4970 #5296 2021-05-23 10:32:09 -07:00
Gram
3d8865d925
Fix some PEP-8 violations in Python code (#5295) 
* reformat python code using autopep8

* manually wrap some too long lines and adjust some checks

* run autopep8 in aggressive mode

* run autopep8 in very aggressive mode

* manually reformat z3types.py

* unify: use double quotes

* use sys.version_info instead of sys.version

* drop accidentally commited src/util/z3_version.h
 2021-05-23 10:27:55 -07:00
Nuno Lopes
f1545b04d2 optimize symbol table for single-threaded mode 
remotes a bunch of mem allocs + unnecessary computations on every string lookup
 2021-05-23 16:35:44 +01:00
Nuno Lopes
aef38099bf vector.h: add assert to fail compilation if alignment isn't ok 
let's see if all buildbots are happy with this..
 2021-05-23 15:57:56 +01:00
Nuno Lopes
8fd7226b6f typo 2021-05-23 14:28:42 +01:00
Nuno Lopes
f1e0d5dc8a remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
Nuno Lopes
f8406623b4 switch parameter to an std::variant 
plus fix mem leak & move constructor for zstrings
 2021-05-23 13:07:29 +01:00
Nuno Lopes
9eb566b401 simplify some constructors/destructors 2021-05-23 12:39:49 +01:00
Nuno Lopes
79201e5ce6 buffer.h c++17 improvements 
1) ensure data is properly aligned
2) add move constructor (useful for zstrings)
 2021-05-23 12:11:12 +01:00
Nuno Lopes
34e8a2f0f6 simplify 2021-05-23 12:01:04 +01:00