From 45b44e86a506aef03ff23f601abc13cb353fd01a Mon Sep 17 00:00:00 2001
From: Valentin Blot <24938579+vblot@users.noreply.github.com>
Date: Thu, 14 Dec 2017 15:29:24 +0100
Subject: dependency graph for the native version

---
 dependencies_native.dot | 66 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)
 create mode 100644 dependencies_native.dot

(limited to 'dependencies_native.dot')

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" ;
+}
-- 
cgit