- edited description
Bug in XSB: recursion over negation
The test
[==========] Running 1 test from 1 test case.
[----------] Global test environment set-up.
[----------] 1 test from ModelExpansionLong/SlowMXsatTest
[ RUN ] ModelExpansionLong/SlowMXsatTest.DoesSlowMXWithBounds/11
Testing /home/bartb/software/idp/tests/mx/satmxlongrunning/SATdpll.idp
Mx took 0.54 sec
Found SAT, expected SAT.
[ OK ] ModelExpansionLong/SlowMXsatTest.DoesSlowMXWithBounds/11 (1969 ms)
[----------] 1 test from ModelExpansionLong/SlowMXsatTest (1969 ms total)
[----------] Global test environment tear-down
[==========] 1 test from 1 test case ran. (1969 ms total)
[ PASSED ] 1 test.
in slow started to fail after acceptance of the pull request "xsb recursion over negation".
(I'm guessing that something goes wrong in the checks).
This file has a lot of definitions, hence is probably a good test example...
After inclusion of the recursion over negation:
[==========] Running 1 test from 1 test case.
[----------] Global test environment set-up.
[----------] 1 test from ModelExpansionLong/SlowMXsatTest
[ RUN ] ModelExpansionLong/SlowMXsatTest.DoesSlowMXWithBounds/11
Testing /home/bartb/software/idp/tests/mx/satmxlongrunning/SATdpll.idp
Mx took 0.57 sec
Found an invalid partial model.
structure : V {
Clause = { 1..6 }
Lit = { 1; 2; 3; "min1"; "min2"; "min3" }
Sign = { "n"; "p" }
Step = { 0..20 }
Assigned = { }
BTStep = { 0,0; 1,0; 4,4; 5,5; 6,6; 7,7; 8,8; 9,9; 10,10; 11,11; 12,12; 13,13; 14,14; 15,15; 16,16; 17,17; 18,18; 19,19; 20,20 }
BackTracked = { 1,0; 2,0; 3,0; 4,0; 5,0; 6,0; 7,0; 8,0; 9,0; 10,0; 11,0; 12,0; 13,0; 14,0; 15,0; 16,0; 17,0; 18,0; 19,0; 20,0 }
Conflict = { 0; 1; 2 }
InClause = { 1,2; 1,"min1"; 2,3; 2,"min2"; 3,"min1"; 3,"min3"; 4,1; 4,"min2"; 5,2; 5,"min3"; 6,1; 6,3 }
PropTrue = { 0,1; 0,2; 0,3; 0,"min1"; 0,"min2"; 0,"min3"; 1,1; 1,2; 1,3; 1,"min1"; 1,"min2"; 1,"min3"; 2,1; 2,2; 2,3; 2,"min1"; 2,"min2"; 2,"min3" }
SAT = false
SAT = { }
True = { }
UNSAT = { 2; 3 }
ChoiceLit = { 0->"min3"; 1->3; 2->3 }
MaxStep = 3
Neg = "n"
Neg = { 1->"min1"; 2->"min2"; 3->"min3"; "min1"->1; "min2"->2; "min3"->3 }
Pos = "p"
}
/home/bartb/software/idp/tests/TestUtils.cpp:30: Failure
Value of: result
Actual: failed
Expected: Status::SUCCESS
Which is: success
[ FAILED ] ModelExpansionLong/SlowMXsatTest.DoesSlowMXWithBounds/11, where GetParam() = "/home/bartb/software/idp/tests/mx/satmxlongrunning/SATdpll.idp" (1469 ms)
[----------] 1 test from ModelExpansionLong/SlowMXsatTest (1469 ms total)
[----------] Global test environment tear-down
[==========] 1 test from 1 test case ran. (1469 ms total)
[ PASSED ] 0 tests.
[ FAILED ] 1 test, listed below:
[ FAILED ] ModelExpansionLong/SlowMXsatTest.DoesSlowMXWithBounds/11, where GetParam() = "/home/bartb/software/idp/tests/mx/satmxlongrunning/SATdpll.idp"
1 FAILED TEST
Comments (14)
-
reporter -
How did this get through the make check? Is this part of the make test, but not make check?
-
reporter Slow tests are not incorporated in make check (they tend to be slow)
-
reporter But... Buildbot runs those slow tests
-
these are part of the executable ./tests/slow then?
-
reporter yes
-
The model that is produced by both versions ("old" - pre xsb recneg vs "new") is the same. The "old" version did not have the error in this particular test. For some reason, the "new" version returns a non-nil, empty "sols" at line 135 in satisfiability.idp
-
reporter - attached test.idp
Geisoleerde bug toegevoegd.
Deze definitie bevat geen recursie over negatie.
-
Een eigenaardig geval. Het model wordt niet opnieuw geproduceerd met de voorziene output structuur. Ik vermoed dat er ergens in de lelijke stukken van ixforall/2 zit in de xsb_compiler.P
-
- attached xsb_bug_simple.idp
Further refined test file.
-
reporter - attached testsimple.idp
Het is zelfs niet gewoon een model dat niet "opnieuw" wordt geprouceerd.
Met XSB wordt er gewoon een foutief model gevonden! (zie nieuwe bijlage)
-
It seems this bug has always been in the system, but only now surfaced because XSB is now turned on by default and used more extensively in tests.
-
reporter Ik dacht (maar kan mis zijn) dat hij voor het eerst faalde nadat de branch "recneg" was geintroduceerd
(ben dus niet zeker)
-
- changed status to resolved
Solved in pull request #333
- Log in to comment