SMT2 uninterpreted functions #5791
Conversation
kroening
commented
Jan 29, 2021
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- n/a 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).
- n/a 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.
The grammar for the SMT-LIB 2 command declare-fun does not expect a parameter identifier.
Uninterpreted functions don't have a definition, which has previously caused a crash.
This adds a test for an uninterpreted function, added using declare-fun.
kroening
requested review from
allredj,
martin-cs,
peterschrammel,
romainbrenguier and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #5791 +/- ##
===========================================
+ Coverage 69.67% 69.68% +0.01%
===========================================
Files 1242 1242
Lines 100885 100882 -3
===========================================
+ Hits 70290 70299 +9
+ Misses 30595 30583 -12
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
| else if(expr.id() == ID_function_application) | ||
| { | ||
| functions.record(to_function_application_expr(expr)); | ||
| return prop.new_variable(); | ||
| } |
There was a problem hiding this comment.
Does this also have implications outside SMT2, i.e., were uninterpreted functions previously broken in some way?
There was a problem hiding this comment.
Yeah; I agree with @tautschnig this seems like it should have a visible / testable effect on the usual back-end.
There was a problem hiding this comment.
Does this also have implications outside SMT2, i.e., were uninterpreted functions previously broken in some way?
I've added a further test that uses the C front-end.
| else if(expr.id() == ID_function_application) | ||
| { | ||
| functions.record(to_function_application_expr(expr)); | ||
| return prop.new_variable(); | ||
| } |
There was a problem hiding this comment.
Yeah; I agree with @tautschnig this seems like it should have a visible / testable effect on the usual back-end.
This adds support for uninterpreted functions that have a Boolean codomain.
