comparison.h

Go to the documentation of this file.

// This file is part of MARTY.
// 
// MARTY 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 3 of the License, or
// (at your option) any later version.
// 
// MARTY 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 MARTY. If not, see <https://www.gnu.org/licenses/>.

#ifndef COMPARISON_H_INCLUDED
#define COMPARISON_H_INCLUDED

#include "abstract.h"
#include "literal.h"
#include "numerical.h"

namespace csl {

class Arbitrary: public AbstractLiteral{

    public:

    /* \brief Constructor.
     * \param n Index of the Arbitrary object, will determine its identity
     * in comparisons.
     * \param t_type Specific type that can be set. If given, the Arbitrary will
     * be compared to only that type of expressions.
     */
    Arbitrary(int n, csl::Type t_type=csl::Type::NoType);

    Arbitrary(const Arbitrary& other) = default;

    ~Arbitrary(){};

    std::string const &getName() const override;

    bool isArbitrary() const override;

    csl::PrimaryType getPrimaryType() const override;

    csl::Type getType() const override;

    void print(int mode=0,
               std::ostream& out=std::cout,
               bool lib = false) const override;

    std::string printLaTeX(int mode=0) const override;

    std::optional<Expr> evaluate(
            csl::eval::mode user_mode = csl::eval::base
            ) const override;

    unique_Expr copy_unique() const override;

    long long int getNum() const override;

    bool operator==(Expr_info expr) const override;

    bool operator<(const Abstract* expr) const override;


    private:

    int number;

    std::string name;

    csl::Type type;
};

class Comparator{

    friend class Arbitrary;
    // Member functions

    public:

    static Expr dummy(int n, csl::Type type=csl::Type::NoType);

    static bool dummyComparison(Expr_info expr, Expr_info dummyExpr);

    static bool dummyComparison(Expr const& expr, Expr const& dummyExpr);

    static bool dummyVecIntComparison(Expr_info A,
                                      Expr_info B);

    static bool getFreeIndexComparisonActive() {
        return freeIndexComparisonActive;
    }

    static void setFreeIndexComparisonActive(bool t_activ);

    static std::string dummyName();

    static bool freeIndexComparison(const Abstract* A, Expr_info B);

    static bool compare(const Index& A, const Index& B);

    static void clear();

    static bool getDummyComparisonActive() {
        return dummyComparisonActive;
    }

    static bool getDummyVecIntComparisonActive() {
        return dummyVecIntComparisonActive;
    }

    static void setDummyComparisonActive(bool state);

    static void setDummyVecIntComparisonActive(bool state);

    private:

    static bool compare(Expr_info expr, Expr_info dummy);
    
    // Static Attributes

    public:

    static bool freeIndexComparisonActive;

    static std::map<Index,Index> indexCorrespondance;

    static bool dummyVecIntComparisonActive;

    private:

    static bool dummyComparisonActive;

    static std::map<int,Expr> arbitrary;

    static std::map<int,Expr> correspondance;
};

} // End of namespace csl

#endif