Skip to content

Refactor #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
kondortech wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Refactor #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion solver/include/solver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ namespace CDCL

UnitPropagationStatus unit_propagate(std::vector<VariableValueDecision> &current_variables_stack);
void apply_new_variables(std::vector<VariableValueDecision> &current_variables_stack,
const std::unordered_map<int, CNF::Value> &value_by_id);;
const std::unordered_map<int, CNF::Value> &value_by_id);

void updateClausesValue();

Expand Down
5 changes: 4 additions & 1 deletion solver/include/utils.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,10 @@ namespace utils
T value;
bool has_value;

Maybe(T value = -1, bool hasValue = false) : value(value), has_value(hasValue)
explicit Maybe(T value) : value(value), has_value(true)
{}

Maybe() : has_value(false)
{}
};
}
Expand Down
21 changes: 9 additions & 12 deletions solver/src/CNF.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
utils::Maybe<CNF::Variable> CNF::Clause::get_maybe_updatable_variable_id() const
{
if (isTrue) {
return utils::Maybe<CNF::Variable>(Variable(), false);
return {};
}
CNF::Variable var_with_val(-1, Value::Undefined);
for (const auto &literal : literals)
Expand All @@ -13,18 +13,14 @@ utils::Maybe<CNF::Variable> CNF::Clause::get_maybe_updatable_variable_id() const
if (var_with_val.value == Value::Undefined)
{
var_with_val.id = literal.var->id;
if (literal.has_negate) {
var_with_val.value = Value::False;
} else {
var_with_val.value = Value::True;
}
var_with_val.value = literal.has_negate ? Value::False : Value::True;
continue;
}
return utils::Maybe<Variable>(Variable(), false);
return {};
}
}

return utils::Maybe<CNF::Variable>(var_with_val, var_with_val.value != Value::Undefined);
return var_with_val.value != Value::Undefined ? utils::Maybe(var_with_val) : utils::Maybe<CNF::Variable>();
}

void CNF::Clause::update_clause_value()
Expand All @@ -33,29 +29,30 @@ void CNF::Clause::update_clause_value()
for (const auto &literal : literals) {
if (literal.get_value() == Value::True) {
isTrue = true;
break;
}
}
}

CNF::Value CNF::Literal::get_value() const
{
if (var->value == Value::Undefined)
auto value = var->value;
if (value == Value::Undefined)
{
return Value::Undefined;
}
if (has_negate)
{
return var->value == Value::True ? Value::False : Value::True;
return value == Value::True ? Value::False : Value::True;
}
return var->value;
return value;
}

std::ostream &operator<<(std::ostream &out, const CNF::Variable &var)
{
out << var.id << " = ";
switch (var.value)
{

case CNF::Value::False:
out << 0;
break;
Expand Down
28 changes: 14 additions & 14 deletions solver/src/solver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,13 +34,13 @@ namespace CDCL
std::vector<VariableValueDecision> current_variables_stack;
while (current_variables_stack.size() != variables.size())
{
auto PropagatingStatus = unit_propagate(current_variables_stack);
while (PropagatingStatus == Good) {
PropagatingStatus = unit_propagate(current_variables_stack);
}
if (PropagatingStatus == Bad) {
UnitPropagationStatus propagating_status;
do {
propagating_status = unit_propagate(current_variables_stack);
} while (propagating_status == Good);
if (propagating_status == Bad) {
if (!change_last_decision(current_variables_stack)) {
return {{}, false};
return {};
}
continue;
}
Expand All @@ -50,7 +50,6 @@ namespace CDCL
current_variables_stack.emplace_back(next_variable_id, false, false);
variables[next_variable_id]->value = CNF::Value::False;
updateClausesValue();

}


Expand All @@ -60,7 +59,7 @@ namespace CDCL
result.emplace_back(var_with_decision.var_id, var_with_decision.cur_value);
}

return {result, true};
return utils::Maybe(result);
}

Solver::UnitPropagationStatus Solver::unit_propagate(std::vector<VariableValueDecision> &current_variables_stack)
Expand Down Expand Up @@ -118,18 +117,19 @@ namespace CDCL
{
// This is like we are looking for the least ancestor which has more "righter" path
while (!current_variables_stack.empty()) {
if (current_variables_stack.back().isAutomaticallyDetermined) {
variables[current_variables_stack.back().var_id]->value = CNF::Value::Undefined;
auto &stack_back = current_variables_stack.back();
if (stack_back.isAutomaticallyDetermined) {
variables[stack_back.var_id]->value = CNF::Value::Undefined;
current_variables_stack.pop_back();
continue;
}
if (current_variables_stack.back().cur_value) {
variables[current_variables_stack.back().var_id]->value = CNF::Value::Undefined;
if (stack_back.cur_value) {
variables[stack_back.var_id]->value = CNF::Value::Undefined;
current_variables_stack.pop_back();
continue;
}
variables[current_variables_stack.back().var_id]->value = CNF::Value::True;
current_variables_stack.back().cur_value = true;
variables[stack_back.var_id]->value = CNF::Value::True;
stack_back.cur_value = true;
updateClausesValue();
return true;
}
Expand Down