#pragma once

#include "common.hpp"
#include "smt.hpp"

#include <utility>
#include <vector>
#include <string>
#include <set>
#include <map>
#include <deque>

namespace shoop
{

// Our goal is to find which (formal) parameters are "interesting". Simply said, a parameter is
// interesting if an error can manifest depending on its value (i.e. there is both a value
// for which an error occurs and a value for which the same error does not occur). To this end, we
// repeatedly run Divine with unit and counit abstract values.
//
// See also:
// - dios/lamp/shoop.hpp

enum class parameter_domain : uint8_t
{
    unit,  // The "search all" domain
    sunit, // The "search nothing" domain (silencing unit)
    term   // The bitvector term domain
};

template < typename T >
inline T &&from_domain(
    parameter_domain d,
    T &&unit,
    T &&sunit,
    T &&term
)
{
    return std::forward< T >
    (
        d == parameter_domain::unit  ? unit  :
        d == parameter_domain::sunit ? sunit :
                                       term
    );
}

// This represents a list of parameter domains that can describe a single function invocation,
// e.g. [unit, sunit, unit].
struct invocation_lattice_node
{
    // Invariant: _pattern.size() <= 64
    // TODO: Consider changing for a bitset?
    std::vector< parameter_domain > _pattern;

    explicit invocation_lattice_node( std::vector< parameter_domain > pattern ) : _pattern( std::move( pattern ) )
    {
        ASSERT_LEQ( _pattern.size(), 64 );
    }

    // Create an invocation that has all 'num_params' filled with silencing units.
    static invocation_lattice_node bottom( uint8_t num_params )
    {
        return invocation_lattice_node( std::vector< parameter_domain >( num_params, parameter_domain::sunit ) );
    }

    static invocation_lattice_node top( uint8_t num_params )
    {
        return invocation_lattice_node( std::vector< parameter_domain >( num_params, parameter_domain::unit ) );
    }

    // Promote every unit parameter that is referenced by the given precondition to a term.
    invocation_lattice_node promote( const formula &pre ) const;

    // Promote every unit parameter to term.
    invocation_lattice_node promote() const;

    // Get invocation_parameters that have units exactly on those positions where either *this
    // or other has units.
    // invocation_lattice_node union_with( const invocation_lattice_node &other ) const;

    // Create a list of all invocation patterns that are the same as this one except
    // that exactly one silencing unit is turned into unit.
    // Example: [sunit, sunit, unit] has successors [unit, sunit, unit], [sunit, unit, unit],
    //          but not [unit, unit, unit].
    std::vector< invocation_lattice_node > get_successors() const;

    const std::vector< parameter_domain > &parameters() const { return _pattern; }
    std::size_t size() const { return _pattern.size(); }

    using cipr = const invocation_lattice_node &;

    // These operators exist to allow this to be stored in 'std::map' but do not respect the
    // ordering that we want to have (i.e. boolean algebra isomorphic to P(_pattern.size())).
    // TODO: Do we want this, or perhaps store in hashmap? 
    friend bool operator==( cipr a, cipr b )
    {
        ASSERT_EQ( a._pattern.size(), b._pattern.size() ); // Such comparison would be an error.
        return a._pattern == b._pattern;
    }

    friend bool operator<=( cipr a, cipr b )
    {
        ASSERT_EQ( a._pattern.size(), b._pattern.size() );
        return a._pattern <= b._pattern;
    }

    friend bool operator!=( cipr a, cipr b ) { return !(a == b);        }
    friend bool operator< ( cipr a, cipr b ) { return a <= b && a != b; }
    friend bool operator> ( cipr a, cipr b ) { return b < a;            }
    friend bool operator>=( cipr a, cipr b ) { return !(a < b);         }

    std::string to_string(
        const std::string &unit,
        const std::string &sunit,
        const std::string &term,
        const std::string &separator
    ) const;
};

struct invocation_lattice
{
    invocation_lattice_node _bottom;
    std::map< invocation_lattice_node, std::set< formula > > _precondition_conjuncts;

    explicit invocation_lattice( std::size_t num_params )
        : _bottom{ invocation_lattice_node::bottom( num_params ) },
          _precondition_conjuncts{ { _bottom, { formula::constant( true ) } } }
    {}

    formula build_precondition( const invocation_lattice_node& node ) const
    {
        ASSERT_LT( 0, _precondition_conjuncts.count( node ) );
        const auto &conjuncts = _precondition_conjuncts.at( node );

        return formula::conjunction( conjuncts.cbegin(), conjuncts.cend() );
    }

    formula top_precondition() const
    {
        return build_precondition( invocation_lattice_node::top( _bottom.size() ) );
    }

    void add_precondition_conjunct( const invocation_lattice_node& node, formula pre )
    {
        _precondition_conjuncts[ node ].emplace( std::move( pre ) );
    }

    // Do a BFS search on the complete lattice starting from the bottom. Callback is called with every
    // node that we encounter (it should therefore accept invocation_lattice_node) and should return
    // the precondition that was computed in that node (it is propagated up).
    template < typename Func >
    void traverse( Func callback )
    {
        auto q = std::deque< invocation_lattice_node >();
        auto visited = std::set< invocation_lattice_node >();

        q.push_back( _bottom );
        visited.insert( _bottom );

        while ( !q.empty() )
        {
            const auto current_node = q.front();
            q.pop_front();

            const auto pre = callback( current_node );

            for ( auto &succ : current_node.get_successors() )
            {
                add_precondition_conjunct( succ, pre );

                if ( visited.count( succ ) == 0 )
                {
                    visited.insert( succ );
                    q.emplace_back( std::move( succ ) );
                }
            }
        }
    }
};

}