Commit 8aa775bb authored by Jindřich Sedláček's avatar Jindřich Sedláček
Browse files

feat(unit propagation): continue refactor, seems to work

parent 6d1fa223

src/engine.cpp

+16 −7
Original line number Diff line number Diff line
@@ -301,21 +301,21 @@ void Engine::learn(Clause clause) 
    int true_idx = 0;

    int unknown_idx = 0;



    for (int idx = 0; idx < info.clause.size(); idx++)

    for (int i = 0; i < info.clause.size(); i++)

    {

        AssignmentState state = literal_status(clause.body[idx]);

        AssignmentState state = literal_status(info.clause.body[i]);



        if (state.is_true())

        {

            std::swap(clause.body[true_idx], clause.body[unknown_idx]);

            std::swap(clause.body[true_idx], clause.body[idx]);

            std::swap(info.clause.body[true_idx], info.clause.body[unknown_idx]);

            std::swap(info.clause.body[true_idx], info.clause.body[i]);



            unknown_idx++;

            true_idx++;

        }

        else if (state.is_unknown())

        {

            std::swap(clause.body[unknown_idx], clause.body[idx]);

            std::swap(info.clause.body[unknown_idx], info.clause.body[i]);

            unknown_idx++;

        }

    }
@@ -323,9 +323,18 @@ void Engine::learn(Clause clause) 
    // we can unit propagate the unknown (now first) literal

    if (true_idx == 0 && unknown_idx == 1)

    {

        set_literal_to_true(clause.body[0]);

        _variable_infos[info.clause.body[0].get_variable()].reason = idx;

        set_literal_to_true(info.clause.body[0]);

    }

    else

    {

        // our solver should never get here as it is written;

        // assert(false);

    }



    set_up_watch(idx, true);

    set_up_watch(idx, false);



    return;



    bool has_true = false;

src/solver.cpp

+1 −1
Original line number Diff line number Diff line
@@ -238,7 +238,7 @@ SolverResult Solver::run_CDCL() 


        while (unit_propagation_result.has_value())

        {

            if (_engine.can_backtrack())

            if (!_engine.can_backtrack())

            {

                return SolverResult::UNSAT;

            }