search

viperproject / axiom-profiler-2

The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
https://viperproject.github.io/axiom-profiler-2/
15 stars 3 forks source link

CDCL docs #61

Open oskari1 opened 3 months ago

oskari1 commented 3 months ago

I added these into smt-log-parser/design-docs/. It includes, among other things, what I found out about the Z3 internals on CDCL and some details on the meaning of the [assign]-lines in the Z3 log.

The accompanying code is in PR #55.