mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity
17880 commits 49 branches 53 tags 182 MiB
Commit graph

17880 commits

This branch
This branch
All branches
Author SHA1 Message Date
Zachary Wimer
831afa8124
Cpp api add missing fp methods (return type correction) (#5200) 
* added is_nan and is_inf to API

* added support to to_ieee_bv

* bug fix
 2021-04-19 17:55:23 -07:00
Zachary Wimer
10e9345cd7
C++ API add missing FP methods (#5199) 
* added is_nan and is_inf to API

* added support to to_ieee_bv
 2021-04-19 15:24:09 -07:00
Jakob Rath
4da1b7b03c
Add functionality for BDD vectors (#5198) 
* Fix XOR over BDDs

* Add operator<< for find_int_t

* Add equality assertion macro that prints expression values on failure

* Adapt contains_int and find_int to take externally-defined bits

* Add more operations on BDD vectors

* Remove old functions

* Additional bddv functions

* Rename some things

* Make bddv a class and add operators

* Fix find_num/contains_num calls
 2021-04-19 09:05:19 -07:00
Zachary Wimer
542878dea3
Add sge and sgt to API; now has sge,sgt,sle,slt, and unsigned counterparts (#5194) 2021-04-19 08:53:43 -07:00
Zachary Wimer
f8228ff50e
[c++ api] add const (#5195) 2021-04-19 10:24:12 +01:00
Nikolaj Bjorner
981839ee73 separate out search throttle 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-17 14:36:50 -07:00
Nikolaj Bjorner
0d65b19c20 cr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-17 14:27:47 -07:00
Nikolaj Bjorner
4b35c75712 add code review and replacement for mk_int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-17 14:19:17 -07:00
Nuno Lopes
e67b9ebcf7 try to fix ARM32 build (#2776) 2021-04-17 16:14:05 +01:00
Nikolaj Bjorner
572197aede add some code review comments, stubs for ule 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-16 12:43:23 -07:00
Nikolaj Bjorner
9df7e9a029 add outline for ule constraints, change bit to var constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-16 12:31:11 -07:00
Nikolaj Bjorner
5706c7a93b addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-16 10:37:53 -07:00
Nikolaj Bjorner
c7868579c0 add sample bdd vector operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-16 10:22:48 -07:00
Nikolaj Bjorner
af2376e9e4 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-16 10:00:44 -07:00
Jakob Rath
f72e30e539
Add BDD utilities; use them for narrowing/propagation of linear equality constraints (#5192) 
* Add a few helper methods for encoding sets of integers as BDDs

* Use BDD functions in solver

* Add bdd::find_int

* Use bdd::find_int in solver

* Add narrowing for linear equality constraints

* Simplify code for linear propagation

* Add test for later

* Narrowing can only handle linear constraints with a single variable

* Need to push_cjust
 2021-04-16 08:44:18 -07:00
Zachary Wimer
a1741e0e16
z3 c++ api: delete implicit constructor (#5191) 2021-04-16 10:46:03 +01:00
Nikolaj Bjorner
e970fe5034 sketch bit-constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-15 23:04:25 -07:00
Nikolaj Bjorner
dce9740a38 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-15 21:53:27 -07:00
Nikolaj Bjorner
12ccd99e84 trail 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-15 17:39:00 -07:00
Nikolaj Bjorner
549b984c88 move to self-contained trail instructions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-15 17:38:36 -07:00
Nikolaj Bjorner
2eadcd586a add new file for eq_constraint 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-15 14:34:01 -07:00
Nikolaj Bjorner
c733789467 move more equality functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-15 14:24:50 -07:00
Zachary Wimer
239ace4353
expr move semantics supported via ast (#5190) 2021-04-15 13:37:31 -07:00
Nikolaj Bjorner
5163492d5b move constraint handler functionality to self-contained / separate classes. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-15 13:08:25 -07:00
Nikolaj Bjorner
0d78a10630 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-15 12:11:33 -07:00
Jakob Rath
55a908e357
Fix Windows build (#5188) 2021-04-15 09:18:20 -07:00
Jakob Rath
cb9dda19dd
Polysat (#5187) 
* test_l2 works now

* Linear propagation: test whether a is odd

* Linear propagation with even coefficients (wip)
 2021-04-15 08:37:14 -07:00
Jakob Rath
feb31045f5
Add more logging to polysat (#5186) 
* Add polysat logging support

* Don't really need the usual log levels

* Indent log headings

* Add display method to ptr_vector

* Add some logging to solver

* Use __FUNCSIG__ on MSVC
 2021-04-15 08:35:57 -07:00
Jakob Rath
7067fc16ae
Test and fix PDD subst_val (#5185) 2021-04-15 08:35:46 -07:00
Nikolaj Bjorner
bb7754a767 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 22:41:56 -07:00
Nikolaj Bjorner
9a2b7677bf na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 22:03:28 -07:00
Nikolaj Bjorner
034132d245 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 21:46:59 -07:00
Nikolaj Bjorner
ce75656e2b del-var 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 21:46:13 -07:00
Nikolaj Bjorner
e6c9f27de4 misc fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 14:15:43 -07:00
Nuno Lopes
21e59f7c6e
change model evaluator to respect resource limits (#5184) 2021-04-14 11:48:39 -07:00
Jakob Rath
8a260d89cd
Small polysat fixes (#5183) 
* Add some display functions

* Add new variables to free vars
 2021-04-14 10:29:58 -07:00
Rolf Eike Beer
7f8e2a9f75
clean up CMake code (#5182) 
* CMake: simplify FindGMP.cmake

Remove printing of all the different variables, and let FPHSA output the library
name. Add an imported target, which bundles the library and the include
directories for easier usage.

* fix build: vector::c_ptr() now is vector::data()

* CMake: use Threads::Threads imported module

Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect.

* CMake: remove needless policy setting

The minimum required version is CMake 3.4, where these policies are already set
to new because they were introduced earlier.

* CMake: remove needless variable expansion
 2021-04-14 10:29:15 -07:00
Nuno Lopes
ce96182746 micro opt: dont reallocate an hashtable in a destructor 2021-04-14 17:32:34 +01:00
Nikolaj Bjorner
3730a0373d Merge branch 'master' of https://github.com/z3prover/z3 into polysat 2021-04-14 05:08:26 -07:00
Nikolaj Bjorner
892e6d9ed5 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 05:06:46 -07:00
Nikolaj Bjorner
a45687d5db add very basic unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 05:03:44 -07:00
Nikolaj Bjorner
de66c12b93 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 04:53:13 -07:00
Nikolaj Bjorner
8c9aae5640 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-04-14 04:49:00 -07:00
Nikolaj Bjorner
332c123244 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 04:48:53 -07:00
Jakob Rath
324d9ed461
Add more PDD utilities (div, pow) (#5180) 
* Expose 'inv' on rationals to get reciprocal value

* Align parameter names with implementation

* Add cached operation that divides PDD by a constant

* Fix display for constant PDDs

* operator^ should probably call ^ instead of + (mk_xor instead of add)

* Add helper function 'pow' on PDDs
 2021-04-14 04:48:42 -07:00
Nikolaj Bjorner
2f7069a8b7 move include path in test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 04:06:50 -07:00
Nikolaj Bjorner
57486f0b3d split into parts, add stats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 04:05:35 -07:00
Nikolaj Bjorner
21baa2a70a Merge branch 'master' of https://github.com/z3prover/z3 into polysat 2021-04-14 03:51:12 -07:00
Nikolaj Bjorner
4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
a0d112b7b0 general form migration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-13 13:00:47 -07:00