UFInstance.h

Go to the documentation of this file.

/**
 * @file UFInstance.h
 * @author Florian Corzilius <corzilius@cs.rwth-aachen.de>
 * @since 2014-10-30
 * @version 2014-10-30
 */
 
#pragma once
 
#include <carl-arith/core/Variables.h>
#include "UVariable.h"
#include "UninterpretedFunction.h"
 
#include <iostream>
#include <utility>
#include <vector>
 
namespace carl
{
    class UTerm;
 
    /**
     * Implements an uninterpreted function instance.
     */
    class UFInstance {
        public:
            friend class UFInstanceManager;
 
        private:
            /// A unique id.
            std::size_t mId = 0;
 
            /**
             * Constructs an uninterpreted function instance.
             * @param id
             */
            explicit UFInstance(std::size_t id) noexcept: mId(id) {}
 
        public:
            UFInstance() = default;
            /**
             * @return The unique id of this uninterpreted function instance.
             */
            std::size_t id() const {
                return mId;
            }
 
            /**
             * @return The underlying uninterpreted function of this instance.
             */
            const UninterpretedFunction& uninterpretedFunction() const;
 
            /**
             * @return The arguments of this uninterpreted function instance.
             */
            const std::vector<UTerm>& args() const;
 
            std::size_t complexity() const;
 
            void gatherVariables(carlVariables& vars) const;
            void gatherUFs(std::set<UninterpretedFunction>& ufs) const;
    };
 
    static_assert(std::is_trivially_copyable<UFInstance>::value, "UFInstance should be trivially copyable.");
    static_assert(sizeof(UFInstance) == sizeof(std::size_t), "UFInstance should be as large as its id");
 
    /**
     * @param lhs The left function instance.
     * @param rhs The right function instance.
     * @return true, if lhs == rhs.
     */
    inline bool operator==(const UFInstance& lhs, const UFInstance& rhs) {
        return lhs.id() == rhs.id();
    }
 
    /**
     * @param lhs The left function instance.
     * @param rhs The right function instance.
     * @return true, if lhs < rhs.
     */
    inline bool operator<(const UFInstance& lhs, const UFInstance& rhs) {
        return lhs.id() < rhs.id();
    }
 
    /**
     * Prints the given uninterpreted function instance on the given output stream.
     * @param os The output stream to print on.
     * @param ufun The uninterpreted function instance to print.
     * @return The output stream after printing the given uninterpreted function instance on it.
     */
    std::ostream& operator<<(std::ostream& os, const UFInstance& ufun);
} // end namespace carl
 
namespace std {
    /**
     * Implements std::hash for uninterpreted function instances.
     */
    template<>
    struct hash<carl::UFInstance> {
    public:
        /**
         * @param ufi The uninterpreted function instance to get the hash for.
         * @return The hash of the given uninterpreted function instance.
         */
        std::size_t operator()(const carl::UFInstance& ufi) const {
            return carl::hash_all(ufi.id());
        }
    };
}