/*
 * This file is part of a parser for an extension of the PRISM language.
 *
 * This 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.
 *
 * The parser 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 the program this parser part of.
 * If not, see <http://www.gnu.org/licenses/>.
 *
 * Copyright 2007-2010 Bjoern Wachter (Bjoern.Wachter@comlab.ox.ac.uk)
 * Copyright 2009-2010 Ernst Moritz Hahn (emh@cs.uni-sb.de)
 */

#ifndef __EXPRMANAGER_H__
#define __EXPRMANAGER_H__

#include <cvc3/vcl.h>
#include "Util.h"

namespace prismparser {

  class Type;
  class Value;
  class BasicExpr;
  class ExtractExpr;

  extern CVC3::VCL vc;

  /*! \brief Class that manages all expression and caches results from Decision Procedure calls */
  class ExprManager {
  public:

    static void Init();
    static void Done();

    static bool IsTrue(const CVC3::Expr& e) ;

    static bool IsFalse(const CVC3::Expr& e) ;

    static bool DisjointWith(const CVC3::Expr& e1, const CVC3::Expr& e2) ;
    static lbool DisjointWithSyntactic(const CVC3::Expr& e1, const CVC3::Expr& e2);

    static bool EquivalentTo(const CVC3::Expr& e1, const CVC3::Expr& e2) ;

    static bool LvalueCompatible(const CVC3::Expr& e1, const CVC3::Expr& e2) ;
    static void ComputeLvalues(const CVC3::Expr& e, std::set<CVC3::Expr>& result);

    static void getTopLevelConjuncts(const CVC3::Expr& e, std::vector<CVC3::Expr>& result);
    static void getTopLevelConjuncts(const CVC3::Expr& e, std::set<CVC3::Expr>& result);

    static CVC3::Expr Conjunction(const std::vector<CVC3::Expr>&);
    static CVC3::Expr Conjunction(const std::set<CVC3::Expr>&);
    static CVC3::Expr Disjunction(const std::vector<CVC3::Expr>&);

    static void CollectExprs(const CVC3::Expr& e, std::hash_set<CVC3::Expr>& exprs);
    static void CollectExprs(const CVC3::Expr& e, std::set<CVC3::Expr>& exprs);

    static void SplitExprSet(const std::vector<CVC3::Expr> &arg,std::vector< std::vector<CVC3::Expr> > &res);

    /** \brief decompose an expression into conjuncts with disjoint support */
    static void getDisjointSupportDecomposition(const CVC3::Expr& e,
						std::vector<CVC3::Expr>& result);

    static CVC3::Expr getExprCube(const Cube& c, const std::vector<CVC3::Expr>& vec);
    static bool IsInterval(const CVC3::Expr& e, CVC3::Expr& lower, CVC3::Expr& x, CVC3::Expr& upper);

  private:
    static lbool Solve(const CVC3::Expr& e);
    static lbool queryCaches(const CVC3::ExprHashMap<bool>& cache1,
			     const CVC3::ExprHashMap<bool>& cache2,
			     const CVC3::Expr& e);



  };

}


#endif

