Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add a SMT-LIB compliant printer for Expr #952

Merged
merged 3 commits into from
Nov 22, 2023
Merged

Add a SMT-LIB compliant printer for Expr #952

merged 3 commits into from
Nov 22, 2023

Commits on Nov 22, 2023

  1. Adding a SMT-LIB compliant printer for Expr 

    We plan to use expression from `Expr` to store model values but we
haven't appropriate printer for it in the SMT-LIB format. Indeed, the current
SMT-LIB printer of `Expr` is wrong, both on formulas and simple symbols as
rational numbers or bitvector literals.

This commit changes the SMT-LIB printer of `Expr` in order to always
print SMT-LIB format.

The new SMT-LIB printer have only two limitations:
1. it doesn't print the triggers of lemmas when the verbose flag is up
   because there is no appropriate syntax in the SMT-LIB standard.
2. it doesn't print the detail of the semantic trigger `In`.

Notice that multi-triggers are now printed as DNF formulae.

After discussion, we decide to keep the actual printer of `Symbols` as
we need it for debugging messages. Instead I split it in several
printers in module's implementation and I expose a new printer
`pp_operator` for sake of code factorisation.

Notice that printing names and literal constants should be sufficient to
output models but for sake of completeness, this commit refactors
completely the SMT-LIB printer of `Expr`.

I also clean up the code of both `Symbols` and `Expr` printers in the
following way:
- I use everywhere `Fmt` and in particular `Fmt.list` and `Fmt.iter`.
- I rename some functions but I keep the previous API. I just add a new
  function `pp_operator` to the signature of `Symbols`.
- I remove some useless test with `Options.get_output_smtlib`.
    @Halbaroth
    Halbaroth committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    8e9a8d5 View commit details
    Browse the repository at this point in the history

  2. Review changes 

    Add some boxes to improve the output of the printers of `Expr`.
    @Halbaroth
    Halbaroth committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    7531455 View commit details
    Browse the repository at this point in the history

  3. Add a link to issue 958

    @Halbaroth
    Halbaroth committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    e3cf52c View commit details
    Browse the repository at this point in the history