propagate.h

#ifndef CLINGO_PROPAGATE_H
#define CLINGO_PROPAGATE_H
 
#include <clingo/base.h>
#include <clingo/core.h>
#include <clingo/shared.h>
#include <clingo/symbol.h>
 
#ifdef __cplusplus
extern "C" {
#endif
 
typedef struct clingo_control clingo_control_t;
 
 
 
typedef struct clingo_assignment clingo_assignment_t;
 
enum clingo_truth_value_e {
    clingo_truth_value_free = 0, 
    clingo_truth_value_true = 1, 
    clingo_truth_value_false = 2 
};
typedef int clingo_truth_value_t;
 
 
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_thread_id(clingo_assignment_t const *assignment, clingo_id_t *id);
 
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_decision_level(clingo_assignment_t const *assignment, uint32_t *level);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_root_level(clingo_assignment_t const *assignment, uint32_t *level);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_has_conflict(clingo_assignment_t const *assignment,
                                                              bool *is_conflicting);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_has_literal(clingo_assignment_t const *assignment,
                                                             clingo_literal_t literal, bool *is_valid);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_level(clingo_assignment_t const *assignment, clingo_literal_t literal,
                                                       uint32_t *level);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_decision(clingo_assignment_t const *assignment, uint32_t level,
                                                          clingo_literal_t *literal);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_fixed(clingo_assignment_t const *assignment,
                                                          clingo_literal_t literal, bool *is_fixed);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_true(clingo_assignment_t const *assignment,
                                                         clingo_literal_t literal, bool *is_true);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_false(clingo_assignment_t const *assignment,
                                                          clingo_literal_t literal, bool *is_false);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_truth_value(clingo_assignment_t const *assignment,
                                                             clingo_literal_t literal, clingo_truth_value_t *value);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_size(clingo_assignment_t const *assignment, size_t *size);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_at(clingo_assignment_t const *assignment, size_t offset,
                                                    clingo_literal_t *literal);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_total(clingo_assignment_t const *assignment, bool *is_total);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_size(clingo_assignment_t const *assignment, uint32_t *size);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_begin(clingo_assignment_t const *assignment, uint32_t level,
                                                             uint32_t *offset);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_end(clingo_assignment_t const *assignment, uint32_t level,
                                                           uint32_t *offset);
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_at(clingo_assignment_t const *assignment, uint32_t offset,
                                                          clingo_literal_t *literal);
 
 
enum clingo_propagator_check_mode_e {
    clingo_propagator_check_mode_none = 0,     
    clingo_propagator_check_mode_total = 1,    
    clingo_propagator_check_mode_fixpoint = 2, 
    clingo_propagator_check_mode_both =
        3, 
};
typedef int clingo_propagator_check_mode_t;
 
enum clingo_propagator_undo_mode_e {
    clingo_propagator_undo_mode_default = 0, 
    clingo_propagator_undo_mode_always = 1,  
};
typedef int clingo_propagator_undo_mode_t;
 
enum clingo_weight_constraint_type_e {
    clingo_weight_constraint_type_implication_left = -1, 
    clingo_weight_constraint_type_implication_right = 1, 
    clingo_weight_constraint_type_equivalence = 0,       
};
typedef int clingo_weight_constraint_type_t;
 
typedef struct clingo_propagate_control clingo_propagate_control_t;
 
typedef struct clingo_propagate_init clingo_propagate_init_t;
 
 
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_solver_literal(clingo_propagate_init_t const *init,
                                                                    clingo_literal_t aspif_literal,
                                                                    clingo_literal_t *solver_literal);
 
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_freeze_literal(clingo_propagate_init_t *init,
                                                                    clingo_literal_t solver_literal);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_library(clingo_propagate_init_t const *init, clingo_lib_t **lib);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_base(clingo_propagate_init_t const *init,
                                                          clingo_base_t const **base);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_number_of_threads(clingo_propagate_init_t const *init,
                                                                       clingo_id_t *threads);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_set_check_mode(clingo_propagate_init_t *init,
                                                                    clingo_propagator_check_mode_t mode);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_get_check_mode(clingo_propagate_init_t const *init,
                                                                    clingo_propagator_check_mode_t *mode);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_set_undo_mode(clingo_propagate_init_t *init,
                                                                   clingo_propagator_undo_mode_t mode);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_get_undo_mode(clingo_propagate_init_t const *init,
                                                                   clingo_propagator_undo_mode_t *mode);
 
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_control(clingo_propagate_init_t const *init,
                                                             clingo_propagate_control_t **control);
 
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_minimize(clingo_propagate_init_t *init,
                                                                  clingo_literal_t solver_literal,
                                                                  clingo_weight_t weight, clingo_weight_t priority);
 
 
enum clingo_clause_type_e {
    clingo_clause_type_learnt = 0, 
    clingo_clause_type_static = 1, 
    clingo_clause_type_volatile =
        2, 
    clingo_clause_type_volatile_static =
        3 
};
typedef int clingo_clause_type_t;
 
 
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_literal(clingo_propagate_control_t *control, bool freeze,
                                                                    clingo_literal_t *result);
 
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_watch(clingo_propagate_control_t *control,
                                                                  clingo_literal_t literal);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_has_watch(clingo_propagate_control_t const *control,
                                                                  clingo_literal_t literal, bool *has_watch);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_remove_watch(clingo_propagate_control_t *control,
                                                                     clingo_literal_t literal);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_clause(clingo_propagate_control_t *control,
                                                                   clingo_literal_t const *literals, size_t size,
                                                                   clingo_clause_type_t type, bool *result);
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_weight_constraint(
    clingo_propagate_control_t *control, clingo_literal_t solver_literal, clingo_weighted_literal_t const *literals,
    size_t size, clingo_weight_t bound, clingo_weight_constraint_type_t type, bool *result);
 
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_propagate(clingo_propagate_control_t *control, bool *result);
 
 
typedef bool (*clingo_propagator_init_callback_t)(clingo_assignment_t const *, clingo_propagate_init_t *, void *);
 
typedef bool (*clingo_propagator_attach_callback_t)(clingo_assignment_t const *, clingo_propagate_control_t *, void *);
 
typedef bool (*clingo_propagator_propagate_callback_t)(clingo_assignment_t const *, clingo_propagate_control_t *,
                                                       clingo_literal_t const *, size_t, void *);
 
typedef void (*clingo_propagator_undo_callback_t)(clingo_assignment_t const *, clingo_literal_t const *, size_t,
                                                  void *);
 
typedef bool (*clingo_propagator_check_callback_t)(clingo_assignment_t const *, clingo_propagate_control_t *, void *);
 
typedef struct clingo_propagator {
    bool (*init)(clingo_assignment_t const *assignment, clingo_propagate_init_t *init, void *data);
    bool (*attach)(clingo_assignment_t const *assignment, clingo_propagate_control_t *control, void *data);
 
    bool (*propagate)(clingo_assignment_t const *assignment, clingo_propagate_control_t *control,
                      clingo_literal_t const *changes, size_t size, void *data);
    void (*undo)(clingo_assignment_t const *assignment, clingo_literal_t const *changes, size_t size, void *data);
    bool (*check)(clingo_assignment_t const *assignment, clingo_propagate_control_t *control, void *data);
    bool (*decide)(clingo_assignment_t const *assignment, clingo_literal_t fallback, void *data,
                   clingo_literal_t *decision);
    void (*free)(void *data);
} clingo_propagator_t;
 
CLINGO_VISIBILITY_DEFAULT bool clingo_control_register_propagator(clingo_control_t *control,
                                                                  clingo_propagator_t const *propagator, void *data);
 
#ifdef __cplusplus
}
#endif
 
#endif