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

722 commits

Author SHA1 Message Date
Nikolaj Bjorner
56b9c4c8a2 fix bugs reported by phan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-17 04:20:24 +02:00
Nikolaj Bjorner
1bcf5b8b5f remove auxiliary variables from weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 11:42:28 +02:00
Nikolaj Bjorner
15b64261dd fix wmaxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 04:55:56 +02:00
Nikolaj Bjorner
ddd0bf875d fix bugs in optimization for integers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 08:46:24 +02:00
Nikolaj Bjorner
fe5c42c90f fixes to bugs exposed by regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 05:23:47 +02:00
Nikolaj Bjorner
50f18a77af disable 'optimization' that led to wrong model' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 02:40:52 +02:00
Nikolaj Bjorner
ac893e907f fixes to maxsmt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 16:06:03 +02:00
Nikolaj Bjorner
5f72325e99 working on maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 10:00:21 +02:00
Nikolaj Bjorner
04824d86df fixes to model generation of weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 09:37:42 +02:00
Nikolaj Bjorner
5225ea18b7 fix lower/upper bound updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 09:04:48 +02:00
Nikolaj Bjorner
8c85ee6b7c fixing lex optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-13 23:36:42 +01:00
Nikolaj Bjorner
df5c2adc4e debug opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-12 15:39:38 -06:00
Nikolaj Bjorner
f41d23bc0f debugging model generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-12 12:18:34 -06:00
Nikolaj Bjorner
eacb48268c fixing bugs exposed by msf unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-11 19:02:36 -06:00
Anh-Dung Phan
a737639790 Skip lower bound assertions for unbounded objectives 2013-12-11 12:56:48 -08:00
Anh-Dung Phan
34c96a8fe0 Simple guard in order to not get model before setting solver 2013-12-10 17:10:23 -08:00
Nikolaj Bjorner
2c577a304d bug fixes to pb; working on model extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-10 15:16:58 -08:00
Nikolaj Bjorner
0f0397b05f hunt bugs exposed by so.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 18:58:48 -08:00
Nikolaj Bjorner
97b2fc9ee7 fix bugs exposed by testSolver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 18:34:28 -08:00
Nikolaj Bjorner
f0ef339623 fix bug exposed by lia2maxsmt4 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 12:30:52 -08:00
Nikolaj Bjorner
ddb30c51b5 debugging lia2maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 12:17:33 -08:00
Nikolaj Bjorner
370a4b66de update lower bounds from feasible solutiosn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-07 22:09:57 -08:00
Nikolaj Bjorner
e307c5fdda fix minimize->maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-07 14:47:47 -08:00
Nikolaj Bjorner
da348fe1c0 first pass on normalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-07 14:38:09 -08:00
Nikolaj Bjorner
a617eac010 enable bounding for various domains 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-06 19:36:12 -08:00
Nikolaj Bjorner
437a545c3b fix pretty printer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-06 13:12:35 -08:00
Nikolaj Bjorner
4d6aa1a0f3 add to_string and get_help methods to optimize API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-06 11:34:41 -08:00
Anh-Dung Phan
d38e2b9b78 Expose objective indices to .NET API 2013-12-05 17:30:40 -08:00
Nikolaj Bjorner
192ce11ca6 change model binding time 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-05 11:42:04 -08:00
Nikolaj Bjorner
56c4fa8f6d expose models, working on network flow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-04 17:39:54 -08:00
Nikolaj Bjorner
b980a15177 fix leak by commenting out probe experiment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-04 13:02:49 -08:00
Nikolaj Bjorner
e3fe80fd4d add .NET interface and finish C interface for optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-03 20:20:24 -08:00
Nikolaj Bjorner
9e2908c3f5 exposing lower/upper 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-03 17:46:52 -08:00
Nikolaj Bjorner
838a32206c adjust parsing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-03 14:10:07 -08:00
Nikolaj Bjorner
18815e3e53 reorganizing input 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-03 13:36:25 -08:00
Nikolaj Bjorner
51704b7b95 tweaking input processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-03 08:51:46 -08:00
Nikolaj Bjorner
03f5020d0b Nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-02 22:06:15 -08:00
Nikolaj Bjorner
af5d989d6c change verbosity level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-02 21:51:20 -08:00
Nikolaj Bjorner
c14c778735 debugging multi-objective interface and pb revisions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-02 14:30:17 -08:00
Nikolaj Bjorner
faa59ba7f9 debugging multi-objective interface and pb revisions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-02 14:14:44 -08:00
Nikolaj Bjorner
191efbb72f use expression structure for objectives instead of custom s-expression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-02 13:00:51 -08:00
Nikolaj Bjorner
a016caa5d8 add expression conversion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-02 09:47:59 -08:00
Anh-Dung Phan
5ed8a48ac2 Add push/pop to box optimization 2013-11-26 14:16:59 -08:00
Anh-Dung Phan
4aa9c742ab Revise optimize commands 2013-11-26 12:54:18 -08:00
Anh-Dung Phan
dbc791d385 Reorganize combination of objectives 2013-11-26 09:20:11 +01:00
Anh-Dung Phan
87a2b99091 Clean up 2013-11-25 12:16:34 -08:00
Nikolaj Bjorner
2ff51e9a60 move model_evaluator from pdr to model, call it model_implicant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-23 21:33:35 +01:00
Nikolaj Bjorner
97dfb6d521 moving to rational coefficients 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-21 15:55:08 -08:00
Nikolaj Bjorner
ee0abfbfe9 rename card->pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 21:25:02 -08:00
Nikolaj Bjorner
2b2d0e155c debugged new pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 18:03:49 -08:00