literal.h

Go to the documentation of this file.

// 
// Copyright (c) 2006-2007, Benjamin Kaufmann
// 
// This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 
// 
// Clasp is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
// 
// Clasp is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
// 
// You should have received a copy of the GNU General Public License
// along with Clasp; if not, write to the Free Software
// Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
//
#ifndef CLASP_LITERAL_H_INCLUDED
#define CLASP_LITERAL_H_INCLUDED

#ifdef _MSC_VER
#pragma once
#pragma warning (disable : 4996)
#endif
#include <clasp/util/platform.h>
#include <clasp/pod_vector.h>
#include <algorithm>  // std::swap
#include <limits>
namespace Clasp {

typedef uint32 Var;

const Var varMax = (Var(1) << 30);

const Var sentVar = 0;

const uint32 idMax = UINT32_MAX;

struct Var_t {
        enum Type { atom_var = 1, body_var = 2, atom_body_var = atom_var | body_var};
        static bool isBody(Type t) {
                return (static_cast<uint32>(t) & static_cast<uint32>(body_var)) != 0;
        }
        static bool isAtom(Type t) { 
                return (static_cast<uint32>(t) & static_cast<uint32>(atom_var)) != 0; 
        }
};
typedef Var_t::Type VarType;

typedef int32 weight_t;
typedef int64 wsum_t;


class Literal {
public:
        Literal() : rep_(0) { }
        

        Literal(Var var, bool sign) : rep_( (var<<2) + (uint32(sign)<<1) ) {
                assert( var < varMax );
        }


        uint32 index() const { return rep_ >> 1; }
        

        static Literal fromIndex(uint32 idx) {
                assert( idx < (uint32(1)<<31) );
                return Literal(idx<<1);
        }

        static Literal fromRep(uint32 rep) { return Literal(rep); }
        
        uint32& asUint()        { return rep_; }
        uint32  asUint() const  { return rep_; }

        Var var() const { return rep_ >> 2; }
        

        bool sign() const { return test_bit(rep_, 1); }

        void swap(Literal& other) { std::swap(rep_, other.rep_); }
        
        void watch() { store_set_bit(rep_, 0); }
        
        void clearWatch() { store_clear_bit(rep_, 0); }
        
        bool watched() const { return test_bit(rep_, 0); }


        inline Literal operator~() const {
                return Literal( (rep_ ^ 2) & ~static_cast<uint32>(1u) );
        }


        inline bool operator==(const Literal& rhs) const {
                return index() == rhs.index();
        }
private:
        Literal(uint32 rep) : rep_(rep) {}
        uint32 rep_;
};
inline Literal operator^(Literal lhs, bool sign) { return Literal::fromIndex( lhs.index() ^ uint32(sign) ); }
inline Literal operator^(bool sign, Literal rhs) { return rhs ^ sign; }
// Common interface

inline Literal negLit(Var v) { return Literal(v, true);}
inline Literal posLit(Var v) { return Literal(v, false);}

inline uint32 index(Var v) { return v << 1; }

inline bool isSentinel(Literal p) { return p.var() == sentVar; }

inline bool operator<(const Literal& lhs, const Literal& rhs) {
        return lhs.index() < rhs.index();
}

inline bool operator!=(const Literal& lhs, const Literal& rhs) {
        return ! (lhs == rhs);
}

inline void swap(Literal& l, Literal& r) {
        l.swap(r);
}

typedef PodVector<Var>::type VarVec;          
typedef PodVector<Literal>::type LitVec;      
typedef PodVector<weight_t>::type WeightVec;  
typedef PodVector<wsum_t>::type SumVec;       
typedef std::pair<Literal, weight_t> WeightLiteral;  
typedef PodVector<WeightLiteral>::type WeightLitVec; 

// Truth values
typedef uint8 ValueRep;           
const ValueRep value_true   = 1;  
const ValueRep value_false  = 2;  
const ValueRep value_free   = 0;  
typedef PodVector<ValueRep>::type ValueVec;


inline ValueRep trueValue(const Literal& lit) { return 1 + lit.sign(); }


inline ValueRep falseValue(const Literal& lit) { return 1 + !lit.sign(); }


inline bool valSign(ValueRep v) { return v != value_true; }


class SymbolTable {
private:
        struct String {
                String(const char* n) : str(n) {}
                bool        empty() const { return str == 0 || !*str; }
                const char* c_str() const { return str; }
                char        operator[](uint32 i) const { return str[i]; }
        private: const char* str;
        };
public:
        typedef uint32                           key_type;
        typedef String                           data_type;
        struct                                   symbol_type {
                symbol_type(Literal x = negLit(0), data_type d = 0)
                        : lit(x), name(d) {}
                mutable  Literal lit;
                data_type        name;
        };
        typedef std::pair<key_type, symbol_type> value_type;
        typedef PodVector<value_type>::type      map_type;
        typedef map_type::const_iterator         const_iterator;
        enum MapType { map_direct, map_indirect };

        SymbolTable() : lastSort_(0), lastStart_(0), end_(varMax), type_(map_indirect) { }
        ~SymbolTable() { clear();  }
        void   copyTo(SymbolTable& o) {
                o.clear();
                o.map_.reserve(map_.size());
                for (const_iterator it = map_.begin(), end = map_.end(); it != end; ++it) {
                        o.map_.push_back(value_type(it->first, symbol_type(it->second.lit, dupName(it->second.name.c_str()))));
                }
                o.lastSort_ = lastSort_;
                o.lastStart_= lastStart_;
        }

        MapType type()    const { return type_; }
        uint32  size()    const { return type() == map_indirect ? (uint32)map_.size() : end_; }
        const_iterator begin()    const { return map_.begin(); }
        const_iterator curBegin() const { return map_.begin() + lastStart_; }
        const_iterator end()      const { return map_.begin() + lastSort_;  }
        const symbol_type* find(key_type i) const {
                const_iterator it = std::lower_bound(begin(), end(), i, LessKey());
                return it != end() && it->first == i ? &it->second : 0;
        }
        const_iterator lower_bound(const_iterator start, key_type i) const {
                return std::lower_bound(start, end(), i, LessKey());
        }

        const symbol_type& operator[](key_type id) const {
                const symbol_type* a = find(id); assert(a);
                return *a;
        }
        void   clear()      { 
                for (const_iterator it = map_.begin(), end = map_.end(); it != end; ++it) {
                        freeName(it->second.name.c_str());
                }
                map_.clear(); 
                lastSort_ = 0; 
                lastStart_= 0; 
        }
        void startInit() {
                lastStart_ = map_.size();
                lastSort_  = lastStart_;
        }

        symbol_type& addUnique(key_type id, const char* name) {
                assert((lastSort_ == 0 || map_[lastSort_-1].first < id) && "Symbol table: Invalid id in incremental step!");
                map_.push_back(value_type(id, symbol_type(negLit(0), dupName(name))));
                return map_.back().second;
        }
        /*
         * \param type Type of mapping.
         * \param end  Only for direct mapping: end of mapped range (i.e. [0, end)).
         */
        void endInit(MapType type = map_indirect, Var end = varMax) {
                std::sort(map_.begin()+lastSort_, map_.end(), LessKey());
                assert(unique() && "Symbol table: Duplicate atoms are not allowed\n");
                lastSort_ = map_.size();
                end_      = varMax;
                if ((type_=type) == map_direct) {
                        end_    = end;
                }
        }
private:
        SymbolTable(const SymbolTable&);
        SymbolTable& operator=(const SymbolTable&);
        const char* dupName(const char* n) const {
                if (!n) return 0;
                std::size_t len = std::strlen(n);
                char*       dest= new char[len+1];
                std::strncpy(dest, n, len+1);
                return dest;
        }
        void freeName(const char* n) const { delete [] n; }
        bool unique() const {
                for (const_iterator it = map_.begin() + lastSort_, end = map_.end(), n = it + (it != end); n != end; it = n++) {
                        if (it->first == n->first)  { return false; }
                }
                return true;
        }
        struct LessKey {
                bool operator()(const value_type& lhs, const value_type& rhs) const { return lhs.first < rhs.first; }
                bool operator()(const value_type& lhs, key_type i) const { return lhs.first < i; }
                bool operator()(key_type i, const value_type& rhs) const { return i < rhs.first; }
        };
        map_type            map_;
        map_type::size_type lastSort_;
        map_type::size_type lastStart_;
        uint32              end_;
        MapType             type_;
};

class ClaspError : public std::runtime_error {
public:
        explicit ClaspError(const std::string& msg) 
                : std::runtime_error(msg){}
};

}
#endif