mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 10:19:23 +00:00
Code Activity
15277 commits 46 branches 52 tags 178 MiB
Commit graph

15277 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
ee081f7434 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-20 14:05:28 -07:00
Nikolaj Bjorner
ce8184382d add dummy implementations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-20 14:02:12 -07:00
Nikolaj Bjorner
fc60690742 tidy, initial polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-20 12:21:50 -07:00
Nikolaj Bjorner
82bc6474a3 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-04-20 12:03:33 -07:00
Nikolaj Bjorner
831edba1c8 fixplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-20 12:03:28 -07:00
Jakob Rath
77350d97da
BDD vectors: add subtract and quot_rem, move finite domain abstraction out of bdd_manager (#5201) 
* Coding style

* Simplify bddv class

* mk_eq: run loop from below

* Add unit test for bddv unsigned comparison

* Add test that shows contains_num/find_num fail after reordering

* Add BDD vector subtraction

* Call apply_rec in mk_ite_rec instead of apply

* Question about mk_quant

* Implement quot_rem over BDD vectors

* Move shl/shr to bddv

* Make unit test smaller

* Add class dd::fdd to manage association between BDDs and numbers

* Remove contains_num/find_num from bdd_manager
 2021-04-20 09:09:32 -07:00
alexandernutz
bc695a5a97
monotonicity unit tests (#5202) 
* monotonicity unit tests

* indentation
 2021-04-20 09:09:17 -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
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
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
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
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
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
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
Nikolaj Bjorner
7025d85da3 migrating to general form 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-13 11:21:41 -07:00
Nuno Lopes
524dcd35f9 reorder fields of context_params to save memory 
plus improve error checking in context_params::set_uint
 2021-04-13 18:35:58 +01:00
Nuno Lopes
49906a5a58 api_context: remove basic&arith fids fields 
these are now constant,s o we can save some space
the remaining ones need to be made constant as well..
 2021-04-13 17:42:42 +01:00