prestaf-formula.h

Go to the documentation of this file.

/*
 * prestaf-formula.h -- add a comment about this file
 * 
 * This file is a part of the PresTAF project. 
 * 
 * Copyright (C) 2010 CNRS UMR 5800 & Université Bordeaux I (see AUTHORS file).
 * 
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 * 
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
 * 02110-1301  USA
 */

#ifndef __PRESTAF_FORMULA_H__
# define __PRESTAF_FORMULA_H__

# include <ccl/ccl-log.h>
# include <ccl/ccl-hash.h>
# include <prestaf/prestaf-predicate.h>

BEGIN_C_DECLS

typedef struct prestaf_formula_st prestaf_formula;

typedef struct prestaf_linear_term_st prestaf_linear_term;


extern ccl_list *
prestaf_formula_get_variables (prestaf_formula *f);

extern prestaf_formula *
prestaf_formula_add_reference (prestaf_formula *f);

extern void
prestaf_formula_del_reference (prestaf_formula *f);

extern void
prestaf_formula_display (ccl_log_type log, prestaf_formula *f);

extern prestaf_predicate *
prestaf_formula_solutions (prestaf_formula *f);


extern prestaf_formula *
prestaf_formula_create_from_file (const char *filename);

extern prestaf_formula *
prestaf_formula_create_boolean_cst (int value);

extern prestaf_formula *
prestaf_formula_create_or (prestaf_formula *f1, prestaf_formula *f2);

extern prestaf_formula *
prestaf_formula_create_and (prestaf_formula *f1, prestaf_formula *f2);

extern prestaf_formula *
prestaf_formula_create_xor (prestaf_formula *f1, prestaf_formula *f2);

extern prestaf_formula *
prestaf_formula_create_equiv (prestaf_formula *f1, prestaf_formula *f2);

extern prestaf_formula *
prestaf_formula_create_imply (prestaf_formula *f1, prestaf_formula *f2);

extern prestaf_formula *
prestaf_formula_create_not (prestaf_formula *f);

extern prestaf_formula *
prestaf_formula_create_forall (ccl_list *variables, prestaf_formula *f);

extern prestaf_formula *
prestaf_formula_create_exists (ccl_list *variables, prestaf_formula *f);

extern prestaf_formula *
prestaf_formula_create_single_exists (ccl_ustring v, prestaf_formula *f);

extern prestaf_formula *
prestaf_formula_create_eq (prestaf_linear_term *t1, prestaf_linear_term  *t2);

extern prestaf_formula *
prestaf_formula_create_neq (prestaf_linear_term *t1, prestaf_linear_term *t2);

extern prestaf_formula *
prestaf_formula_create_lt (prestaf_linear_term *t1, prestaf_linear_term *t2);

extern prestaf_formula *
prestaf_formula_create_leq (prestaf_linear_term *t1, prestaf_linear_term *t2);

extern prestaf_formula *
prestaf_formula_create_gt (prestaf_linear_term *t1, prestaf_linear_term *t2);

extern prestaf_formula *
prestaf_formula_create_geq (prestaf_linear_term *t1, prestaf_linear_term *t2);

extern prestaf_linear_term *
prestaf_linear_term_create (uint32_t n, int *a, ccl_ustring *x, int b);

extern prestaf_linear_term *
prestaf_linear_term_plus (prestaf_linear_term *t1, prestaf_linear_term *t2);

extern prestaf_linear_term *
prestaf_linear_term_minus (prestaf_linear_term *t1, prestaf_linear_term *t2);

extern prestaf_linear_term *
prestaf_linear_term_neg (prestaf_linear_term *t);

extern prestaf_linear_term *
prestaf_linear_term_add_reference (prestaf_linear_term *t);

extern void
prestaf_linear_term_del_reference (prestaf_linear_term *t);

extern int
prestaf_linear_term_get_coef (prestaf_linear_term *t, ccl_ustring x);

extern int
prestaf_linear_term_get_ith_coef (prestaf_linear_term *t, uint32_t i);

extern void
prestaf_formula_statistics (prestaf_formula *F, ccl_log_type log);

extern prestaf_formula *
prestaf_formula_linear_transform (prestaf_formula *F, ccl_hash *c, int a);

extern int
prestaf_formula_get_size (prestaf_formula *F);

extern void
prestaf_formula_display_automaton (prestaf_formula *F, ccl_log_type log);

END_C_DECLS

#endif /* ! __PRESTAF_FORMULA_H__ */