Skip to content

Commit

Permalink
tune log
Browse files Browse the repository at this point in the history
  • Loading branch information
Chronosymbolic committed Oct 1, 2023
1 parent 2f739d0 commit 42c0ee4
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion experiment/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@ The structure of the log is as follows:

2. The "Hyperparameters" section shows all the hyperparameters in `config.yml`.

3. The "CHC Solving" part shows the results of solving all instances in the test suite. For each instance, it shows the file names, the size of the `*.smt2` or `*.smt` instance, the overall running time and time of each component, auxiliary info generated when running our tool (not important), the satisfiability of the CHC (correctness of corresponding program) and the proof (solution interpretation of predicates), and the double check procedure ensuring the correctness of the proof.
3. The "CHC Solving" part shows the results of solving all instances in the test suite. For each instance, it shows the file names, the size of the `*.smt2` or `*.smt` instance, the overall running time and time of each component, auxiliary info generated when running our tool (not important), the satisfiability of the CHC (correctness of corresponding program) and the proof (solution interpretation of predicates), and the double check procedure ensuring the correctness of the proof. The figure below shows the detailed explanation of this part of log.

![log](https://github.com/Chronosymbolic/Chronosymbolic-Learning/blob/main/experiment/log_explanation.png)

4. At the end of the log, it shows the total time elapsed and the number of solved instances. It also provides a list of instances that our tool cannot solve.

Expand Down

0 comments on commit 42c0ee4

Please sign in to comment.