SATSolver/sat_remapper.cpp at master · slavam2605/SATSolver · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
#include <cmath>
#include "sat_remapper.h"
#include "debug.h"

sat_remapper::sat_remapper(uint32_t nb_vars) {
    old_nb_vars = nb_vars;
    prior_map.resize(nb_vars + 1);
    std::fill(prior_map.begin(), prior_map.end(), preprocessor_value_state::UNDEF);
    variable_map.resize(nb_vars + 1);
    next_var = 1;
}

void sat_remapper::add_prior(int var, preprocessor_value_state value) {
    prior_map[var] = value;
}

void sat_remapper::add_undef_var(int var) {
    variable_map[var] = next_var++;
}

void sat_remapper::add_ver_var(int var, const std::vector<std::vector<int>>& clauses) {
    prior_map[var] = preprocessor_value_state::VER;
    remap_events.emplace_back(var, remap_event::create_ver(clauses));
}

void sat_remapper::add_any_var(int var) {
    // TODO: Support ANY (replace TRUE with ANY here)
    prior_map[var] = preprocessor_value_state::TRUE;
}

void sat_remapper::add_eq_var(int var, int eq_var) {
    prior_map[var] = preprocessor_value_state::EQ;
    remap_events.emplace_back(var, remap_event::create_eq(eq_var));
}

std::vector<int8_t> sat_remapper::remap(std::vector<int8_t> values) {
    std::vector<preprocessor_value_state> result;
    result.push_back(preprocessor_value_state::UNDEF);
    for (auto var = 1; var <= old_nb_vars; var++) {
        auto value = prior_map[var];
        switch (value) {
            case preprocessor_value_state::TRUE:
            case preprocessor_value_state::FALSE:
                result.push_back(value);
                break;
            case preprocessor_value_state::UNDEF: {
                auto new_var = variable_map[var];
                result.push_back(values[new_var] ? preprocessor_value_state::TRUE : preprocessor_value_state::FALSE);
                break;
            }
            case preprocessor_value_state::ANY:
                // TODO support iteration over all solutions
                result.push_back(preprocessor_value_state::TRUE);
                break;
            case preprocessor_value_state::VER:
                result.push_back(preprocessor_value_state::VER);
                break;
            case preprocessor_value_state::EQ:
                result.push_back(preprocessor_value_state::EQ);
                break;
        }
    }
    for (auto riter = remap_events.rbegin(); riter != remap_events.rend(); ++riter) {
        const auto& [var, event] = *riter;
        switch (event.type) {
            case remap_event_type::VER: {
                for (const auto& clause: event.ver_clauses) {
                    auto unsat = true;
                    auto var_positive = true;
                    for (int signed_var: clause) {
                        if (signed_var == var) {
                            var_positive = true;
                            continue;
                        }
                        if (signed_var == -var) {
                            var_positive = false;
                            continue;
                        }
                        auto value = result[abs(signed_var)];
                        switch (value) {
                            case preprocessor_value_state::TRUE:
                            case preprocessor_value_state::FALSE:
                                break;
                            default:
                            debug(debug_logic_error("Expected TRUE or FALSE, found: " << (int) result[var]))
                        }
                        if ((value == preprocessor_value_state::TRUE && signed_var > 0) ||
                            (value == preprocessor_value_state::FALSE && signed_var < 0)) {
                            unsat = false;
                            break;
                        }
                    }
                    if (!unsat)
                        continue;

                    result[var] = var_positive ? preprocessor_value_state::TRUE : preprocessor_value_state::FALSE;
                    break;
                }
                if (result[var] == preprocessor_value_state::VER) {
                    // TODO: Support ANY (replace TRUE with ANY here)
                    result[var] = preprocessor_value_state::TRUE;
                }
                break;
            }
            case remap_event_type::EQ: {
                debug(if (result[abs(event.eq_var)] != preprocessor_value_state::TRUE && result[abs(event.eq_var)] != preprocessor_value_state::FALSE)
                    debug_logic_error("eq_var is not TRUE or FALSE, value: " << (int) result[abs(event.eq_var)]))

                auto value = (result[abs(event.eq_var)] == preprocessor_value_state::TRUE) ^ (event.eq_var < 0);
                result[var] = value ? preprocessor_value_state::TRUE : preprocessor_value_state::FALSE;
                break;
            }
        }
    }
    std::vector<int8_t> bool_result;
    bool_result.push_back(false);
    for (auto var = 1; var <= old_nb_vars; var++) {
        switch (result[var]) {
            case preprocessor_value_state::TRUE:
                bool_result.push_back(true);
                break;
            case preprocessor_value_state::FALSE:
                bool_result.push_back(false);
                break;
            default:
                debug(debug_logic_error("Unexpected value in final remap: " << (int) result[var]))
        }
    }
    return bool_result;
}

preprocessor_value_state sat_remapper::get_prior(int var) {
    return prior_map[var];
}

int sat_remapper::get_mapped_variable(int var) {
    return variable_map[var];
}