/home/mine/apron/apronxx/apxx_lincons0.hh

Go to the documentation of this file.

/* -*- C++ -*-
 * apxx_lincons0.hh
 *
 * APRON Library / C++ class wrappers
 *
 * Copyright (C) Antoine Mine' 2007
 *
 */
/* This file is part of the APRON Library, released under LGPL license
   with an exception allowing the redistribution of statically linked
   executables.
  
   Please read the COPYING file packaged in the distribution.
*/
 
#ifndef __APXX_LINCONS0_HH
#define __APXX_LINCONS0_HH
 
#include <vector>
#include "ap_lincons0.h"
#include "apxx_linexpr0.hh"
 
 
namespace apron {
 

struct unsat {};
 
 
 
/* ================================= */
/* lincons0                          */
/* ================================= */
 


 * A lincons0 object represents a linear constraint: expr==0, expr>=0, expr>0, expr!=0, or expr==0 mod c.
 * It stores and manages a linexpr0 (linear expression with scalar or interval coefficients), 
 * a constraint type (==, >=, >, !=, mod), and (for modulo constraint) an auxiliary scalar (c).
 */
class lincons0 : public use_malloc {
 
protected:
  
  ap_lincons0_t l;  


  lincons0(ap_lincons0_t l);
 
  friend class abstract0;
  
public:
 
  
  /* constructors */
  /* ============ */




  lincons0(ap_constyp_t constyp=AP_CONS_SUPEQ);

   * The auxiliary scalar is not created (has_modulo returns false).
   * \arg \c constyp can be \c AP_CONS_EQ, \c AP_CONS_SUPEQ, \c AP_CONS_SUP, or \c AP_CONS_DISEQ (but not \c AP_CONS_EQMOD).
   */
  lincons0(ap_constyp_t constyp, const linexpr0& lin);

  lincons0(ap_constyp_t constyp, const linexpr0& lin, const scalar& modulo);

  lincons0(const lincons0& x);

  lincons0(const lincons0& x, const dimchange& d);


  lincons0(const lincons0& x, const dimperm& d);

  lincons0(unsat x);

 
 
  /* destructor */
  /* ========== */

  /** @name Destructor */

  ~lincons0();

    
 
  /* assignment */
  /* ========== */


  //@{

  lincons0& operator= (const lincons0& x);


  lincons0& operator= (unsat x);

   */
  void set_modulo(const scalar& c);  


  void set_linexpr(const linexpr0& c);

 
 
  /* dimension operations */
  /* ==================== */


  /*! \brief Resizes the underlying linear expression.
   *
   * \throw std::invalid_argument if no valid linear expression has been defined.
   */
  void resize(size_t size);


  void add_dimensions(const dimchange& d);


  void permute_dimensions(const dimperm& d);

 
 
  /* access */
  /* ====== */

 
  /* size */

  size_t size() const;
 
 
  /* get */
 

   * \return either \c AP_CONS_EQ, \c AP_CONS_SUPEQ, \c AP_CONS_SUP, \c AP_CONS_EQMOD, or \c AP_CONS_DISEQ.
   */
  ap_constyp_t& get_constyp();
  

   * \return either \c AP_CONS_EQ, \c AP_CONS_SUPEQ, \c AP_CONS_SUP, \c AP_CONS_EQMOD, or \c AP_CONS_DISEQ.
   */
  const ap_constyp_t& get_constyp() const;

  bool has_modulo() const;


   * \note The only way the linear expression may be invalid is when accessing fields of uninitialised 
   * (or enlarged) lincons0_array.
   */
  bool has_linexpr() const;

   * \throw std::invalid_argument if no valid auxiliary scalar has been defined.
   */
  scalar& get_modulo();
 
  const scalar& get_modulo() const;


   */
  linexpr0& get_linexpr();
 

  const linexpr0& get_linexpr() const;

  /*! \brief Returns a (modifiable) reference to the constant coefficient.
   *
   * \throw std::invalid_argument if no valid linear expression has been defined.
   */
  coeff& get_cst();

  /*! \brief Returns a reference to the constant coefficient.
   *
   * \throw std::invalid_argument if no valid linear expression has been defined.
   */
  const coeff& get_cst() const;

  /*! \brief Returns a (modifiable) reference to the coefficient corresponding to the given dimension.
   *
   * \throw std::out_of_range if the expression is dense and the dimension exceeds the size
   * of the expression; if the expression is sparse, it will be extended and no exception is thrown
   * \throw std::invalid_argument if no valid linear expression has been defined.
   */
  coeff& operator[](ap_dim_t dim);
  
   * of the expression; if the expression is sparse, it will be extended and no exception is thrown
   * \throw std::invalid_argument if no valid linear expression has been defined.
   */
  const coeff& operator[](ap_dim_t dim) const;

  //@}
 
 
  /* print */
  /* ===== */


   * auxiliary scalar is missing (for modulo).
   */
  friend std::ostream& operator<< (std::ostream& os, const lincons0& s);


  void print(char** name_of_dim=NULL, FILE* stream=stdout) const;

 
 
  /* tests */
  /* ===== */



   */
 
  bool is_unsat() const;
  

   */
  bool is_linear() const;


   * \throw std::invalid_argument if no valid linear expression has been defined.
   */
  bool is_quasilinear() const;
 
  // TODO: equal, compare (currently not in ap_lincons0.h) ???

 
  /* TODO: evaluation, linearization, intelligent constructors */
 
 
  /* C-level compatibility */
  /* ===================== */



  const ap_lincons0_t* get_ap_lincons0_t() const;

  ap_lincons0_t* get_ap_lincons0_t();

};
 
 
 
/* ================================= */
/* lincons0_array                    */
/* ================================= */
 

class lincons0_array : public use_malloc {
 
protected:
 
  ap_lincons0_array_t a;  

  lincons0_array(ap_lincons0_array_t& a) : a(a) {}
 
  friend class lincons1_array;
  friend class abstract0;
 
public:
  
  /* constructors */
  /* ============ */



   *
   * has_modulo and has_linexpr will return false on all elements of the array.
   */
  lincons0_array(size_t size);

  //! (Deep) copy.
  lincons0_array(const lincons0_array& x);

  lincons0_array(const lincons0_array& x, const dimchange& d);

  lincons0_array(const lincons0_array& x, const dimperm& d);

  //! Creates a lincons0_array from an array of constraints of the given size (copied).
  lincons0_array(size_t size, const lincons0 x[]);

  lincons0_array(const std::vector<lincons0>& x);

 
 
  /* destructor */
  /* ========== */


  //! Frees the space used by the array and all its constraints.
  ~lincons0_array();

 
 
  /* assignment */
  /* ========== */


  //@{

  lincons0_array& operator= (const lincons0_array& x);


   *
   * \arg x should contain (at least) size elements.
   */
  lincons0_array& operator= (const lincons0 x[]);


  lincons0_array& operator= (const std::vector<lincons0>& x);

 
 
  /* dimension operations */
  /* ==================== */


  void resize(size_t size);

  void add_dimensions(const dimchange& d);

  //! Applies permute_dimensions to all constraints in the array.
  void permute_dimensions(const dimperm& d);

 
 
  /* access */
  /* ====== */

  /** @name Accesses */

  size_t size() const;

  lincons0* contents();

  //! Returns a pointer to the start of the internal array holding the constraints. 
  const lincons0* contents() const;
  
  lincons0& operator[](size_t i);

  const lincons0& operator[](size_t i) const;


  lincons0& get(size_t i);

  /*! \brief Returns a reference to an element (bound-checked).
   *
   * \throw std::out_of_range if the index is invalid.
   */
  const lincons0& get(size_t i) const;

 
 
  /* conversion */
  /* ========== */
  

  operator std::vector<lincons0>() const;

 
 
  /* print */
  /* ===== */


  friend std::ostream& operator<< (std::ostream& os, const lincons0_array& s);

  void print(char** name_of_dim = NULL, FILE* stream=stdout) const;

 
 
  /* tests */
  /* ===== */


  bool is_linear() const;

  bool is_quasilinear() const;

 
 
  /* C-level compatibility */
  /* ===================== */


  const ap_lincons0_array_t* get_ap_lincons0_array_t() const;

  ap_lincons0_array_t* get_ap_lincons0_array_t();

 
};
 
#include "apxx_lincons0_inline.hh"
 
}
 
#endif /* __APXX_LINCONS0_HH */