mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity
16763 commits 23 branches 48 tags 157 MiB
Commit graph

16763 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
a623865a82 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-06 05:44:31 +02:00
Jakob Rath
613b0db4cc fix refcount issue 2022-03-19 04:19:16 +01:00
Jakob Rath
d41d3fa6ea fix some bugs 2022-03-18 16:05:51 +01:00
Jakob Rath
fd353bff17 unsat core 2022-03-18 15:49:44 +01:00
Jakob Rath
509a007ed7 Integrate univariate solver in polysat 2022-03-18 15:43:06 +01:00
Jakob Rath
9d47d7959d helper functions to add constraints to univariate_solver 2022-03-17 14:08:00 +01:00
Jakob Rath
edeba9b56a support op_constraint in univariate solver 2022-03-17 14:03:42 +01:00
Jakob Rath
c4370eb7e6 univariate solver seems to work 2022-03-11 18:06:32 +01:00
Jakob Rath
1de51da67e get univariate coefficients 2022-03-11 18:03:39 +01:00
Jakob Rath
74281fa830 compile 2022-03-11 08:33:10 +01:00
Jakob Rath
8b1f1d0e11 begin univariate solver impl 2022-03-10 17:58:37 +01:00
Jakob Rath
78028bedae use solver_factory 2022-03-10 16:57:08 +01:00
Jakob Rath
4a86c3fb67 looks like QF_BV is handled by inc_sat_solver 2022-03-10 16:19:35 +01:00
Jakob Rath
c648b57493 forbidden intervals only used by viable 2022-03-10 16:12:13 +01:00
Jakob Rath
afc711d6ec move into separate component 2022-03-10 16:10:56 +01:00
Jakob Rath
d4a28d4553 implementation stub 2022-03-10 11:13:06 +01:00
Jakob Rath
6aee62ef2f Univariate solver interface 2022-03-10 11:01:57 +01:00
Jakob Rath
9b20f17f9c compile 2022-03-10 10:57:49 +01:00
Jakob Rath
22411f8b43 one more special case 2022-03-10 10:32:23 +01:00
Nikolaj Bjorner
1faccffd0d add smul over and underflow predicate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-20 11:39:45 +02:00
Nikolaj Bjorner
dc3b921712 eq explain 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 19:00:24 +02:00
Nikolaj Bjorner
8c9835bca6 smul no overflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 18:55:07 +02:00
Nikolaj Bjorner
89d6f1c191 update mk_project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-02 18:04:52 -08:00
Nikolaj Bjorner
57d3abbf64 compile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-02 08:40:44 -08:00
Nikolaj Bjorner
4c4f916917 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-02 08:24:58 -08:00
Nikolaj Bjorner
32edbfa28e two bugs: check for always false, adjust start of list was incorrect during re-insert 2022-02-02 07:37:35 -08:00
Nikolaj Bjorner
1a36b74143 dbg 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-01 19:32:07 -08:00
Nikolaj Bjorner
18291543d6 fixing corner cases for viable intervals 2022-02-01 13:21:51 -08:00
Nikolaj Bjorner
c48f14e537 updated conflict state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-01 11:47:33 -08:00
Nikolaj Bjorner
486cc632d0 notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-31 09:16:48 -08:00
Jakob Rath
5ee02ec5df Merge remote-tracking branch 'origin/polysat' into polysat 2022-01-31 15:36:22 +01:00
Jakob Rath
15854301b2 Generalize refine_disequal_lin 2022-01-31 15:35:25 +01:00
Jakob Rath
f80eb6237d includes shouldn't depend on debug/release mode 2022-01-31 15:29:25 +01:00
Nikolaj Bjorner
697b561c7a update comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-30 17:34:00 -08:00
Nikolaj Bjorner
b488a1fadd WIP revamp conflict state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-29 16:17:58 -08:00
Nikolaj Bjorner
60248d0981 resolution is still wrong 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-29 09:32:14 -08:00
Jakob Rath
67647433ba log justifications during conflict resolution 2022-01-28 15:52:52 +01:00
Nikolaj Bjorner
0eb0306ae2 update comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 17:47:27 -08:00
Nikolaj Bjorner
93541ccdf2 enable try-push-block 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 17:42:33 -08:00
Nikolaj Bjorner
0677eb1c05 fixing up missing dependencies during resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 16:58:16 -08:00
Nikolaj Bjorner
1264fe462d merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 14:33:38 -08:00
Nikolaj Bjorner
ff4b471f93 resurrect Booelan decisions to deal with quot-rem and similar axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 14:26:41 -08:00
Jakob Rath
4236830a8e Also check clauses when returning SAT 2022-01-27 12:23:57 +01:00
Nikolaj Bjorner
be790b8892 add back minimize vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 18:01:26 -08:00
Nikolaj Bjorner
6df23fbce3 add note about a bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 16:58:00 -08:00
Nikolaj Bjorner
0eaf5a8510 factor cache pointers are invalid if the table is resized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 16:18:18 -08:00
Nikolaj Bjorner
d1fcc41c7f merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 21:53:10 +01:00
Nikolaj Bjorner
0895ce8723 update mk_project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 21:44:56 +01:00
Nikolaj Bjorner
ff93c03972 integrate polysat into bv solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 20:20:45 +01:00
Jakob Rath
d7548f6867 Now we can have a working binary add_eq/add_diseq 2022-01-26 11:50:49 +01:00