Notes

Michaelmas

Week 5 - 6

• Updated Minisat interface to be more functional
  • New Solver type
    • Initially tried to have a record type contain the current Solver type (so that a Solver would would keep track of the number of variables it has), but this approach did not work
    • Wrote getLiterals that requires the number of variables to be specified (not ideal)
  • Updated partial IC3 implementation to work with the new interface
• Set up Cabal and the Minisat submodule
  • Included aiger.h and aiger.c (possibly not good to do this)
  • Seems to build fine except for an issue with hsc2hs
• Misc changes suggested by HLint

Week 6 - 7

• Strengthening (based on CTI) portion of IC3 algorithm written
• Wrote example that requires strengthening to prove
  • Wrote in BLIF and used AIGER utilities to convert BLIF circuit into AIGER format
  • Debugging based on results from testing on the example in progress
    • Updating Minisat interface so that conflict vectors can be used for CTI
• Compared results with reference implementation
  • Agreement on all simple examples that do not require strengthening
  • Notes: README has wrong usage information; the reference implementation reads from stdin

Week 7 - 8

• Reworked strengthening portion of the algorithm
  • Does not recursively call prove
    • Consecution query only for current frame
  • CTIs handled completely by ctiFound
    • Tries to prove all possible literals in the negated CTI clause
• Another example added
  • Reference implementation proves it
  • This does not prove it; cannot prove the CTI is unreachable from the initial state (need to look into/fix)
• Changes to Minisat interface
  • Should fix Minisat so that solver -> solve(*assumps) does not need to be called before getting assigned or conflicting literals
• Tests with HUnit and Cabal

Break

• Fixed implementation errors; can now prove the example that could not be proven previously
• Minisat implementation now returns structs; fewer calls necessary
• Using the SimpSolver will give full models (all variables assigned), except in certain cases...
• Several issues fixed, but there is still an issue with getting the CTIs:
  • Minisat appears to give SAT results for things that are sometimes not satisfiable
  • E.g. from the example that cannot be proven by this implementation, using the SimpSolver seems to yield a model for a certain set of clauses; asserting the assignments provided in the model and querying again will give an UNSAT result
    • Converting the clauses to DIMACS CNF format (see cnfTest) gives the same results
  • Seems to be solved:
    • Updated version of gcc (problems with Minisat on older versions of gcc)
    • Updated Minisat interface to match the output when solving with DIMACS CNF input to Minisat
      • Using SimpSolver without trying to get further assignments seems to solve the examples correctly