Bugfix: can match constructors starting with "d"

[alex-ozdemir]

Summary

• constructors which start with "d" can now be pattern matched against.

Detail

Before if you had a constructor for a data-type that started with a "d", like the dn null element and dc cons element for the list type list below, then attempts to pattern match against the constructor would result in an unknown identifier error.

Thus simple programs like this one could not be type-checked:

; Declare an item type
(declare item type)

; Declare a list type with null and cons constructors
(declare list type)
(declare dn list)
(declare dc (! i item (! r list list)))

; Returns the length of a list
(program length ((l list)) mpz
         (match l
                ; ERROR: "n" is unknown!?
                (dn 0)
                ; ERROR: "c" is unknown!?
                ((dc i l') (mp_add 1 (length l')))))

The cause of this was some poorly-planned code paths in the part of the parser that detects default cases in a match expression.

Testing

I tested the fix by

1. verifying that the test program above now type-checks.
2. verifying that many signatures from CVC4 still check out, by running this command (zsh): /path/to/lfscc /path/to/CVC4/proofs/signatures/{sat.plf,smt.plf,th_base.plf,th_bv.plf,th_bv_bitblast.plf,th_arrays.plf,th_int.plf,th_quant.plf}
   • I got that list of theories from Yoni -- those are the thoeries he always loads with LFSC, but its not gauranteed to be exhaustive -- if I should test with others, let me know.

[yoni206]

Good stuff! For testing, please verify that all proofs that are produced by cvc4 in the regressions are correctly checked. This can be done by compiling cvc4 in debug, with proofs and lfsc enabled, and then run make check. Perhaps also make regress2, make regress3, make regress4. @4tXJ7f and @ajreynol - any other ideas for testing?

[4tXJ7f]

Great find and thanks for the quick fix! I think that running it on all of the regression tests should be good for now. Make sure that you configure CVC4 --with-lfsc to make sure that it actually checks proofs.

Related: We really should have a test suite for LFSC, I've meant to implement this for a while now... It shouldn't be too bad to do. We can discuss this on Wednesday.

[ajreynol]

Thanks for the fix, this is indeed a really nice bug find, that code is 10+ years old. As Yoni and Andres mention, the important thing is to test CVC4's regressions (LFSC is not independently tested).

[4tXJ7f]

Were you able to test the regressions already? Btw. when testing the regressions, make sure that you are not using the contrib/get-lfsc script to download LFSC as it will not include the changes here (may be obvious but just wanted to point that out :) ). Instead, use the --lfsc-dir option of configure.sh to point to your LFSC folder.

[alex-ozdemir]

I gave it a shot, but a number of regression tests failed because of an unrelated problem (or so matthias/aina said). I'll give it another shot today.

[alex-ozdemir]

Update:

Most CVC4 regression tests pass on my machine using the new LFSC. There are 6 (5 regression4 and 1 regression3) tests that fail using the new LFSC, but they also fail on my machine using the old LFSC.

I'm not sure why they're failing on my machine with the old version of LFSC -- is this expected behavior? Might I be doing something wrong?

Long Version:

Test Procedure

Phase 1: Verify that my changes to LFSC are being picked up by the CVC4 test suite:

1. Make a change to LFSC that will cause it to miss-parse most pattern matching (s/(/{/ on line 78 of code.cpp)
2. Run make install in the build directory of LFSC
3. Configure CVC4 with LFSC's install location indicated.
4. make check in CVC4. Verify that tons of test errors are happening.
5. Kill the check with SIG-INT to save time.

Phase 2: Verify that my changes to LFSC are not causing regressions in the CVC4 test suite.

1. Make sure the code in this PR is in the file system.

2. make install LFSC

3. Configure CVC4 with LFSC's install location indicated.

4. make check in CVC4

5. Be very patient.

6. Verify that no regress0 or regress1 tests fail.

7. ctest -j8 -L 'regress[2-4]'

8. Be very patient

9. Find that only the following tests fail:

   The following tests FAILED:
   1758 - regress3/pp-regfile.smt (Failed)
   1760 - regress4/C880mul.miter.shuffled-as.sat03-348.smt (Failed)
   1762 - regress4/bug143.smt (Failed)
   1763 - regress4/comb2.shuffled-as.sat03-420.smt (Failed)
   1764 - regress4/hole10.cvc (Failed)
   1765 - regress4/instance_1151.smt (Failed)

10. I then checked out an old version of LFSC, rebuilt and installed it, reconfigured CVC4, and ran regress4 tests, as well as the guilty regress3 test:

1/6 Test #1756: regress4/NEQ016_size5.smt ..........................   Passed  295.43 sec
2/6 Test #1759: regress4/hole10.cvc ................................***Failed  613.08 sec
3/6 Test #1755: regress4/C880mul.miter.shuffled-as.sat03-348.smt ...***Failed  727.66 sec
4/6 Test #1757: regress4/bug143.smt ................................***Failed  825.82 sec
5/6 Test #1760: regress4/instance_1151.smt .........................***Failed  1200.07 sec
6/6 Test #1758: regress4/comb2.shuffled-as.sat03-420.smt ...........***Failed  1200.20 sec

...

1/1 Test #1753: regress3/pp-regfile.smt ..........***Failed  1200.21 sec

So the same tests fail without my modifications?

My intuition is that these failures are unrelated, since it would be odd for a bug in the LFSC parser to cause only the hardesr CVC4 tests to fail.

[alex-ozdemir]

Per offline discussion with Andre & Yoni, we think that these test failures have nothing to do with LFSC, so we're comfortable merging this. Could someone with write-access do so?

[yoni206]

I don't have it, but maybe @ajreynol ?

[ajreynol]

Looks good, I'll merge now.