|
OKlibrary
0.2.1.6
|
Updated and corrected version. More...
#include <stdio.h>#include <stdlib.h>#include <limits.h>#include <stdbool.h>#include <sys/times.h>#include <unistd.h>Go to the source code of this file.
Updated and corrected version.
Definition in file satz215.2.c.
| #define ACTIVE 1 |
Definition at line 109 of file satz215.2.c.
Referenced by add_resolvant(), backtracking(), branch(), branch1(), build_sat_instance(), choose_and_instantiate_variable_in_clause(), copy_clauses(), further_examin(), get_nb(), get_neg_clause_nb(), get_pos_clause_nb(), get_resolvant_nb(), manage_clauses(), my_manage_clauses(), my_simple_manage_clauses(), remove_clauses(), reset_all(), reset_context(), satisfy_literal(), simple_manage_clauses(), and unitclause_process().
| #define ACTIVE2 2 |
Definition at line 568 of file satz215.2.c.
Referenced by add_resolvant(), and build_sat_instance().
| #define complement | ( | lit1, | |
| lit2 | |||
| ) | ((lit1<lit2) ? lit2-lit1 == NB_VAR : lit1-lit2 == NB_VAR) |
Definition at line 100 of file satz215.2.c.
Referenced by OKlib::Concepts::AtomicCondition< AC >::constraints(), get_resolvant(), and redundant().
| #define double_tab_clause_size 2*tab_clause_size |
Definition at line 195 of file satz215.2.c.
| #define double_tab_clause_size 2*tab_clause_size |
Definition at line 195 of file satz215.2.c.
| #define EXITCODE_INPUT_ERROR 101 |
Definition at line 61 of file satz215.2.c.
Referenced by main().
| #define EXITCODE_PARAMETER_FAILURE 100 |
Definition at line 60 of file satz215.2.c.
Referenced by main().
| #define EXITCODE_SAT 10 |
Definition at line 63 of file satz215.2.c.
Referenced by main().
| #define EXITCODE_UNSAT 20 |
Definition at line 64 of file satz215.2.c.
Referenced by main().
| #define EXITCODE_VERIFICATION_FAILED 102 |
Definition at line 62 of file satz215.2.c.
Referenced by main().
| #define FALSE 0 |
Definition at line 54 of file satz215.2.c.
Referenced by add_resolvant(), already_present(), backtracking(), branch(), branch1(), build_sat_instance(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), further_examin_var_if_positive(), further_testable(), get_resolvant(), main(), manage_clauses(), my_manage_clauses(), redundant(), satisfy_literal(), search_redundence(), unitclause_process(), and verify_solution().
| #define get_var_from_lit | ( | negative_literal | ) | negative_literal-NB_VAR |
Definition at line 97 of file satz215.2.c.
Referenced by add_resolvant(), branch(), branch1(), further_examin(), get_nb(), get_resolvant_nb(), remove_link(), satisfy_literal(), search_redundence(), set_link(), unitclause_process(), and verify_solution().
| #define MAX_CLAUSE_LENGTH 1000 |
Definition at line 75 of file satz215.2.c.
Referenced by build_sat_instance().
| #define MAX_NODE_NUMBER 6000 |
Definition at line 110 of file satz215.2.c.
Referenced by allocate_node().
| #define MAX_NUMBER_CLAUSES 800000 |
Definition at line 71 of file satz215.2.c.
Referenced by build_sat_instance().
| #define MAX_NUMBER_VARIABLES 200000 |
Definition at line 67 of file satz215.2.c.
Referenced by build_sat_instance().
| #define my_tab_clause_size ((tab_clause_size/2<2000) ? 2000 : tab_clause_size/2) |
Definition at line 89 of file satz215.2.c.
| #define my_tab_unitclause_size ((tab_unitclause_size/2<1000) ? 1000 : tab_unitclause_size/2) |
Definition at line 91 of file satz215.2.c.
| #define my_tab_variable_size ((tab_variable_size/2<1000) ? 1000 : tab_variable_size/2) |
Definition at line 87 of file satz215.2.c.
Definition at line 96 of file satz215.2.c.
Referenced by get_nb(), and verify_solution().
| #define NEGATIVE 0 |
Definition at line 106 of file satz215.2.c.
| #define NEW_CLAUSE_REDUNDANT 7 |
Definition at line 350 of file satz215.2.c.
Referenced by add_resolvant(), already_present(), build_sat_instance(), redundant(), and search_redundence().
| #define NONE -1 |
Definition at line 55 of file satz215.2.c.
Referenced by add_resolvant(), already_present(), backtracking(), branch(), branch1(), build_sat_instance(), choose_and_instantiate_variable_in_clause(), copy_clauses(), dpl(), examine(), examine1(), examine2(), examine3(), further_examin(), further_examin_var_if_negative(), further_examin_var_if_positive(), get_nb(), get_neg_clause_nb(), get_pos_clause_nb(), get_resolvant(), get_resolvant_nb(), main(), manage_clauses(), my_manage_clauses(), my_simple_manage_clauses(), redundant(), remove_clauses(), remove_link(), remove_link_for_resolv(), satisfy_literal(), search_redundence(), set_link(), set_link_for_resolv(), simple_manage_clauses(), treat_implied_lits(), unitclause_process(), and verify_solution().
| #define OLD_CLAUSE_REDUNDANT 77 |
Definition at line 349 of file satz215.2.c.
Referenced by redundant(), and search_redundence().
| #define PASSIVE 0 |
Definition at line 108 of file satz215.2.c.
Referenced by already_present(), branch(), branch1(), build_sat_instance(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), further_examin_var_if_positive(), remove_clauses(), satisfy_literal(), search_redundence(), and unitclause_process().
| #define pop | ( | stack | ) | stack[--stack ## _fill_pointer] |
Definition at line 102 of file satz215.2.c.
Referenced by backtracking().
Definition at line 95 of file satz215.2.c.
Referenced by add_resolvant(), branch(), branch1(), further_examin(), get_complement(), get_resolvant_nb(), remove_link(), satisfy_literal(), search_redundence(), set_link(), unitclause_process(), and verify_solution().
| #define POSITIVE 1 |
Definition at line 107 of file satz215.2.c.
| #define push | ( | item, | |
| stack | |||
| ) | stack[stack ## _fill_pointer++] = item |
Definition at line 103 of file satz215.2.c.
Referenced by already_present(), backtracking(), branch(), branch1(), build_sat_instance(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), further_examin_var_if_positive(), manage_clauses(), my_manage_clauses(), my_simple_manage_clauses(), remove_clauses(), satisfy_literal(), simple_manage_clauses(), and unitclause_process().
| #define RESOLVANT_LENGTH 3 |
Definition at line 98 of file satz215.2.c.
Referenced by add_resolvant(), and get_resolvant().
| #define RESOLVANT_SEARCH_THRESHOLD 5000 |
Definition at line 99 of file satz215.2.c.
| #define satisfiable | ( | ) | CLAUSE_STACK_fill_pointer == NB_CLAUSE |
Definition at line 104 of file satz215.2.c.
Referenced by dpl(), main(), and UnitPropagation::unit_propagation_simple().
| #define T 10 |
Definition at line 58 of file satz215.2.c.
Referenced by Algorithms::adopt_rand(), choose_and_instantiate_variable_in_clause(), ConceptDefinitions::FiniteDomain_concept< B >::constraints(), OKlib::Concepts::CopyConstructible< T >::constraints(), OKlib::Concepts::DefaultConstructible< T >::constraints(), OKlib::Concepts::Assignable< T >::constraints(), StringHandling::fromString(), StringHandling::fromString_nc(), main(), Doc_Object::operator>>(), XercesTools::operator>>(), setzenbelegt(), and StringHandling::toString().
| #define tab_clause_size MAX_NUMBER_CLAUSES |
Definition at line 83 of file satz215.2.c.
Referenced by build_sat_instance().
| #define tab_literal_size 2*tab_variable_size |
Definition at line 93 of file satz215.2.c.
| #define tab_unitclause_size ((tab_clause_size/4<2000) ? 2000 : tab_clause_size/4) |
Definition at line 85 of file satz215.2.c.
Definition at line 82 of file satz215.2.c.
| #define TRUE 1 |
Definition at line 53 of file satz215.2.c.
Referenced by add_resolvant(), backtracking(), branch(), branch1(), build_sat_instance(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), further_examin(), further_examin_var_if_negative(), further_examin_var_if_positive(), further_testable(), get_resolvant(), insert_var_if_necessary1(), main(), manage_clauses(), my_manage_clauses(), satisfy_literal(), search_redundence(), treat_implied_lits(), unitclause_process(), and verify_solution().
| #define VAR_NODES1_nb 6 |
Definition at line 203 of file satz215.2.c.
Referenced by insert_var_if_necessary1().
| #define WEIGTH 5 |
Definition at line 57 of file satz215.2.c.
Referenced by get_nb_clauses(), and get_resolvant_nb().
| #define WORD_LENGTH 100 |
The maximal length of words to be read (otherwise segmentation fault!)
Definition at line 50 of file satz215.2.c.
Referenced by build_sat_instance(), and main().
| typedef signed int my_type |
Definition at line 45 of file satz215.2.c.
| typedef unsigned int my_unsigned_type |
Definition at line 46 of file satz215.2.c.
| typedef unsigned long StatisticsCount |
Definition at line 192 of file satz215.2.c.
| int add_resolvant | ( | int * | lits | ) |
Definition at line 602 of file satz215.2.c.
References ACTIVE, ACTIVE2, already_present(), node::clause, clause_length, clause_state, FALSE, get_resolvant(), get_var_from_lit, NB_CLAUSE, NEW_CLAUSE_REDUNDANT, node::next, NONE, OLD_CLAUSE_SUPPRESED, positive, RESOLVANT_LENGTH, sat, search_redundence(), set_link_for_resolv(), and TRUE.
Referenced by build_sat_instance().
| struct node* allocate_node | ( | ) | [read] |
Definition at line 127 of file satz215.2.c.
References CLAUSE_NODES, CLAUSE_NODES_pointer, MAX_NODE_NUMBER, ressource::next, ressource::pnode, and ressources.
Referenced by set_link(), and set_link_for_resolv().
| struct var_node* allocate_var_node1 | ( | ) | [read] |
Definition at line 208 of file satz215.2.c.
References VAR_NODES1, and VAR_NODES1_index.
Referenced by insert_var_if_necessary1().
| int already_present | ( | int * | resolvant | ) |
Definition at line 535 of file satz215.2.c.
References node::clause, CLAUSE_INVOLVED, clause_length, clause_state, FALSE, INVOLVED_CLAUSE_STACK, INVOLVED_CLAUSE_STACK_fill_pointer, NEW_CLAUSE_REDUNDANT, node::next, NONE, PASSIVE, push, remove_link(), and remove_link_for_resolv().
Referenced by add_resolvant().
| int backtracking | ( | ) |
Definition at line 307 of file satz215.2.c.
References ACTIVE, clause_length, CLAUSE_STACK, CLAUSE_STACK_fill_pointer, clause_state, FALSE, MANAGEDCLAUSE_STACK, MANAGEDCLAUSE_STACK_fill_pointer, NB_BACK, neg_in, NONE, pop, pos_in, push, remove_clauses(), saved_clause_stack, saved_managedclause_stack, simple_manage_clauses(), TRUE, UNITCLAUSE_STACK_fill_pointer, OKlib::Literals::var(), var_current_value, var_rest_value, var_state, VARIABLE_STACK, and VARIABLE_STACK_fill_pointer.
Referenced by dpl().
| int branch | ( | ) |
Definition at line 1140 of file satz215.2.c.
References ACTIVE, clause_state, FALSE, get_var_from_lit, IMPLIED_LITS, LIT_IMPLIED, MANAGEDCLAUSE_STACK_fill_pointer, my_manage_clauses(), NB_FIXED, NB_SEARCH, neg_in, NONE, PASSIVE, pos_in, positive, push, sat, TRUE, UNITCLAUSE_STACK, UNITCLAUSE_STACK_fill_pointer, OKlib::Literals::var(), var_current_value, var_state, and VARIABLE_STACK.
Referenced by examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), and further_examin_var_if_positive().
| int branch1 | ( | ) |
Definition at line 1268 of file satz215.2.c.
References ACTIVE, clause_state, FALSE, get_var_from_lit, MANAGEDCLAUSE_STACK_fill_pointer, my_manage_clauses(), NB_FIXED, NB_SEARCH, neg_in, NONE, PASSIVE, pos_in, positive, push, sat, TRUE, UNITCLAUSE_STACK, UNITCLAUSE_STACK_fill_pointer, OKlib::Literals::var(), var_current_value, var_state, and VARIABLE_STACK.
Referenced by further_examin_var_if_negative(), and further_examin_var_if_positive().
| my_type build_sat_instance | ( | char *const | input_file | ) |
Definition at line 667 of file satz215.2.c.
References ACTIVE, ACTIVE2, add_resolvant(), CLAUSE_INVOLVED, clause_length, clause_state, copy_clauses(), FALSE, free_ressources(), INIT_NB_CLAUSE, INVOLVED_CLAUSE_STACK, INVOLVED_CLAUSE_STACK_fill_pointer, MAX_CLAUSE_LENGTH, MAX_NUMBER_CLAUSES, MAX_NUMBER_VARIABLES, NB_CLAUSE, NB_VAR, neg_in, NEW_CLAUSE_REDUNDANT, NONE, PASSIVE, pos_in, push, remove_link_for_resolv(), sat, search_redundence(), set_link(), set_link_for_resolv(), tab_clause_size, TRUE, unitclause_process(), UNITCLAUSE_STACK, var_state, and WORD_LENGTH.
Referenced by main().
Definition at line 1534 of file satz215.2.c.
References ACTIVE, CLAUSE_STACK_fill_pointer, examine1(), examine2(), examine3(), FALSE, get_neg_clause_nb(), get_pos_clause_nb(), IMPLIED_LITS, IMPLIED_LITS_fill_pointer, LIT_IMPLIED, MANAGEDCLAUSE_STACK_fill_pointer, MAX_REDUCED, NB_BRANCHE, NB_MONO, nb_neg_clause_of_length2, nb_pos_clause_of_length2, NB_VAR, neg_in, NONE, PASSIVE, pos_in, push, reduce_if_negative_nb, reduce_if_positive_nb, remove_clauses(), saved_clause_stack, saved_managedclause_stack, simple_manage_clauses(), T, TESTED_VAR_STACK, TESTED_VAR_STACK_fill_pointer, treat_implied_lits(), TRUE, unitclause_process(), OKlib::Literals::var(), var_current_value, VAR_NODES1_index, var_rest_value, var_state, and VARIABLE_STACK.
Referenced by dpl().
| int* copy_clauses | ( | struct node * | node_in | ) |
Definition at line 644 of file satz215.2.c.
References ACTIVE, node::clause, clause_state, node::next, and NONE.
Referenced by build_sat_instance().
| void dpl | ( | ) |
Definition at line 1661 of file satz215.2.c.
References backtracking(), choose_and_instantiate_variable_in_clause(), NB_VAR, NONE, reset_all(), satisfiable, test_flag, unitclause_process(), UNITCLAUSE_STACK_fill_pointer, OKlib::Literals::var(), and VARIABLE_STACK_fill_pointer.
Referenced by main().
| int examine | ( | int | tested_var | ) |
Definition at line 985 of file satz215.2.c.
References branch(), FALSE, MANAGEDCLAUSE_STACK_fill_pointer, my_simple_manage_clauses(), neg_in, NONE, PASSIVE, pos_in, push, reduce_if_negative_nb, reduce_if_positive_nb, remove_clauses(), reset_context(), simple_manage_clauses(), TESTED_VAR_STACK, TRUE, var_current_value, var_rest_value, var_state, VARIABLE_STACK, and VARIABLE_STACK_fill_pointer.
| int examine1 | ( | int | tested_var | ) |
Definition at line 922 of file satz215.2.c.
References branch(), FALSE, get_resolvant_nb(), MANAGEDCLAUSE_STACK_fill_pointer, my_simple_manage_clauses(), neg_in, NONE, PASSIVE, pos_in, push, reduce_if_negative_nb, reduce_if_positive_nb, remove_clauses(), reset_context(), simple_manage_clauses(), TESTED_VAR_STACK, TRUE, var_current_value, var_rest_value, var_state, VARIABLE_STACK, and VARIABLE_STACK_fill_pointer.
Referenced by choose_and_instantiate_variable_in_clause().
| int examine2 | ( | int | tested_var | ) |
Definition at line 1071 of file satz215.2.c.
References branch(), FALSE, get_nb(), MANAGEDCLAUSE_STACK_fill_pointer, my_simple_manage_clauses(), neg_in, NONE, PASSIVE, pos_in, push, reduce_if_negative_nb, reduce_if_positive_nb, remove_clauses(), reset_context(), simple_manage_clauses(), TESTED_VAR_STACK, TRUE, var_current_value, var_rest_value, var_state, VARIABLE_STACK, and VARIABLE_STACK_fill_pointer.
Referenced by choose_and_instantiate_variable_in_clause().
| int examine3 | ( | const int | tested_var | ) |
Definition at line 1434 of file satz215.2.c.
References branch(), FALSE, further_examin(), further_testable(), MANAGEDCLAUSE_STACK_fill_pointer, my_simple_manage_clauses(), neg_in, NONE, PASSIVE, pos_in, push, reduce_if_negative_nb, reduce_if_positive_nb, remove_clauses(), reset_context(), simple_manage_clauses(), TESTED_VAR_STACK, TRUE, var_current_value, var_rest_value, var_state, VARIABLE_STACK, and VARIABLE_STACK_fill_pointer.
Referenced by choose_and_instantiate_variable_in_clause().
| void free_ressources | ( | ) |
Definition at line 140 of file satz215.2.c.
References ressource::next, ressource::pnode, and ressources.
Referenced by build_sat_instance().
| int further_examin | ( | int | saved_managedclause_fill_pointer | ) |
Definition at line 1384 of file satz215.2.c.
References ACTIVE, clause_length, further_examin_var_if_negative(), further_examin_var_if_positive(), get_var_from_lit, MANAGEDCLAUSE_STACK, MANAGEDCLAUSE_STACK_fill_pointer, MAX_REDUCED, nb_neg_clause_of_length2, nb_pos_clause_of_length2, NB_SEARCH, NONE, positive, sat, test_flag, TRUE, OKlib::Literals::var(), and var_state.
Referenced by examine3().
| int further_examin_var_if_negative | ( | int | var | ) |
Definition at line 1352 of file satz215.2.c.
References branch(), branch1(), FALSE, IMPLIED_LITS, LIT_IMPLIED, MANAGEDCLAUSE_STACK_fill_pointer, my_simple_manage_clauses(), NB_SEARCH, NB_SECOND_FIXED, NB_SECOND_SEARCH, neg_in, NONE, PASSIVE, pos_in, push, reset_context(), TRUE, OKlib::Literals::var(), var_current_value, var_state, VARIABLE_STACK, and VARIABLE_STACK_fill_pointer.
Referenced by further_examin().
| int further_examin_var_if_positive | ( | int | var | ) |
Definition at line 1319 of file satz215.2.c.
References branch(), branch1(), FALSE, get_complement(), IMPLIED_LITS, LIT_IMPLIED, MANAGEDCLAUSE_STACK_fill_pointer, my_simple_manage_clauses(), NB_SEARCH, NB_SECOND_FIXED, NB_SECOND_SEARCH, neg_in, NONE, PASSIVE, pos_in, push, reset_context(), TRUE, OKlib::Literals::var(), var_current_value, var_state, VARIABLE_STACK, and VARIABLE_STACK_fill_pointer.
Referenced by further_examin().
| int further_testable | ( | const int | saved_managedclause_fill_pointer | ) |
Definition at line 1425 of file satz215.2.c.
References FALSE, MANAGEDCLAUSE_STACK_fill_pointer, MAX_REDUCED, T_SEUIL, and TRUE.
Referenced by examine3().
| int get_complement | ( | int | lit | ) |
Definition at line 1233 of file satz215.2.c.
References NB_VAR, and positive.
Referenced by further_examin_var_if_positive().
| int get_nb | ( | int | saved_managedclause_fill_pointer | ) |
Definition at line 1044 of file satz215.2.c.
References ACTIVE, node::clause, clause_length, get_var_from_lit, MANAGEDCLAUSE_STACK, MANAGEDCLAUSE_STACK_fill_pointer, nb_neg_clause_of_length2, nb_pos_clause_of_length2, negative, NONE, sat, OKlib::Literals::var(), and var_state.
Referenced by examine2().
| int get_nb_clauses | ( | int | var | ) |
Definition at line 865 of file satz215.2.c.
References nb_neg_clause_of_length2, nb_neg_clause_of_length3, nb_pos_clause_of_length2, nb_pos_clause_of_length3, OKlib::Literals::var(), and WEIGTH.
| int get_neg_clause_nb | ( | const int | var | ) |
Definition at line 1501 of file satz215.2.c.
References ACTIVE, clause_length, clause_state, nb_neg_clause_of_length2, nb_neg_clause_of_length3, neg_in, NONE, and OKlib::Literals::var().
Referenced by choose_and_instantiate_variable_in_clause().
| int get_pos_clause_nb | ( | const int | var | ) |
Definition at line 1515 of file satz215.2.c.
References ACTIVE, clause_length, clause_state, nb_pos_clause_of_length2, nb_pos_clause_of_length3, NONE, pos_in, and OKlib::Literals::var().
Referenced by choose_and_instantiate_variable_in_clause().
| my_type get_resolvant | ( | int * | clause1, |
| int * | clause2, | ||
| int * | resolvant | ||
| ) |
Definition at line 386 of file satz215.2.c.
References complement, FALSE, NONE, RESOLVANT_LENGTH, smaller_than(), and TRUE.
Referenced by add_resolvant().
| int get_resolvant_nb | ( | int | saved_managedclause_fill_pointer | ) |
Definition at line 872 of file satz215.2.c.
References ACTIVE, node::clause, clause_length, get_var_from_lit, MANAGEDCLAUSE_STACK, MANAGEDCLAUSE_STACK_fill_pointer, nb_neg_clause_of_length2, nb_neg_clause_of_length3, nb_pos_clause_of_length2, nb_pos_clause_of_length3, NONE, positive, sat, OKlib::Literals::var(), var_state, and WEIGTH.
Referenced by examine1().
| int insert_var_if_necessary1 | ( | int | var | ) |
Definition at line 1238 of file satz215.2.c.
References allocate_var_node1(), var_node::next, reduce_if_negative_nb, reduce_if_positive_nb, TRUE, OKlib::Literals::var(), var_node::var, VAR_FOR_TEST1, VAR_NODES1_nb, and var_node::weight.
| int main | ( | const int | argc, |
| char *const | argv[] | ||
| ) |
Definition at line 1672 of file satz215.2.c.
References build_sat_instance(), CLAUSE_STACK_fill_pointer, dpl(), EPS, EXITCODE_INPUT_ERROR, EXITCODE_PARAMETER_FAILURE, EXITCODE_SAT, EXITCODE_UNSAT, EXITCODE_VERIFICATION_FAILED, FALSE, H_SEUIL, INIT_NB_CLAUSE, MANAGEDCLAUSE_STACK_fill_pointer, NB_BACK, NB_BRANCHE, NB_CLAUSE, NB_FIXED, NB_MONO, NB_SEARCH, NB_SECOND_FIXED, NB_SECOND_SEARCH, NB_UNIT, NB_VAR, NONE, print_values(), satisfiable, T, T_SEUIL, TRUE, VARIABLE_STACK_fill_pointer, verify_solution(), and WORD_LENGTH.
| int manage_clauses | ( | register int * | clauses | ) |
Definition at line 231 of file satz215.2.c.
References ACTIVE, clause_length, clause_state, FALSE, MANAGEDCLAUSE_STACK, NONE, push, TRUE, and UNITCLAUSE_STACK.
Referenced by satisfy_literal(), and unitclause_process().
| int my_manage_clauses | ( | register int * | clauses | ) |
Definition at line 277 of file satz215.2.c.
References ACTIVE, clause_length, clause_state, FALSE, MANAGEDCLAUSE_STACK, NONE, push, TRUE, and UNITCLAUSE_STACK.
| void my_simple_manage_clauses | ( | register int * | clauses | ) |
Definition at line 263 of file satz215.2.c.
References ACTIVE, clause_length, clause_state, MANAGEDCLAUSE_STACK, NONE, push, and UNITCLAUSE_STACK.
Referenced by examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), and further_examin_var_if_positive().
| void print_values | ( | int | nb_var | ) |
Definition at line 357 of file satz215.2.c.
References complement, FALSE, NEW_CLAUSE_REDUNDANT, NONE, OLD_CLAUSE_REDUNDANT, and smaller_than().
Referenced by search_redundence().
| void remove_clauses | ( | register int * | clauses | ) |
Definition at line 221 of file satz215.2.c.
References ACTIVE, CLAUSE_STACK, clause_state, NONE, PASSIVE, and push.
Referenced by backtracking(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), satisfy_literal(), and unitclause_process().
| void remove_link | ( | int | clause | ) |
Definition at line 448 of file satz215.2.c.
References node::clause, get_var_from_lit, node::next, NONE, positive, and sat.
Referenced by already_present(), and search_redundence().
| void remove_link_for_resolv | ( | int | resolv | ) |
Definition at line 508 of file satz215.2.c.
References node::clause, node::next, NONE, and sat.
Referenced by already_present(), and build_sat_instance().
| void reset_all | ( | ) |
Definition at line 1642 of file satz215.2.c.
References ACTIVE, clause_length, CLAUSE_STACK, CLAUSE_STACK_fill_pointer, clause_state, MANAGEDCLAUSE_STACK, MANAGEDCLAUSE_STACK_fill_pointer, NB_BACK, NB_BRANCHE, NB_FIXED, NB_MONO, NB_SEARCH, NB_SECOND_FIXED, NB_SECOND_SEARCH, NB_UNIT, UNITCLAUSE_STACK_fill_pointer, var_state, VARIABLE_STACK, and VARIABLE_STACK_fill_pointer.
Referenced by dpl().
| void reset_context | ( | int | saved_var_stack_fill_pointer, |
| int | saved_managedclause_fill_pointer | ||
| ) |
Definition at line 900 of file satz215.2.c.
References ACTIVE, clause_length, MANAGEDCLAUSE_STACK, MANAGEDCLAUSE_STACK_fill_pointer, UNITCLAUSE_STACK, UNITCLAUSE_STACK_fill_pointer, var_state, VARIABLE_STACK, and VARIABLE_STACK_fill_pointer.
Referenced by examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), and further_examin_var_if_positive().
| int satisfy_literal | ( | int | lit | ) |
Definition at line 1190 of file satz215.2.c.
References ACTIVE, FALSE, get_var_from_lit, manage_clauses(), neg_in, NONE, PASSIVE, pos_in, positive, push, remove_clauses(), TRUE, unitclause_process(), OKlib::Literals::var(), var_current_value, var_rest_value, var_state, and VARIABLE_STACK.
Referenced by treat_implied_lits().
| int search_redundence | ( | int * | lits | ) |
Definition at line 570 of file satz215.2.c.
References node::clause, clause_state, FALSE, get_var_from_lit, NEW_CLAUSE_REDUNDANT, node::next, NONE, OLD_CLAUSE_REDUNDANT, OLD_CLAUSE_SUPPRESED, PASSIVE, positive, redundant(), remove_link(), sat, and TRUE.
Referenced by add_resolvant(), and build_sat_instance().
| void set_link | ( | int | clause | ) |
Definition at line 476 of file satz215.2.c.
References allocate_node(), node::clause, get_var_from_lit, node::next, NONE, positive, and sat.
Referenced by build_sat_instance().
| void set_link_for_resolv | ( | int | resolv | ) |
Definition at line 496 of file satz215.2.c.
References allocate_node(), node::clause, node::next, NONE, and sat.
Referenced by add_resolvant(), and build_sat_instance().
| void simple_manage_clauses | ( | register int * | clauses | ) |
Definition at line 248 of file satz215.2.c.
References ACTIVE, clause_length, clause_state, MANAGEDCLAUSE_STACK, NONE, push, and UNITCLAUSE_STACK.
Referenced by backtracking(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), and examine3().
| int smaller_than | ( | int | lit1, |
| int | lit2 | ||
| ) |
Definition at line 352 of file satz215.2.c.
References NB_VAR.
Referenced by get_resolvant(), and redundant().
| int treat_implied_lits | ( | ) |
Definition at line 1222 of file satz215.2.c.
References IMPLIED_LITS, IMPLIED_LITS_fill_pointer, LIT_IMPLIED, NONE, satisfy_literal(), and TRUE.
Referenced by choose_and_instantiate_variable_in_clause().
| int unitclause_process | ( | ) |
Definition at line 815 of file satz215.2.c.
References ACTIVE, clause_state, FALSE, get_var_from_lit, manage_clauses(), NB_UNIT, neg_in, NONE, PASSIVE, pos_in, positive, push, remove_clauses(), sat, TRUE, UNITCLAUSE_STACK, UNITCLAUSE_STACK_fill_pointer, OKlib::Literals::var(), var_current_value, var_rest_value, var_state, and VARIABLE_STACK.
Referenced by build_sat_instance(), choose_and_instantiate_variable_in_clause(), dpl(), and satisfy_literal().
| int verify_solution | ( | ) |
Definition at line 793 of file satz215.2.c.
References FALSE, get_var_from_lit, NB_CLAUSE, negative, NONE, positive, sat, TRUE, and var_current_value.
Referenced by main().
Definition at line 533 of file satz215.2.c.
Referenced by already_present(), and build_sat_instance().
Definition at line 172 of file satz215.2.c.
Referenced by add_resolvant(), already_present(), backtracking(), build_sat_instance(), further_examin(), get_nb(), get_neg_clause_nb(), get_pos_clause_nb(), get_resolvant_nb(), look_fix_big_clauses(), manage_clauses(), my_manage_clauses(), my_simple_manage_clauses(), reset_all(), reset_context(), restore_big_clauses(), and simple_manage_clauses().
| struct node* CLAUSE_NODES |
Definition at line 124 of file satz215.2.c.
Referenced by allocate_node().
Definition at line 122 of file satz215.2.c.
Referenced by allocate_node().
Definition at line 180 of file satz215.2.c.
Referenced by backtracking(), remove_clauses(), and reset_all().
| int CLAUSE_STACK_fill_pointer = 0 |
Definition at line 175 of file satz215.2.c.
Referenced by backtracking(), choose_and_instantiate_variable_in_clause(), main(), and reset_all().
Definition at line 171 of file satz215.2.c.
Referenced by add_resolvant(), already_present(), backtracking(), branch(), branch1(), build_sat_instance(), copy_clauses(), get_neg_clause_nb(), get_pos_clause_nb(), manage_clauses(), my_manage_clauses(), my_simple_manage_clauses(), remove_clauses(), reset_all(), search_redundence(), simple_manage_clauses(), and unitclause_process().
| int H_SEUIL |
Definition at line 216 of file satz215.2.c.
Referenced by main().
Definition at line 1137 of file satz215.2.c.
Referenced by branch(), choose_and_instantiate_variable_in_clause(), further_examin_var_if_negative(), further_examin_var_if_positive(), and treat_implied_lits().
| int IMPLIED_LITS_fill_pointer = 0 |
Definition at line 1136 of file satz215.2.c.
Referenced by choose_and_instantiate_variable_in_clause(), and treat_implied_lits().
| struct node* in_resolv[tab_literal_size] |
Definition at line 152 of file satz215.2.c.
| int INIT_NB_CLAUSE |
Definition at line 189 of file satz215.2.c.
Referenced by build_sat_instance(), and main().
Definition at line 531 of file satz215.2.c.
Referenced by already_present(), and build_sat_instance().
Definition at line 532 of file satz215.2.c.
Referenced by already_present(), and build_sat_instance().
Definition at line 1138 of file satz215.2.c.
Referenced by branch(), choose_and_instantiate_variable_in_clause(), further_examin_var_if_negative(), further_examin_var_if_positive(), and treat_implied_lits().
Definition at line 182 of file satz215.2.c.
Referenced by backtracking(), further_examin(), get_nb(), get_resolvant_nb(), manage_clauses(), my_manage_clauses(), my_simple_manage_clauses(), reset_all(), reset_context(), and simple_manage_clauses().
| int MANAGEDCLAUSE_STACK_fill_pointer = 0 |
Definition at line 177 of file satz215.2.c.
Referenced by backtracking(), branch(), branch1(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), further_examin(), further_examin_var_if_negative(), further_examin_var_if_positive(), further_testable(), get_nb(), get_resolvant_nb(), main(), reset_all(), and reset_context().
| int MAX_REDUCED |
Definition at line 214 of file satz215.2.c.
Referenced by choose_and_instantiate_variable_in_clause(), further_examin(), and further_testable().
Definition at line 193 of file satz215.2.c.
Referenced by backtracking(), main(), and reset_all().
Definition at line 193 of file satz215.2.c.
Referenced by choose_and_instantiate_variable_in_clause(), main(), and reset_all().
| int NB_CLAUSE |
Definition at line 188 of file satz215.2.c.
Referenced by add_resolvant(), build_sat_instance(), main(), and verify_solution().
| long NB_FIXED = 0 |
Definition at line 813 of file satz215.2.c.
Referenced by branch(), branch1(), main(), and reset_all().
Definition at line 193 of file satz215.2.c.
Referenced by choose_and_instantiate_variable_in_clause(), main(), and reset_all().
Definition at line 162 of file satz215.2.c.
Referenced by choose_and_instantiate_variable_in_clause(), further_examin(), get_nb(), get_nb_clauses(), get_neg_clause_nb(), and get_resolvant_nb().
Definition at line 163 of file satz215.2.c.
Referenced by get_nb_clauses(), get_neg_clause_nb(), and get_resolvant_nb().
Definition at line 164 of file satz215.2.c.
Referenced by choose_and_instantiate_variable_in_clause(), further_examin(), get_nb(), get_nb_clauses(), get_pos_clause_nb(), and get_resolvant_nb().
Definition at line 165 of file satz215.2.c.
Referenced by get_nb_clauses(), get_pos_clause_nb(), and get_resolvant_nb().
| long NB_SEARCH = 0 |
Definition at line 813 of file satz215.2.c.
Referenced by branch(), branch1(), further_examin(), further_examin_var_if_negative(), further_examin_var_if_positive(), main(), and reset_all().
| long NB_SECOND_FIXED = 0 |
Definition at line 219 of file satz215.2.c.
Referenced by further_examin_var_if_negative(), further_examin_var_if_positive(), main(), and reset_all().
| long NB_SECOND_SEARCH = 0 |
Definition at line 218 of file satz215.2.c.
Referenced by further_examin_var_if_negative(), further_examin_var_if_positive(), main(), and reset_all().
Definition at line 193 of file satz215.2.c.
Referenced by main(), reset_all(), and unitclause_process().
| int NB_VAR |
Definition at line 187 of file satz215.2.c.
Referenced by build_sat_instance(), choose_and_instantiate_variable_in_clause(), dpl(), get_complement(), main(), and smaller_than().
| int* neg_in[tab_variable_size] |
Definition at line 154 of file satz215.2.c.
Referenced by backtracking(), branch(), branch1(), build_sat_instance(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), further_examin_var_if_positive(), get_neg_clause_nb(), satisfy_literal(), and unitclause_process().
| struct node* node_neg_in[tab_variable_size] |
Definition at line 150 of file satz215.2.c.
| struct node* node_pos_in[tab_variable_size] |
Definition at line 151 of file satz215.2.c.
Definition at line 567 of file satz215.2.c.
Referenced by add_resolvant(), and search_redundence().
| int* pos_in[tab_variable_size] |
Definition at line 155 of file satz215.2.c.
Referenced by backtracking(), branch(), branch1(), build_sat_instance(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), further_examin_var_if_positive(), get_pos_clause_nb(), satisfy_literal(), and unitclause_process().
Definition at line 190 of file satz215.2.c.
Referenced by main(), and OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::perform_ucp().
Definition at line 167 of file satz215.2.c.
Referenced by choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), and insert_var_if_necessary1().
Definition at line 168 of file satz215.2.c.
Referenced by choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), and insert_var_if_necessary1().
| struct ressource* ressources = NULL |
Definition at line 125 of file satz215.2.c.
Referenced by allocate_node(), and free_ressources().
| int* sat[tab_clause_size] |
Definition at line 170 of file satz215.2.c.
Referenced by add_resolvant(), branch(), branch1(), build_sat_instance(), DLL_Algorithms::DLL_1(), ExperimentDurchfuehrung::Durchfuehrung(), further_examin(), get_nb(), get_resolvant_nb(), main(), remove_link(), remove_link_for_resolv(), search_redundence(), set_link(), set_link_for_resolv(), unitclause_process(), and verify_solution().
Definition at line 160 of file satz215.2.c.
Referenced by backtracking(), and choose_and_instantiate_variable_in_clause().
Definition at line 161 of file satz215.2.c.
Referenced by backtracking(), and choose_and_instantiate_variable_in_clause().
| int T_SEUIL |
Definition at line 215 of file satz215.2.c.
Referenced by further_testable(), and main().
Definition at line 212 of file satz215.2.c.
Referenced by dpl(), and further_examin().
Definition at line 184 of file satz215.2.c.
Referenced by choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), and examine3().
| int TESTED_VAR_STACK_fill_pointer = 0 |
Definition at line 185 of file satz215.2.c.
Referenced by choose_and_instantiate_variable_in_clause().
Definition at line 181 of file satz215.2.c.
Referenced by branch(), branch1(), build_sat_instance(), manage_clauses(), my_manage_clauses(), my_simple_manage_clauses(), reset_context(), simple_manage_clauses(), and unitclause_process().
| int UNITCLAUSE_STACK_fill_pointer = 0 |
Definition at line 176 of file satz215.2.c.
Referenced by backtracking(), branch(), branch1(), dpl(), reset_all(), reset_context(), and unitclause_process().
Definition at line 156 of file satz215.2.c.
Referenced by backtracking(), branch(), branch1(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), further_examin_var_if_positive(), print_values(), satisfy_literal(), unitclause_process(), and verify_solution().
| struct var_node* VAR_FOR_TEST1 = NULL |
Definition at line 206 of file satz215.2.c.
Referenced by insert_var_if_necessary1().
| struct var_node VAR_NODES1[10 *VAR_NODES1_nb] |
Definition at line 205 of file satz215.2.c.
Referenced by allocate_var_node1().
| int VAR_NODES1_index = 0 |
Definition at line 204 of file satz215.2.c.
Referenced by allocate_var_node1(), and choose_and_instantiate_variable_in_clause().
Definition at line 157 of file satz215.2.c.
Referenced by backtracking(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), satisfy_literal(), and unitclause_process().
Definition at line 158 of file satz215.2.c.
Referenced by backtracking(), branch(), branch1(), build_sat_instance(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), further_examin(), further_examin_var_if_negative(), further_examin_var_if_positive(), get_nb(), get_resolvant_nb(), reset_all(), reset_context(), satisfy_literal(), and unitclause_process().
Definition at line 179 of file satz215.2.c.
Referenced by backtracking(), branch(), branch1(), choose_and_instantiate_variable_in_clause(), examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), further_examin_var_if_positive(), reset_all(), reset_context(), satisfy_literal(), and unitclause_process().
| int VARIABLE_STACK_fill_pointer = 0 |
Definition at line 174 of file satz215.2.c.
Referenced by backtracking(), dpl(), examine(), examine1(), examine2(), examine3(), further_examin_var_if_negative(), further_examin_var_if_positive(), main(), reset_all(), and reset_context().