mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-25 13:23:32 +00:00
Code Activity
14999 commits 73 branches 58 tags 226 MiB
Commit graph

559 commits

Author SHA1 Message Date
Nikolaj Bjorner
9e4a7ae4b8 add pdd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 16:59:33 -08:00
Nikolaj Bjorner
7d65100330 sat -> dd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 10:14:49 -08:00
Nikolaj Bjorner
20598e3bd2 address clang warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-11 07:16:46 -08:00
Nikolaj Bjorner
d866a93627 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-03 10:29:10 +01:00
Nikolaj Bjorner
376d2c1ed4 add unit test based on #2658 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-25 18:07:43 -07:00
Nikolaj Bjorner
60dde9f3d5 unit test for #2650 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-24 10:32:56 -07:00
Nikolaj Bjorner
a1cb3a21f6 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 07:46:40 -07:00
Nikolaj Bjorner
9c74c05854 address min-int overflow reported in #2565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-17 18:19:55 -04:00
Bruce Mitchener
258b798a6b test-z3: Improve help output. Provide help when no args. 2019-08-16 03:20:57 -07:00
Bruce Mitchener
f02170feb4 Clean up whitespace. 2019-08-16 03:20:57 -07:00
Nikolaj Bjorner
90415a18d3 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-03 08:42:16 -07:00
Lev Nachmanson
e9e950062a fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-08-01 14:09:26 -07:00
Nikolaj Bjorner
d17248821a include chronological backtracking, two-phase sat, xor inprocessing, probsat, ddfw 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-13 08:45:21 -07:00
Nuno Lopes
46d23ea8d7 fix assertion violation in nlsat test 2019-06-13 16:36:03 +01:00
Nuno Lopes
d1cbde3390 fix crash in 'test-z3 prime_generator' 2019-06-13 14:35:52 +01:00
Nikolaj Bjorner
bd109c4522 fix memory leak when using prime_generator as non-static object 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 11:14:25 -07:00
Lev Nachmanson
eae4fd6afd fix the build lp.cpp in test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-19 19:45:33 -07:00
Nikolaj Bjorner
4c76d43670 add binary_merge encoding option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 08:35:22 -08:00
Nikolaj Bjorner
d9a51f8f8a fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 14:44:12 -08:00
Nikolaj Bjorner
064c9faf11 fix test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 20:13:21 +01:00
Nikolaj Bjorner
cda78d8d0b #2117 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:34:45 -08:00
Nikolaj Bjorner
eaa80d5b02 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 11:33:23 -08:00
Nikolaj Bjorner
b6bf299b8b update upolynmial test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 17:41:50 -08:00
Nikolaj Bjorner
360d6f963e reduce output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 17:05:48 -08:00
Bruce Mitchener
1b91694d9b Enable dl_table tests on non-Windows/Cygwin. 2018-12-09 21:02:06 +07:00
Bruce Mitchener
3149d7f7a4 Fix typos. 2018-11-30 22:19:30 +07:00
Bruce Mitchener
e570940662 Prefer using empty rather than size comparisons. 2018-11-27 21:42:04 +07:00
Bruce Mitchener
edf8ba44d1 Switch from using Z3_bool to using bool. 
This is a continuation of the work started by using stdbool and
continued by switching from Z3_TRUE|FALSE to true|false.
 2018-11-20 11:27:09 +07:00
Bruce Mitchener
56bbed173e Remove usages of Z3_TRUE / Z3_FALSE. 
Now that this is all using stdbool.h, we can just use true/false.

For now, we leave the aliases in place in z3_api.h.
 2018-11-20 00:25:37 +07:00
Nikolaj Bjorner
727929c9af fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-14 12:04:31 -08:00
Florian Pigorsch
326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Nikolaj Bjorner
aad09816cb build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 15:16:23 -07:00
Bruce Mitchener
7bc283b84e Avoid unnecessary copies in for-range loops. 2018-10-02 10:38:41 +07:00
Bruce Mitchener
cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nikolaj Bjorner
91dbcbc36f fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-20 18:57:47 -07:00
Lev Nachmanson
b90d571d9a fixing the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-18 15:36:01 -07:00
Nikolaj Bjorner
36a14a354a disable dotnet in ci script. It seems to get turned on even if dotnet bindings are not requested 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-11 03:14:31 -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
a3c692c05f fix include paths 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 13:49:26 -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
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
Lev
a4a468660d remove an assert 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-10 12:05:23 -07:00
Nikolaj Bjorner
3ae0ea8246 add circuit and unate encoding besides sorting option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 21:09:13 -07:00
Lev Nachmanson
8b4223fef2 make lp_tst optional 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-02 19:50:29 -07:00
Nikolaj Bjorner
ca3c076394 fixed reduce 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 08:26:10 -07:00
Nikolaj Bjorner
05738702d6 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 08:10:47 -07:00
Nikolaj Bjorner
fad1e611aa build warnings, updates to reduce-invertible, change is_algebraic tester to use int return type 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 12:34:55 -07:00
Lev Nachmanson
e5eea467b7 adjust hnf 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

change in settings + random in adding terms to hnf

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

add terms in hnf from the beginning

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

adjusting settings

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

remove non used determinant()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-27 12:19:06 -07:00
Lev Nachmanson
eeaca949e0 cleanup in hnf.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fixex in maximize_term

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

prepare for LIRA (#76)

* merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* simple mixed integer example

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Nikolaj's fixes in theory_lra.cpp

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

fixes in maximize_term, disable find_cube for mixed case

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

fix cube heuristic for the mixed case

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

fix the build

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

fix in find cube delta's calculation

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

remove a printout

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

remove a blank line

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

test credentials

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

avoid double checks to add terms in hnf_cutter

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

fixes in add terms to hnf_cutter

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

remove a variable used for debug only

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

remove a field

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

remove a warning and hide m_A_orig under debug

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

use var_register to deal with mapping between external and local variables

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

tighten the loop in explain_implied_bound

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

fixes in theory_lra and relaxing debug checks in pop(), for the case when push() has been done from not fully initialized state

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

suppress hnf cutter when the numbers become too large

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

remove some debug code

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

adjusting hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-27 12:19:02 -07:00
Lev Nachmanson
9ba4026bc6 avoid going creating hnf_cuts if all involved vars have integral values 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

add explanations to hnf cuts

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

nits and virtual methods (#68)

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

cleanup from std::cout

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

handle the case when the number of terms is greater than the number of variables in hnf

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

method name's fix

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

restore hnf_cutter to work with m_row_count <= m_column_count

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

tune addition of rational numbers (#70)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

give shorter explanations, call hnf only when have a not integral var

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

overhaul of mpq (#71)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

fix for 32 bit build (#72)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

yes (#74)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

fix the merge

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

fixes in maximize_term untested

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

fix compilation (#75)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* relax check

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* change for gcc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 12:16:58 -07:00