mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 02:41:52 +00:00
Code Activity
9792 commits 23 branches 48 tags 156 MiB
Commit graph

9792 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
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
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