Implement sending commands to solver in incremental SMT2 backend #6357

thomasspriggs · 2021-09-22T09:40:54Z

This PR includes implementation of sending commands to solver in incremental SMT2 backend, based on the exprts recieved. This is sufficient to get a sat/unsat response from the solver in sufficiently simple cases. However parsing the result from the solver is not included in this PR and will be in a follow up PR.

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).
N/A - Non claimed. ~~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.

So that the z3 sub process is actually started and expecting smt2 commands from the pipe in this test.

So that we can see the text sent to the solver when debugging and so that the text can be checked in regression tests. The commands are shown as debug output messages rather than written to file because a file based approach is not well suited to incremental solving.

TGWDB · 2021-09-22T09:48:04Z

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

+  send_to_solver(smt_set_option_commandt{smt_option_produce_modelst{true}});
+  send_to_solver(smt_set_logic_commandt{
+    smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});


Do we want to send these at solver construction time, or do we want to send/update these per query? I don't have a good answer now, but there was comment on another issue/PR that the logic could vary for different calls/inputs. Also do we want to be able to change these later (and is this allowed/easy to do)?

According to section 4.1 of the SMTLIB standard version 2.6, the set-logic command can only be issued whilst the solver is in "Start mode" and the only way to return to this mode is to issue the reset command. The actions of the reset command include undefining all functions and assertions we have sent to the solver. Therefore if we were reseting and setting different logics for different rounds of solving, then we would no longer be carrying out incremental solving.

TLDR; We should be sending these commands at construction time.

NlightNFotis

LGTM

So that instances of `symbol_exprt` can be handled correctly.

The identifier for guards includes the `\` character. Therefore this commit is needed for allowing smt identifiers to be constructed including this character and converted to string.

In order to check that guards are converted ok.

codecov · 2021-09-22T19:33:48Z

Codecov Report

Merging #6357 (71d746a) into develop (0c2ff32) will increase coverage by 0.03%.
The diff coverage is 89.04%.

@@             Coverage Diff             @@
##           develop    #6357      +/-   ##
===========================================
+ Coverage    75.90%   75.93%   +0.03%     
===========================================
  Files         1515     1521       +6     
  Lines       164002   164232     +230     
===========================================
+ Hits        124482   124715     +233     
+ Misses       39520    39517       -3

Impacted Files	Coverage Δ
src/solvers/smt2_incremental/smt_responses.h	`0.00% <0.00%> (ø)`
...rc/solvers/smt2_incremental/smt_solver_process.cpp	`25.00% <25.00%> (ø)`
src/goto-checker/solver_factory.cpp	`76.49% <66.66%> (+1.61%)`	⬆️
src/solvers/smt2_incremental/smt_solver_process.h	`66.66% <66.66%> (ø)`
...ncremental/smt2_incremental_decision_procedure.cpp	`78.43% <93.82%> (+78.43%)`	⬆️
...ncremental/smt2_incremental_decision_procedure.cpp	`96.00% <96.00%> (ø)`
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	`36.33% <100.00%> (+1.13%)`	⬆️
..._incremental/smt2_incremental_decision_procedure.h	`75.00% <100.00%> (+75.00%)`	⬆️
src/solvers/smt2_incremental/smt_terms.cpp	`94.44% <100.00%> (ø)`
...t/solvers/smt2_incremental/convert_expr_to_smt.cpp	`100.00% <100.00%> (ø)`
... and 23 more

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 76ff675...71d746a. Read the comment docs.

peterschrammel · 2021-09-23T09:44:10Z

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

    number_of_solver_calls{0},
-    solver_process{split_string(solver_command, ' ', false, true)}
+    solver_process{split_string(solver_command, ' ', false, true)},


The split_string looks brittle.

The arguments are provided to cbmc in space separated form. Therefore they currently need to be split in order separate them. Any suggestions for making this less brittle?

peterschrammel · 2021-09-23T09:51:50Z

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

+
+/// \brief Defines any functions which \p expr depends on, which have not yet
+///   been defined, along with their dependencies in turn.
+void smt2_incremental_decision_proceduret::define_dependent_functions(


Would be great to unit-test this somehow.

I have added unit tests of smt2_incremental_decision_proceduret these tests indirectly test the functionality of this define_dependent_functions function, via the handle and set_to functions of the public interface.

These tests currently fail when run on Windows due to issues with `piped_processt`. This commit can be reverted once the debugging is complete.

So that `smt2_incremental_decision_proceduret` can be unit tested in isolation using a mock smt solver process.

Because there was previously an assumption that all symbols in the symbol table had values and it is more straight forward to make the this code deal with that than to add an invariant.

The previous implementation contained 2x "not" operations. By appling De Morgan's laws these operations can be dispensed with and the code is thus made more readable.

NlightNFotis

The rest of the stuff looks good, but the refactoring of the condition expression changed its semantics.

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

In order to improve the chances of being able to see what is wrong when/if the tests fail.

This makes the behaviour of the conversion predictable. This has the advantage of being easier to unit test and reducing the possiblity of hard to re-produce bugs.

chrisr-diffblue

Nothing blocking - though I've left a couple of small comments that might be worth considering.

chrisr-diffblue · 2021-10-04T09:02:28Z

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

+        return expr_identifier.first;
+      });
+  std::stack<exprt> to_be_defined;
+  const auto dependencies_needed = [&](const exprt &expr) {


Any particular reason why this is a lambda, rather than a helper function, such as a hypothetical push_dependencies_needed(exprt, std::stack<exprt>) which might be more descriptive? Either way, I'd be tempted to change the name to make its behaviour more explicit... At the moment, it superficially looks like a call to dependencies_needed(e) would be state-free - but actually its changing the state of the method via the stack of exprts... I'd make that behaviour explicit in the name for ease of code reading...

Because it was the quickest way for me to de-duplicate this code in the 2 places it is needed. A separate function would also have needed an additional parameter. I agree that the name I assigned to this lambda isn't necessarily the best. I think doing some pair programming together could be helpful in trying to come up with a more readable implementation.

chrisr-diffblue · 2021-10-04T09:13:57Z

src/solvers/smt2_incremental/smt_terms.cpp

@@ -50,7 +50,7 @@ bool smt_bool_literal_termt::value() const

 static bool is_valid_smt_identifier(irep_idt identifier)
 {
-  static const std::regex valid{R"(^[^\|\\]*$)"};
+  static const std::regex valid{R"(^[^\|]*$)"};


Minor quibble - but for the more hieroglyphic regex's like this its nice to include a comment showing an/some examples of what the regex is attempting to match.

I agree this would be better with a comment. I didn't add one when I first wrote this, as it is relatively short and I am relatively comfortable with regex. I'll try and remember to comment this in a follow-up PR.

thomasspriggs added 6 commits September 22, 2021 10:34

Make decision procedure use piped solver

e5676af

Update existing test to add correct z3 arguments

829c778

So that the z3 sub process is actually started and expecting smt2 commands from the pipe in this test.

Send initialisation commands to solver

aad1bf5

Add test of the setup commands sent to smt2 solver

778962e

Implement symbol_exprt to smt_termt conversion

9027d98

thomasspriggs requested review from chrisr-diffblue, kroening, NlightNFotis, peterschrammel, tautschnig and TGWDB as code owners September 22, 2021 09:40

thomasspriggs self-assigned this Sep 22, 2021

TGWDB approved these changes Sep 22, 2021

View reviewed changes

NlightNFotis approved these changes Sep 22, 2021

View reviewed changes

thomasspriggs added 5 commits September 22, 2021 19:21

Add namespace access to smt2_incremental_decision_proceduret

fba0629

So that instances of `symbol_exprt` can be handled correctly.

Add conversion of exprs to SMT2 and sending to solver process

f286c07

Implement dec_solve

6bc8b1f

Fix guard identifier processing

b6bfe48

The identifier for guards includes the `\` character. Therefore this commit is needed for allowing smt identifiers to be constructed including this character and converted to string.

Add test of an example with control flow

74a83f7

In order to check that guards are converted ok.

thomasspriggs force-pushed the tas/incremtal_backed_to_solver branch from cee99cf to 74a83f7 Compare September 22, 2021 18:24

peterschrammel reviewed Sep 23, 2021

View reviewed changes

Disable running incremental smt2 tests on Windows

5f01e32

These tests currently fail when run on Windows due to issues with `piped_processt`. This commit can be reverted once the debugging is complete.

thomasspriggs force-pushed the tas/incremtal_backed_to_solver branch from 288cdad to ca5c91c Compare September 28, 2021 19:08

Refactor to separate solver communication from decision process

3bc5ee4

So that `smt2_incremental_decision_proceduret` can be unit tested in isolation using a mock smt solver process.

thomasspriggs force-pushed the tas/incremtal_backed_to_solver branch from ca5c91c to 3bc5ee4 Compare September 28, 2021 19:14

thomasspriggs added 3 commits September 30, 2021 19:20

Fix handling of symbols with no value

6c33e07

Because there was previously an assumption that all symbols in the symbol table had values and it is more straight forward to make the this code deal with that than to add an invariant.

Refactor symbol lookup

28759bc

The previous implementation contained 2x "not" operations. By appling De Morgan's laws these operations can be dispensed with and the code is thus made more readable.

Add smt2_incremental_decision_proceduret unit tests

91da8ba

NlightNFotis suggested changes Oct 1, 2021

View reviewed changes

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp Show resolved Hide resolved

NlightNFotis approved these changes Oct 1, 2021

View reviewed changes

thomasspriggs added 2 commits October 1, 2021 12:15

Improve error printing in smt2 decision procedure unit test

7a0da55

In order to improve the chances of being able to see what is wrong when/if the tests fail.

Make the order of SMT commands for sub-expressions deterministic

71d746a

This makes the behaviour of the conversion predictable. This has the advantage of being easier to unit test and reducing the possiblity of hard to re-produce bugs.

thomasspriggs force-pushed the tas/incremtal_backed_to_solver branch from 5491bd6 to 71d746a Compare October 1, 2021 16:06

chrisr-diffblue approved these changes Oct 4, 2021

View reviewed changes

peterschrammel approved these changes Oct 8, 2021

View reviewed changes

thomasspriggs merged commit 8694d4e into diffblue:develop Oct 8, 2021

thomasspriggs deleted the tas/incremtal_backed_to_solver branch October 8, 2021 09:56

thomasspriggs mentioned this pull request Oct 11, 2021

Address incremental SMT2 related code review comments from PR6357 #6388

Merged

7 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Implement sending commands to solver in incremental SMT2 backend #6357

Implement sending commands to solver in incremental SMT2 backend #6357

Uh oh!

thomasspriggs commented Sep 22, 2021

Uh oh!

TGWDB Sep 22, 2021

Uh oh!

thomasspriggs Sep 23, 2021

Uh oh!

NlightNFotis left a comment

Uh oh!

codecov bot commented Sep 22, 2021 •

edited

Loading

Uh oh!

peterschrammel Sep 23, 2021

Uh oh!

thomasspriggs Sep 30, 2021

Uh oh!

peterschrammel Sep 23, 2021

Uh oh!

thomasspriggs Sep 30, 2021

Uh oh!

NlightNFotis left a comment

Uh oh!

Uh oh!

chrisr-diffblue left a comment

Uh oh!

chrisr-diffblue Oct 4, 2021

Uh oh!

thomasspriggs Oct 8, 2021

Uh oh!

chrisr-diffblue Oct 4, 2021

Uh oh!

thomasspriggs Oct 8, 2021

Uh oh!

Uh oh!

Implement sending commands to solver in incremental SMT2 backend #6357

Implement sending commands to solver in incremental SMT2 backend #6357

Uh oh!

Conversation

thomasspriggs commented Sep 22, 2021

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Sep 22, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov bot commented Sep 22, 2021 •

edited

Loading