mirror of
https://github.com/Z3Prover/z3
synced 2025-10-28 18:29:23 +00:00
Commit graph
Select branches
Hide pull requests
7677-potential-issue-in-arithmetic-optimization
arie
copilot/add-finite-set-constructors
copilot/add-finite-set-rewriter
copilot/add-finite-set-value-factory
copilot/add-implementation-finite-set-axioms
copilot/add-rewrite-rules-finite-set-rewriter
copilot/complete-finite-set-header
copilot/fix-7941
copilot/fix-8720d50e-3ea8-4d98-8aed-98393b4b96aa
copilot/fix-dd97045b-5ca3-4f7b-8edf-c3764fc4e5fd
copilot/fix-finite-set-decl-plugin
copilot/implement-fresh-value-algorithm
copilot/implement-inverter-functions-finite-set-operators
copilot/rename-set-select-to-filter
copilot/update-api-z3-mk-datatype-sort
copilot/update-finite-set-check-function
copilot/update-finite-set-fully-interp
daily-backlog-burner-clang-format-6fb0b10f9edf9f15
daily-backlog-burner-fix-dylib-versioning-aad58f6ba3afa571
daily-backlog-burner-issue-templates-a5164506b19a6d1c
daily-backlog-burner/add-clang-format-b2c2bf893132649d
daily-perf-improver-699a33043be4ab3a
daily-test-coverage-improver-533b3200fa126ff4
daily-test-improver-array-peq-tests-4dee5e83be600bcf
daily-test-improver-ast-printer-tests-f01c21ee11444fc9
daily-test-improver-expr-context-simplifier-tests-92d84ac6eb401c41
dependabot/github_actions/actions/download-artifact-6
dependabot/github_actions/actions/upload-artifact-5
finite-sets
ilana
lws
master
nl2lin
par
parallel
perf/xxhash-optimization-8cab442e0c080529
poly
polysat
pyodide-ci
revert-7981-copilot/add-finite-set-value-factory
rs
smtmus
synth
upoly
xor
#1
#1
#1000
#1002
#1004
#1007
#1010
#1013
#1017
#1018
#1020
#1024
#1026
#1031
#1033
#1036
#1037
#104
#1040
#1040
#1049
#1050
#106
#1066
#1069
#107
#107
#1070
#1073
#1076
#108
#108
#1084
#1089
#1090
#1091
#1094
#1095
#1096
#1099
#11
#1104
#1105
#1110
#1111
#1114
#1115
#1117
#1119
#1126
#1129
#1131
#1136
#1138
#1142
#1144
#1145
#1146
#1147
#1158
#1162
#1166
#117
#1174
#1181
#1182
#1183
#1185
#1188
#1189
#12
#12
#1205
#1207
#1208
#1216
#1220
#1222
#1225
#1226
#1228
#1229
#1232
#1238
#1253
#1256
#1256
#1259
#126
#1262
#127
#127
#1270
#1271
#128
#1280
#1281
#1282
#1289
#130
#1300
#1301
#1307
#1307
#1312
#1315
#1323
#1324
#1325
#1336
#1337
#1338
#134
#1341
#1351
#1351
#1355
#1360
#1363
#1363
#1381
#1385
#1385
#1391
#1396
#1400
#1400
#1401
#1410
#1412
#1430
#1431
#1432
#1433
#1434
#1435
#1436
#1438
#1440
#1453
#146
#1462
#1464
#1464
#1465
#1466
#1467
#147
#147
#1472
#1473
#1474
#1478
#1479
#1480
#1482
#1483
#1485
#1486
#1487
#1494
#1495
#1497
#15
#1501
#1503
#1506
#1506
#1508
#1517
#1518
#1519
#152
#152
#1527
#1528
#1537
#1541
#1542
#1546
#155
#155
#1552
#1552
#1556
#1557
#1559
#1560
#1562
#1565
#1588
#1591
#1596
#1597
#16
#1606
#1610
#1611
#1612
#1613
#1624
#1630
#1631
#1635
#164
#1640
#1641
#1642
#1646
#1650
#1651
#1656
#166
#1660
#1660
#1666
#1669
#1669
#1671
#1671
#1673
#1679
#1684
#1686
#1687
#169
#1691
#1692
#1693
#1697
#170
#170
#1700
#1701
#1705
#1706
#1706
#1707
#1708
#1708
#1709
#1710
#1715
#1716
#172
#172
#1721
#1723
#1724
#1727
#1728
#1728
#173
#173
#1731
#1731
#1732
#1737
#1738
#1740
#1743
#1744
#1747
#1748
#1748
#1750
#1751
#1751
#1756
#1758
#1771
#1773
#1774
#1775
#1777
#1779
#1781
#1790
#1792
#1796
#1797
#1799
#18
#1809
#1815
#1818
#1823
#1826
#1829
#1834
#1837
#1838
#1839
#1840
#1840
#1843
#1845
#1848
#1849
#1849
#1850
#1852
#1853
#1854
#1855
#1856
#1857
#1858
#1859
#1860
#1861
#1862
#1863
#1865
#1867
#1869
#1873
#1876
#1877
#1878
#188
#188
#1880
#1881
#1883
#1884
#1886
#1887
#1888
#1893
#1894
#1902
#1906
#1915
#1918
#1930
#1931
#1935
#1938
#1939
#1942
#1947
#1949
#1950
#1951
#1952
#1954
#1955
#1960
#1963
#1964
#1967
#1969
#1972
#1973
#1974
#1975
#1976
#1977
#1982
#1983
#1986
#1990
#1991
#1992
#1993
#1995
#1996
#1997
#1998
#1999
#2
#2
#2001
#2002
#2003
#2004
#2005
#2008
#2010
#2011
#2012
#2013
#2014
#2015
#2016
#2017
#2020
#2021
#2024
#2025
#2026
#2032
#2033
#2034
#2049
#2050
#2051
#2052
#2056
#2062
#2064
#2065
#2066
#2073
#2084
#2088
#21
#2103
#2105
#2121
#2124
#2132
#2133
#2143
#2146
#2147
#2148
#2150
#2163
#2166
#2167
#2170
#218
#2180
#2181
#2183
#2189
#2192
#2193
#2204
#2206
#2224
#2227
#2229
#2233
#2264
#2275
#2280
#2281
#2283
#2292
#2294
#23
#2311
#2312
#2313
#2315
#2329
#2330
#2334
#2335
#2338
#2339
#234
#2345
#235
#2356
#236
#2368
#238
#2382
#2383
#2389
#2393
#2399
#24
#24
#242
#242
#2428
#2438
#244
#2454
#2455
#2459
#246
#2462
#2463
#2464
#2465
#2472
#2475
#2477
#2482
#2485
#2486
#2488
#2490
#2492
#2493
#2494
#2495
#2496
#2499
#2528
#2529
#253
#2538
#2540
#2541
#2545
#255
#2550
#2554
#256
#2568
#2594
#26
#2600
#261
#2611
#2614
#2620
#2627
#2628
#2634
#2635
#2638
#2639
#2645
#2648
#2651
#2655
#2660
#2661
#267
#2677
#268
#2683
#270
#271
#2710
#2719
#272
#273
#2730
#2731
#2732
#2738
#2739
#274
#2745
#2746
#275
#275
#2754
#276
#2769
#2786
#280
#282
#283
#2834
#2839
#284
#284
#2846
#285
#2853
#2858
#286
#2862
#2864
#287
#2876
#2880
#2881
#289
#2893
#2895
#2899
#2907
#2931
#2940
#2942
#2947
#295
#296
#2964
#2971
#2972
#298
#2987
#2988
#299
#2997
#2999
#3002
#3007
#3008
#303
#3032
#3048
#305
#3050
#3059
#306
#306
#309
#3091
#3093
#3094
#3095
#3097
#310
#3102
#3112
#3117
#3117
#3139
#321
#3228
#329
#33
#33
#3321
#334
#3368
#338
#3394
#340
#344
#3445
#346
#347
#349
#3498
#350
#350
#351
#3541
#355
#356
#357
#3596
#3617
#362
#363
#3671
#3687
#37
#3706
#373
#374
#3745
#375
#378
#379
#380
#3818
#3821
#3823
#385
#3851
#3875
#389
#389
#390
#390
#3900
#394
#3946
#3950
#396
#3965
#398
#4
#4
#401
#4011
#4043
#4056
#4059
#4068
#4070
#4072
#4075
#408
#409
#4092
#4094
#4101
#412
#413
#414
#4157
#4160
#4170
#4184
#4198
#4199
#4205
#4206
#4207
#4215
#4247
#4248
#4249
#4253
#4254
#427
#4274
#4276
#4277
#4278
#4298
#4312
#4313
#4319
#4320
#4321
#4325
#4329
#4331
#4333
#4341
#4342
#4356
#4358
#4360
#4361
#4368
#437
#4381
#4382
#4384
#4385
#4386
#4397
#4399
#441
#4413
#4415
#4420
#444
#4440
#4443
#446
#4462
#4464
#4468
#4472
#4477
#4482
#4484
#4487
#4488
#449
#4490
#4492
#4495
#4496
#4499
#4501
#4504
#4505
#4506
#4509
#4514
#4516
#4517
#4528
#4529
#453
#4535
#4545
#4550
#4551
#4556
#4558
#4560
#4562
#4585
#459
#459
#4595
#4596
#4597
#4598
#4599
#4602
#4603
#4605
#461
#4610
#4611
#4612
#4617
#4619
#4620
#4621
#4629
#4636
#4638
#4647
#4650
#4654
#4656
#4657
#4658
#4659
#466
#4663
#4666
#4667
#467
#4674
#4676
#468
#4681
#4682
#4684
#4685
#4692
#4693
#4695
#4698
#470
#470
#4703
#4705
#4707
#4709
#471
#4710
#4714
#4719
#4722
#4723
#4729
#4733
#4739
#4741
#4748
#4751
#4753
#4755
#4757
#4759
#4760
#4761
#4771
#4782
#4785
#4803
#4818
#483
#4832
#4833
#484
#4846
#4850
#4857
#486
#4864
#487
#4878
#4887
#49
#49
#490
#4906
#4911
#4915
#4917
#4954
#4958
#4959
#4960
#4976
#498
#4981
#499
#4996
#500
#500
#5001
#5003
#5004
#5005
#5008
#5015
#5021
#503
#5038
#5039
#504
#5040
#505
#5055
#506
#5079
#5081
#5082
#5091
#5097
#5098
#5104
#5105
#5116
#5118
#5120
#5128
#513
#5130
#5155
#5156
#516
#5163
#5165
#5169
#517
#5170
#5171
#5172
#5173
#5174
#5175
#5176
#5177
#5180
#5182
#5183
#5184
#5185
#5186
#5187
#5188
#5189
#519
#5190
#5191
#5192
#5194
#5195
#5198
#5199
#5200
#5201
#5202
#5203
#5209
#521
#5214
#5217
#5218
#5220
#5221
#5222
#5227
#5228
#523
#5230
#5231
#5234
#5240
#5241
#5242
#5246
#525
#5251
#526
#5265
#5268
#527
#5275
#528
#5288
#529
#529
#5290
#5291
#5292
#5293
#5295
#531
#5310
#5311
#5322
#5326
#5327
#5332
#5348
#5351
#5353
#5355
#5360
#5364
#5366
#5368
#5369
#537
#537
#5370
#5371
#5372
#5383
#5385
#5386
#5387
#5389
#539
#540
#5411
#5413
#5416
#5431
#5440
#5442
#5444
#545
#5451
#5453
#5458
#5459
#5463
#5466
#5475
#5477
#5483
#5489
#5496
#55
#550
#5512
#5513
#5514
#552
#5520
#5521
#5524
#5525
#5529
#553
#553
#5534
#5536
#554
#5540
#5547
#5549
#5550
#5555
#5567
#5569
#5585
#5587
#5588
#5600
#5601
#5602
#5607
#5616
#5617
#5618
#5620
#5622
#5625
#5626
#5628
#5631
#5632
#5633
#5634
#5640
#5654
#566
#5669
#568
#5690
#5695
#5696
#5697
#5703
#5709
#5717
#5721
#5723
#5724
#5728
#5729
#5730
#5731
#5739
#575
#5756
#576
#5760
#5762
#5782
#5787
#580
#5821
#583
#5832
#5835
#5839
#5843
#5844
#5845
#5854
#5859
#5864
#5868
#5878
#5879
#5881
#5884
#5888
#5892
#5893
#5897
#5898
#5901
#5901
#5902
#5905
#5916
#5921
#5923
#5944
#5947
#5951
#5956
#5960
#5963
#5964
#5966
#597
#5971
#5972
#5974
#5975
#5976
#5977
#5978
#5979
#598
#5982
#5992
#5994
#5996
#5997
#600
#6000
#6003
#601
#601
#6010
#6025
#6026
#6029
#603
#6035
#6037
#6048
#606
#6063
#6064
#6065
#6066
#6067
#6068
#6069
#6072
#6073
#6074
#6075
#6077
#608
#6086
#6093
#6096
#6099
#6101
#6102
#6103
#6118
#6120
#6125
#6136
#6139
#6146
#6148
#6150
#6152
#6156
#6161
#6162
#6166
#6175
#618
#618
#6185
#6186
#6186
#6188
#6189
#6191
#6192
#6195
#6198
#6199
#6202
#6203
#6204
#6207
#6209
#621
#621
#6210
#6211
#6216
#6217
#6219
#622
#6220
#6221
#6222
#6223
#6224
#6225
#6226
#6227
#6231
#6232
#6233
#6234
#6235
#6236
#6238
#6239
#6242
#6245
#6246
#6247
#6249
#6251
#6252
#6253
#6254
#6256
#6257
#6261
#6266
#6269
#627
#627
#6277
#6278
#6280
#6284
#6287
#6290
#6291
#6297
#630
#630
#6306
#6307
#6312
#6318
#6321
#6325
#6327
#6329
#6332
#6345
#6353
#6358
#6360
#6361
#6362
#6378
#6381
#639
#6393
#6402
#6405
#6406
#641
#6411
#6412
#6419
#6420
#6422
#6424
#6434
#6435
#6448
#6449
#645
#6458
#646
#6468
#6472
#648
#6483
#6489
#6497
#6509
#6514
#6516
#6526
#6527
#6528
#6529
#6533
#6534
#6540
#6541
#6549
#6562
#6567
#6569
#6576
#6596
#6597
#6608
#661
#6612
#6613
#6618
#6619
#6623
#6625
#6626
#6627
#6628
#6639
#6653
#6656
#6663
#6673
#6678
#6707
#6712
#6715
#6720
#6723
#6733
#6739
#675
#6750
#6755
#6756
#6759
#6765
#6771
#6772
#6773
#6774
#6779
#6780
#6786
#6791
#6795
#6797
#6803
#6814
#6816
#6820
#6829
#6831
#6833
#6834
#6840
#6841
#6844
#6845
#6846
#6859
#6862
#6863
#6864
#6867
#6875
#6878
#6879
#6883
#6884
#6887
#6888
#6895
#6896
#6905
#6906
#6909
#6910
#6911
#6929
#6931
#6932
#6938
#6939
#6940
#6948
#6949
#695
#6954
#6960
#6961
#6963
#6966
#6968
#6973
#6975
#6976
#6979
#6980
#6985
#6992
#6993
#6999
#700
#7002
#7008
#7013
#7014
#7015
#7016
#7019
#7021
#7022
#7025
#7028
#7030
#7034
#7039
#7042
#7043
#7044
#7045
#7051
#7052
#7054
#7057
#7058
#7059
#7060
#7063
#7065
#7066
#7067
#7068
#7069
#7071
#7075
#7077
#708
#7088
#7095
#7097
#7099
#710
#710
#7108
#7115
#7116
#7118
#7119
#713
#713
#7131
#7133
#7136
#7137
#7138
#7139
#7140
#7145
#7147
#7148
#7149
#715
#715
#7150
#7152
#7153
#7155
#7157
#7159
#7163
#7169
#7170
#7171
#7173
#7184
#7192
#7200
#722
#7226
#7227
#7230
#7235
#7244
#7251
#7254
#7257
#7261
#7265
#7269
#7271
#728
#7280
#7288
#7289
#729
#7293
#7294
#7296
#7297
#7298
#7299
#73
#730
#7300
#7301
#7303
#7304
#7307
#7308
#7312
#7313
#7316
#7317
#7320
#7322
#7323
#7324
#7327
#7328
#7333
#7337
#7338
#7339
#735
#7350
#7351
#7353
#7354
#7356
#736
#7365
#737
#7384
#7387
#7388
#739
#7396
#74
#7400
#7401
#7408
#741
#7412
#742
#7422
#7423
#7426
#7428
#7429
#7437
#7439
#7442
#7452
#746
#7462
#7469
#747
#7471
#7473
#7477
#7479
#7480
#7481
#7495
#7496
#7497
#7498
#75
#750
#7503
#7504
#7506
#7508
#7514
#7516
#7519
#752
#7529
#7530
#7531
#7533
#7534
#7535
#7537
#7540
#7545
#7547
#7548
#7551
#7553
#7557
#7565
#757
#7576
#7577
#7579
#7587
#759
#7597
#7598
#7599
#76
#760
#7608
#761
#7610
#7612
#7613
#7614
#7615
#7617
#7618
#7619
#7620
#7628
#7631
#764
#7645
#7646
#7649
#7651
#7652
#7653
#7654
#7656
#7657
#7660
#7662
#7666
#7672
#7681
#7686
#7688
#7689
#7691
#7693
#7695
#7696
#7698
#7701
#7703
#7704
#7705
#7706
#7708
#7710
#7711
#7712
#7713
#7714
#7716
#7717
#7719
#7721
#7726
#7729
#7734
#7737
#7741
#7748
#7751
#7752
#7755
#7756
#7758
#7759
#7761
#7764
#7766
#7768
#7769
#7771
#7773
#7774
#7775
#7777
#7778
#7780
#7782
#7783
#7785
#7787
#7788
#779
#7790
#7793
#7794
#7795
#780
#7802
#7803
#7804
#7807
#7808
#7809
#7810
#7811
#7812
#7813
#7814
#7815
#7819
#7820
#7821
#7823
#7824
#7827
#7829
#7830
#7831
#7832
#7833
#7834
#7835
#7836
#7838
#7839
#7840
#7844
#7845
#7846
#7847
#7848
#7849
#7851
#7852
#7854
#7856
#7858
#7860
#7862
#7863
#7865
#7866
#7868
#7870
#7871
#7877
#7878
#7879
#7880
#7881
#7882
#7885
#7886
#7887
#7887
#7888
#7889
#789
#7890
#7892
#7894
#7896
#7898
#7899
#79
#7900
#7901
#7902
#7904
#7905
#7906
#7907
#7908
#7908
#7909
#7910
#7911
#7912
#7914
#7915
#7916
#7917
#7918
#7919
#7920
#7921
#7922
#7923
#7924
#7925
#7926
#7927
#7927
#7928
#7929
#7930
#7931
#7932
#7935
#7938
#7939
#7942
#7945
#7947
#7954
#7955
#7959
#796
#7960
#7961
#7963
#7966
#7967
#7968
#7969
#797
#7971
#7972
#7973
#7974
#7975
#7976
#7977
#7978
#7979
#7980
#7981
#7982
#7984
#7985
#7986
#7987
#7988
#7989
#7993
#7994
#7995
#7996
#7997
#7998
#7998
#7999
#7999
#800
#800
#805
#81
#829
#833
#833
#838
#838
#841
#849
#85
#853
#854
#857
#857
#869
#87
#87
#881
#882
#885
#907
#908
#910
#92
#921
#922
#923
#924
#925
#926
#927
#936
#937
#938
#94
#94
#940
#940
#941
#942
#954
#954
#969
#969
#97
#980
#981
#982
#982
#983
#984
#988
#992
#993
#995
#999
Nightly
Z3-4.8.5
last-pure-pure
last-pure-unstable
z3-4.1.1
z3-4.10.0
z3-4.10.1
z3-4.10.2
z3-4.11.0
z3-4.11.2
z3-4.12.0
z3-4.12.1
z3-4.12.2
z3-4.12.3
z3-4.12.4
z3-4.12.5
z3-4.12.6
z3-4.13.0
z3-4.13.2
z3-4.13.3
z3-4.13.4
z3-4.14.0
z3-4.14.1
z3-4.15.0
z3-4.15.1
z3-4.15.2
z3-4.15.3
z3-4.3.0
z3-4.3.1
z3-4.3.2
z3-4.4.0
z3-4.4.1
z3-4.5.0
z3-4.6.0
z3-4.7.1
z3-4.8.1
z3-4.8.10
z3-4.8.11
z3-4.8.12
z3-4.8.13
z3-4.8.14
z3-4.8.15
z3-4.8.16
z3-4.8.17
z3-4.8.3
z3-4.8.4
z3-4.8.6
z3-4.8.7
z3-4.8.8
z3-4.8.9
z3-4.9.0
z3-4.9.1
-
7ff64fdd2fMerge
8e8799dbd3intoefd5d04af5Don Syme
2025-10-28 13:21:19 +01:00 -
e13e85c4ab
swap signs of coefficients compared to sign of variables. They are on different sides of inequality
arie
Nikolaj Bjorner
2025-10-28 03:16:12 -07:00 -
ae9a09ba26Merge
4b18085154intoefd5d04af5dependabot[bot]
2025-10-27 22:31:21 +00:00 -
4b18085154Bump actions/download-artifact from 5 to 6 dependabot/github_actions/actions/download-artifact-6
dependabot[bot]
2025-10-27 22:31:18 +00:00 -
84284b7cd3Merge
dfe0b21af3intoefd5d04af5dependabot[bot]
2025-10-27 22:25:46 +00:00 -
dfe0b21af3Bump actions/upload-artifact from 4 to 5 dependabot/github_actions/actions/upload-artifact-5
dependabot[bot]
2025-10-27 22:25:42 +00:00 -
b8cadfac56
don't add boolean disequality .
finite-sets
Nikolaj Bjorner
2025-10-27 14:08:12 -07:00 -
a82af886eb
formatting
Nikolaj Bjorner
2025-10-27 14:01:30 -07:00 -
580e796358Merge
7c51accb30intoefd5d04af5Don Syme
2025-10-27 13:10:27 -07:00 -
2f06bcc731
add finite_set to quantifieed theories in smt_setup, fix type signature for map-inverse axioms
Nikolaj Bjorner
2025-10-27 20:34:13 +01:00 -
c0ca3b5a0a
streamline axioms
Nikolaj Bjorner
2025-10-27 18:58:45 +01:00 -
4464ab9431
fix empty set declaration, add axioms and rewrites
Nikolaj Bjorner
2025-10-27 18:18:46 +01:00 -
4630373a97
add finite sets to datatype recursion, delay initialize finite_set plugin, fix bugs in are_distinct and equality simplification
Nikolaj Bjorner
2025-10-27 10:37:19 +01:00 -
d847a28589
bug fixes
Nikolaj Bjorner
2025-10-27 05:51:42 +01:00 -
f8a1f98fce
try Lazard project
upoly
Lev Nachmanson
2025-10-26 12:15:50 -07:00 -
c832802183
disable tracking literals, they are not used
Nikolaj Bjorner
2025-10-26 16:21:33 +01:00 -
a66cb88c78
fix build
Nikolaj Bjorner
2025-10-18 13:30:46 +02:00 -
e980f92a9e
enable always add all coeffs in nlsat
Lev Nachmanson
2025-10-24 17:47:16 -07:00 -
7b095ca733
throttle grobner method more actively
Lev Nachmanson
2025-10-22 21:36:22 -07:00 -
a15b21bc62
try exponential delay in grobner
Lev Nachmanson
2025-10-22 17:00:16 -07:00 -
ba03d35957
Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988)
hwisungi
2025-10-22 05:18:25 -07:00 -
06d142119f
Bump actions/setup-node from 5 to 6 (#7994)
dependabot[bot]
2025-10-21 21:17:35 +02:00 -
afaf0e3dd7
Add a fast-path to _coerce_exprs. (#7995)
Nelson Elhage
2025-10-21 12:16:54 -07:00 -
0d285a9b41
add the "noexcept" keyword to value_score=(value_score&&) declaration
Lev Nachmanson
2025-10-20 11:53:34 -07:00 -
0ae54c34fd
disable manylinux until segfault is resolved
Nikolaj Bjorner
2025-10-20 08:28:08 +02:00 -
1477ce2a99
build fixes
Nikolaj Bjorner
2025-10-19 20:55:45 +02:00 -
39913667c6
add explicit constructors for nightly mac build failure
Nikolaj Bjorner
2025-10-19 20:14:20 +02:00 -
90d36ed915
Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985)
Nikolaj Bjorner
2025-10-16 13:18:35 +02:00 -
85e1a39c09
Add finite_set_value_factory for creating finite set values in model generation (#7981)
Copilot
2025-10-16 13:16:54 +02:00 -
351c0401fb
restore the method behavior
Lev Nachmanson
2025-10-15 16:41:32 -07:00 -
d9ca739499
restore single cell
Lev Nachmanson
2025-10-14 17:43:48 -07:00 -
f324c5286c
trim parametric datatype test
Nikolaj Bjorner
2025-10-15 21:39:39 +02:00 -
0d85b86334
Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966)
Copilot
2025-10-15 20:51:21 +02:00 -
64295b5876
Bump github/codeql-action from 3 to 4 (#7971)
dependabot[bot]
2025-10-14 18:08:27 +02:00 -
23ce6917c5
parameter eval order
Lev Nachmanson
2025-10-07 10:30:58 -07:00 -
6bca12d399
parameter eval order
Lev Nachmanson
2025-10-07 10:26:40 -07:00 -
e75da050d2
parameter eval order
Lev Nachmanson
2025-10-07 10:21:09 -07:00 -
4f93fc7b2a
parameter eval order
Lev Nachmanson
2025-10-07 10:19:24 -07:00 -
5a3d33a615
parameter eval order
Lev Nachmanson
2025-10-07 10:14:02 -07:00 -
6146fe9ff8
parameter eval order
Lev Nachmanson
2025-10-07 10:06:43 -07:00 -
0a2328af1d
parameter eval order
Lev Nachmanson
2025-10-07 09:17:12 -07:00 -
0fbf4010a5
param eval order
Lev Nachmanson
2025-10-07 09:13:21 -07:00 -
b22f4d8802
param eval
Lev Nachmanson
2025-10-07 09:04:24 -07:00 -
e113d39aa8
parameter evaluation order
Lev Nachmanson
2025-10-07 08:53:49 -07:00 -
28c625a170
parameter eval order
Lev Nachmanson
2025-10-07 08:40:24 -07:00 -
1aaf2f8448
param order evaluation
Lev Nachmanson
2025-10-07 08:34:56 -07:00 -
97bb035416
param order
Lev Nachmanson
2025-10-06 15:51:53 -07:00 -
74c28532f4
param order
Lev Nachmanson
2025-10-06 15:44:41 -07:00 -
f8b2268424
base implementation for cardinality constraints
Nikolaj Bjorner
2025-10-26 10:35:37 +01:00 -
c72da53d19
align the univariate helper manager with the main polynomial manager
Lev Nachmanson
2025-10-25 12:02:54 -07:00 -
53e4d9562a
implement a todo item to calc gcd on uni-polynomials
Lev Nachmanson
2025-10-25 11:25:22 -07:00 -
2eb75d8a71Merge
7652d5a3e4intoefd5d04af5Don Syme
2025-10-25 17:58:36 +02:00 -
efd5d04af5
enable always add all coeffs in nlsat
master
Lev Nachmanson
2025-10-24 17:47:16 -07:00 -
4068460a0f
fix bogus axioms
Nikolaj Bjorner
2025-10-24 13:35:41 +02:00 -
5079b10597
fix up documentation
Nikolaj Bjorner
2025-10-24 13:13:52 +02:00 -
bfe6670b73Fix finite_set sort cardinality computation for finite base sorts (#7997)
Copilot
2025-10-23 17:30:17 +02:00 -
69e0793f6c
add overloads for finite sets
Nikolaj Bjorner
2025-10-23 17:29:11 +02:00 -
541a554ecdAdd finite set API functions to access term constructors from finite_set_decl_plugin.h (#7996)
Copilot
2025-10-23 17:10:47 +02:00 -
4c67a7271e
extend proof logging
Nikolaj Bjorner
2025-10-23 09:48:43 +02:00 -
b96624727d
remove ad-hoc membership axioms, enable boundary point saturatino
Nikolaj Bjorner
2025-10-23 09:42:25 +02:00 -
887ecc0c98
throttle grobner method more actively
Lev Nachmanson
2025-10-22 21:36:22 -07:00 -
58e64ea826
try exponential delay in grobner
Lev Nachmanson
2025-10-22 17:00:16 -07:00 -
0fcb0b6492
Fix unit tests for infinite base sorts
copilot/fix-finite-set-decl-plugin
copilot-swe-agent[bot]
2025-10-22 12:45:37 +00:00 -
8b3fd63434Update finite_set_decl_plugin.cpp
Nikolaj Bjorner
2025-10-22 14:20:42 +02:00 -
2bf1cc7d61Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988)
hwisungi
2025-10-22 05:18:25 -07:00 -
a4bcd74ba5Setting up param tuning python prototyping experiment (#7993) parallel
Ilana Shapiro
2025-10-22 04:47:11 -07:00 -
07f6f84645
Reviewed and updated configuration for Python build and added comment for CFG.
Hwi-sung Im
2025-10-21 13:46:35 -07:00 -
7ab0049612
Add documentation for finite set API
copilot/add-finite-set-constructors
copilot-swe-agent[bot]
2025-10-21 20:29:12 +00:00 -
4029161cb4
Add C++ bindings for finite sets
copilot-swe-agent[bot]
2025-10-21 20:23:13 +00:00 -
d9c354f809
Add Python bindings for finite sets
copilot-swe-agent[bot]
2025-10-21 20:19:29 +00:00 -
2dd4221451
Fix configuration error for non-MSVC compilers.
Hwi-sung Im
2025-10-21 13:19:19 -07:00 -
064f7e3088
Add C API for finite sets
copilot-swe-agent[bot]
2025-10-21 20:11:11 +00:00 -
488dce0edb
Implement cardinality computation for finite_set sorts
copilot-swe-agent[bot]
2025-10-21 20:08:51 +00:00 -
39ec6764b6Merge branch 'parallel' into param-tuning
Ilana Shapiro
2025-10-21 13:02:52 -07:00 -
0dc50cf668
Initial plan
copilot-swe-agent[bot]
2025-10-21 19:38:46 +00:00 -
68d18c6125
Initial plan
copilot-swe-agent[bot]
2025-10-21 19:38:16 +00:00 -
61f48ab156Merge branch 'Z3Prover:master' into param-tuning
Ilana Shapiro
2025-10-21 12:32:00 -07:00 -
68a7d1e1b1Bump actions/setup-node from 5 to 6 (#7994)
dependabot[bot]
2025-10-21 21:17:35 +02:00 -
9a2867aeb7Add a fast-path to _coerce_exprs. (#7995)
Nelson Elhage
2025-10-21 12:16:54 -07:00 -
f6168cad62
Add a fast-path to _coerce_exprs.
Nelson Elhage
2025-10-19 13:26:06 -07:00 -
43197f52d8
expose a status flag for clauses but every single one is being coded as an assumption...
Ilana Shapiro
2025-10-20 20:04:12 -07:00 -
ef1862ad2cBump actions/setup-node from 5 to 6
dependabot[bot]
2025-10-20 22:03:36 +00:00 -
2e4402c8f3
add interpretations when there are ranges
Nikolaj Bjorner
2025-10-20 23:21:30 +02:00 -
06ed96dbda
add the "noexcept" keyword to value_score=(value_score&&) declaration
Lev Nachmanson
2025-10-20 11:53:34 -07:00 -
f2e7abbdc1
disable manylinux until segfault is resolved
Nikolaj Bjorner
2025-10-20 08:28:08 +02:00 -
f520e6875bMerge branch 'Z3Prover:master' into param-tuning
Ilana Shapiro
2025-10-19 22:25:13 -07:00 -
564ececf3f
fix logic about checking clauses individually, and add proof prefix clause selection (naively) via the OnClause hook
Ilana Shapiro
2025-10-19 22:15:16 -07:00 -
da85ed8cdd
fix some bugs, it seems to run now
Ilana Shapiro
2025-10-19 19:01:16 -07:00 -
2480b5a359
change multithread to multiprocess seems to have resolved current deadlock
Ilana Shapiro
2025-10-19 15:34:49 -07:00 -
629408ba87
fix some more things but now it hangs
Ilana Shapiro
2025-10-19 15:06:18 -07:00 -
8371f11dac
fixes
Ilana Shapiro
2025-10-19 12:33:42 -07:00 -
aaaa32b4a0
build fixes
Nikolaj Bjorner
2025-10-19 20:55:45 +02:00 -
d65c0fbcd6
add explicit constructors for nightly mac build failure
Nikolaj Bjorner
2025-10-19 20:14:20 +02:00 -
65f38eac16
fixup proof log annotations of rules
Nikolaj Bjorner
2025-10-19 10:04:18 +02:00 -
86d7790c42
update pythonnn prototyping experiment, need to add a couple more things
Ilana Shapiro
2025-10-19 00:01:49 -07:00 -
0baaa3f9ce
relax an assert
lws
Lev Nachmanson
2025-10-18 14:44:23 -07:00 -
c2661e34fc
normalize before pushing
Lev Nachmanson
2025-10-18 13:14:22 -07:00 -
b85cba762c
create a better queue on properties
Lev Nachmanson
2025-10-18 12:50:20 -07:00 -
6485808b49
adding proof hint output
Nikolaj Bjorner
2025-10-18 19:26:19 +02:00 -
eb10ab1633Rename set.select to set.filter and OP_FINITE_SET_SELECT to OP_FINITE_SET_FILTER (#7989)
Copilot
2025-10-18 17:16:32 +02:00