1 files changed, 78 insertions, 0 deletions
diff --git a/books/workshops/2004/ruiz-et-al/support/dag-quadratic-C/README b/books/workshops/2004/ruiz-et-al/support/dag-quadratic-C/README
new file mode 100644
index 0000000..59104c6
--- /dev/null
+++ b/books/workshops/2004/ruiz-et-al/support/dag-quadratic-C/README
@@ -0,0 +1,78 @@
+Title: A Formally Verified Quadratic Unification Algorithm
+Authors: J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Martin
+-------------------------------------------------------------------
+
+C implementation of the unification algorithm, a straightforward translation of
+the ACL2 implementation.
+
+Contents description:
+=====================
+
+* lists.c: Ordered symbol lists and integer lists
+
+* terms.c: Prefix term representation and examples
+
+* dags.c: Dag term representation and quadratic unification algorithm
+
+How to use:
+===========
+
+Make the binary:
+
+  > make
+
+The program has four arguments:
+ 
+  > qdag problem number inc rep
+
+* The 'problem' argument select the example to be done:
+  problem = 0 --> 'Un' problem as it is presented in the paper
+
+   Un = {x_n=f(x_{n-1},x_{n-1}),...,x_1=f(x_0,x_0)}
+
+  problem = 1 --> 'Un' problem in reverse order
+
+   Un' = {x_1=f(x_0,x_0),...,x_n=f(x_{n-1},x_{n-1})}
+
+  problem = 2 --> 'Qn' problem as it is presented in the paper
+  
+   Qn = {x_n=f(x_{n-1},x_{n-1}),...,x_1=f(x_0,x_0),
+         y_n=f(y_{n-1},y_{n-1}),...,y_1=f(y_0,y_0), x_n=y_n}. 
+
+  problem = 3 --> 'Qn' problem modified to be not unifiable
+
+   Qn' = {x_n=f(x_{n-1},x_{n-1}),...,x_1=f(x_0,x_0),
+          y_n=f(y_{n-1},y_{n-1}),...,y_1=f(y_0,y_0), x_n=y_n, a=b}. 
+
+* The 'number' argument is the number of different tests
+
+* The 'inc' argument is the initial value of 'n'
+
+* The 'rep' argument is the number of repetitions of the same test
+
+So 'qdag 2 10 100 5' tests the algorithm with the 'Qn' problem for values
+100, 200, 300, 400, 500, 600, 700, 800, 900 and 1000. Each test is repeated 5
+times. The program return times data.
+
+> ./qdag 2 10 100 5
+exp_unif_problem_q
+------------------
++=========+=========+=========+=========+=========+=========+=========+
+| Formula | Time                                            | Mean    |
++---------+---------+---------+---------+---------+---------+---------+
+|    100  |   0.010 |   0.000 |   0.000 |   0.000 |   0.000 |   0.002 |
+|    200  |   0.010 |   0.010 |   0.000 |   0.010 |   0.000 |   0.006 |
+|    300  |   0.010 |   0.010 |   0.020 |   0.010 |   0.010 |   0.012 |
+|    400  |   0.030 |   0.030 |   0.020 |   0.010 |   0.030 |   0.024 |
+|    500  |   0.050 |   0.020 |   0.040 |   0.030 |   0.040 |   0.036 |
+|    600  |   0.050 |   0.060 |   0.050 |   0.040 |   0.050 |   0.050 |
+|    700  |   0.060 |   0.060 |   0.070 |   0.060 |   0.070 |   0.064 |
+|    800  |   0.080 |   0.090 |   0.080 |   0.090 |   0.100 |   0.088 |
+|    900  |   0.090 |   0.110 |   0.100 |   0.110 |   0.090 |   0.100 |
+|   1000  |   0.130 |   0.140 |   0.120 |   0.140 |   0.130 |   0.132 |
++---------+---------+---------+---------+---------+---------+---------+
+
+
+
+
+