|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WatchPb | Line # 43 | 166 | 50 | 60,6% |
0.6062718
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
WatchPb() WatchPb() | 103 103 | 0.0 0 | 1.0 1 | -1.0 - |
-1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
WatchPb(IDataStructurePB) WatchPb(IDataStructurePB) | 106 106 | 6.0 6 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
WatchPb(int[],BigInteger[],BigInteger) WatchPb(int[],BigInteger[],BigInteger) | 118 118 | 4.0 4 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
isAssertive(int) : boolean isAssertive(int) : boolean | 132 132 | 11.0 11 | 11.0 11 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
calcReason(int,IVecInt) : void calcReason(int,IVecInt) : void | 161 161 | 3.0 3 | 3.0 3 | 0.6 60% |
0.6
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
get(int) : int get(int) : int | 181 181 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
getCoef(int) : BigInteger getCoef(int) : BigInteger | 192 192 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
getActivity() : double getActivity() : double | 202 202 | 1.0 1 | 1.0 1 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
niceParameters(IVecInt,IVec<BigInteger>,boolean,BigInteger,ILits) : IDataStructurePB niceParameters(IVecInt,IVec<BigInteger>,boolean,BigInteger,ILits) : IDataStructurePB | 206 206 | 5.0 5 | 3.0 3 | 0.5555556 55,6% |
0.5555556
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
niceCheckedParameters(IVecInt,IVec<BigInteger>,boolean,BigInteger,ILits) : IDataStructurePB niceCheckedParameters(IVecInt,IVec<BigInteger>,boolean,BigInteger,ILits) : IDataStructurePB | 220 220 | 22.0 22 | 9.0 9 | 0.8684211 86,8% |
0.8684211
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
incActivity(double) : void incActivity(double) : void | 258 258 | 1.0 1 | 1.0 1 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
slackConstraint() : BigInteger slackConstraint() : BigInteger | 268 268 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
slackConstraint(BigInteger[],BigInteger) : BigInteger slackConstraint(BigInteger[],BigInteger) : BigInteger | 282 282 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
recalcLeftSide(BigInteger[]) : BigInteger recalcLeftSide(BigInteger[]) : BigInteger | 294 294 | 5.0 5 | 3.0 3 | 0.36363637 36,4% |
0.36363637
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
recalcLeftSide() : BigInteger recalcLeftSide() : BigInteger | 311 311 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
isSatisfiable() : boolean isSatisfiable() : boolean | 320 320 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
learnt() : boolean learnt() : boolean | 330 330 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
locked() : boolean locked() : boolean | 340 340 | 1.0 1 | 1.0 1 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
ppcm(BigInteger,BigInteger) : BigInteger ppcm(BigInteger,BigInteger) : BigInteger | 353 353 | 1.0 1 | 1.0 1 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
rescaleBy(double) : void rescaleBy(double) : void | 363 363 | 1.0 1 | 1.0 1 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
selectionSort(int,int) : void selectionSort(int,int) : void | 367 367 | 14.0 14 | 4.0 4 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
setLearnt() : void setLearnt() : void | 390 390 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
simplify() : boolean simplify() : boolean | 399 399 | 7.0 7 | 4.0 4 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
size() : int size() : int | 414 414 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
sort() : void sort() : void | 421 421 | 5.0 5 | 3.0 3 | 0.7692308 76,9% |
0.7692308
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
sort(int,int) : void sort(int,int) : void | 442 442 | 23.0 23 | 6.0 6 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
toString() : String toString() : String | 479 479 | 16.0 16 | 3.0 3 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
assertConstraint(UnitPropagationListener) : void assertConstraint(UnitPropagationListener) : void | 504 504 | 4.0 4 | 4.0 4 | 0.9 90% |
0.9
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
getDegree() : BigInteger getDegree() : BigInteger | 519 519 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
register() : void register() : void | 523 523 | 3.0 3 | 2.0 2 | 0.6 60% |
0.6
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
toVecBigInt(IVecInt) : IVec<BigInteger> toVecBigInt(IVecInt) : IVec<BigInteger> | 533 533 | 4.0 4 | 2.0 2 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
toBigInt(int) : BigInteger toBigInt(int) : BigInteger | 540 540 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
getCoefs() : BigInteger[] getCoefs() : BigInteger[] | 544 544 | 3.0 3 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
getLits() : int[] getLits() : int[] | 550 550 | 3.0 3 | 1.0 1 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
getVocabulary() : ILits getVocabulary() : ILits | 556 556 | 1.0 1 | 1.0 1 | 1.0 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
computeAnImpliedClause() : IVecInt computeAnImpliedClause() : IVecInt | 563 563 | 10.0 10 | 6.0 6 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
coefficientsEqualToOne() : boolean coefficientsEqualToOne() : boolean | 580 580 | 1.0 1 | 1.0 1 | 0.0 0% |
0.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
(181) | |||
Result | |||
0.60278744
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata103
![]() |
1 PASS | |
0.60278744
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata83
![]() |
1 PASS | |
0.60278744
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata63
![]() |
1 PASS | |
0.60278744
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc103
![]() |
1 PASS | |
0.60278744
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc83
![]() |
1 PASS | |
0.60278744
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc63
![]() |
1 PASS | |
0.5505226
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN7
![]() |
1 PASS | |
0.5505226
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN9
![]() |
1 PASS | |
0.5505226
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN8
![]() |
1 PASS | |
0.5505226
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN10
![]() |
3 FAIL | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testHole6
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testHole7
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testHole8
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testHole9
![]() |
3 FAIL | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH41
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH43
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH46
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH48
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH23
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH24
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH21
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH22
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH20
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH17
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH18
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH16
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH11
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH12
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH9
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH10
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH40
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH39
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH38
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH37
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH36
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH34
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH33
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH32
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH30
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH29
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH28
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH27
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH26
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH25
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testIi15
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH6
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH7
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH2
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH1
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH4
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testJNH3
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testIi21
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testIi24
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testIi23
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testIi17
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testIi16
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testIi20
![]() |
1 PASS | |
0.5470383
|
org.sat4j.minisat.AbstractM2Test.testIi18
![]() |
1 PASS | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnc8
![]() |
1 PASS | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnC432
![]() |
1 PASS | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5051
![]() |
3 FAIL | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3536
![]() |
3 FAIL | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4041
![]() |
3 FAIL | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3031
![]() |
3 FAIL | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2021
![]() |
3 FAIL | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1011
![]() |
3 FAIL | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1516
![]() |
3 FAIL | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncmb
![]() |
1 PASS | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnmux
![]() |
1 PASS | |
0.5296167
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnmyadder
![]() |
1 PASS | |
0.5087108
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata43
![]() |
1 PASS | |
0.5087108
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc43
![]() |
1 PASS | |
0.5052265
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncm42a
![]() |
1 PASS | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5060
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4050
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4045
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5055
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3540
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3545
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2030
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3035
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3040
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1520
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1525
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2025
![]() |
3 FAIL | |
0.46689895
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1020
![]() |
3 FAIL | |
0.46341464
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN5
![]() |
1 PASS | |
0.46341464
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN4
![]() |
1 PASS | |
0.46341464
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN6
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT12
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH49
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT13
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH50
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT14
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT15
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT8
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT9
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT10
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT11
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT4
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH42
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT5
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT6
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH44
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT7
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH45
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT16
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT1
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH47
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT2
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT3
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT5
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT4
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT7
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT6
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT1
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT3
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT2
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH19
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH15
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH13
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH14
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH35
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH31
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testIi11
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testIi4
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testIi5
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testIi6
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT8
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testIi1
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testIi3
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH5
![]() |
1 PASS | |
0.4599303
|
org.sat4j.minisat.AbstractM2Test.testJNH8
![]() |
1 PASS | |
0.4390244
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg3
![]() |
1 PASS | |
0.4390244
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg1
![]() |
1 PASS | |
0.4390244
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg2
![]() |
1 PASS | |
0.4390244
|
org.sat4j.minisat.constraints.pb.WatchPbTest.testNormalize
![]() |
1 PASS | |
0.4216028
|
org.sat4j.minisat.AbstractM2Test.testIi22
![]() |
1 PASS | |
0.41811848
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnb1
![]() |
1 PASS | |
0.40418118
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncc
![]() |
1 PASS | |
0.40418118
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testn9symml
![]() |
1 PASS | |
0.40418118
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg9
![]() |
1 PASS | |
0.40418118
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg7
![]() |
1 PASS | |
0.40418118
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg8
![]() |
1 PASS | |
0.40418118
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg5
![]() |
1 PASS | |
0.40418118
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg6
![]() |
1 PASS | |
0.40418118
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg4
![]() |
1 PASS | |
0.40069687
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg15
![]() |
1 PASS | |
0.40069687
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg16
![]() |
1 PASS | |
0.40069687
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg13
![]() |
1 PASS | |
0.40069687
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg14
![]() |
1 PASS | |
0.40069687
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg11
![]() |
1 PASS | |
0.40069687
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg12
![]() |
1 PASS | |
0.40069687
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg10
![]() |
1 PASS | |
0.40069687
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg18
![]() |
1 PASS | |
0.40069687
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg17
![]() |
1 PASS | |
0.37979093
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1015
![]() |
3 FAIL | |
0.3379791
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN56
![]() |
1 PASS | |
0.3379791
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN45
![]() |
1 PASS | |
0.3379791
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN78
![]() |
1 PASS | |
0.3379791
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN67
![]() |
1 PASS | |
0.3379791
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN34
![]() |
1 PASS | |
0.3379791
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN910
![]() |
1 PASS | |
0.3379791
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN89
![]() |
1 PASS | |
0.33449477
|
org.sat4j.minisat.AbstractM2Test.testIi12
![]() |
1 PASS | |
0.33449477
|
org.sat4j.minisat.AbstractM2Test.testIi13
![]() |
1 PASS | |
0.33449477
|
org.sat4j.minisat.AbstractM2Test.testIi14
![]() |
1 PASS | |
0.33449477
|
org.sat4j.minisat.AbstractM2Test.testIi8
![]() |
1 PASS | |
0.33449477
|
org.sat4j.minisat.AbstractM2Test.testIi9
![]() |
1 PASS | |
0.33449477
|
org.sat4j.minisat.AbstractM2Test.testIi10
![]() |
1 PASS | |
0.33449477
|
org.sat4j.minisat.AbstractM2Test.testIi7
![]() |
1 PASS | |
0.33449477
|
org.sat4j.minisat.AbstractM2Test.testIi2
![]() |
1 PASS | |
0.31707317
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnC17
![]() |
1 PASS | |
0.3031359
|
org.sat4j.minisat.CounterPBConstrWithClauseLearningOnCNFTest.testPropagation
![]() |
1 PASS | |
0.3031359
|
org.sat4j.minisat.CounterPBConstrWithPBConstrLearningOnCNFTest.testPropagation
![]() |
1 PASS | |
0.29965156
|
org.sat4j.minisat.CounterPBConstrWithClauseLearningOnCNFTest.testPropagation2
![]() |
1 PASS | |
0.29965156
|
org.sat4j.minisat.CounterPBConstrWithPBConstrLearningOnCNFTest.testPropagation2
![]() |
1 PASS | |
0.2578397
|
org.sat4j.minisat.WatchedPBConstrWithClauseLearningOnCNFTest.testPropagation
![]() |
1 PASS | |
0.2578397
|
org.sat4j.minisat.WatchedPBConstrWithClauseLearningOnCNFTest.testPropagation2
![]() |
1 PASS | |
0.2578397
|
org.sat4j.minisat.WatchedPBConstrWithPBConstrLearningOnCNFTest.testPropagation2
![]() |
1 PASS | |
0.2578397
|
org.sat4j.minisat.WatchedPBConstrWithPBConstrLearningOnCNFTest.testPropagation
![]() |
1 PASS | |
1 | /* | |
2 | * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre | |
3 | * | |
4 | * Based on the original minisat specification from: | |
5 | * | |
6 | * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the | |
7 | * Sixth International Conference on Theory and Applications of Satisfiability | |
8 | * Testing, LNCS 2919, pp 502-518, 2003. | |
9 | * | |
10 | * This library is free software; you can redistribute it and/or modify it under | |
11 | * the terms of the GNU Lesser General Public License as published by the Free | |
12 | * Software Foundation; either version 2.1 of the License, or (at your option) | |
13 | * any later version. | |
14 | * | |
15 | * This library is distributed in the hope that it will be useful, but WITHOUT | |
16 | * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS | |
17 | * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more | |
18 | * details. | |
19 | * | |
20 | * You should have received a copy of the GNU Lesser General Public License | |
21 | * along with this library; if not, write to the Free Software Foundation, Inc., | |
22 | * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA | |
23 | * | |
24 | */ | |
25 | ||
26 | package org.sat4j.minisat.constraints.pb; | |
27 | ||
28 | import java.io.Serializable; | |
29 | import java.math.BigInteger; | |
30 | import java.util.Random; | |
31 | ||
32 | import org.sat4j.core.Vec; | |
33 | import org.sat4j.core.VecInt; | |
34 | import org.sat4j.minisat.constraints.cnf.Lits; | |
35 | import org.sat4j.minisat.core.Constr; | |
36 | import org.sat4j.minisat.core.ILits; | |
37 | import org.sat4j.minisat.core.Undoable; | |
38 | import org.sat4j.minisat.core.UnitPropagationListener; | |
39 | import org.sat4j.specs.ContradictionException; | |
40 | import org.sat4j.specs.IVec; | |
41 | import org.sat4j.specs.IVecInt; | |
42 | ||
43 | public abstract class WatchPb implements PBConstr, Undoable, Serializable { | |
44 | ||
45 | /** | |
46 | * constant for the initial type of inequality less than or equal | |
47 | */ | |
48 | public static final boolean ATMOST = false; | |
49 | ||
50 | /** | |
51 | * constant for the initial type of inequality more than or equal | |
52 | */ | |
53 | public static final boolean ATLEAST = true; | |
54 | ||
55 | /** | |
56 | * variable needed for the sort method | |
57 | */ | |
58 | private static final Random rand = new Random(91648253); | |
59 | ||
60 | /** | |
61 | * constraint activity | |
62 | */ | |
63 | protected double activity; | |
64 | ||
65 | /** | |
66 | * coefficients of the literals of the constraint | |
67 | */ | |
68 | protected BigInteger[] coefs; | |
69 | ||
70 | /** | |
71 | * degree of the pseudo-boolean constraint | |
72 | */ | |
73 | protected BigInteger degree; | |
74 | ||
75 | /** | |
76 | * literals of the constraint | |
77 | */ | |
78 | protected int[] lits; | |
79 | ||
80 | /** | |
81 | * true if the constraint is a learned constraint | |
82 | */ | |
83 | protected boolean learnt = false; | |
84 | ||
85 | /** | |
86 | * true if the constraint is the origin of unit propagation | |
87 | */ | |
88 | protected boolean locked; | |
89 | ||
90 | /** | |
91 | * sum of the coefficients of the literals satisfied or unvalued | |
92 | */ | |
93 | protected BigInteger watchCumul = BigInteger.ZERO; | |
94 | ||
95 | /** | |
96 | * constraint's vocabulary | |
97 | */ | |
98 | protected ILits voc; | |
99 | ||
100 | /** | |
101 | * This constructor is only available for the serialization. | |
102 | */ | |
103 | 0 |
![]() |
104 | } | |
105 | ||
106 | 2053815 |
![]() |
107 | 2053815 | int size = mpb.size(); |
108 | 2053815 | lits = new int[size]; |
109 | 2053815 | this.coefs = new BigInteger[size]; |
110 | 2053815 | mpb.buildConstraintFromMapPb(lits, coefs); |
111 | ||
112 | 2053815 | this.degree = mpb.getDegree(); |
113 | ||
114 | // On peut trier suivant les coefficients | |
115 | 2053815 | sort(); |
116 | } | |
117 | ||
118 | 369792 |
![]() |
119 | 369792 | this.lits = lits; |
120 | 369792 | this.coefs = coefs; |
121 | 369792 | this.degree = degree; |
122 | // On peut trier suivant les coefficients | |
123 | 369792 | sort(); |
124 | } | |
125 | ||
126 | /** | |
127 | * This predicate tests wether the constraint is assertive at decision level dl | |
128 | * | |
129 | * @param dl | |
130 | * @return true iff the constraint is assertive at decision level dl. | |
131 | */ | |
132 | 0 |
![]() |
133 | 0 | BigInteger slack = BigInteger.ZERO; |
134 | 0 | for (int i = 0; i < lits.length; i++) { |
135 | 0 | if ((coefs[i].signum() > 0) |
136 | && ((!voc.isFalsified(lits[i]) || voc.getLevel(lits[i]) >= dl))) | |
137 | 0 | slack = slack.add(coefs[i]); |
138 | } | |
139 | 0 | slack = slack.subtract(degree); |
140 | 0 | if (slack.signum() < 0) |
141 | 0 | return false; |
142 | 0 | for (int i = 0; i < lits.length; i++) { |
143 | 0 | if ((coefs[i].signum() > 0) |
144 | && (voc.isUnassigned(lits[i]) || voc.getLevel(lits[i]) >= dl) | |
145 | && (slack.compareTo(coefs[i]) < 0)) { | |
146 | 0 | return true; |
147 | } | |
148 | } | |
149 | 0 | return false; |
150 | } | |
151 | ||
152 | /** | |
153 | * compute the reason for the assignment of a literal | |
154 | * | |
155 | * @param p | |
156 | * a falsified literal (or Lit.UNDEFINED) | |
157 | * @param outReason | |
158 | * list of falsified literals for which the negation is the reason of the assignment | |
159 | * @see Constr#calcReason(int, IVecInt) | |
160 | */ | |
161 | 186250858 |
![]() |
162 | 186250858 | for (int q : lits) { |
163 | if (voc.isFalsified(q)) { | |
164 | 706009647 | outReason.push(q ^ 1); |
165 | } | |
166 | } | |
167 | } | |
168 | ||
169 | abstract protected void computeWatches() throws ContradictionException; | |
170 | ||
171 | abstract protected void computePropagation(UnitPropagationListener s) | |
172 | throws ContradictionException; | |
173 | ||
174 | /** | |
175 | * to obtain the i-th literal of the constraint | |
176 | * | |
177 | * @param i | |
178 | * index of the literal | |
179 | * @return the literal | |
180 | */ | |
181 | 52543755 |
![]() |
182 | 52543755 | return lits[i]; |
183 | } | |
184 | ||
185 | /** | |
186 | * to obtain the coefficient of the i-th literal of the constraint | |
187 | * | |
188 | * @param i | |
189 | * index of the literal | |
190 | * @return coefficient of the literal | |
191 | */ | |
192 | 21951450 |
![]() |
193 | 21951450 | return coefs[i]; |
194 | } | |
195 | ||
196 | /** | |
197 | * to obtain the activity value of the constraint | |
198 | * | |
199 | * @return activity value of the constraint | |
200 | * @see Constr#getActivity() | |
201 | */ | |
202 | 0 |
![]() |
203 | 0 | return activity; |
204 | } | |
205 | ||
206 | 2683812 |
![]() |
207 | IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg, | |
208 | ILits voc) throws ContradictionException { | |
209 | // Ajouter les simplifications quand la structure sera d?finitive | |
210 | 2683812 | if (ps.size() == 0) { |
211 | 0 | throw new ContradictionException("Creating Empty clause ?"); |
212 | 2683812 | } else if (ps.size() != bigCoefs.size()) { |
213 | 0 | throw new IllegalArgumentException( |
214 | "Contradiction dans la taille des tableaux ps=" + ps.size() | |
215 | + " coefs=" + bigCoefs.size() + "."); | |
216 | } | |
217 | 2683812 | return niceCheckedParameters(ps, bigCoefs, moreThan, bigDeg, voc); |
218 | } | |
219 | ||
220 | 2897309 |
![]() |
221 | IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg, | |
222 | ILits voc) { | |
223 | 2897309 | assert ps.size() != 0 && ps.size() == bigCoefs.size(); |
224 | 2897309 | int[] lits = new int[ps.size()]; |
225 | 2897309 | ps.copyTo(lits); |
226 | 2897309 | BigInteger[] bc = new BigInteger[bigCoefs.size()]; |
227 | 2897309 | bigCoefs.copyTo(bc); |
228 | 2897309 | BigInteger bigDegree = bigDeg; |
229 | 2897309 | if (!moreThan) { |
230 | 242572 | for (int i = 0; i < lits.length; i++) { |
231 | 218646 | bc[i] = bc[i].negate(); |
232 | } | |
233 | 23926 | bigDegree = bigDegree.negate(); |
234 | } | |
235 | ||
236 | 24340395 | for (int i = 0; i < bc.length; i++) |
237 | 21443086 | if (bc[i].signum() < 0) { |
238 | 10279806 | lits[i] = lits[i] ^ 1; |
239 | 10279806 | bc[i] = bc[i].negate(); |
240 | 10279806 | bigDegree = bigDegree.add(bc[i]); |
241 | } | |
242 | ||
243 | 2897309 | IDataStructurePB mpb = new MapPb(voc); |
244 | 2897309 | if (bigDegree.signum() > 0) |
245 | 2897309 | bigDegree = mpb.cuttingPlane(lits, bc, bigDegree); |
246 | 2897309 | if (bigDegree.signum() > 0) |
247 | 2897309 | bigDegree = mpb.saturation(); |
248 | 2897309 | if (bigDegree.signum() <= 0) |
249 | 0 | return null; |
250 | 2897309 | return mpb; |
251 | } | |
252 | ||
253 | /** | |
254 | * increase activity value of the constraint | |
255 | * | |
256 | * @see Constr#incActivity(double claInc) | |
257 | */ | |
258 | 0 |
![]() |
259 | 0 | activity += claInc; |
260 | } | |
261 | ||
262 | /** | |
263 | * compute the slack of the current constraint | |
264 | * slack = poss - degree of the constraint | |
265 | * | |
266 | * @return la marge | |
267 | */ | |
268 | 213497 |
![]() |
269 | 213497 | return recalcLeftSide().subtract(this.degree); |
270 | } | |
271 | ||
272 | /** | |
273 | * compute the slack of a described constraint | |
274 | * slack = poss - degree of the constraint | |
275 | * | |
276 | * @param coefs | |
277 | * coefficients of the constraint | |
278 | * @param degree | |
279 | * degree of the constraint | |
280 | * @return slack of the constraint | |
281 | */ | |
282 | 335708 |
![]() |
283 | 335708 | return recalcLeftSide(coefs).subtract(degree); |
284 | } | |
285 | ||
286 | /** | |
287 | * compute the sum of the coefficients of the satisfied or non-assigned literals | |
288 | * of a described constraint (usually called poss) | |
289 | * | |
290 | * @param coefs | |
291 | * coefficients of the constraint | |
292 | * @return poss | |
293 | */ | |
294 | 837641255 |
![]() |
295 | 837641255 | BigInteger poss = BigInteger.ZERO; |
296 | // Pour chaque litteral | |
297 | 375624557 | for (int i = 0; i < lits.length; i++) |
298 | if (!voc.isFalsified(lits[i])) { | |
299 | assert coefs[i].signum() >= 0; | |
300 | poss = poss.add(coefs[i]); | |
301 | } | |
302 | 837641255 | return poss; |
303 | } | |
304 | ||
305 | /** | |
306 | * compute the sum of the coefficients of the satisfied or non-assigned literals | |
307 | * of the current constraint (usually called poss) | |
308 | * | |
309 | * @return poss | |
310 | */ | |
311 | 837305547 |
![]() |
312 | 837305547 | return recalcLeftSide(this.coefs); |
313 | } | |
314 | ||
315 | /** | |
316 | * D?termine si la contrainte est toujours satisfiable | |
317 | * | |
318 | * @return la contrainte est encore satisfiable | |
319 | */ | |
320 | 13297631 |
![]() |
321 | 13297631 | return recalcLeftSide().compareTo(degree) >= 0; |
322 | } | |
323 | ||
324 | /** | |
325 | * is the constraint a learnt constrainte ? | |
326 | * | |
327 | * @return true si la contrainte est apprise, false sinon | |
328 | * @see Constr#learnt() | |
329 | */ | |
330 | 186250858 |
![]() |
331 | 186250858 | return learnt; |
332 | } | |
333 | ||
334 | /** | |
335 | * The constraint is the reason of a unit propagation. | |
336 | * | |
337 | * @return true | |
338 | * @see Constr#locked() | |
339 | */ | |
340 | 0 |
![]() |
341 | 0 | return true; |
342 | } | |
343 | ||
344 | /** | |
345 | * Calcule le ppcm de deux nombres | |
346 | * | |
347 | * @param a | |
348 | * premier nombre de l'op?ration | |
349 | * @param b | |
350 | * second nombre de l'op?ration | |
351 | * @return le ppcm en question | |
352 | */ | |
353 | 0 |
![]() |
354 | 0 | return a.divide(a.gcd(b)).multiply(b); |
355 | } | |
356 | ||
357 | /** | |
358 | * Permet le r??????chantillonage de l'activit??? de la contrainte | |
359 | * | |
360 | * @param d | |
361 | * facteur d'ajustement | |
362 | */ | |
363 | 0 |
![]() |
364 | 0 | activity *= d; |
365 | } | |
366 | ||
367 | 2996433 |
![]() |
368 | 2996433 | int i, j, best_i; |
369 | 2996433 | BigInteger tmp; |
370 | 2996433 | int tmp2; |
371 | ||
372 | 19242230 | for (i = from; i < to - 1; i++) { |
373 | 16245797 | best_i = i; |
374 | 94259683 | for (j = i + 1; j < to; j++) { |
375 | 78013886 | if (coefs[j].compareTo(coefs[best_i]) > 0) |
376 | 1476764 | best_i = j; |
377 | } | |
378 | 16245797 | tmp = coefs[i]; |
379 | 16245797 | coefs[i] = coefs[best_i]; |
380 | 16245797 | coefs[best_i] = tmp; |
381 | 16245797 | tmp2 = lits[i]; |
382 | 16245797 | lits[i] = lits[best_i]; |
383 | 16245797 | lits[best_i] = tmp2; |
384 | } | |
385 | } | |
386 | ||
387 | /** | |
388 | * La contrainte est apprise | |
389 | */ | |
390 | 213301 |
![]() |
391 | 213301 | learnt = true; |
392 | } | |
393 | ||
394 | /** | |
395 | * Simplifie la contrainte(l'all???ge) | |
396 | * | |
397 | * @return true si la contrainte est satisfaite, false sinon | |
398 | */ | |
399 | 0 |
![]() |
400 | 0 | BigInteger cumul = BigInteger.ZERO; |
401 | ||
402 | 0 | int i = 0; |
403 | 0 | while (i < lits.length && cumul.compareTo(degree) < 0) { |
404 | 0 | if (voc.isSatisfied(lits[i])) { |
405 | // Mesure pessimiste | |
406 | 0 | cumul = cumul.add(coefs[i]); |
407 | } | |
408 | 0 | i++; |
409 | } | |
410 | ||
411 | 0 | return (cumul.compareTo(degree) >= 0); |
412 | } | |
413 | ||
414 | 451382926 |
![]() |
415 | 451382926 | return lits.length; |
416 | } | |
417 | ||
418 | /** | |
419 | * sort coefficient and literal arrays | |
420 | */ | |
421 | 2423607 |
![]() |
422 | 2423607 | assert this.lits != null; |
423 | 2423607 | if (coefs.length > 0) { |
424 | 2423607 | this.sort(0, size()); |
425 | 2423607 | BigInteger buffInt = coefs[0]; |
426 | 19242130 | for (int i = 1; i < coefs.length; i++) { |
427 | 16818523 | assert buffInt.compareTo(coefs[i]) >= 0; |
428 | 16818523 | buffInt = coefs[i]; |
429 | } | |
430 | ||
431 | } | |
432 | } | |
433 | ||
434 | /** | |
435 | * sort partially coefficient and literal arrays | |
436 | * | |
437 | * @param from | |
438 | * index for the beginning of the sort | |
439 | * @param to | |
440 | * index for the end of the sort | |
441 | */ | |
442 | 3569259 |
![]() |
443 | 3569259 | int width = to - from; |
444 | 3569259 | if (to - from <= 15) |
445 | 2996433 | selectionSort(from, to); |
446 | ||
447 | else { | |
448 | 572826 | BigInteger pivot = coefs[rand.nextInt(width) + from]; |
449 | 572826 | BigInteger tmp; |
450 | 572826 | int i = from - 1; |
451 | 572826 | int j = to; |
452 | 572826 | int tmp2; |
453 | ||
454 | 572826 | for (;;) { |
455 | 7656858 | do |
456 | 8627904 | i++; |
457 | 8627904 | while (coefs[i].compareTo(pivot) > 0); |
458 | 7656858 | do |
459 | 8686928 | j--; |
460 | 8686928 | while (pivot.compareTo(coefs[j]) > 0); |
461 | ||
462 | 7656858 | if (i >= j) |
463 | 572826 | break; |
464 | ||
465 | 7084032 | tmp = coefs[i]; |
466 | 7084032 | coefs[i] = coefs[j]; |
467 | 7084032 | coefs[j] = tmp; |
468 | 7084032 | tmp2 = lits[i]; |
469 | 7084032 | lits[i] = lits[j]; |
470 | 7084032 | lits[j] = tmp2; |
471 | } | |
472 | ||
473 | 572826 | sort(from, i); |
474 | 572826 | sort(i, to); |
475 | } | |
476 | ||
477 | } | |
478 | ||
479 | 0 |
![]() |
480 | public String toString() { | |
481 | 0 | StringBuffer stb = new StringBuffer(); |
482 | ||
483 | 0 | if (lits.length > 0) { |
484 | 0 | for (int i = 0; i < lits.length; i++) { |
485 | // if (voc.isUnassigned(lits[i])) { | |
486 | 0 | stb.append(" + "); |
487 | 0 | stb.append(this.coefs[i]); |
488 | 0 | stb.append("."); |
489 | 0 | stb.append(Lits.toString(this.lits[i])); |
490 | 0 | stb.append("["); |
491 | 0 | stb.append(voc.valueToString(lits[i])); |
492 | 0 | stb.append("@"); |
493 | 0 | stb.append(voc.getLevel(lits[i])); |
494 | 0 | stb.append("]"); |
495 | 0 | stb.append(" "); |
496 | // } | |
497 | } | |
498 | 0 | stb.append(">= "); |
499 | 0 | stb.append(this.degree); |
500 | } | |
501 | 0 | return stb.toString(); |
502 | } | |
503 | ||
504 | 213497 |
![]() |
505 | 213497 | BigInteger tmp = slackConstraint(); |
506 | 6538313 | for (int i = 0; i < lits.length; i++) { |
507 | 6324816 | if (voc.isUnassigned(lits[i]) && tmp.compareTo(coefs[i]) < 0) { |
508 | 227404 | boolean ret = s.enqueue(lits[i], this); |
509 | 227404 | assert ret; |
510 | } | |
511 | } | |
512 | } | |
513 | ||
514 | // protected abstract WatchPb watchPbNew(Lits voc, VecInt lits, VecInt | |
515 | // coefs, boolean moreThan, int degree, int[] indexer); | |
516 | /** | |
517 | * @return Returns the degree. | |
518 | */ | |
519 | 1978815 |
![]() |
520 | 1978815 | return degree; |
521 | } | |
522 | ||
523 | 213301 |
![]() |
524 | 213301 | assert learnt; |
525 | 213301 | try { |
526 | 213301 | computeWatches(); |
527 | } catch (ContradictionException e) { | |
528 | 0 | System.out.println(this); |
529 | assert false; | |
530 | } | |
531 | } | |
532 | ||
533 | 1005312 |
![]() |
534 | 1005312 | IVec<BigInteger> bigVec = new Vec<BigInteger>(vec.size()); |
535 | 4092760 | for (int i = 0; i < vec.size(); ++i) |
536 | 3087448 | bigVec.push(BigInteger.valueOf(vec.get(i))); |
537 | 1005312 | return bigVec; |
538 | } | |
539 | ||
540 | 1005312 |
![]() |
541 | 1005312 | return BigInteger.valueOf(i); |
542 | } | |
543 | ||
544 | 9709 |
![]() |
545 | 9709 | BigInteger[] coefsBis = new BigInteger[coefs.length]; |
546 | 9709 | System.arraycopy(coefs, 0, coefsBis, 0, coefs.length); |
547 | 9709 | return coefsBis; |
548 | } | |
549 | ||
550 | 0 |
![]() |
551 | 0 | int[] litsBis = new int[lits.length]; |
552 | 0 | System.arraycopy(lits, 0, litsBis, 0, lits.length); |
553 | 0 | return litsBis; |
554 | } | |
555 | ||
556 | 232392 |
![]() |
557 | 232392 | return voc; |
558 | } | |
559 | ||
560 | /** | |
561 | * compute an implied clause on the literals with the greater coefficients | |
562 | */ | |
563 | 0 |
![]() |
564 | 0 | BigInteger cptCoefs = BigInteger.ZERO; |
565 | 0 | int index = coefs.length; |
566 | 0 | while ((cptCoefs.compareTo(degree) > 0) && (index > 0)) { |
567 | 0 | cptCoefs = cptCoefs.add(coefs[--index]); |
568 | } | |
569 | 0 | if (index > 0 && index < size() / 2) { |
570 | // System.out.println(this); | |
571 | // System.out.println("index : "+index); | |
572 | 0 | IVecInt literals = new VecInt(index); |
573 | 0 | for (int j = 0; j <= index; j++) |
574 | 0 | literals.push(lits[j]); |
575 | 0 | return literals; |
576 | } | |
577 | 0 | return null; |
578 | } | |
579 | ||
580 | 0 |
![]() |
581 | 0 | return false; |
582 | } | |
583 | ||
584 | } |
|