Bruce Mitchener
|
1067a5363f
|
theory_lra: Remove unused variable.
|
2018-10-02 10:42:54 +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 |
|
Nikolaj Bjorner
|
b2430f5a0a
|
Merge pull request #1858 from waywardmonkeys/remove-unused-sat-par
Remove unused sat_par files.
|
2018-10-01 19:26:46 -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 |
|
Michał Janiszewski
|
661826e27f
|
Add missing template instantion for lar_core_solver::m_r_solver
|
2018-10-01 21:35:48 +02:00 |
|
Christoph M. Wintersteiger
|
aaae3118de
|
CI Test
|
2018-10-01 20:26:05 +01:00 |
|
Christoph M. Wintersteiger
|
f145873603
|
CI Test
|
2018-10-01 20:22:20 +01: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 |
|
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 |
|