diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-12-14 15:29:24 +0100 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-12-14 15:29:24 +0100 |
| commit | 45b44e86a506aef03ff23f601abc13cb353fd01a (patch) | |
| tree | 6f63f92edb93893e0c063a812a5fdef81b9e9670 /dependencies_native.dot | |
| parent | df87cbf270ade1dfacd2f2d8866ac007f015c78c (diff) | |
| download | smtcoq-45b44e86a506aef03ff23f601abc13cb353fd01a.tar.gz smtcoq-45b44e86a506aef03ff23f601abc13cb353fd01a.zip | |
dependency graph for the native version
Diffstat (limited to 'dependencies_native.dot')
| -rw-r--r-- | dependencies_native.dot | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/dependencies_native.dot b/dependencies_native.dot new file mode 100644 index 0000000..e0c0e84 --- /dev/null +++ b/dependencies_native.dot @@ -0,0 +1,66 @@ +digraph { + node [style=filled, color=green2] ; + "Syntactic.v" -> "SMT_terms.v" ; + "Operators.v" -> "SMT_terms.v" ; + "Assumptions.v" -> "SMT_terms.v" ; + "Arithmetic.v" -> "Lia.v" ; + "Lia.v" -> "SMT_terms.v" ; + "Extract.v" -> "SMTCoq.v" ; + "Euf.v" -> "SMT_terms.v" ; + "Cnf.v" -> "SMT_terms.v" ; + "Trace.v" -> "Arithmetic.v" ; + "Trace.v" -> "Assumptions.v" ; + "Trace.v" -> "Cnf.v" ; + "Trace.v" -> "Euf.v" ; + "Trace.v" -> "Operators.v" ; + "Trace.v" -> "Structures.v" ; + "Trace.v" -> "Syntactic.v" ; + "SMT_terms.v" -> "Misc.v" ; + "SMT_terms.v" -> "State.v" ; + "SMTCoq.v" -> "Trace.v" ; + node [style=filled, color=yellow] ; + "zchaffParser.ml" -> "satParser.ml" ; + "zchaffParser.ml" -> "smtTrace.ml" ; + "zchaff.ml" -> "cnfParser.ml" ; + "zchaff.ml" -> "zchaffParser.ml" ; + "cnfParser.ml" -> "satAtom.ml" ; + "cnfParser.ml" -> "satParser.ml" ; + "veritSyntax.ml" -> "lia.ml" ; + "veritParser.ml" -> "veritSyntax.ml" ; + "verit.ml" -> "smtCommands.ml" ; + "verit.ml" -> "smtlib2_genConstr.ml" ; + "verit.ml" -> "veritLexer.ml" ; + "veritLexer.ml" -> "veritParser.ml" ; + "smtTrace.ml" -> "smtCertif.ml" ; + "smtMisc.ml" -> "structures.ml" ; + "smtForm.ml" -> "coqTerms.ml" ; + "smtCommands.ml" -> "smtAtom.ml" ; + "smtCnf.ml" -> "smtTrace.ml" ; + "smtCertif.ml" -> "smtForm.ml" ; + "smtAtom.ml" -> "smtTrace.ml" ; + "satAtom.ml" -> "smtCnf.ml" ; + "coqTerms.ml" -> "smtMisc.ml" ; + "smtlib2_parse.ml" -> "smtlib2_ast.ml" ; + "smtlib2_lex.ml" -> "smtlib2_parse.ml" ; + "smtlib2_genConstr.ml" -> "smtlib2_lex.ml" ; + "smtlib2_genConstr.ml" -> "veritSyntax.ml" ; + "smtlib2_ast.ml" -> "smtlib2_util.ml" ; + "lia.ml" -> "smtAtom.ml" ; + "zchaff_checker.ml" -> "sat_checker.ml" ; + "zchaff_checker.ml" -> "zchaff.ml" ; + "verit_checker.ml" -> "smt_checker.ml" ; + "verit_checker.ml" -> "verit.ml" ; + "test.ml" -> "verit_checker.ml" ; + "test.ml" -> "zchaff_checker.ml" ; + "smtcoq.ml" -> "verit_checker.ml" ; + "smtcoq.ml" -> "zchaff_checker.ml" ; + "SMTCoq.v" -> "smtcoq_plugin.ml4" ; + "smt_checker.ml" -> "extrNative.ml" ; + "sat_checker.ml" -> "extrNative.ml" ; + "coqTerms.ml" -> "Trace.v" ; + "smtcoq_plugin.ml4" -> "zchaff.ml" ; + "smtcoq_plugin.ml4" -> "verit.ml" ; + edge [style=dotted, label=extract] ; + "smt_checker.ml" -> "Extract.v" ; + "sat_checker.ml" -> "Extract.v" ; +} |