Skip to content

Allow unquoted symbols in new SMT backend output if they observe the simple_symbols definition. #6745

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

Jump to bottom
Closed
wants to merge 9 commits into from
Closed

Allow unquoted symbols in new SMT backend output if they observe the simple_symbols definition. #6745

wants to merge 9 commits into from

Conversation

NlightNFotis
Copy link
Contributor

Allow for symbols to be printed in an unquoted form
in the output of the new SMT backend if said symbols
are obeying the definition of a simple_symbol from the SMTLIB
specification.

This allows our new SMT backend to work with some solvers
that are not 100% SMTLIB compliant (namely cvc4/cvc5).

This is for now a draft, to allow CI to run and let me
observe results from test runs on CI.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@NlightNFotis NlightNFotis changed the title Escape symbols smt Escape simple_symbols in SMT printed output from new SMT backend. Mar 22, 2022
@NlightNFotis NlightNFotis changed the title Escape simple_symbols in SMT printed output from new SMT backend. Allow unquoted symbols in new SMT backend output if they observe the simple_symbols definition. Mar 22, 2022
thomasspriggs
thomasspriggs reviewed Mar 22, 2022
View reviewed changes
regression/cbmc-incr-smt2/CMakeLists.txt Outdated
add_test_pl_profile(
"cbmc-new-smt-backend-cvc5"
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang smt --incremental' --validate-goto-model --validate-ssa-equation --slice-formula ${exclude_win_broken_tests}"
"-C;-X;broken-cvc5;-s;new-smt-cvc5"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🤔 The broken-cvc5 tag probably isn't needed if you have fixed all the problems locally before raising the PR.

martin-cs
martin-cs reviewed Mar 23, 2022
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Given that cvc5 is under active and rapid development, is coming up to a major release and takes a pretty strict line on SMT-LIB compliance... is this the best way to address this problem? Is there an issue open on the cvc5 tracker for what the problem with compliance is?

@thomasspriggs
Copy link
Contributor

Given that cvc5 is under active and rapid development, is coming up to a major release and takes a pretty strict line on SMT-LIB compliance... is this the best way to address this problem? Is there an issue open on the cvc5 tracker for what the problem with compliance is?

We haven't opened an issue on the cvc5 tracker. We have observed the issue this PR is intending to address on both the stable cvc4 and on cvc5. The output from cbmc is smtlib2.6 compatible both with and without the changes in this PR. I think the issue is with cvc5 rather than cbmc. Section 3.1 of the standard states the following -

For additional flexibility, arbitrary
sequences of whitespace and printable characters (except for | and ) enclosed in vertical bars are also allowed as symbols. Following Common Lisp’s conventions, enclosing
a simple symbol in vertical bars does not produce a new symbol. This means for instance that
abc and |abc| are the same symbol.

It seems that if we add | around function identifiers from the core theory such = to make |=|, the two representations of the same symbol are treated differently by cvc.

@NlightNFotis
Change Makefile in regression/cbmc-incr-smt2 to support testing w…
4b7cbff 
…ith multiple solvers.

Previously the command that was enabling the new SMT backend (and providing
the script for invoking the appropriate SMT solver) was passed as part of the
options passed in `test.desc`.

Since this was removed, and passed as part of the test configuration in the
`CMakeLists.txt`, we need to do the same here.
@NlightNFotis NlightNFotis mentioned this pull request Apr 1, 2022
Merged
7 tasks
@NlightNFotis
Copy link
Contributor Author

Closing this, as #6777 is a substitute for this PR.

@NlightNFotis NlightNFotis deleted the escape_symbols_smt branch April 29, 2022 15:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@martin-cs martin-cs martin-cs left review comments

@thomasspriggs thomasspriggs thomasspriggs left review comments

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel will be requested when the pull request is marked ready for review peterschrammel is a code owner

@TGWDB TGWDB Awaiting requested review from TGWDB TGWDB will be requested when the pull request is marked ready for review TGWDB is a code owner

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@NlightNFotis @thomasspriggs @martin-cs