Commit 80e8b81d authored by Vladimír Uhlík's avatar Vladimír Uhlík
Browse files

src: Use 32 bit ints and change type of reason clause.

parent f658ebb8

src/types.hpp

+11 −11
Original line number Diff line number Diff line
@@ -25,14 +25,14 @@ namespace zilla 
    struct clause;

    struct formula;



    using var_t = std::uint64_t;

    using lit_t = std::int64_t;

    using idx_t = std::uint64_t;

    using var_t = std::uint32_t;

    using lit_t = std::int32_t;

    using idx_t = std::uint32_t;



    template< typename T >

    using vec = std::vector< T >;



    static constexpr idx_t max_level = std::numeric_limits< idx_t >::max();

    static constexpr idx_t max_idx = std::numeric_limits< idx_t >::max();



    struct variable

    {
@@ -71,9 +71,9 @@ namespace zilla 
        variable *var;

        literal *dual;

        LitKind kind;

        idx_t level = max_level;

        idx_t level = max_idx;

        std::set< idx_t > wcls;

        std::optional< idx_t > reason = std::nullopt;

        idx_t reason = max_idx;



        literal() : var( nullptr ), dual( nullptr ), kind( LitKind::UNDEF ) {}

        literal( lit_t l, literal *d, variable &vs ) :
@@ -387,7 +387,7 @@ namespace zilla 
                if ( clauses[ i ].update_watchers() == 1 )

                {

                    literal *l = clauses[ i ].find_unassigned();

                    if ( l && !l->reason.has_value() )

                    if ( l && l->reason == max_idx )

                    {

                        l->reason = i;

                        to_resolve.push_back( l );
@@ -421,8 +421,8 @@ namespace zilla 
                auto &lit = literals[ trail.back() ];



                lit.var->set_state( VarState::UNDEC );

                lit.set_level( max_level );

                lit.reason = std::nullopt;

                lit.set_level( max_idx );

                lit.reason = max_idx;



                var_prior.insert( lit.var->get_var() - 1 );
@@ -432,7 +432,7 @@ namespace zilla 
            decisions.pop_back();



            for ( auto *l : to_resolve )

                l->reason = std::nullopt;

                l->reason = max_idx;



            to_resolve.clear();

            update_watchers();
@@ -450,7 +450,7 @@ namespace zilla 
                    continue;



                top->assign_var();

                top->set_level( decisions.empty() ? max_level : decisions.back() );

                top->set_level( decisions.empty() ? max_idx : decisions.back() );

                update_watchers();

                trail.push_back( get_literal_idx( top->get_var() ) );