Skip to content

SMT2 parser: use hash tables instead of if() ... else... #5143

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.

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

Merged
merged 3 commits into from
Oct 8, 2019

Conversation

kroening
Copy link
Member

@kroening kroening commented Oct 2, 2019

This refactors the SMT2 parser to use hash tables instead of chains of if()...else if()... for commands, sorts and expressions.

This enables extensions, and may have a performance benefit as the number of commands/expressions/sorts grows.

  • 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.
  • n/a 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.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@kroening kroening requested a review from tautschnig October 2, 2019 11:34
@kroening kroening changed the title SMT2 parser: use has tables instead of if() ... else... SMT2 parser: use hash tables instead of if() ... else... Oct 2, 2019
@kroening kroening marked this pull request as ready for review October 2, 2019 12:59
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 0b4db94).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/130035567
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: 4ce9a7e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/130040813

@codecov-io
Copy link

codecov-io commented Oct 5, 2019

Codecov Report

Merging #5143 into develop will increase coverage by 0.01%.
The diff coverage is 76.83%.

Impacted file tree graph

@@            Coverage Diff             @@
##           develop   #5143      +/-   ##
==========================================
+ Coverage    67.08%   67.1%   +0.01%     
==========================================
  Files         1149    1149              
  Lines        94035   94073      +38     
==========================================
+ Hits         63086   63123      +37     
- Misses       30949   30950       +1
Flag Coverage Δ
#cproversmt2 42.77% <74.9%> (+0.04%) ⬆️
#regression 63.59% <72.97%> (+0.01%) ⬆️
#unit 31.94% <ø> (ø) ⬆️
Impacted Files Coverage Δ
src/solvers/smt2/smt2_solver.cpp 83.01% <100%> (+1.13%) ⬆️
src/solvers/smt2/smt2_parser.h 100% <100%> (ø) ⬆️
src/solvers/smt2/smt2_parser.cpp 66.56% <74.57%> (+1.12%) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 00c7e3d...a8aa594. Read the comment docs.

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: 2f7c9fb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/130524976

@polgreen
Copy link
Contributor

polgreen commented Oct 8, 2019

This doesn't allow declaration of variables that have the same names as variables in function signatures, which would be allowed by SMT. e.g.,

(set-logic LIA)
(define-fun myfun ((x Int) (y Int)) Int
  (+ x y))
(declare-const x Int)

(assert (= (myfun x x)(+ x x )))
(check-sat)

Daniel Kroening added 3 commits October 8, 2019 08:25
This refactors the SMT2 parser to use hash tables instead of chains of
if()...else if()...  for commands.

This enables extensions, and may have a performance benefit as the number of
commands grows.
This refactors the SMT2 parser to use hash tables instead of chains of
if()...else if()...  for sorts.

This enables extensions, and may have a performance benefit as the number of
sorts grows.
This refactors the SMT2 parser to use hash tables instead of chains of
if()...else if()...  for expressions.

This enables extensions, and may have a performance benefit as the number of
expressions grows.
@kroening
Copy link
Member Author

kroening commented Oct 8, 2019

This doesn't allow declaration of variables that have the same names as variables in function signatures, which would be allowed by SMT. e.g.,

Indeed; will make that a separate PR!

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: a8aa594).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/130873673

kroening pushed a commit that referenced this pull request Oct 8, 2019
SMT-LIB2 function definitions have scopes for the identifiers of the parameters.

This was raised in #5143.
@kroening kroening merged commit db4c76b into develop Oct 8, 2019
@kroening kroening deleted the smt2_parser_table branch October 8, 2019 16:53
@polgreen
Copy link
Contributor

polgreen commented Oct 8, 2019

This doesn't allow declaration of variables that have the same names as variables in function signatures, which would be allowed by SMT. e.g.,

Indeed; will make that a separate PR!

I think the lack of local variable tracking may also affect let expressions

@polgreen
Copy link
Contributor

polgreen commented Oct 8, 2019

Another failing case. Needs to expand function applications:

(set-logic LIA)
(define-fun myfun ((x Int) (y Int)) Int
  (+ x y))
(declare-const z Int)

(assert (= (myfun z z)(+ z z )))
(check-sat)

This invariant fails because the procedure isn't implemented for function_applications

--- begin invariant violation report ---
Invariant check failed
File: flattening/boolbv_width.cpp:196 function: get_entry
Condition: false
Reason: Unimplemented

kroening pushed a commit that referenced this pull request Oct 9, 2019
SMT-LIB2 function definitions have scopes for the identifiers of the
parameters.  The same holds for let expressions.

This was raised in #5143.
@kroening
Copy link
Member Author

kroening commented Oct 9, 2019

I think the lack of local variable tracking may also affect let expressions

Indeed, added a test for that.

@kroening
Copy link
Member Author

kroening commented Oct 9, 2019

This invariant fails because the procedure isn't implemented for function_applications

The problem here is that we don't have an integer solver. The example works on bit-vectors.

kroening pushed a commit that referenced this pull request Oct 9, 2019
SMT-LIB2 function definitions have scopes for the identifiers of the
parameters.  The same holds for let expressions.

This was raised in #5143.

The need to make the scoped identifiers unique will be removed once the IR
bindings have scopes.
kroening pushed a commit that referenced this pull request Oct 9, 2019
SMT-LIB2 function definitions have scopes for the identifiers of the
parameters.  The same holds for let expressions.

This was raised in #5143.

The need to make the scoped identifiers unique will be removed once the IR
bindings have scopes.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants