/***********************************************************************************[SolverTypes.h]

Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson

Copyright (c) 2007-2010, Niklas Sorensson

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and

associated documentation files (the "Software"), to deal in the Software without restriction,

including without limitation the rights to use, copy, modify, merge, publish, distribute,

sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is

furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or

substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT

NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND

NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,

DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT

OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

**************************************************************************************************/

#ifndef BVMinisat_SolverTypes_h

#define BVMinisat_SolverTypes_h

#include "base/check.h"

#include "prop/bvminisat/mtl/Alg.h"

#include "prop/bvminisat/mtl/Alloc.h"

#include "prop/bvminisat/mtl/IntTypes.h"

#include "prop/bvminisat/mtl/Map.h"

#include "prop/bvminisat/mtl/Vec.h"

namespace cvc5 {

namespace BVMinisat {

class Solver;

}

template <class Solver>

class TSatProof;

}  // namespace cvc5

namespace cvc5 {

namespace BVMinisat {

//=================================================================================================

// Variables, literals, lifted booleans, clauses:

// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,

// so that they can be used as array indices.

typedef int Var;

#define var_Undef (-1)

struct Lit {

    int     x;

    // Use this as a constructor:

    friend Lit mkLit(Var var, bool sign);

};

// Mapping Literals to and from compact integers suitable for array indexing:

struct LitHashFunction {

  size_t operator () (const Lit& l) const {

    return toInt(l);

  }

};

//const Lit lit_Undef = mkLit(var_Undef, false);  // }- Useful special constants.

//const Lit lit_Error = mkLit(var_Undef, true );  // }

const Lit lit_Undef = { -2 };  // }- Useful special constants.

const Lit lit_Error = { -1 };  // }

//=================================================================================================

// Lifted booleans:

//

// NOTE: this implementation is optimized for the case when comparisons between

// values are mostly

//       between one variable and one constant. Some care had to be taken to

//       make sure that gcc does enough constant propagation to produce sensible

//       code, and this appears to be somewhat fragile unfortunately.

#ifndef l_True

#define l_True  (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.

#endif

#ifndef l_False

#define l_False (lbool((uint8_t)1))

#endif

#ifndef l_Undef

#define l_Undef (lbool((uint8_t)2))

#endif

class lbool {

    uint8_t value;

public:

    lbool()       : value(0) { }

    lbool operator&&(lbool b) const

    {

      uint8_t sel = (this->value << 1) | (b.value << 3);

      uint8_t v = (0xF7F755F4 >> sel) & 3;

      return lbool(v);

    }

    lbool operator || (lbool b) const {

        uint8_t sel = (this->value << 1) | (b.value << 3);

        uint8_t v   = (0xFCFCF400 >> sel) & 3;

        return lbool(v); }

    friend int   toInt  (lbool l);

    friend lbool toLbool(int   v);

};

inline int   toInt  (lbool l) { return l.value; }

inline lbool toLbool(int   v) { return lbool((uint8_t)v);  }

//=================================================================================================

// Clause -- a simple class for representing a clause:

class Clause;

typedef RegionAllocator<uint32_t>::Ref CRef;

class Clause {

    struct {

        unsigned mark      : 2;

        unsigned learnt    : 1;

        unsigned has_extra : 1;

        unsigned reloced   : 1;

        unsigned size      : 27; }                            header;

    union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];

    friend class ClauseAllocator;

    // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).

    template<class V>

            else

        }

public:

    {

    const Lit&   last        ()      const   { return data[header.size-1].lit; }

    // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for

    //       subsumption operations to behave correctly.

    {

    }

    uint32_t abstraction() const

    {

      Assert(header.has_extra);

      return data[header.size].abs;

    }

    Lit          subsumes    (const Clause& other) const;

    void         strengthen  (Lit p);

};

//=================================================================================================

// ClauseAllocator -- a simple class for allocating memory for clauses:

const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;

const CRef CRef_Lazy  = RegionAllocator<uint32_t>::Ref_Undef - 1;

{

 public:

    bool extra_clause_field;

    template<class Lits>

    {

          clauseWord32Size(ps.size(), use_extra));

    }

    // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):

    Ref           ael       (const Clause* t){ return RegionAllocator<uint32_t>::ael((uint32_t*)t); }

    {

    void reloc(CRef& cr, ClauseAllocator& to);

};

//=================================================================================================

// OccLists -- a class for maintaining occurence lists with lazy deletion:

template<class Idx, class Vec, class Deleted>

{

    vec<Vec>  occs;

    vec<char> dirty;

    vec<Idx>  dirties;

    Deleted   deleted;

 public:

    // Vec&  operator[](const Idx& idx){ return occs[toInt(idx)]; }

    void  cleanAll  ();

    void  clean     (const Idx& idx);

        }

};

template<class Idx, class Vec, class Deleted>

{

        // Dirties may contain duplicates so check here if a variable is already cleaned:

template<class Idx, class Vec, class Deleted>

{

    int  i, j;

//=================================================================================================

// CMap -- a class for mapping clauses to values:

template<class T>

class CMap

{

    struct CRefHash {

        uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };

    typedef Map<CRef, T, CRefHash> HashTable;

    HashTable map;

 public:

    // Size-operations:

    void     clear       ()                           { map.clear(); }

    int      size        ()                const      { return map.elems(); }

    // Insert/Remove/Test mapping:

    void     insert      (CRef cr, const T& t){ map.insert(cr, t); }

    void     growTo      (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility

    void     remove      (CRef cr)            { map.remove(cr); }

    bool     has         (CRef cr, T& t)      { return map.peek(cr, t); }

    // Vector interface (the clause 'c' must already exist):

    const T& operator [] (CRef cr) const      { return map[cr]; }

    T&       operator [] (CRef cr)            { return map[cr]; }

    // Iteration (not transparent at all at the moment):

    int  bucket_count() const { return map.bucket_count(); }

    const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }

    // Move contents to other map:

    void moveTo(CMap& other){ map.moveTo(other.map); }

    // TMP debug:

    void debug(){

        printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }

};

/*_________________________________________________________________________________________________

|

|  subsumes : (other : const Clause&)  ->  Lit

|

|  Description:

|       Checks if clause subsumes 'other', and at the same time, if it can be

used to simplify 'other' |       by subsumption resolution.

|

|    Result:

|       lit_Error  - No subsumption or simplification

|       lit_Undef  - Clause subsumes 'other'

|       p          - The literal p can be deleted from 'other'

|________________________________________________________________________________________________@*/

{

    //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)

    //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))

        // search for c[i] or ~c[i]

            }

        // did not find it

    }

}

{

//=================================================================================================

}  // namespace BVMinisat

}  // namespace cvc5

#endif