mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-07 19:41:15 +00:00
Code Activity
19430 commits 49 branches 53 tags 194 MiB
Commit graph

1808 commits

Author SHA1 Message Date
Jakob Rath
1d805807e9 Allow setting a default debug action 
Helps avoiding user interaction when running a batch of unit tests.
 2022-11-08 17:13:36 +01:00
Nikolaj Bjorner
4d8860c0bc wip - adding context equation solver 
the solve_eqs_tactic is to be replaced by a re-implementation that uses solve_eqs in the simplifiers directory.
The re-implementation should address efficiency issues with the previous code.
At this point it punts on low level proofs. The plan is to use coarser
dependency tracking instead of low level proofs for pre-processing. Dependencies can be converted into a proof hint representation that can be checked using a stronger checker.
 2022-11-05 10:34:57 -07:00
Nikolaj Bjorner
ae2672f132 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-04 14:11:24 -07:00
Nikolaj Bjorner
154b09309b fixing build, wip on model reconstruction integration into dependent-expr-state 2022-11-04 14:04:44 -07:00
Nikolaj Bjorner
49d1490454 add ad-hoc any-of for cross compatibility and simplifying interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-04 12:48:30 -07:00
Nikolaj Bjorner
90490cb22f make visited_helper independent of literals 
re-introduce shorthands in sat::solver for visited and have them convert literals to unsigned.
 2022-11-03 03:54:39 -07:00
Clemens Eisenhofer
6790f18132
Added limit to "visit" to allow detecting multiple visits (#6435) 
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation

* Added limit to "visit" to allow detecting multiple visits

* Putting visit in a separate class
(Reason: We will probably need two of them in the sat::solver)

* Bugfix
 2022-11-03 03:34:52 -07:00
Clemens Eisenhofer
ae707ffff7
Added 64-bit "1" counting (#6434) 
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation

* Added 64-bit "1" counting
 2022-11-02 10:02:29 -07:00
Nuno Lopes
4431fd17ce memory_manager: add support for MacOS & Windows to the new size tracking system 2022-10-24 10:09:56 +01:00
Gleb Popov
5b76a7c2f2
Enable HAS_MALLOC_USABLE_SIZE on FreeBSD (#6402) 2022-10-17 10:14:04 -07:00
Nikolaj Bjorner
2d8b7b5ac6 deal with compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-13 17:55:47 +02:00
Nuno Lopes
8ad480ab59 fix compiler warnings 2022-10-12 09:43:50 +01:00
Nuno Lopes
a41520acf1 mpf: fix some string copies 2022-10-11 11:59:29 +01:00
Nuno Lopes
661a1624b4 avoid string copying in mpf_manager::set 2022-10-07 14:03:13 +01:00
Jakob Rath
e18bc46de1 Move on_scope_exit to util.h 2022-10-07 14:23:26 +02:00
Nuno Lopes
a792251a82 remove old compat code 2022-10-06 17:22:17 +01:00
Jakob Rath
f184545aca Debug dlist insertion 
Found because of assertion failure in
test_polysat::test_fixed_point_arith_div_mul_inverse()
 2022-10-05 17:24:28 +02:00
Jakob Rath
9cc9d1fac4 count 2022-10-04 14:08:44 +02:00
Jakob Rath
cd2d197bb9 Add compact version of std::all_of 2022-10-03 10:55:13 +02:00
Jakob Rath
0bea276e82 Add dll_iterator 2022-10-03 10:54:24 +02:00
Nuno Lopes
be3c7d7115 delete dead code 2022-10-02 21:44:08 +01:00
Jakob Rath
1df749ad33 Merge branch 'master' into polysat 2022-09-23 17:14:26 +02:00
Nikolaj Bjorner
9a987237d5 don't rename uint_set but keep the original name 2022-09-18 17:22:59 -07:00
Nuno Lopes
9717dadd9f
Use glibc's malloc_usable_size when available (#6321) 2022-09-05 13:40:02 -07:00
Nikolaj Bjorner
2f8b13368d add redirect for warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-23 15:55:55 -07:00
Nikolaj Bjorner
0eea021dc3 include global parameters and fixup for HTML meta-characters 2022-08-22 14:25:18 -07:00
Nuno Lopes
d5d77dfe64 minor code simplifications 2022-08-20 12:56:45 +01:00
Nikolaj Bjorner
e83a70f9ad add newlines for description 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-19 06:57:39 -07:00
Nikolaj Bjorner
9d6de2f873 parameters neatified 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 09:14:34 -07:00
Nikolaj Bjorner
b169292743 add parameter descriptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 08:26:53 -07:00
Nikolaj Bjorner
77a313ff76 redo #6242 
revert to byte based high watermark
add mb based high watermark
 2022-08-08 11:26:18 +03:00
Bruce Mitchener
5014b1a34d Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
Nikolaj Bjorner
c51af91256 #6257 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-05 09:19:49 +03:00
Nikolaj Bjorner
78a0f57398 for #6257 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-05 08:09:39 +03:00
Bruce Mitchener
1d9345c3de Fix typos. 2022-08-05 07:40:50 +03:00
Jakob Rath
d7f0181c46 Merge branch 'master' into polysat 2022-08-04 08:53:34 +02:00
Saloed
d908ebec4c fix memory_high_watermark parameter according to documentation 2022-08-03 18:50:54 +03:00
Jakob Rath
6c4d60c5af Basic support for non-copyable types in map 2022-08-02 12:31:29 +02:00
Jakob Rath
e105a91d4a Merge branch 'master' into polysat 2022-08-02 11:31:01 +02:00
Bruce Mitchener
886c3abec1 Remove remnants of _MP_MSBIGNUM checks. 2022-08-02 09:28:57 +03:00
Bruce Mitchener
9a99c78ffb Enable thread_local code more broadly. 
This was only being enabled on Windows, Linux, and FreeBSD. (FreeBSD
only had it enabled in the legacy build system, not in cmake.)

`thread_local` is part of C++11, so now that we require C++17
or later and more recent compilers, this should work everywhere
that threading does, so only disable it within a `SINGLE_THREAD`
build.
 2022-08-02 09:24:51 +03:00
Bruce Mitchener
82d853e5f8 Use = delete to delete special methods. 
This provides a better experience than just marking them as
private and leaving them as undefined symbols.
 2022-08-02 09:23:14 +03:00
Jakob Rath
5d858da58a union_find::reserve 2022-08-01 18:37:11 +03:00
Jakob Rath
e8e64d3098 dlist::insert_before/after 2022-08-01 18:37:11 +03:00
Jakob Rath
6eae27ffad numeral helper functions 2022-08-01 18:37:11 +03:00
Jakob Rath
e31926d132 var_queue display 2022-08-01 18:37:11 +03:00
Jakob Rath
6a929f91c8 scoped_ptr_vector usability 2022-08-01 18:37:11 +03:00
Jakob Rath
d2fe174320 Add SASSERT_EQ and VERIFY_EQ 2022-08-01 18:37:11 +03:00
Jakob Rath
79ee543d25 Move tbv to util 2022-08-01 18:37:11 +03:00
Jakob Rath
0f51f3ed17 Merge branch 'master' into polysat 2022-08-01 15:03:03 +02:00