mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity
10237 commits 23 branches 48 tags 157 MiB
Commit graph

8487 commits

Author SHA1 Message Date
Nikolaj Bjorner f5fea8ae30 add parameter to force sat-cleaning on initialization and on simplification phases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-11 22:05:04 -07:00
xlauko 3b86ea3f8a Add a floating-point support to c++ api. 2018-10-11 16:30:59 +02:00
nilsbecker 91dd01d6ff Merge branch 'master' of https://github.com/Z3Prover/z3 2018-10-09 16:42:30 +02:00
nilsbecker 547fbd4764 avoid rechecking whether equality explanations are already logged 2018-10-09 16:42:10 +02:00
Nikolaj Bjorner 2f9853f1b5
Merge pull request #1865 from ahelwer/master 
Files and changes for Z3 NuGet package
 2018-10-06 21:46:52 -07:00
Andrew Helwer 7941074fd1 Added packaging directions, removed linkresource flag 2018-10-06 18:22:55 -07:00
Nikolaj Bjorner f14a2b9a7c fix java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 16:13:23 -07:00
Nikolaj Bjorner aad09816cb build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 15:16:23 -07:00
Nikolaj Bjorner c4829dfa22 fix #1577 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 09:01:01 -07:00
Nikolaj Bjorner 44a0dbbc61 fix #1864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 08:06:51 -07:00
nilsbecker a0f6447a33 logging which theory added constraints 2018-10-05 13:58:22 +02:00
Lev 99339798ee fix the value oflar_solver.m_status during pop() 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-10-04 19:43:01 -07:00
Nikolaj Bjorner 2097983db3 fix java bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-04 14:05:38 -07:00
Nikolaj Bjorner b540868cd7 Merge branch 'master' of https://github.com/z3prover/z3 2018-10-04 13:43:04 -07:00
Nikolaj Bjorner a549e73b86 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-04 13:43:01 -07:00
Nikolaj Bjorner f8e5d989bf fix #1577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 17:49:57 -07:00
Nikolaj Bjorner 3bc2213d54 fix #1577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 17:43:42 -07:00
Nikolaj Bjorner 46cdefac4d fix memory leak when cuber isn't run to completion. Found by Daniel Selsam 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 10:57:02 -07:00
Nikolaj Bjorner fd9fd52271 fixing #1847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-02 17:13:46 -07:00
Nikolaj Bjorner 8b981e545d
Merge pull request #1855 from mtrberzi/refactoring-arith 
Z3str3: refactoring, arith_value
 2018-10-02 14:10:36 -07:00
Nikolaj Bjorner 69f35a2970
Merge branch 'master' into intel-compiler 2018-10-02 11:54:52 -07:00
Murphy Berzish b2f0051114 Merge remote-tracking branch 'upstream/master' into refactoring-arith 2018-10-02 12:38:40 -04:00
Murphy Berzish 39fbf1e174 Z3str3: don't use arith_value::get_value in get_arith_value 2018-10-02 12:28:53 -04:00
Nikolaj Bjorner 55cc89b6bb
Merge pull request #1862 from kbobyrev/arith_eq_solver-cleanup 
[NFC] Cleanup arith_eq_solver.(cpp|h)
 2018-10-02 08:48:49 -07:00
Nikolaj Bjorner cc312d2f68
Merge pull request #1861 from waywardmonkeys/macos-naming 
Refer to macOS rather than Mac OS / OSX.
 2018-10-02 08:28:02 -07:00
Nikolaj Bjorner 5bf57c2700 fix cubing semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-02 08:14:19 -07:00
Kirill Bobyrev a376a8d343 [NFC] Cleanup arith_eq_solver.(cpp|h) 
Use for-range loops instead of for-index loops where possible, remove
trailing whitespaces.

This patch does not affect functionality.
 2018-10-02 16:14:01 +03:00
Bruce Mitchener a76397d3b8 Refer to macOS rather than Mac OS / OSX. 2018-10-02 17:38:09 +07:00
Nikolaj Bjorner 620c5d1d81
Merge pull request #1850 from Nils-Becker/master 
adding call to update_max_generation
 2018-10-01 21:49:14 -07:00
Nikolaj Bjorner 2cf6ada38e
Merge pull request #1856 from waywardmonkeys/minor-fixes 
Minor fixes
 2018-10-01 20:46:27 -07:00
Nikolaj Bjorner c84182b42a
Merge pull request #1859 from waywardmonkeys/for-range-copy 
Avoid unnecessary copies in for-range loops.
 2018-10-01 20:44:52 -07:00
Nikolaj Bjorner 7082d85115
Merge pull request #1860 from waywardmonkeys/modernize-use-override 
Use 'override' where possible.
 2018-10-01 20:43:56 -07:00
Bruce Mitchener 6d2936e5fc watch_list: Fix indentation. 2018-10-02 10:43:00 +07:00
Bruce Mitchener 1067a5363f theory_lra: Remove unused variable. 2018-10-02 10:42:54 +07:00
Bruce Mitchener 7bc283b84e Avoid unnecessary copies in for-range loops. 2018-10-02 10:38:41 +07:00
Bruce Mitchener 373b691709 Use 'override' where possible. 2018-10-02 10:26:38 +07:00
Nikolaj Bjorner 5eb24d3118 Merge branch 'master' of https://github.com/z3prover/z3 2018-10-01 20:22:10 -07:00
Nikolaj Bjorner 9d0aa4d02d update empty cube case for sat/undef cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 20:22:02 -07:00
Nikolaj Bjorner 3c7e7a7ffd
Merge pull request #1852 from janisozaur/unused-const 
Drop unused CV-qualifiers from scalar return values
 2018-10-01 20:10:21 -07:00
Nikolaj Bjorner 4bc6720af7
Merge pull request #1853 from janisozaur/solve-ax-eq-b 
Add missing template instantion for lar_core_solver::m_r_solver
 2018-10-01 20:09:50 -07:00
Nikolaj Bjorner be8a9c611e incorporate #1854 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 19:49:18 -07:00
Nikolaj Bjorner 096a6c088d Merge branch 'master' of https://github.com/z3prover/z3 2018-10-01 19:32:52 -07:00
Nikolaj Bjorner bb979a194e remove unused return value of mk_enode following #1856 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 19:32:44 -07:00
Nikolaj Bjorner b0dac346dc
Merge pull request #1857 from waywardmonkeys/modernize-use-nullptr 
Use nullptr.
 2018-10-01 19:28:58 -07:00
Bruce Mitchener 489582f7fa Remove unused sat_par files. 
These look like they were replaced by `sat_parallel` files and
aren't currently built or used.
 2018-10-02 09:19:14 +07:00
Bruce Mitchener cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nikolaj Bjorner 808d2eb60f Merge branch 'master' of https://github.com/z3prover/z3 2018-10-01 15:52:25 -07:00
Nikolaj Bjorner 08c58ae614 make the unsat/sat verdicts from cubing produce empty clause and models respectively 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 15:52:22 -07:00
Murphy Berzish 03d9047490 Merge remote-tracking branch 'upstream/master' into refactoring-arith 2018-10-01 17:51:12 -04:00
Michał Janiszewski 5c9b1c7b11 Add support for Intel Compiler 2018-10-01 21:45:01 +02:00
Michał Janiszewski 661826e27f Add missing template instantion for lar_core_solver::m_r_solver 2018-10-01 21:35:48 +02:00
Michał Janiszewski cdbfd9654f Drop unused CV-qualifiers from scalar return values 2018-10-01 21:14:25 +02:00
Christoph M. Wintersteiger 7a2a2a32cc Merge branch 'master' of https://github.com/Z3Prover/z3 2018-10-01 17:25:14 +01:00
Christoph M. Wintersteiger 48ec7c1175
Follow-up fix for fpa2bv_converter. 2018-10-01 17:25:02 +01:00
Nikolaj Bjorner 75b77979fe Merge branch 'master' of https://github.com/z3prover/z3 2018-10-01 09:18:46 -07:00
Nikolaj Bjorner aaba1b9b15 fix sort retrieval for lambdas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 09:18:40 -07:00
nilsbecker c92c431570 adding call to update_max_generation 2018-10-01 16:32:04 +02:00
Christoph M. Wintersteiger 2a92de0aee
Fixed side conditions for UFs translated from FP to BV. Fixes #1825. 2018-10-01 15:20:00 +01:00
Christoph M. Wintersteiger 35bf63d563 Fixed filename in CMakeLists.txt 2018-10-01 12:29:14 +01:00
Christoph M. Wintersteiger f0e74b7f2a Fix for module name clash (and thus linking error) in the Visual Studio solution. 2018-10-01 12:11:42 +01:00
Nikolaj Bjorner 90fca8b378 add psat to available tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-30 17:44:28 -07:00
Nikolaj Bjorner faf96ca910 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-30 17:40:16 -07:00
Nikolaj Bjorner a5762a78e9 change to ast-vector 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-30 17:39:18 -07:00
Lev 5d586c8fd1 set lar_solver.m_status = UNKNOWN in the constructor 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-30 15:12:50 -07:00
Nikolaj Bjorner 6dcec4ce79 z3_assert -> _z3_assert 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-28 16:38:43 -07:00
Nikolaj Bjorner e0490450f3 add capabilities to python API, fix model extraction for qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-28 13:23:28 -07:00
Nikolaj Bjorner 70094d5213 Merge branch 'master' of https://github.com/z3prover/z3 2018-09-25 23:54:53 -07:00
Nikolaj Bjorner 26d40865fa add verbose output to capture cases for empty cube 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-25 23:54:48 -07:00
Lev Nachmanson e68deab443 Merge branch 'master' of https://github.com/Z3Prover/z3 2018-09-25 13:34:23 -07:00
Lev Nachmanson 0b2b6b1306 assert all_constraints_hold() rarely 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-25 13:33:30 -07:00
Nikolaj Bjorner af41255a9d fix regression in model generation for UFLRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-25 10:00:13 -07:00
Nikolaj Bjorner b4b9da9d8b Merge branch 'master' of https://github.com/z3prover/z3 2018-09-24 16:53:41 -07:00
Nikolaj Bjorner 7335b3bf56 remove debug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-24 16:53:15 -07:00
Nikolaj Bjorner 80d0c5cf82 fix #1836 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-24 16:52:25 -07:00
Lev Nachmanson 867368c0cd
Merge pull request #1845 from levnach/gomory 
refactor some parameters into fields in Gomory cuts
 2018-09-23 20:45:53 -07:00
Lev Nachmanson 066b5334ad refactor some parameters into fields in Gomory cuts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-22 20:57:59 -07:00
Nikolaj Bjorner 9a09689dfa add documentation on the cuber 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-22 19:19:05 -07:00
Lev Nachmanson 2d46234fd0
Merge pull request #1843 from levnach/gomory 
changes in column_info of lar_solver
 2018-09-22 14:29:40 -07:00
Nikolaj Bjorner 7b3b1b6e9f pop to base before incremental internalization to ensure that units are not lost 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-22 14:04:15 -07:00
Lev Nachmanson 43f89dc2cc changes in column_info of lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-22 12:01:24 -07:00
Nikolaj Bjorner 3113901c8f rename is_atom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-21 23:15:57 -07:00
Nikolaj Bjorner f349d3d013 fix extraction of non-units 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-21 21:15:28 -07:00
Nikolaj Bjorner 984e74428a fix include path for z3_version.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-21 20:41:26 -07:00
Nikolaj Bjorner 8e0eebf507 fix include path for z3_version.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-21 20:37:13 -07:00
Nikolaj Bjorner e391416855 fix include path for z3_version.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-21 20:30:50 -07:00
Nikolaj Bjorner 0c4754d94b rename version.h to z3_version.h to differentiate name in install include directory. Add support for z3_version.h in python build system. #1833 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-21 20:13:58 -07:00
Nikolaj Bjorner 38c6429184
Merge pull request #1838 from NikolajBjorner/master 
remove offsets from terms to fix cut generation
 2018-09-21 17:03:42 -07:00
Nuno Lopes 0b7918c52e remove spurious pragma 2018-09-21 09:37:36 +01:00
Nikolaj Bjorner 618e1bee5b merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-20 20:41:00 -07:00
Nikolaj Bjorner c59a957737 add non-units method 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-20 20:37:14 -07:00
Nikolaj Bjorner 4e75efa485
Merge pull request #1839 from dselsam/master 
extend(src/api/c++/z3++.h): support units() for solver class
 2018-09-20 20:04:17 -07:00
Nikolaj Bjorner 39ed27101e include version.h in install include directory for cmake build #1833 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-20 19:56:55 -07:00
Daniel Selsam d6a1d17d69 extend(src/api/c++/z3++.h): support units() for solver class 2018-09-20 19:47:32 -07:00
Nikolaj Bjorner 382bce4bb7 fix #1836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-20 19:19:40 -07:00
Nikolaj Bjorner 91dbcbc36f fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-20 18:57:47 -07:00
Nikolaj Bjorner d75b6fd9c1 remove offsets from terms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-20 11:06:05 -07:00
Nikolaj Bjorner dcda39e76e merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-19 17:12:32 -07:00
Nikolaj Bjorner 3c553c17e8 fix dump utility for cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-19 14:32:56 -07:00
Lev Nachmanson a99ebed907 keep the coefficients of 'at lower' variables positive, and the rest negative for Gomory cuts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-19 10:17:27 -07:00
Nikolaj Bjorner ed19af4c4e merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-19 09:02:37 -07:00
Lev Nachmanson b90d571d9a fixing the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-18 15:36:01 -07:00
Lev 041458f97a fixes the +- bug in gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-18 14:42:32 -07:00
Lev b940b7873b work on Gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-18 13:47:18 -07:00
Lev ca3ce964ce work on Gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-18 13:34:05 -07:00
Murphy Berzish 144b72244e clean up pragmas, Z3str3 refactoring 2018-09-18 16:11:47 -04:00
Murphy Berzish 7e419137b1 Z3str3: refactor regex automata to subroutine, use arith_value 2018-09-17 16:13:34 -04:00
Nikolaj Bjorner 5bbe0508e4 Merge branch 'master' of https://github.com/z3prover/z3 2018-09-16 13:43:55 -07:00
Nikolaj Bjorner 1a3fe1edd3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-16 13:43:38 -07:00
Nikolaj Bjorner 286126dde9 fix #1828, add self-contained utility to extract arithmetical values for use in theory_seq and theory_str and other theories that access current values assigned to numeric variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-16 13:31:37 -07:00
Lev 106b677201 fixes in gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-15 17:47:54 -07:00
Lev 34bdea750c fixes in gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-15 17:46:16 -07:00
Lev 8c122ba9bd fixes in gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-15 17:33:35 -07:00
Lev 03d55426bb fixes in gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-15 17:15:46 -07:00
Lev 324396e403 separate the gomory cut functionality in a separate file 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 17:12:49 -07:00
Lev 26764b076f adjust cuts and branch (m_t and m_k) for terms 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 12:39:46 -07:00
Lev 257ba6218f remove gomory.h 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 11:54:10 -07:00
Lev 22213a9e73 rebase 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 11:53:54 -07:00
Lev Nachmanson 57357b7ece does not compile 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-14 11:52:44 -07:00
Lev 5dee39721a rebase 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 11:52:14 -07:00
Lev e705e5a309 branch on inf basic in gomory 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 11:49:39 -07:00
Nikolaj Bjorner 78950fde17 initialize solver before parse is invoked. Fixes issue reported by Selsam 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-13 19:05:45 -07:00
Daniel Selsam 2a8d207bf4 remove duplicate method definitions 2018-09-13 14:31:52 -07:00
Nikolaj Bjorner 6ea4aff622 add validation code for cuts, fix missing unit propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-13 10:47:50 -07:00
Nikolaj Bjorner 4ffd860375 narrowing incorrect lemma generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-11 11:31:19 -07:00
Nikolaj Bjorner 3bf072557e disable branches when arguments are non-integral #1824 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-11 04:14:28 -07:00
Nikolaj Bjorner b1423e17a1 Merge branch 'master' of https://github.com/z3prover/z3 2018-09-11 03:14:41 -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
Lev Nachmanson da20d949c6
Merge pull request #1823 from levnach/bound_vars 
Create special lemmas for "div"
 2018-09-10 18:47:52 -07:00
Nikolaj Bjorner 445546b684 fix gc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-10 17:20:40 -07:00
Nikolaj Bjorner 18bec88a8a purify non-constant terms by default to enforce theory #1820 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-10 15:52:02 -07:00
Lev Nachmanson f810a5d8c3 remove an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-10 15:22:48 -07:00
Nikolaj Bjorner e818b7bd27 fix #1812 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-10 15:15:00 -07:00
Nikolaj Bjorner a37d05d54b fix #1819 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-10 13:53:44 -07:00
Nikolaj Bjorner def6f19edb
Merge pull request #1818 from mtrberzi/str-const-canonical 
Z3str3/Seq: canonicalize encoding of string constants/symbols
 2018-09-10 13:46:51 -07:00
Lev Nachmanson 813b906341 do not bound all free vars 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-10 13:43:29 -07:00
Lev Nachmanson 8068c64cab avoid using not initialized variables in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-10 11:02:38 -07:00
Nikolaj Bjorner e61373cd4f Merge branch 'master' of https://github.com/z3prover/z3 2018-09-10 08:57:38 -07:00
Nikolaj Bjorner fae66671d8 fix #1817 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-10 08:57:35 -07:00
Nikolaj Bjorner 67a2a26009 fixing bound detection (#86) 
* fixing bound detection

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

* check-idiv bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-09 14:26:46 -07:00
Lev Nachmanson 211210338a bound vars 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-07 22:00:25 -07:00
Nikolaj Bjorner 13abf5c6a6 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-06 17:49:52 -07:00
Murphy Berzish b09035565a canonicalize encoding of string constants/symbols 2018-09-05 19:04:11 -04:00
Arie Gurfinkel f67346d16e Fix is_infty_level to treat 2^16-1 as infinity 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 5d2f682f7a Enable proof mode in add_cover 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 7bff74dec0 Minor pass on synchronize transform 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 24044429a7 Rename cache to m_cache 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 0516e6f21f Integrating synchronize pass 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 8400122596 mk_synchronize rule transformation 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 3a01fd791b Replace rule API 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 0035d9b8cb Background external invariants 
Background external invariants are constraints that are assumed to be
true of the system. This commit introduces a mode in which
background invariants are used only duing inductive generalization
and lemma pushing, but not during predecessor computation.

It is believed that this will be more efficient used of background
external invariants since they will not be able to disturb how
predecessors are generalized and computed.

Based on a patch by Jorge Navas
 2018-09-04 21:49:59 -04:00
Arie Gurfinkel 533e9c5837 Expand equality literals when eq_prop is disabled 
When equality propagation is disabled for arithmetic,
equality atoms are expanded into inequality for potentially
better generalization with interpolation
 2018-09-04 21:49:59 -04:00
Nikolaj Bjorner f53b7aaca2 fix none-case 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-04 15:46:10 -07:00
Nikolaj Bjorner 9ad17296c2 update parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-03 17:22:48 -07:00
Nikolaj Bjorner c8730daea7 fix memory leak, add strengthening 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-03 16:56:07 -07:00
Nikolaj Bjorner c39d7c8565 updated resolvents 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-03 11:17:50 -07:00
Nikolaj Bjorner e8a78ec696 remove std::max for #1752 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-03 10:24:01 -07:00
Nikolaj Bjorner 85e7b18451 fix name to divisible, guard under smtlib2_compliant as sugguested in #1757 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-01 18:22:10 -07:00
Nikolaj Bjorner 43807a7edc adding roundingSat strategy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-31 20:25:49 -05:00
Nikolaj Bjorner 94ffa3963e fix #1800 by converting large integers to strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-24 16:54:22 +02:00
Nikolaj Bjorner 7230461671 adding properities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-20 23:51:51 +02:00
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 fd5cfbe402 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-15 10:38:23 -07:00
Nikolaj Bjorner 03bd010b05 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 21:19:06 -07:00
Nikolaj Bjorner d67bfd78b9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 21:15:55 -07:00
Nikolaj Bjorner 40a79694ea add job/resource axioms on demand 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 16:33:34 -07:00
Nikolaj Bjorner 2839f64f0d rename to csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 11:05:55 -07:00
Nikolaj Bjorner a478f95999 remove debug assert 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 10:56:52 -07:00
Nikolaj Bjorner 502c071266 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 09:57:06 -07:00
Nikolaj Bjorner d55fe1ac59 na' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 09:41:43 -07:00
Nikolaj Bjorner a096ec648c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-13 17:11:22 -07:00
Nikolaj Bjorner 540baa88f4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-13 17:08:34 -07:00
Nikolaj Bjorner 3478b8b924 add js-model interfacing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-12 18:14:06 -07:00
Nikolaj Bjorner 0af00e62de abstract arithmetic value extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-12 12:42:26 -07:00
Nikolaj Bjorner abd902d58c n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-11 18:14:32 -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 55f15b0921 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-10 17:52:34 -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
Nikolaj Bjorner baeff82e59 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-10 09:46:21 -07:00
Nikolaj Bjorner 0d8de8f65f add theory outlline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-09 20:19:26 -07:00
Nikolaj Bjorner 2b968f9e63 initial decl plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-09 15:29:39 -07: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
Nikolaj Bjorner b59fa3ebd7 fix #1746 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 09:05:24 -07:00
Lev c4c52ad104 enable printing in Release 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Lev Nachmanson 5c712d471f create hnf cuts too, when gomory_cut_period is 2 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Lev Nachmanson c518ddac6f rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Lev Nachmanson fd980952ea rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Lev Nachmanson 367fff618d setting smt.arith.solver=6 by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Nikolaj Bjorner fc4627a24f force the new arithmetic solver for QF_LIA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 16:33:48 -07:00
Nikolaj Bjorner 567fbac27f add back old multiplication for comparison 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 14:33:32 -07:00
Nikolaj Bjorner de454db58c guard expensive ite rewrites under configuration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 14:17:39 -07:00
Nikolaj Bjorner 8373bec6ad only assign, if there isn't already a true literal incube/clause mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 10:33:56 -07:00
Nikolaj Bjorner efe440839e Merge branch 'master' of https://github.com/z3prover/z3 2018-07-09 09:19:37 -07:00
Nikolaj Bjorner 605dcc40a3 fix #1741 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 09:19:13 -07:00
Nikolaj Bjorner 4b802fd5cd
Merge pull request #1740 from alexanderjsummers/master 
Added return value to bool-typed function
 2018-07-09 09:05:52 -07:00
Nuno Lopes 009708ed07 remove unneeded creation of tmp mpz_manager 2018-07-09 10:52:27 +01:00
Nuno Lopes 6f7271a5e8 remove virtual destructor from api::pmanager 2018-07-09 10:37:26 +01:00
alexanderjsummers d6a3afd2a1
Added return value to bool-typed function 
It seems that without this, the build fails with a default Visual C++ on Windows; see https://docs.microsoft.com/en-gb/cpp/error-messages/compiler-warnings/compiler-warning-level-1-c4716 

Another option would be to add the #pragma directive mentioned there.
 2018-07-09 11:30:24 +02:00
Nuno Lopes c5a282dadb sat_allocator: align allocation size with page boundary to reduce memory consumption 2018-07-08 18:04:32 +01:00
Nuno Lopes a85a4f41c7 ast_exception: remove str copies 2018-07-08 15:32:01 +01:00
Nuno Lopes fd75eccfec don't even bother allocating traces in release mode 2018-07-08 13:21:16 +01:00
Nikolaj Bjorner a2d078f6f5
Merge pull request #1737 from Nils-Becker/master 
Equality Explanation Logging
 2018-07-07 15:39:08 -07:00
Nikolaj Bjorner 290302dca8
Merge pull request #1738 from agurfinkel/deep_space 
Fix bug in proof checking
 2018-07-07 15:36:39 -07:00
Nuno Lopes d2b77b1170 remove dead code 2018-07-07 19:07:13 +01:00
Arie Gurfinkel 1de0f8fe5e Fix bug in proof checking 2018-07-07 19:10:16 +03:00