Get rid of the legacy frontend finally! #1251

Halbaroth · 2024-10-07T10:57:58Z

This PR removes:

the deprecated legacy frontend (parser and typechecker),
the deprecated AB-Why3 plugin which depends on the legacy parser,
the associated opam packages and dependencies (including shell.nix
and our Makefile),
all the reference in the documentation to these features,
simplify gentest and rename the tag dolmen and models into default in tests/ and
remove it when it is useless,
the option frontend in Options.

We keep the --frontend option but now it is a no op command and we
output an appropriate message if users still use it.

This PR removes: - the deprecated legacy frontend (parser and typechecker), - the deprecated AB-Why3 plugin which depends on the legacy parser, - the associated opam packages and dependencies (including `shell.nix` and our Makefile), - all the reference in the documentation to these features, - simplify `gentest` and rename the tag `dolmen` into `cdcl` in `tests/` and remove it when it is useless, - the option `frontend` in `Options`. I also update the `Lib_usage` example because we now use Dolmen. We keep the `--frontend` option but now it is a no op command and we output an appropriate message if users still use it.

Halbaroth · 2024-10-08T09:52:08Z

I rollbacked modifications I have done in the tests directory and gentest script. I merged models and dolmen into an new default tag.

Notice that the +2662 comes from the fact I rename D_cnf into Cnf. There is absolutely no new line in this file but Github didn't manage to produce a proper diff. This happens also for some test files.

bclement-ocp

Feels good to finally see this go!

Notice that the +2662 comes from the fact I rename D_cnf into Cnf. There is absolutely no new line in this file but Github didn't manage to produce a proper diff. This happens also for some test files.

Hm that is unfortunate. I think this is because the Cnf module already exists before this PR. It's not only a (minor) issue for viewing the PR but I think it will also mess up git facilities for tracking a specific line across renames, I'd prefer if we could work around it.

Anyways this module should not be called Cnf because it doesn't actually perform anything related to CNF-conversion (and the previous Cnf module did not either). What about calling it Convert or Translate instead? This would make more sense and also solve the +2k issue.

bclement-ocp · 2024-10-08T10:07:24Z

src/bin/common/parse_command.ml

+  let set_frontend _ = () in
+
  let set_frontend =
    Term.(const set_frontend $ frontend)


Suggested change

let set_frontend _ = () in

let set_frontend =

Term.(const set_frontend $ frontend)

let set_frontend =

Term.(const ignore $ frontend)

removes one level of indirection for the reader

bclement-ocp · 2024-10-08T10:10:30Z

src/lib/reasoners/theory.ml

@@ -619,7 +619,7 @@ module Main_Default : S = struct
    | Unknown ->
      (* In the current implementation of optimization, the function
         [CC_X.optimizing_objective] cannot fail to optimize the objective
-         function [obj]. First of all, the legacy parser only accepts
+         function [obj]. First of all, the parser only accepts


I believe this is false given that #898 works. I think it's fine to say that CC_X.optimizing_objective is required to actually optimize the objective function as an internal invariant and raise an internal error here if it fails.

Indeed, this documentation is outdated. I will update it now. Notice that the point of this comment was not to explain we have not implemented the feature for some theory but our implementation of optimizing_objective for the Int and Real theories will always produce an answer even if this answer is not correct. Calling optimizing_objective on a split involving unsupported theory will produce None:

None means that no theory knows how to optimize this value,

Unknown means the split has no already be optimized.

I will clarify this point in the documentation of Rel.optimizing_objective.

bclement-ocp · 2024-10-08T10:45:53Z

tests/models/bitv/bvxor-1.smt2

+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x (_ BitVec 8))
+(declare-const y (_ BitVec 8))
+(assert (= x (bvxor #b10100101 y)))
+(check-sat)
+(get-model)


I think this is duplication with bvxor-1.default.smt2 (same for many others); is it intended?

Nope, I duplicate some tests by accident as you can see with my last commit. I removed it.

bclement-ocp

Looks like there are still some duplicated tests — everything else is OK!

bclement-ocp · 2024-10-08T13:28:02Z

tests/models/adt/small.smt2

+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes ((data1 0) (data2 0)) (
+  ((cons1 (d1 data1)) (cons2 (d2 data2)))
+  ((cons3 (d3 data1)) (cons4 (d4 Int) (d5 Int) (d6 Bool))
+                      (cons5 (d7 Bool)))
+))
+(declare-const a data1)
+(assert ((_ is cons1) a))
+(check-sat)
+(get-model)


Looks like there are still duplicates (with small.default.smt2)?

bclement-ocp

I hate to be a bother but there are still duplicate tests 😅

I think the following should solve it:

$ find tests -name '*.default.smt2' -exec sh -c 'rm -f ${0%.default.smt2}.smt2' {} \;
$ find tests -name '*.default.ae' -exec sh -c 'rm -f ${0%.default.ae}.ae' {} \;
$ find tests -name '*.default.expected' -exec sh -c 'rm -f ${0%.default.expected}.expected' {} \;

Halbaroth · 2024-10-08T16:10:06Z

Done!

bclement-ocp

And with that the net difference is over 10k lines removed 🎉

(Although it was already over 9000)

719.err is stlil duplicate!

bclement-ocp · 2024-10-08T16:14:43Z

tests/models/issues/719.err.smt2

+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const a (Array Int Int))
+(declare-const s Int)
+(assert (and (<= 0 s) (<= s 10)))
+(assert (forall ((k Int)) (=> (and (<= 0 k) (< k s)) (<= (select a k) (select a s)))))
+(assert (forall ((k Int)) (=> (and (< s k) (<= k 10)) (<= (select a s) (select a k)))))
+(assert (
+  forall ((p Int) (q Int))
+    (=> (and (<= 0 p) (< p q) (<= q (- s 1))) (<= (select a p) (select a q)))))
+(assert (
+  forall ((p Int) (q Int))
+    (=> (and (<= (+ s 1) p) (< p q) (<= q 10)) (<= (select a p) (select a q)))))
+(assert (not (
+  forall ((p Int) (q Int))
+    (=> (and (<= 0 p) (< p q) (<= q 10)) (<= (select a p) (select a q))))))
+(check-sat)
+(get-model)
+; (get-model) should fail because the problem is UNSAT.


I think this one is the last duplicate actually which was not caught by the script because the new file is called .default.err (and not err.default)!

AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAH

bclement-ocp

Approving conditionally to the removal of 719.err ; you can click the big green button once that one is removed.

Halbaroth added frontend clean-up labels Oct 7, 2024

This was referenced Oct 7, 2024

CDCL produces model values for popped symbols #1243

Open

Rewrite Lib_usage #1252

Open

Halbaroth added 2 commits October 8, 2024 10:56

Remove Lib_usage

a68caf8

Restore tests directory

967ac13

Halbaroth force-pushed the die-die-die branch 2 times, most recently from 5592515 to 6405283 Compare October 8, 2024 09:36

Halbaroth marked this pull request as ready for review October 8, 2024 09:36

Halbaroth added 2 commits October 8, 2024 11:37

Rewrite gentest and merge models and dolmen into default tag

6405283

Remove duplicated tests

233ac54

Halbaroth requested a review from bclement-ocp October 8, 2024 09:52

bclement-ocp reviewed Oct 8, 2024

View reviewed changes

Halbaroth added 3 commits October 8, 2024 13:28

Simplify set_frontend

7b1559a

Remove duplicated tests again

2b1f718

Rename Cnf into Translate

b92fe5b

Halbaroth requested a review from bclement-ocp October 8, 2024 13:20

Update documentation of Th.optimize_obj

9fb4279

bclement-ocp reviewed Oct 8, 2024

View reviewed changes

Halbaroth requested a review from bclement-ocp October 8, 2024 15:46

Remove duplicated tests again and again

cce8bc7

bclement-ocp reviewed Oct 8, 2024

View reviewed changes

Halbaroth requested a review from bclement-ocp October 8, 2024 16:10

remove ALL the duplicated tests!

6d1cd74

bclement-ocp previously approved these changes Oct 8, 2024

View reviewed changes

bclement-ocp reviewed Oct 8, 2024

View reviewed changes

bclement-ocp approved these changes Oct 8, 2024

View reviewed changes

pew pew

27794bc

Halbaroth enabled auto-merge (squash) October 8, 2024 16:21

Halbaroth merged commit 26fe265 into OCamlPro:next Oct 8, 2024
17 checks passed

Halbaroth mentioned this pull request Oct 9, 2024

Remove Parsed AST #1254

Merged

hra687261 mentioned this pull request Oct 9, 2024

Get rid of the legacy front-end? #556

Closed

Halbaroth mentioned this pull request Oct 28, 2024

Use term_cst as identifiers of names #1229

Closed

This was referenced Nov 13, 2024

[RFC] Remove dynlinked parsers #266

Closed

[RFC] Removing the Why3 parser #642

Closed

Using one opam package for the library, the binary and the parsers #910

Closed

[RFC] Removing the support for custom parser #643

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Get rid of the legacy frontend finally! #1251

Get rid of the legacy frontend finally! #1251

Halbaroth commented Oct 7, 2024 •

edited

Loading

Halbaroth commented Oct 8, 2024

bclement-ocp left a comment

bclement-ocp Oct 8, 2024

bclement-ocp Oct 8, 2024

Halbaroth Oct 8, 2024 •

edited

Loading

bclement-ocp Oct 8, 2024

Halbaroth Oct 8, 2024

bclement-ocp left a comment

bclement-ocp Oct 8, 2024

bclement-ocp left a comment

Halbaroth commented Oct 8, 2024

bclement-ocp left a comment

bclement-ocp Oct 8, 2024

Halbaroth Oct 8, 2024

bclement-ocp left a comment

Get rid of the legacy frontend finally! #1251

Get rid of the legacy frontend finally! #1251

Conversation

Halbaroth commented Oct 7, 2024 • edited Loading

Halbaroth commented Oct 8, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

bclement-ocp Oct 8, 2024

Choose a reason for hiding this comment

bclement-ocp Oct 8, 2024

Choose a reason for hiding this comment

Halbaroth Oct 8, 2024 • edited Loading

Choose a reason for hiding this comment

bclement-ocp Oct 8, 2024

Choose a reason for hiding this comment

Halbaroth Oct 8, 2024

Choose a reason for hiding this comment

bclement-ocp left a comment

Choose a reason for hiding this comment

bclement-ocp Oct 8, 2024

Choose a reason for hiding this comment

bclement-ocp left a comment

Choose a reason for hiding this comment

Halbaroth commented Oct 8, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

bclement-ocp Oct 8, 2024

Choose a reason for hiding this comment

Halbaroth Oct 8, 2024

Choose a reason for hiding this comment

bclement-ocp left a comment

Choose a reason for hiding this comment

Halbaroth commented Oct 7, 2024 •

edited

Loading

Halbaroth Oct 8, 2024 •

edited

Loading