void assign_discriminator_counts(Interp a, Plist discriminators);
Interp canon_interp(Interp a);Return the (unique) canonical form of the interp. The input interp (which is not changed) is assumed to be in normal form.
Ordertype compare_interp(Interp a, Interp b);Compare two compatible interpretations. Return SAME_AS, GREATER_THAN, or LESS_THAN.
Interp compile_interp(Term t, BOOL allow_incomplete);This routine takes a term representing an interpretation and builds a data structure that allows fast evaluation of clauses and formulas w.r.t. the interpretation. Here is an example of the term form of an interpretation.
interpretation(3, [
function(e, [0]),
function(*(_,_), [0,1,2,1,2,0,2,0,1]),
relation(p, [1])
relation(q(_), [1,0,1])
])
The given Term t is not changed.
Interp copy_interp(Interp p);This routine copies an interpretation. We don't check for errors.
void create_profile(Interp a, Plist discriminators);
BOOL eval_formula(Formula f, Interp p);This routine evaluates a closed formula in an interpretation.
All natural numbers are interpreted as domain values, and if any domain values are out of range, a fatal error occurs.
A fatal error occurs if any constant, function or predicate symbol in the formula (other than eq_sym(), which is always built in) is absent from the interpetation.
A fatal error occurs if the formula contains any terms of type VARIABLE. (Variables bound by quantifier are represented as terms of type CONSTANT.)
BOOL eval_literals(Literals lits, Interp p);This routine evaluates a clause in an interpretation. If all instances (over the domain of the interpretation) of the clause are true in the interpretaion, TRUE is returned. If any instance is false, FALSE is returned.
Note that if the interpretation has d elements and the clause has v variables, it takes d^v evaluations to verify the clause.
All natural numbers are interpreted as domain values, and if any domain values are out of range, a fatal error occurs.
A fatal error occurs if any constant, function or predicate symbol in the clause (other than eq_sym(), which is always built in) is absent from the interpetation.
int eval_literals_false_instances(Literals lits, Interp p);
int eval_literals_true_instances(Literals lits, Interp p);This routine evaluates a clause in an interpretation. The number of false instances is returned.f The variables in the clause must be normal (0,1,2,...).
int eval_term_ground(Term t, Interp p, int *vals);
BOOL eval_topform(Topform tf, Interp p);
BOOL evaluable_atom(Term a, Interp p);
BOOL evaluable_formula(Formula f, Interp p);
BOOL evaluable_literals(Literals lits, Interp p);
BOOL evaluable_term(Term t, Interp p);
BOOL evaluable_topform(Topform tf, Interp p);
long unsigned factorial(int n);If overflow, return 0.
void fprint_interp_cooked(FILE *fp, Interp p);This routine prints (to FILE *fp) a compiled interpretation, in cooked form, e.g., f(0,2)=1.
void fprint_interp_mem(FILE *fp, BOOL heading);This routine prints (to FILE *fp) memory usage statistics for data types associated with the interp package. The Boolean argument heading tells whether to print a heading on the table.
void fprint_interp_portable(FILE *fp, Interp p);This routine prints (to FILE *fp) a compiled interpretation, in portable form.
void fprint_interp_raw(FILE *fp, Interp p);This routine pretty prints (to FILE *fp) an interpretation in raw form.
void fprint_interp_standard(FILE *fp, Interp p);This routine prints (to FILE *fp) a compiled interpretation, in standard form, with each operation on a separate line.
void fprint_interp_standard2(FILE *fp, Interp p);This routine prints (to FILE *fp) a compiled interpretation, in standard form, with each operation on a separate line, except that binary operations are printed on multiple lines.
void fprint_interp_tabular(FILE *fp, Interp p);This routine pretty prints (to FILE *fp) an interpretation in tabular (not easily parsable). Arities > 2 are not pretty.
void fprint_interp_tex(FILE *fp, Interp p);This routine prints (to FILE *fp) a compiled interpretation, in a form that might be useful as input to LaTeX.
void fprint_interp_xml(FILE *fp, Interp p);This routine prints (to FILE *fp) a compiled interpretation, in a form that might be useful as input to LaTeX.
BOOL ident_interp(Interp a, Interp b);Are interpretations A and B identical? It is assumed that A and B are the same size and have the same symbols.
BOOL ident_interp_perm(Interp a, Interp b, int *p);Is interpretation B identical to a given permutation of interpretation A? If so, then A and B are isomorphic. It is assumed that A and B are the same size and have the same symbols.
int int_power(int n, int exp);Return n^exp. If exp is negative, return -1. If the result is too big to fit into an int, return INT_MAX.
Term interp_comments(Interp a);Return the comments of an interpretation.
void interp_remove_constants(Term t);In a non-compiled interpretation, remove all constants.
Term interp_remove_constants_recurse(Term ops);In a non-compiled interpretation, remove all constants.
void interp_remove_others(Term t, Plist keepers);In a non-compiled interpretation, remove all others.
Term interp_remove_others_recurse(Term ops, Plist keepers);In a non-compiled interpretation, remove all others.
int interp_size(Interp a);Return the domain size of an interpretation.
int *interp_table(Interp p, char *sym, int arity);Given a symbol and arity, return the corresponding table.
long unsigned iso_checks(void);Return the number of isomorphism checks. For normal checks, ones where the occurrence-types don't match are not counted.
long unsigned iso_perms(void);Return the number of permutations seen during isomorphism checks.
BOOL isomorphic_interps(Interp a, Interp b, BOOL normal);Are interpretations A and B isomorphic? We assume they are compatible (same operations/arities). If the flag normal is set, it is assumed that both interps were produced by normal_interp(); this allows some optimization.
Interp normal3_interp(Interp a, Plist discriminators);
Interp normal_interp(Interp a);This routine returns a normalized copy of an interpretation. Normalized interpretations are used to speed up isomorphism checking.
Consider, in all of the function tables, the number of occurrences of each element. If we have a size-4 interpretation with a binary function, a unary function, and a constant, the occurrence array might be something like [7,6,4,4], meaning that there are 7 occurrences of 0, 6, occurrences of 1, 4 occurrences of 2, and 4 occurrences of 3. If the occurrence array is nonincreasing, the interpretation is in a normal form. (Normal forms are not unique; otherwise, isomorphism checking would be trivial.)
If 2 normal interpretations have different occurrence arrays, they cannot be isomorphic. That's the first check we make.
When checking whether two interpretations are isomorphic, we look at permutations of one of the interpretations, and we can use occurrence array to eliminate some of the permutations. Examples: with occurrence array [7,6,4,4], we look at only 2 permutations: (0,1,2,3) and (0,1,3,2); with occurrence array [4,4,4,3,3], we'd look at 12 (6*2) permutations instead of 120 (5!).
void p_interp(Interp p);This routine prints (to stdout) a compiled interpretation, in portable form, with each operation on a separate line.
void p_interp_mem();This routine prints (to stdout) memory usage statistics for data types associated with the interp package.
void p_interp_profile(Interp a, Plist discriminators);
long unsigned perms_required(Interp a);
Interp permute_interp(Interp source, int *p);This routine returns a permutation of an interpretation. The permuted interpretation does not contain the term representation (because it would be nontrivial to construct it).
BOOL same_discriminator_counts(Interp a, Interp b);
BOOL same_profiles(Interp a, Interp b);
void transpose_binary(Term t);This routine takes a term representing an interpretation and (destructively) transposes all of the binary functions and relations. It is assumed that the interpretation is well-formed. You can check well-formedness first by calling compile_interp().
void update_interp_with_constant(Interp p, Term constant, int val);
void update_profile(Topform c, Interp a, int *next)
/* vecs[domain_element][profile_component] */
;
void zap_interp(Interp p);Free a compiled interpretation.
typedef struct interp *Interp;
enum { SEMANTICS_NOT_EVALUATED,
SEMANTICS_NOT_EVALUABLE,
SEMANTICS_TRUE,
SEMANTICS_FALSE
};