/**CHeaderFile***************************************************************** FileName [smt.h] PackageName [smt] Synopsis [Internal declarations.] Author [Hyondeuk Kim] Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado All rights reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.] ******************************************************************************/ /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ #include #ifdef __cplusplus extern "C" { #endif #include #include #include #include #include #include #include #include #include "sat.h" #include "aig.h" #include "util.h" #include "st.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #ifndef CUR_DATE #define CUR_DATE "" #endif #ifndef CUR_VER #define CUR_VER "U of Colorado/Boulder, CUSP Release 1.0" #endif /** Global Variable & Smt Manager **/ #define SAT_MASK 0x1 #define RESET_SAT_MASK 0xfffffffe #define UNKNOWN_MASK 0x2 #define RESET_UNKNOWN_MASK 0xfffffffd #define CNF_MASK 0x4 #define RESET_CNF_MASK 0xfffffffb #define TERM_ITE_MASK 0x8 #define RESET_TERM_ITE_MASK 0xfffffff7 #define MP_CONST_MASK 0x10 #define RESET_MP_CONST_MASK 0xffffffef #define IDL_MASK 0x1000 #define RESET_IDL_MASK 0xffffefff #define RDL_MASK 0x2000 #define RESET_RDL_MASK 0xffffdfff #define LIA_MASK 0x4000 #define RESET_LIA_MASK 0xffffbfff #define LRA_MASK 0x8000 #define RESET_LRA_MASK 0xffff7fff /** Graph **/ #define FRINGE_MASK 0x1 #define RESET_FRINGE_MASK 0xfffffffe #define REACHED_MASK 0x2 #define RESET_REACHED_MASK 0xfffffffd #define DES_MASK 0x4 #define RESET_DES_MASK 0xfffffffb #define RESET_MST_MASK 0xfffffff8 #define VISITED_MASK 0x8 #define RESET_VISITED_MASK 0xfffffff7 #define BFRINGE_MASK 0x1000 #define RESET_BFRINGE_MASK 0xffffefff #define BREACHED_MASK 0x2000 #define RESET_BREACHED_MASK 0xffffdfff #define BDES_MASK 0x4000 #define RESET_BDES_MASK 0xffffbfff #define RESET_BMST_MASK 0xffff8fff #define BVISITED_MASK 0x8000 #define RESET_BVISITED_MASK 0xffff7fff #define FFRINGE_MASK 0x10000 #define RESET_FFRINGE_MASK 0xfffeffff #define FREACHED_MASK 0x20000 #define RESET_FREACHED_MASK 0xfffdffff #define FDES_MASK 0x40000 #define RESET_FDES_MASK 0xfffbffff #define RESET_FMST_MASK 0xfff8ffff #define FVISITED_MASK 0x80000 #define RESET_FVISITED_MASK 0xfff7ffff #define BARR_MASK 0x100000 #define RESET_BARR_MASK 0xffefffff #define FARR_MASK 0x200000 #define RESET_FARR_MASK 0xffdfffff /** Fml **/ #define FML_VISITED_MASK 0x200 #define RESET_FML_VISITED_MASK 0xfffffdff #define ITE_CHAIN_MASK 0x400 #define RESET_ITE_CHAIN_MASK 0xfffffbff #define TRUE_MASK 0x800 #define RESET_TRUE_MASK 0xfffff7ff #define FALSE_MASK 0x1000 #define RESET_FALSE_MASK 0xffffefff #define IN_ARR_MASK 0x2000 #define RESET_IN_ARR_MASK 0xffffdfff #define QUEUED_MASK 0x4000 #define RESET_QUEUED_MASK 0xffffbfff #define NEG_MASK 0x8000 #define RESET_NEG_MASK 0xffff7fff /** Avar **/ #define IMPLIED_MASK 0x1 #define RESET_IMPLIED_MASK 0xfffffffe #define TPROP_MASK 0x2 #define RESET_TPROP_MASK 0xfffffffd #define BOUND_MASK 0x4 #define RESET_BOUND_MASK 0xfffffffb #define DIFF_MASK 0x8 #define RESET_DIFF_MASK 0xfffffff7 #define UNIT_LA_MASK 0x10 #define RESET_UNIT_LA_MASK 0xffffffef #define LA_MASK 0x20 #define RESET_LA_MASK 0xffffffdf #define SIGNED_MASK 0x40 #define RESET_SIGNED_MASK 0xffffffbf /** Bvar **/ #define BTRUE_MASK 0x1 #define RESET_BTRUE_MASK 0xfffffffe #define BFALSE_MASK 0x2 #define RESET_BFALSE_MASK 0xfffffffd /** Nvar **/ #define BASIC_MASK 0x1 #define RESET_BASIC_MASK 0xfffffffe #define BOUNDED_MASK 0x2 #define RESET_BOUNDED_MASK 0xfffffffd #define UNBOUNDED_MASK 0x4 #define RESET_UNBOUNDED_MASK 0xfffffffb /** System **/ #define YYMAXDEPTH 1000000 #define YY_NO_INPUT /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef enum { /* boolean */ IMP_c, /* 0 */ IFF_c, AND_c, OR_c, XOR_c, NAND_c, /* 5 */ NOT_c, ITE_c, TITE_c, EQ_c, NEQ_c, /* 10 */ LT_c, GT_c, LE_c, GE_c, LET_c, /* 15 */ FLET_c, /* arithmetic */ MUL_c, DIV_c, REM_c, /* remainder */ ADD_c, /* 20 */ SUB_c, MINUS_c, NUM_c, NONE_c, /* parsing */ FUN_c, PRED_c, TVAR_c, /* term var */ FVAR_c, /* fml var */ NVAR_c, ATOM_c, REAL_c, INT_c, ARRAY_c } smtFmlType_t; typedef struct smtManagerStruct smtManager_t; typedef struct smtStatsStruct smtStats_t; typedef struct smtGlobalVarStruct smtGlobalVar_t; typedef struct smtClauseStruct smtCls_t; typedef struct smtFormulaStruct smtFml_t; typedef struct smtAvarStruct smtAvar_t; typedef struct smtBvarStruct smtBvar_t; typedef struct smtNvarStruct smtNvar_t; typedef struct smtBoundStruct smtBound_t; typedef struct smtFletStruct smtFlet_t; typedef struct smtMpStruct smtMp_t; typedef struct smtGraphStruct smtGraph_t; typedef struct smtVertexStruct smtVertex_t; typedef struct smtEdgeStruct smtEdge_t; typedef struct smtQueueStruct smtQueue_t; /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ struct smtManagerStruct { satArray_t * clsArr; satArray_t * la_clsArr; satArray_t * avarArr; satArray_t * bvarArr; satArray_t * nvarArr; satArray_t * tmp_nvars; satArray_t * tab_avars; satArray_t * tab_nvars; satArray_t * slacks; satArray_t * basics; satArray_t * fmlArr; satArray_t * avfmlArr; satArray_t * iff_fmlArr; satArray_t * ite_fmlArr; satArray_t * fletArr; satArray_t * id2var; satArray_t * litArr; satArray_t * lemma; satArray_t * tplits; long * id2slack; int * node2id; /* aig node index to var id */ int * node2ins; /* aig node index to node indegree */ smtFml_t ** node2fml; satManager_t * cm; Aig_Manager_t * bm; smtMp_t * mp; smtGraph_t * cG; smtBound_t * bounds; double * tab; st_table * fml_table; st_table * sis_table; smtFml_t * fml; smtStats_t * stats; double * rvalues; double * prvalues; double epsilon; double epsilonless; int flag; int num_var; int num_constants; int cur_index; int limit; int aig_one_id; int aig_zero_id; int aig_none; AigEdge_t obj; int * avalues; int * ivalues; char * filename; }; struct smtStatsStruct { /* double parse_time; double preprocess_time; */ double solve_time; double num_bf_call; double num_bf_conf; double num_assert_call; double num_assert_conf; double num_check_call; double num_check_conf; double num_tprop_call; double num_tprop; double num_simp_tprop_call; double num_simp_tprop; int num_eq; int num_ceq; int num_ineq; int num_eq2ineq; int num_lzero_eq; int num_lzero_ineq; int num_inter_bvar; int num_velm_cand; int num_static_cls; int num_static_pred; int num_avar; int num_row; int num_col; }; struct smtGlobalVarStruct { smtFml_t * fml; smtFml_t * tfml; smtBvar_t * bvar; smtNvar_t * nvar; satArray_t * fmlArr; satArray_t * tfmlArr; satArray_t * avfmlArr; satArray_t * bvarArr; satArray_t * nvarArr; satArray_t * fletArr; double epsilon; /* may not need */ double epsilonless; /* may not need */ long status; int flag; char * filename; char * str; st_table * fun_table; st_table * pred_table; st_table * fml_var_table; st_table * term_var_table; st_table * term_table; st_table * num_table; }; struct smtClauseStruct { satArray_t * litArr; }; struct smtFormulaStruct { int id; int flag; /*smtFmlType_t type;*/ long type; satArray_t * subfmlArr; AigEdge_t aig_node; smtAvar_t * avar; smtBvar_t * bvar; smtNvar_t * nvar; int nNeg; int ins; int value; }; struct smtAvarStruct { char * name; int id; int flag; /*smtFmlType_t type;*/ long type; satArray_t * nvars; array_t * coeffs; array_t * sis_avars; double constant; AigEdge_t aig_node; }; struct smtBvarStruct { char * name; int id; int flag; AigEdge_t aig_node; }; struct smtNvarStruct { char * name; int id; int flag; satArray_t * avarArr; }; struct smtBoundStruct { double ub; double lb; }; struct smtFletStruct { smtFml_t * fvar_fml; smtFml_t * fml; }; struct smtMpStruct { mpq_t * pool; mpq_t * values; /* nvar values */ mpq_t * pvalues; /* nvar values */ mpq_t * constants; mpq_t * weights; mpq_t zero; mpq_t one; mpq_t m_one; int num_avar; int num_nvar; int plimit; }; struct smtGraphStruct { satArray_t * nvarArr; satArray_t * avarArr; satArray_t * cur_edges; satArray_t * neg_edges; satArray_t * bvArr; satArray_t * fvArr; satArray_t * imp_edges; smtVertex_t * vHead; smtVertex_t ** paths; smtVertex_t ** bpaths; smtVertex_t ** fpaths; smtEdge_t * eHead; smtQueue_t * queue; double * rdists; double * brdists; double * frdists; double epsilonless; int * flags; int * idists; int * bidists; int * fidists; int vsize; int esize; }; struct smtVertexStruct { satArray_t * ins; satArray_t * outs; satArray_t * targets; int index; }; struct smtEdgeStruct { int index; smtVertex_t * src; smtVertex_t * dest; satArray_t * implied; smtAvar_t * avar; double weight; }; struct smtQueueStruct { long max; /* max size of queue */ long size; /* the number of current entries */ long front; /* front index of entries */ long rear; /* rear index of entries */ long * array; /* the location to save entries */ }; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ #ifndef SMT_GLOBAL_VARIABLE #define SMT_GLOBAL_VARIABLE extern smtGlobalVar_t * gvar; #endif /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ /* main.c */ /* smt.c */ int smt_main(char * filename, int timeout, int is_model); void smt_read(char * str); void SmtFileSetup(FILE * fp); int SmtYyparse(void); smtManager_t * smt_init(void); smtManager_t * smt_dl_init(void); smtManager_t * smt_la_init(void); void smt_solve(smtManager_t * sm); void smt_report(smtManager_t * sm, int is_model); void smt_postprocess(smtManager_t * sm); void smt_init_global_variable(char * filename); void smt_free_global_variable(void); void smt_free_key_in_table(st_table * table); void smt_free_key_with_array_in_table(st_table * table); smtManager_t * smt_init_manager(void); void smt_free_manager(smtManager_t * sm); void smt_free_clauses(satArray_t * clsArr); void smt_free_clauses(satArray_t * clsArr); void smt_free_atom_variables(satArray_t * avarArr); void smt_free_atom_members(smtAvar_t * avar); void smt_free_bool_variables(satArray_t * bvarArr); void smt_free_numerical_variables(satArray_t * nvarArr); void smt_free_formulas(satArray_t * fmlArr); smtStats_t * smt_init_stats(void); void smt_circus_interface(smtManager_t * sm); void smt_circus_cnf_interface(smtManager_t * sm); satArray_t * smt_get_decision_order(smtManager_t * sm); /* smtPre.c */ void smt_preprocess(smtManager_t * sm); void smt_solve_bool_model(smtManager_t * sm); void smt_generate_level_zero_assignments(smtManager_t * sm); void smt_update_nvar_adjacent_avar_array(smtManager_t * sm); void smt_generate_adjacent_atom_array(smtManager_t * sm); void smt_dl_preprocess(smtManager_t * sm); void smt_convert_atom_to_dl_form(smtManager_t * sm); void smt_generate_avar_sister_array(smtManager_t * sm); void smt_la_preprocess(smtManager_t * sm); void smt_put_la_clause_to_clause_arr(smtManager_t * sm); void smt_convert_lac_into_unit_lac(smtManager_t * sm); void smt_init_convert_lac_into_unit_lac(smtManager_t * sm, int * num_nvars, int * num_lavars, int * max_coeffs, int * flags); satArray_t * smt_check_nvar_in_atom(smtManager_t * sm, int * num_nvars, int * max_coeffs, int * num_lavars); void smt_decide_lac_converting_criterion(smtManager_t * sm, int * flags, int * num_nvars, int * max_coeffs); void smt_create_avar_with_nvar_related_avar(smtManager_t * sm, smtNvar_t * new_nvar, smtNvar_t * nvar, int int_coeff); /* smtFml.c */ smtFml_t * smt_create_formula(smtFmlType_t ftype, satArray_t * subfmlArr); void smt_duplicate_formula(smtFml_t * new_fml, smtFml_t * org); smtFml_t * smt_create_identical_formula(smtFml_t * fml); smtFml_t * smt_simplify_formula(smtFml_t * fml); void smt_increase_subfml_ins(smtFml_t * fml); void smt_add_fml_to_array(smtFml_t * fml); smtFml_t * smt_create_returning_formula(smtFml_t * fml); smtFml_t * smt_create_function_symbol(char * fs_name); smtFml_t * smt_create_predicate_symbol(char * ps_name); smtFml_t * smt_create_constant_predicate_symbol(char * ps_name, int value); smtFml_t * smt_create_fml_variable(char * fname); smtFml_t * smt_create_term_variable(char * fs_name); smtFml_t * smt_create_constant_formula(char * cname); void smt_simplify_term_fml(smtFml_t * fml, st_table * num_table); void smt_save_flet_pair(smtFml_t * fvar_fml, smtFml_t * fml); void smt_init_formula_flag(smtManager_t * sm); void smt_init_fml_visited_flag(smtManager_t * sm); void smt_init_fml_queued_flag(smtManager_t * sm); char * smt_convert_fml_to_string(smtFml_t * fml); char * smt_convert_fml_to_string_with_subfml(smtFmlType_t type, satArray_t * subfmlArr); int smt_is_leaf_fml(smtFml_t * fml); int smt_is_abstract_leaf_fml(smtFml_t * fml); int smt_is_negated_abstract_leaf_fml(smtFml_t * fml); int smt_is_ite_chain_fml(smtFml_t * fml, int num_fml); int smt_is_atom_formula(smtFml_t * fml); int smt_is_negated_atom_formula(smtFml_t * fml); int smt_is_boolean_formula(smtFml_t * fml); int smt_is_negated_boolean_formula(smtFml_t * fml); int smt_is_arith_formula(smtFml_t * fml); int smt_is_multi_arith_formula(smtFml_t * fml); int smt_is_binary_arith_formula(smtFml_t * fml); int smt_is_unary_arith_formula(smtFml_t * fml); int smt_is_term_formula(smtFml_t * fml); int smt_is_bool_atom_fml(smtFml_t * fml); int smt_get_constant_value_in_fml(smtFml_t * fml, int * value); void smt_convert_term_ite_into_bool_ite_main(smtManager_t * sm); void smt_init_convert_term_ite_into_bool_ite(smtManager_t * sm); void smt_convert_term_ite_into_bool_ite(smtManager_t * sm, smtFml_t * fml); smtFml_t * smt_check_fml_for_term_ite_fml(smtFml_t * fml); void smt_convert_term_ite_into_bool_ite_sub(smtManager_t * sm, smtFml_t * fml, smtFml_t * ite_fml); smtFml_t * smt_create_ite_term_fml(smtManager_t * sm, smtFmlType_t type, satArray_t * subfmls, smtFml_t * subfml, int ite_index); void smt_assign_ite_terms_to_ite_fml(smtManager_t * sm, smtFml_t * new_ite, smtFml_t * cond_fml, smtFml_t * new_then, smtFml_t * new_else); int smt_check_ite_for_terminal_case(smtFml_t * ite_fml); void smt_convert_eq_fml_to_ineq_fml(smtManager_t * sm); void smt_add_flet_pair_formula(smtManager_t * sm); void smt_convert_eq_fml_into_ineq_and_fml(smtManager_t * sm, smtFml_t * fml); void smt_convert_diseq_fml_into_ineq_or_fml(smtManager_t * sm, smtFml_t * fml); satArray_t * smt_gather_bvar_in_fml(smtManager_t * sm, smtFml_t * fml); /* smtUtil.c */ smtCls_t * smt_create_clause(void); smtCls_t * smt_duplicate_clause(smtCls_t * cls); smtFmlType_t smt_get_ar_symbol(char * str); smtBvar_t * smt_create_bool_variable(char * name, smtFml_t * bvfml); smtBvar_t * smt_create_intermediate_bool_variable(smtManager_t * sm, AigEdge_t node); smtNvar_t * smt_create_numerical_variable(char * name, smtFml_t * nvfml); void smt_create_dl_atom_variable_main(smtManager_t * sm); void smt_create_la_atom_variable_main(smtManager_t * sm); void smt_convert_dl_atom_fml_to_bool_fml(smtFml_t * fml, smtAvar_t * avar); int smt_convert_atom_to_leq_form(smtManager_t * sm, smtAvar_t * avar); char * smt_get_avar_name(smtManager_t * sm, smtAvar_t * avar); char * smt_get_neg_avar_name(smtManager_t * sm, smtAvar_t * avar); smtAvar_t * smt_create_atom_variable(smtFml_t * avfml); smtAvar_t * smt_create_pure_atom_variable(void); void smt_init_atom_variable_values(smtManager_t * sm); void smt_init_numerical_variable_values(smtManager_t * sm); void smt_gather_atom_member(smtAvar_t * avar, smtFml_t * avfml); void smt_gather_atom_member_in_fml(smtAvar_t * avar, smtFml_t * fml, int nminus, double coeff); void smt_combine_root_fml_with_flet_fml(void); void smt_assign_boolean_variable_id(smtManager_t * sm); void smt_assign_numerical_variable_id(smtManager_t * sm); void smt_assign_numerical_variable_id_in_array(satArray_t * nvarArr); void smt_assign_bool_var_flag(smtManager_t * sm); void smt_sort_nvar_array_with_id(satArray_t * arr); void smt_sort_nvar_array_with_id_aux(long * arr, long size); smtQueue_t * smt_create_queue(long MaxElements); void smt_init_queue(smtQueue_t * Q); void smt_free_queue(smtQueue_t * Q); void smt_enqueue(smtQueue_t * Q, long v); long smt_dequeue(smtQueue_t * Q); int smt_timeout(int timeout); void smt_timeout_handle(void); void smt_none(void); /* smtCnf.c */ void smt_generate_cnf_main(smtManager_t * sm); int smt_generate_cnf(smtManager_t * sm); void smt_generate_cnf_with_aig(smtManager_t * sm); AigEdge_t smt_generate_aig(smtManager_t * sm); int smt_is_ite_terminal_case(AigEdge_t cond_node, AigEdge_t then_node, AigEdge_t else_node); void smt_convert_aig_into_cnf(smtManager_t * sm, AigEdge_t aig_node); void smt_compute_indegree_for_aig_node(smtManager_t * sm); void smt_init_var_id_for_aig_node(smtManager_t * sm); void smt_check_leaf_node_for_aig_node(smtManager_t * sm); satArray_t * smt_sort_formula_in_bfs_manner(smtManager_t * sm, smtFml_t * root); void smt_compute_indegree_in_formula(smtManager_t * sm); array_t * smt_gather_aig_node_from_formula_array(satArray_t * fmlArr); int smt_convert_aig_into_cnf_sub(smtManager_t * sm, AigEdge_t node, array_t * idArr, int * negated); int smt_add_var_id_for_node(smtManager_t * sm, AigEdge_t node, int * var_id, int * negated); void smt_generate_clause_with_aig(smtManager_t * sm, int cur_idx, int var_id, int lvar_id, int rvar_id, array_t * idArr); void smt_add_clause_for_object(smtManager_t * sm, AigEdge_t obj); void smt_add_clause_for_iff_fml(smtManager_t * sm); void smt_add_clause_for_iff_fml_sub(smtManager_t * sm, int z, int x, int y); void smt_add_clause_for_iff_children(smtManager_t * sm, AigEdge_t node_a, AigEdge_t node_b); void smt_add_clause_for_ite_fml(smtManager_t * sm); void smt_add_clause_for_ite_fml_sub(smtManager_t * sm, int x, int y, int z, int f); int smt_add_clause_for_ite_terminal_case(smtManager_t * sm, int x, int y, int z, int f); void smt_add_clause_for_ite_children(smtManager_t * sm, AigEdge_t node_a, AigEdge_t node_b, AigEdge_t node_c); void smt_add_clause_for_ite_chain_fml(smtManager_t * sm, smtFml_t * fml); satArray_t * smt_get_conjunct_in_fml(smtFml_t * fml, int num_fml); void smt_add_clause_for_ite_chain_fml_main(smtManager_t * sm); void smt_add_clause_for_ite_chain_fml(smtManager_t * sm, smtFml_t * fml); satArray_t * smt_get_conjunct_in_fml(smtFml_t * fml, int num_fml); void smt_add_clause_for_ite_chain_fml_sub(smtManager_t * sm, smtFml_t * ite_fml, satArray_t * condsArr, satArray_t * thensArr, satArray_t * elses); void smt_init_generate_cnf(smtManager_t * sm); int smt_create_clause_with_fml(smtManager_t * sm, smtFml_t * fml); int smt_put_lit_to_clause(smtCls_t * cls, smtFml_t * fml); int smt_put_lits_to_clause(smtCls_t * cls, smtFml_t * fml, array_t * conjs); void smt_create_clause_with_conjuncts(smtManager_t * sm, smtCls_t * cls, array_t * conjs); int smt_gather_conjuncts_in_and_fml(smtFml_t * fml, array_t * conjs); int smt_create_clause_with_ands_in_or_fml(smtManager_t * sm, smtFml_t * fml); /* satArray_t * smt_gather_conjuncts_in_and_fml(smtFml_t * fml); */ /* smtSat.c */ int smt_call_theory_solver(satManager_t * m, long bound); int smt_call_dl_theory_solver(smtManager_t * sm, long bound); int smt_call_la_theory_solver(smtManager_t * sm, long bound); void smt_call_dl_theory_solver_preprocess(smtManager_t *sm); void smt_call_la_theory_solver_preprocess(smtManager_t *sm); int smt_theory_solve(smtManager_t * sm); void smt_fit_decision_level_wrt_blocking_clause(satManager_t * m, satArray_t * arr); int smt_get_size_of_atom_variable(satManager_t * m); void smt_dl_theory_undo(smtManager_t * sm); void smt_la_theory_undo(smtManager_t * sm); void smt_update_edge_in_constraint_graph(smtManager_t * sm, smtAvar_t * avar); void smt_delete_edge_in_constraint_graph(smtManager_t * sm, smtEdge_t * e); smtEdge_t * smt_get_right_end_edge(smtManager_t * sm); int smt_get_right_end_edge_index(smtManager_t * sm); void smt_put_right_end_edge_to_deleted(smtEdge_t * deleted, smtEdge_t * rend_edge); void smt_update_nvar_bound_with_avar(smtManager_t * sm, smtAvar_t * avar); void smt_add_theory_clause(satManager_t * cm, smtAvar_t * avar, satArray_t * litArr); /* smtGraph.c */ smtVertex_t * smt_add_vertex(smtGraph_t * G, int vindex); smtEdge_t * smt_add_edge(smtGraph_t * G, smtVertex_t * s, smtVertex_t * d, smtAvar_t * avar, int eindex); smtEdge_t * smt_find_edge(smtVertex_t * s, smtVertex_t * d); /* smtDl.c */ int smt_idl_theory_solve(smtManager_t * sm); int smt_rdl_theory_solve(smtManager_t * sm); void smt_bellman_ford_main(smtManager_t * sm); void smt_dl_theory_propagation_main(smtManager_t * sm); void smt_generate_constraint_graph(smtManager_t * sm); void smt_init_constraint_graph(smtManager_t * sm); void smt_init_dists_in_constraint_graph(smtManager_t * sm); void smt_init_theory_prop_dists(smtManager_t * sm); void smt_free_constraint_graph(smtGraph_t * G); void smt_free_vertex(smtGraph_t * G); void smt_free_edge_implied(satArray_t * imp_edges); void smt_bellman_ford_algorithm(smtManager_t * sm); void smt_init_bellman_ford_algorithm(smtManager_t * sm); void smt_delete_subtree(smtGraph_t * G, smtVertex_t * v); void smt_collect_edges_in_neg_cycle(smtGraph_t * G, smtVertex_t * v); void smt_get_lemma_from_neg_cycle(smtManager_t * sm, satArray_t * neg_edges); void smt_retrieve_previous_distance(smtManager_t * sm); void smt_update_value_with_current_distance(smtManager_t * sm); void smt_init_dl_theory_propagation(smtGraph_t * G); void smt_idl_theory_propagation(smtManager_t * sm); void smt_rdl_theory_propagation(smtManager_t * sm); void smt_idl_gather_backward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar); void smt_idl_gather_forward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar); void smt_rdl_gather_backward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar); void smt_rdl_gather_forward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar); void smt_idl_traverse_backward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth); void smt_idl_traverse_forward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth); void smt_rdl_traverse_backward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth); void smt_rdl_traverse_forward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth); void smt_idl_gather_backward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * src, int * num_avar); void smt_rdl_gather_backward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * src, int * num_avar); void smt_idl_gather_forward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * dest, int * num_avar); void smt_rdl_gather_forward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * dest, int * num_avar); void smt_idl_theory_propagation_with_bv_arr(smtManager_t * sm, smtAvar_t * avar); void smt_idl_theory_propagation_with_fv_arr(smtManager_t * sm, smtAvar_t * avar); void smt_rdl_theory_propagation_with_bv_arr(smtManager_t * sm, smtAvar_t * avar); void smt_rdl_theory_propagation_with_fv_arr(smtManager_t * sm, smtAvar_t * avar); void smt_dl_simple_theory_propagation(smtManager_t * sm); void smt_get_theory_prop_reason(smtManager_t * sm, smtAvar_t * implying, smtAvar_t * implied, smtNvar_t * bnvar, smtNvar_t * fnvar); void smt_idl_init_reachable_vertex(smtGraph_t * G); void smt_rdl_init_reachable_vertex(smtGraph_t * G); /* smtLa.c */ int smt_la_theory_solve(smtManager_t *sm); int smt_la_assert(smtManager_t * sm); int smt_assert_upper(smtManager_t * sm, smtAvar_t * avar); int smt_assert_lower(smtManager_t * sm, smtAvar_t * avar); void smt_la_check(smtManager_t * sm); void smt_pivot(smtManager_t * sm, smtNvar_t * basic, int row, smtNvar_t * nbasic); int smt_get_infeasible_basic_row(smtManager_t * sm); int smt_update_basic_nvar_with_new_value(smtManager_t * sm, smtNvar_t * nvar, double constant); void smt_find_reason_for_upper_bound(smtManager_t * sm, smtNvar_t * nvar); void smt_find_reason_for_lower_bound(smtManager_t *sm, smtNvar_t * nvar); smtNvar_t * smt_get_non_basic_for_increase(smtManager_t * sm, int row); smtNvar_t * smt_get_non_basic_for_decrease(smtManager_t * sm, int row); void smt_update_basic_with_new_value(smtManager_t * sm, smtNvar_t * basic, smtNvar_t * nbasic, int row, double constant); void smt_retrieve_previous_nvar_value(smtManager_t * sm); void smt_save_current_nvar_value(smtManager_t * sm); void smt_la_theory_propagation_main(smtManager_t * sm); void smt_la_simple_theory_propagation(smtManager_t * sm); void smt_la_theory_init(smtManager_t * sm); void smt_la_bound_init(smtManager_t * sm); void smt_generate_tableau(smtManager_t * sm); void smt_gaussian_elimination(smtManager_t * sm); void smt_generate_slack_var_for_atom(smtManager_t * sm); satArray_t * smt_gather_atom_in_database(smtManager_t * sm); int smt_get_unbounded_nbasic_column_index(smtManager_t * sm, int row); /* smtMp.c */ smtMp_t * smt_mp_init(smtManager_t * sm); void smt_mp_init_pool(smtMp_t * mp); void smt_mp_init_nvar_values(smtManager_t * sm); void smt_mp_init_atom_constants(smtManager_t * sm); void smt_mp_free(smtMp_t * mp); void smt_mp_free_pool(smtMp_t * mp); void smt_mp_free_atom_constants(smtMp_t * mp); void smt_mp_free_nvar_values(smtMp_t * mp); void smt_mp_assign_atom_constants(smtManager_t * sm); void smt_mp_assign_atom_constant(smtMp_t * mp, smtFml_t * avfml); void smt_mp_get_atom_constant(smtMp_t * mp, smtFml_t * fml, mpq_t * mp_constant, mpq_t * coeff, int nminus); int smt_mp_dl_theory_solve(smtManager_t * sm); void smt_mp_bellman_ford_main(smtManager_t * sm); void smt_mp_generate_constraint_graph(smtManager_t * sm); void smt_mp_bellman_ford_algorithm(smtManager_t * sm); void smt_mp_init_bellman_ford_algorithm(smtManager_t * sm); void smt_mp_retrieve_previous_distance(smtManager_t * sm); void smt_mp_print_atom_constants(smtManager_t * sm); void smt_mp_print_value(mpq_t * value); /* smtDebug.c */ void smt_print_atom_variable(smtManager_t * sm); void smt_print_atom_variable_in_array(smtManager_t * sm, satArray_t * avarArr); void smt_print_numerical_variable(smtManager_t * sm); void smt_print_numerical_variable_in_array(satArray_t * nvarArr); void smt_print_nvar_with_value(smtManager_t * sm); void smt_print_nvar_value_in_tableau(smtManager_t * sm); void smt_check_nvar_value_with_tableau(smtManager_t * sm); void smt_print_nvar_bound_in_tableau(smtManager_t * sm); void smt_print_atom_for_slack(smtManager_t * sm); void smt_print_boolean_variable(smtManager_t * sm); void smt_print_flet_pair(smtManager_t * sm); void smt_print_cnf_to_smt_file(smtManager_t * sm); void smt_print_cnf_to_smt_file_with_avar(smtManager_t * sm); void smt_print_dimacs_to_smt_file(smtManager_t * sm); void smt_print_cnf_to_dimcas_file(smtManager_t * sm); void smt_print_fml_to_smt_file(smtManager_t * sm, smtFml_t * fml, int index); void smt_print_fml_to_file(smtManager_t * sm, smtFml_t * fml); void smt_print_aig_to_dot_file(Aig_Manager_t * bm); void smt_print_lit_in_array(smtManager_t * sm, satArray_t * litArr); void smt_print_lit_in_array_hor(smtManager_t * sm, satArray_t * litArr); void smt_print_sat_lit_in_array(smtManager_t * sm, satArray_t * litArr); void smt_print_idl_digraph_to_dot_file(smtGraph_t * G, char * filename); void smt_print_rdl_digraph_to_dot_file(smtGraph_t * G, char * filename); int smt_check_dl_lemma_with_yices(smtManager_t * sm); int smt_check_dl_lit_arr_with_yices(smtManager_t * sm); void smt_print_variable_to_smt_file(smtManager_t * sm, FILE * fp); void smt_print_equation_in_tableau(smtManager_t * sm); void smt_report_result(smtManager_t * sm, int is_model); void smt_dl_report_result(smtManager_t * sm); void smt_dl_report_intermediate_result(smtManager_t * sm); void smt_la_report_result(smtManager_t * sm); void smt_check_result(smtManager_t * sm); void smt_print_unknown(void); void smt_print_watched_lits(satManager_t * cm); char * smt_convert_atom_to_string(smtAvar_t * avar); int smt_check_solution(smtManager_t *sm); int smt_mp_check_solution(smtManager_t *sm); void smt_print_solution(smtManager_t * sm); void smt_mp_print_solution(smtManager_t * sm); #ifdef __cplusplus } #endif