mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
19410 commits 23 branches 48 tags 157 MiB
Commit graph

19410 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
5e30323b1a wip - bounded local search for arithmetic 2023-02-11 15:46:39 -08:00
Nikolaj Bjorner
4b2c166e8b fixes to build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-11 10:19:24 -08:00
Nikolaj Bjorner
7bef2f3e6f wip - local search for euf/arithmetic 2023-02-11 09:33:43 -08:00
Nikolaj Bjorner
46c8d78ece fixes for #6577 
- the literal false should not appear in clauses
- the literal true forces a tautology
- fix early return in is_cnf check. It should check all clauses for nested Booleans.
 2023-02-11 09:33:42 -08:00
Nikolaj Bjorner
d22e4aa525 wip - integrating arithmetic local search 2023-02-11 09:33:42 -08:00
Nikolaj Bjorner
1b0c76e3f0 fixes to mbqi in the new core based on #6575 2023-02-10 16:56:06 -08:00
Julian Parsert
d52e893528
Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort* (#6576) 
Co-authored-by: Julian Parsert <julian.parsert@uibk.ac.at>
 2023-02-10 10:00:26 -08:00
Nikolaj Bjorner
2f86d9de75 bypass assertion violation for parity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-09 16:33:30 -08:00
Clemens Eisenhofer
6b48b25beb Draft: Made division/remainder to op_constraints (not yet used - old code still called) 2023-02-09 23:36:15 +01:00
Jakob Rath
4813fcfe0d re-propagate needs to be checked for all literals 2023-02-09 19:06:16 +01:00
Nikolaj Bjorner
e31eb9a6b1 add monotonicity lemma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-09 09:31:43 -08:00
Jakob Rath
c60a2b10a5 inequality::rewrite_equiv 2023-02-09 16:33:59 +01:00
Jakob Rath
06cc15d1cc refinement loop output 2023-02-09 16:28:52 +01:00
Nikolaj Bjorner
02d48adae5 fix #6573 2023-02-08 08:24:52 -08:00
Jakob Rath
a0f5386bdd Use parity helper functions 2023-02-08 15:11:39 +01:00
Nikolaj Bjorner
a8335f2d5e use phase 2023-02-07 19:50:45 -08:00
Nikolaj Bjorner
b3ebce3966 fix compilation 2023-02-07 19:30:45 -08:00
Nikolaj Bjorner
96d815b904 adding arith sls 2023-02-07 19:27:19 -08:00
Nikolaj Bjorner
6a2d60a6ba fix #6571 
most solvers don't support background properties
 2023-02-07 11:04:58 -08:00
Nikolaj Bjorner
601e506d54 remove debug out 2023-02-07 10:40:49 -08:00
Nikolaj Bjorner
a150e58893 update release script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-07 09:21:02 -08:00
Nikolaj Bjorner
90a75866fb elaborating on local-search rephase strategy 2023-02-07 03:17:52 -08:00
Jakob Rath
bf03886a87 elem 2023-02-07 09:57:32 +01:00
Nikolaj Bjorner
f3ae7692ca update stage name 2023-02-06 16:08:14 -08:00
Nikolaj Bjorner
c1cadd37cc update stage name 2023-02-06 16:07:12 -08:00
Nikolaj Bjorner
a7231027c3 try side-by-side nightly 2023-02-06 16:04:54 -08:00
Nikolaj Bjorner
c1c26f0726 restart after sat solution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-06 09:21:35 -08:00
Jakob Rath
984e98c88f Avoid duplicates 2023-02-06 17:52:52 +01:00
Jakob Rath
a37536e0ae clarify unsat_core 2023-02-06 17:52:52 +01:00
Jakob Rath
c79a16db2a Fix dependency tracking for input boolean conflicts 2023-02-06 16:28:41 +01:00
Jakob Rath
d105c1c825 Allow printing other types than unsigned 2023-02-06 16:27:38 +01:00
Jakob Rath
d7797a53df temporary fix 2023-02-06 11:34:28 +01:00
Jakob Rath
8774952aeb Merge remote-tracking branch 'origin/master' into polysat 2023-02-06 10:50:05 +01:00
Nikolaj Bjorner
03a4920f3d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-05 21:41:07 -08:00
Nikolaj Bjorner
75c573877d updates to ddfw, initial local search phase option 2023-02-05 21:35:22 -08:00
Nikolaj Bjorner
992793bd56 update nuget packaging targets #6570 2023-02-05 21:35:22 -08:00
Nikolaj Bjorner
b45f42133d updates to try_div_monotonicity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-04 15:55:14 -08:00
Nikolaj Bjorner
3712cbdbfd fix #6559 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-04 13:33:40 -08:00
Jakob Rath
d69155b9e9
Shared features from polysat branch (#6567) 
* Allow setting default debug action

* Fix dlist and add iterator

* Add var_queue iterator

* Add some helpers

* rational: machine_div2k and pseudo_inverse

* Basic support for non-copyable types in map

* tbv helpers

* pdd updates

* Remove duplicate functions

gcc doesn't like having both versions
 2023-02-03 13:08:47 -08:00
Frederick Robinson
be44ace995
fix typo (#6569) 2023-02-03 13:08:35 -08:00
Jakob Rath
539a4e4eae less eval 2023-02-03 17:43:07 +01:00
Jakob Rath
1a733a3a50 compute polysat unsat core 2023-02-03 17:37:09 +01:00
Jakob Rath
579275a17d cleanup 2023-02-03 16:33:02 +01:00
Jakob Rath
4b1ec583ec Remove outdated assertion 2023-02-03 16:07:58 +01:00
Jakob Rath
63416dbcd7 fix 2023-02-03 15:59:26 +01:00
Jakob Rath
6365e322f3 Try to propagate boolean decisions after backjumping 2023-02-03 15:56:19 +01:00
Jakob Rath
5678c1c592 We need more clause names 2023-02-03 15:54:56 +01:00
Jakob Rath
bdf20f513b debug 2023-02-03 11:18:11 +01:00
Clemens Eisenhofer
ae41f82939 Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat 2023-02-03 07:15:58 +01:00
Clemens Eisenhofer
c042505c34 Another monotonicity lemma 2023-02-03 07:15:10 +01:00