batof-formulas.h File Reference

#include "prestaf-batof-p.h"

Go to the source code of this file.

Functions
armoise_tree *	btf_form_crt_synform (struct msa2form_compilation_data *cd, armoise_tree *P)
armoise_tree *	btf_form_crt_VH_definition (struct msa2form_compilation_data *cd, const char *id, tla_vec_t rho, tla_vec_t xhi, tla_vsp_t V, tla_vec_t alpha, int op)

Function Documentation

armoise_tree* btf_form_crt_synform	(	struct msa2form_compilation_data *	cd,
		armoise_tree *	P
	)

let SynForm := R; in { (X[0], ..., X[m-1]) | (X[0], ..., X[m-1]) in (nat, ..., nat) && SynForm };

armoise_tree* btf_form_crt_VH_definition	(	struct msa2form_compilation_data *	cd,
		const char *	id,
		tla_vec_t	rho,
		tla_vec_t	xhi,
		tla_vsp_t	V,
		tla_vec_t	alpha,
		int	op
	)

$Z^m (x_0 + (V_G H))$