#include "dioph.h"

This page has information from files dioph.h and dioph.c.

Public Routines
Public Definitions
Introduction

Public Routines in File dioph.c

Index

dio	next_combo_b	next_combo_ss
next_combo_a	next_combo_c	p_ac_basis

Details

int dio(int ab[MAX_COEF],
	int m, int n,
	int constraints[MAX_COEF],
	int basis[MAX_BASIS][MAX_COEF],
	int *num_basis);

This routine generates the basis of solutions to the homogeneous linear diophantine equation given by ab, m, n. It uses Huet's algorithm (Information Processing Letters 7(3) 1978).

The equation has the form a1x1 + ... + amxm = b1y1 + ... + bnyn.

ab[] - the vector of coefficients. 1..m is a1..am, m+1..m+n is b1..bn.
m, n - the number of a and b coefficients.
constraints[] - rigid symbol (constant/function)restrictions.
basis[][] (output) - vector of minimal solutions.
num_basis (output) - number of minimal solutions.

Return value:

0 - no solution within constraints
1 - ok, solutions returned
-1 - too many (> MAX_BASIS) base solutions exist

int next_combo_a(int length, int basis[MAX_BASIS][MAX_COEF],
		 int num_basis, int constraints[MAX_COEF],
		 int combo[MAX_BASIS], int sum[MAX_COEF],
		 int start_flag);

This routine gets the first or next appropriate subset of the basis of solutions. "Appropriate" means that each variable gets instantiated to something, and there are no top-level rigid symbol clashes. I think of this as a potential unifier, because he caller still has to worry about recursive unification of subterms.

length -- total number of coefficients (m+n).
basis[][] -- basis of solutions.
num_basis -- number of basis solutions.
constraints[] -- rigid symbol constraints.
combo[] (input and output) -- current subset of the basis.
sum[] (intput and output) -- sum corresponding to combo[].
start_flag -- 1 for first call, 0 for subsequent calls.

We have several algorithms to do this. This implements algorithm A. (For most practical work, the differences in performance are small.)

int next_combo_b(int length, int basis[MAX_BASIS][MAX_COEF],
		 int num_basis, int constraints[MAX_COEF],
		 int combo[MAX_BASIS], int sum[MAX_COEF],
		 int start_flag);

This routine gets the first or next appropriate subset of the basis of solutions. This implements algorithm B. See next_combo_a() for a description.

int next_combo_c(int length, int basis[MAX_BASIS][MAX_COEF],
		 int num_basis, int constraints[MAX_COEF],
		 int combo[MAX_BASIS], int sum[MAX_COEF],
		 int start_flag);

This routine gets the first or next appropriate subset of the basis of solutions. This implements algorithm C. See next_combo_a() for a description.

int next_combo_ss(int length, int basis[MAX_BASIS][MAX_COEF],
		  int num_basis, int constraints[MAX_COEF],
		  int combo[MAX_BASIS], int sum[MAX_COEF],
		  int start_flag,
		  int combos[MAX_COMBOS][MAX_BASIS],
		  int *np,
		  int ss_parm);

This routine gets the first or next appropriate subset of the basis of solutions, subject to the "supserset restriction". It appears to work like the other next_combo routines, but it is not really incremental. To implement the superset restriction, we collect, in combos[] during the first call, up to MAX_COMBOS subsets satisfying the restriction, then give them out in the subsequent calls. The first bunch of parameters are the same as for the other next_combo routines.

length -- total number of coefficients (m+n).
basis[][] -- basis of solutions.
num_basis -- number of basis solutions.
constraints[] -- rigid symbol constraints.
combo[] (input and output) -- current subset of the basis.
sum[] (intput and output) -- sum corresponding to combo[].
start_flag -- 1 for first call, 0 for subsequent calls.

The rest of the parameters are added for the supserset restriction.

combos[][] (input and output) -- this is really just temp storage.
*np (input and output) -- temp storage (# of combos remaining).
ss_parm (input) -- supserset parameter [0...]

void p_ac_basis(int basis[MAX_BASIS][MAX_COEF],
		int num_basis, int m, int n);

This routine prints (to stdout) a basis of solutions.

Public Definitions in File dioph.h

#define MAX_COEF   250  /* total # of coef. from both sides */
#define MAX_BASIS  100  /* must be <= MAX_VARS, because rows are indexed */
#define MAX_COMBOS 200  /* for superset-restricted AC unif. */

Introduction

This package solves linear homogeneous Diophantine equations, which can be used to compute the set of associative-commutative unifiers for a pair of first-order terms. The way this usually works is that you first call dio() to get a basis of solutions, then call one of the the next_combo routines to (incrementally) get the relevant solutions.