ta.hh

Go to the documentation of this file.

/* Copyright 2006 University of Illinois at Urbana-Champaign
 *
 * Ceta 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.
 *
 * This program 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 this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
 */
#ifndef _ta_hh_
#define _ta_hh_

//#include <algorithm>
#include <ostream>
#include <set>
#include <string>
#include <vector>

#include <boost/optional/optional.hpp>
#include <boost/shared_ptr.hpp>
#include <boost/tuple/tuple.hpp>
#include <boost/variant.hpp>

#include <ceta/export.h>

namespace ceta {
  class CETA_DSO_EXPORT kind_t {
  public:
    explicit kind_t(const std::string& name)
      : name_(new std::string(name)) {
    }
  private:
    friend const std::string& name(const kind_t& kind);
    boost::shared_ptr<std::string> name_;
  };
  inline
  const std::string& name(const kind_t& kind) {
    return *(kind.name_);
  }
  inline
  bool operator==(const kind_t& lhs, const kind_t& rhs) {
    return &name(lhs) == &name(rhs);
  }
  inline
  bool operator!=(const kind_t& lhs, const kind_t& rhs) {
    return !(lhs == rhs);
  }
  inline
  bool operator<(const kind_t& lhs, const kind_t& rhs) {
    return &name(lhs) < &name(rhs);
  }
  inline
  std::ostream& operator<<(std::ostream& o, const kind_t& kind) {
    return o << name(kind);
  }

  class CETA_DSO_EXPORT op_t {
  public:
    typedef std::vector<kind_t>::const_iterator input_iterator;
    template<typename InputIterator>
    op_t(const std::string& name, InputIterator inputs_begin,
         InputIterator inputs_end, const kind_t& output)
      : impl_(new impl_t(name,
                         std::vector<kind_t>(inputs_begin, inputs_end),
                         output)) {
    }
  private:
    friend const std::string& name(const op_t& op);
    friend const op_t::input_iterator inputs_begin(const op_t& op);
    friend const op_t::input_iterator inputs_end(const op_t& op);
    friend const kind_t& output(const op_t& op);
    friend bool operator==(const op_t& lhs, const op_t& rhs);
    friend bool operator<( const op_t& lhs, const op_t& rhs);
    typedef boost::tuple<std::string, std::vector<kind_t>, kind_t> impl_t;
    boost::shared_ptr<impl_t> impl_;
  };
  inline
  const std::string& name(const op_t& op) {
    return op.impl_->get<0>();
  }
  inline
  const op_t::input_iterator inputs_begin(const op_t& op) {
    return op.impl_->get<1>().begin();
  }
  inline
  const op_t::input_iterator inputs_end(const op_t& op) {
    return op.impl_->get<1>().end();
  }
  inline
  const kind_t& output(const op_t& op) {
    return op.impl_->get<2>();
  }
  inline
  bool operator==(const op_t& lhs, const op_t& rhs) {
    return lhs.impl_ == rhs.impl_;
  }
  inline
  bool operator<(const op_t& lhs, const op_t& rhs) {
    return lhs.impl_ < rhs.impl_;
  }
  inline
  bool operator!=(const op_t& lhs, const op_t& rhs) {
    return !(lhs == rhs);
  }
  inline
  const kind_t& input(const op_t& op, size_t i) {
    return inputs_begin(op)[i];
  }
  inline
  size_t input_count(const op_t& op) {
    return std::distance(inputs_begin(op), inputs_end(op));
  }
  inline
  bool is_constant(const op_t& op) {
    return inputs_begin(op) == inputs_end(op);
  }
  inline
  bool is_binary(const op_t& op) {
    return (input_count(op) == 2)
        && (input(op, 0) == output(op))
        && (input(op, 1) == output(op));
  }
  inline
  op_t make_constant(const std::string& name, const kind_t& output) {
    const kind_t* end = NULL;
    return op_t(name, end, end, output);
  }
  inline
  op_t make_unary_op(const std::string& name, const kind_t& input1,
                     const kind_t& output) {
    const kind_t inputs[] = { input1, };
    return op_t(name, inputs, inputs + 1, output);
  }
  inline
  op_t make_binary_op(const std::string& name,
                      const kind_t& input1, const kind_t& input2,
                      const kind_t& output) {
    const kind_t inputs[] = { input1, input2 };
    return op_t(name, inputs, inputs + 2, output);
  }
  inline
  std::ostream& operator<<(std::ostream& o, const op_t& op) {
    return o << name(op);
  }

  class term_t;

  void check_constant(const op_t& term) CETA_DSO_EXPORT;
  void check_equal(const kind_t& kind, const kind_t& kind) CETA_DSO_EXPORT;
  void check_well_formed(const op_t& op,
          const std::vector<term_t>& subterms) CETA_DSO_EXPORT;
  class CETA_DSO_EXPORT term_t {
  public:
    typedef std::vector<term_t>::const_iterator subterm_iterator;
    template<typename I>
    term_t(const op_t& op, I subterms_begin, I subterms_end)
      : impl_(new impl_t(op, std::vector<term_t>(subterms_begin,
                                                 subterms_end))) {
      //check_well_formed(op, impl_->get<1>(*impl_));
    }
  private:
    friend const op_t& root(const term_t& term);
    friend term_t::subterm_iterator subterms_begin(const term_t& term);
    friend term_t::subterm_iterator subterms_end(const term_t& term);
    typedef boost::tuple<op_t, std::vector<term_t> > impl_t;
    boost::shared_ptr<impl_t> impl_;
  };
  inline
  const op_t& root(const term_t& term) {
    return term.impl_->get<0>();
  }
  inline
  term_t::subterm_iterator subterms_begin(const term_t& term) {
    return term.impl_->get<1>().begin();
  }
  inline
  term_t::subterm_iterator subterms_end(const term_t& term) {
    return term.impl_->get<1>().end();
  }
  inline
  term_t make_constant(const op_t& op) {
    const term_t* end = NULL;
    return term_t(op, end, end);
  }
  inline
  size_t subterm_count(const term_t& term) {
    return subterms_end(term) - subterms_begin(term);
  }
  inline
  const term_t& subterm(const term_t& term, size_t i) {
    return subterms_begin(term)[i];
  }
  inline
  const kind_t& kind(const term_t& term) {
    return output(root(term));
  }
  inline
  bool is_constant(const term_t& term) {
    return subterms_begin(term) == subterms_end(term);
  }
  std::ostream&
        operator<<(std::ostream& o, const term_t& term) CETA_DSO_EXPORT;

  enum id_type_t {
    id_none,  
    id_left,  
    id_right, 
    id_both   
  };

  class axiom_set_t {
  public:
    axiom_set_t& operator|=(const axiom_set_t& rhs);
  private:
    friend bool is_assoc(const axiom_set_t& axiom);
    friend bool is_comm(const axiom_set_t& axiom);
    friend id_type_t id_type(const axiom_set_t& axiom);
    friend const boost::optional<op_t>& id_symbol(const axiom_set_t& axiom);
    friend const axiom_set_t& none();
    friend const axiom_set_t& assoc();
    friend const axiom_set_t& comm();
    friend const axiom_set_t left_id(const op_t& id);
    friend const axiom_set_t right_id(const op_t& id);
    friend const axiom_set_t id(const op_t& id);
    axiom_set_t(bool is_assoc, bool is_comm, id_type_t id_type = id_none,
                const boost::optional<op_t>& id_symbol
                    = boost::optional<op_t>())
      : is_assoc_(is_assoc),
        is_comm_(is_comm),
        id_type_(id_type),
        id_symbol_(id_symbol) {
    }
    bool is_assoc_;
    bool is_comm_;
    id_type_t id_type_;
    boost::optional<op_t> id_symbol_;
  };
  inline
  bool is_assoc(const axiom_set_t& axiom) {
    return axiom.is_assoc_;
  }
  inline
  bool is_comm(const axiom_set_t& axiom) {
    return axiom.is_comm_;
  }
  inline
  id_type_t id_type(const axiom_set_t& axiom) {
    return axiom.id_type_;
  }
  inline
  const boost::optional<op_t>& id_symbol(const axiom_set_t& axiom) {
    return axiom.id_symbol_;
  }
  inline
  const axiom_set_t& none() {
    static axiom_set_t r(false, false);
    return r;
  }
  inline
  const axiom_set_t& assoc() {
    static axiom_set_t r(true, false);
    return r;
  }
  inline
  const axiom_set_t& comm() {
    static axiom_set_t r(false, true);
    return r;
  }
  inline
  const axiom_set_t left_id(const op_t& id) {
    check_constant(id);
    return axiom_set_t(false, false, id_left, id);
  }
  inline
  const axiom_set_t right_id(const op_t& id) {
    check_constant(id);
    return axiom_set_t(false, false, id_right, id);
  }
  inline
  const axiom_set_t id(const op_t& id) {
    check_constant(id);
    return axiom_set_t(false, false, id_both, id);
  }
  inline
  bool operator==(const axiom_set_t& x, const axiom_set_t& y) {
    return ( is_assoc(x) == is_assoc(y))
        && (  is_comm(x) == is_comm(y))
        && (  id_type(x) == id_type(y))
        && (id_symbol(x) == id_symbol(y));
  }
  inline
  bool operator!=(const axiom_set_t& x, const axiom_set_t& y) {
    return !(x == y);
  }
  inline
  const axiom_set_t operator|(const axiom_set_t& x, const axiom_set_t& y) {
    return axiom_set_t(x) |= y;
  }
  std::ostream&
  operator<<(std::ostream& o, const axiom_set_t& axioms) CETA_DSO_EXPORT;

  class theory_impl;

  class theory_t {
    friend class axiom_set_proxy_t;
  public:
    typedef std::set<kind_t>::const_iterator kind_iterator;
    typedef std::set<op_t>::const_iterator op_iterator;

    theory_t();
  private:
    friend const kind_iterator add_kind(theory_t& theory,
                                        const kind_t& kind);
    friend const op_iterator add_op(theory_t& theory, const op_t& op);
    friend void  set_axioms(theory_t& theory, const op_t& bin_op,
                            const axiom_set_t& axioms);
    friend const axiom_set_t& axioms(const theory_t& theory, const op_t& op);
    friend theory_t::kind_iterator kinds_begin(const theory_t& theory);
    friend theory_t::kind_iterator kinds_end(const theory_t& theory);
    friend bool member(const theory_t& theory, const kind_t& kind);
    friend bool member(const theory_t& theory, const op_t& op);
    friend theory_t::op_iterator ops_begin(const theory_t& theory);
    friend theory_t::op_iterator ops_end(const theory_t& theory);
    friend bool operator==(const theory_t& x, const theory_t& y);
    friend theory_t::op_iterator id_contexts_begin(
            const theory_t& theory, const op_t& id_symbol);
    friend theory_t::op_iterator id_contexts_end(
            const theory_t& theory, const op_t& id_symbol);
    friend bool is_identity(const theory_t& theory, const op_t& id_symbol);
    boost::shared_ptr<theory_impl> impl_;
  };
  const axiom_set_t&
    axioms(const theory_t& theory, const op_t& op) CETA_DSO_EXPORT;
  theory_t::kind_iterator kinds_begin(const theory_t& theory) CETA_DSO_EXPORT;
  theory_t::kind_iterator kinds_end(const theory_t& theory) CETA_DSO_EXPORT;
  bool member(const theory_t& theory, const kind_t& kind) CETA_DSO_EXPORT;
  bool member(const theory_t& theory, const op_t& op) CETA_DSO_EXPORT;
  theory_t::op_iterator ops_begin(const theory_t& theory) CETA_DSO_EXPORT;
  theory_t::op_iterator ops_end(const theory_t& theory) CETA_DSO_EXPORT;
  theory_t::op_iterator id_contexts_begin(
          const theory_t& theory, const op_t& id_symbol) CETA_DSO_EXPORT;
  theory_t::op_iterator id_contexts_end(
          const theory_t& theory, const op_t& id_symbol) CETA_DSO_EXPORT;

  const theory_t::kind_iterator add_kind(theory_t& theory,
                                         const kind_t& kind);
  const theory_t::op_iterator add_op(theory_t& theory, const op_t& op);
  void set_axioms(theory_t& theory, const op_t& bin_op,
                  const axiom_set_t& axioms) CETA_DSO_EXPORT;

  bool operator==(const theory_t& x, const theory_t& y) CETA_DSO_EXPORT;
  inline
  bool operator!=(const theory_t& lhs, const theory_t& rhs) {
    return !(lhs == rhs);
  }
  std::ostream&
  operator<<(std::ostream& o, const theory_t& theory) CETA_DSO_EXPORT;

  class CETA_DSO_EXPORT state_t {
  public:
    state_t(const kind_t& kind, const std::string& name)
      : impl_(new impl_t(kind, name)) {
    }
  private:
    friend const kind_t& kind(const state_t& state);
    friend const std::string& name(const state_t& state);
    friend bool operator==(const state_t& lhs, const state_t& rhs);
    friend bool operator<(const state_t& lhs, const state_t& rhs);
    typedef boost::tuple<kind_t, std::string> impl_t;
    boost::shared_ptr<impl_t> impl_;
  };
  inline
  const kind_t& kind(const state_t& state) {
    return state.impl_->get<0>();
  }
  inline
  const std::string& name(const state_t& state) {
    return state.impl_->get<1>();
  }
  inline
  bool operator==(const state_t& lhs, const state_t& rhs) {
    return lhs.impl_ == rhs.impl_;
  }
  inline
  bool operator<(const state_t& lhs, const state_t& rhs) {
    return lhs.impl_ < rhs.impl_;
  }
  inline
  bool operator!=(const state_t& lhs, const state_t& rhs) {
    return !(lhs == rhs);
  }
  inline
  std::ostream& operator<<(std::ostream& o, const state_t& state) {
    return o << name(state);
  }
  inline
  std::ostream& operator<<(std::ostream& o, const std::set<state_t>& s) {
    o << "{";
    typedef std::set<state_t>::const_iterator set_iter;
    set_iter i = s.begin();
    set_iter end = s.end();
    if (i != end) {
      o << *(i++);
      while (i != end)
        o << ", " << *(i++);
    }
    return o << "}";
  }

  void check_kinds(const kind_t& kind,
                   const std::set<state_t>& states) CETA_DSO_EXPORT;

  struct not_predicate_t;
  struct and_predicate_t;
  struct or_predicate_t;
  class CETA_DSO_EXPORT state_predicate_t {
  public:
    state_predicate_t(const kind_t& kind, bool value);
    state_predicate_t(const state_t& state);
  private:
    state_predicate_t(const not_predicate_t& p);
    state_predicate_t(const and_predicate_t& p);
    state_predicate_t(const or_predicate_t& p);
    typedef boost::variant<bool, state_t, not_predicate_t, and_predicate_t,
            or_predicate_t> variant_t;
    typedef boost::tuple<kind_t, variant_t> impl_t;

    friend
    const state_predicate_t operator!(const state_predicate_t& arg);
    friend
    const state_predicate_t operator&(const state_predicate_t& lhs,
                                      const state_predicate_t& rhs);
    friend
    const state_predicate_t operator|(const state_predicate_t& lhs,
                                      const state_predicate_t& rhs);

    friend const kind_t& kind(const state_predicate_t& pred);
    template<typename Visitor>

    friend
    typename Visitor::result_type
      apply_visitor(const Visitor& visitor, const state_predicate_t& pred);

    friend
    bool operator==(const state_predicate_t& lhs,
                    const state_predicate_t& rhs);

    boost::shared_ptr<impl_t> impl_;
  };
  struct not_predicate_t {
    not_predicate_t(const state_predicate_t& new_arg)
      : arg(new_arg) {
    }
    state_predicate_t arg;
  };
  struct and_predicate_t {
    and_predicate_t(const state_predicate_t& new_lhs,
                    const state_predicate_t& new_rhs)
      : lhs(new_lhs), rhs(new_rhs) {
      check_equal(kind(lhs), kind(rhs));
    }
    state_predicate_t lhs;
    state_predicate_t rhs;
  };
  struct or_predicate_t {
    or_predicate_t(const state_predicate_t& new_lhs,
                   const state_predicate_t& new_rhs)
      : lhs(new_lhs), rhs(new_rhs) {
      check_equal(kind(lhs), kind(rhs));
    }
    state_predicate_t lhs;
    state_predicate_t rhs;
  };
  inline
  state_predicate_t::state_predicate_t(const kind_t& kind, bool value)
    : impl_(new impl_t(kind, value)) {
  }
  inline
  state_predicate_t::state_predicate_t(const state_t& state)
    : impl_(new impl_t(kind(state), state)) {
  }
  inline
  state_predicate_t::state_predicate_t(const not_predicate_t& p)
    : impl_(new impl_t(kind(p.arg), p)) {
  }
  inline
  state_predicate_t::state_predicate_t(const and_predicate_t& p)
    : impl_(new impl_t(kind(p.lhs), p)) {
  }
  inline
  state_predicate_t::state_predicate_t(const or_predicate_t& p)
    : impl_(new impl_t(kind(p.lhs), p)) {
  }
  inline
  const kind_t& kind(const state_predicate_t& pred) {
    return pred.impl_->get<0>();
  }
  template<typename Visitor>
  typename Visitor::result_type
    apply_visitor(const Visitor& visitor, const state_predicate_t& pred) {
    return boost::apply_visitor(visitor, pred.impl_->get<1>());
  }
  inline
  const state_predicate_t operator!(const state_predicate_t& arg) {
    return state_predicate_t(not_predicate_t(arg));
  }
  inline
  const state_predicate_t operator&(const state_predicate_t& lhs,
                                    const state_predicate_t& rhs) {
    return state_predicate_t(and_predicate_t(lhs, rhs));
  }
  inline
  const state_predicate_t operator|(const state_predicate_t& lhs,
                                    const state_predicate_t& rhs) {
    return state_predicate_t(or_predicate_t(lhs, rhs));
  }
  inline
  state_predicate_t& operator&=(state_predicate_t& lhs,
                          const state_predicate_t& rhs) {
    return lhs = lhs & rhs;
  }
  inline
  state_predicate_t& operator|=(state_predicate_t& lhs,
                          const state_predicate_t& rhs) {
    return lhs = lhs | rhs;
  }
  inline
  bool operator==(const state_predicate_t& lhs,
                  const state_predicate_t& rhs) {
    return lhs.impl_ == rhs.impl_;
  }
  inline
  bool operator!=(const state_predicate_t& lhs,
                  const state_predicate_t& rhs) {
    return !(lhs == rhs);
  }
  bool models(const state_predicate_t& pred,
              const std::set<state_t>& model) CETA_DSO_EXPORT;
  std::ostream&
  operator<<(std::ostream& o, const state_predicate_t& p) CETA_DSO_EXPORT;

  class CETA_DSO_EXPORT erule_t {
  public:
    erule_t(const state_t& lhs, const state_t& rhs)
      : lhs_(lhs),
        rhs_(rhs) {
      check_equal(kind(lhs), kind(rhs));
    }
  private:
    friend const state_t& lhs(const erule_t& erule);
    friend const state_t& rhs(const erule_t& erule);
    state_t lhs_;
    state_t rhs_;
  };
  inline
  const state_t& lhs(const erule_t& erule) {
    return erule.lhs_;
  }
  inline
  const state_t& rhs(const erule_t& erule) {
    return erule.rhs_;
  }
  inline
  bool operator==(const erule_t& x, const erule_t& y) {
    return (lhs(x) == lhs(y)) && (rhs(x) == rhs(y));
  }
  inline
  bool operator!=(const erule_t& lhs, const erule_t& rhs) {
    return !(lhs == rhs);
  }
  inline
  bool operator<(const erule_t& x, const erule_t& y) {
    return (lhs(x) <  lhs(y))
        || (lhs(x) == lhs(y)) && (rhs(x) < rhs(y));
  }

  void check_well_formed(const op_t& op,
                         const std::vector<state_t>& lhs_states,
                         const state_t& rhs) CETA_DSO_EXPORT;

  class CETA_DSO_EXPORT rule_t {
  public:
    typedef std::vector<state_t>::const_iterator lhs_state_iterator;
    template <typename InputIterator>
    rule_t(const op_t& op, InputIterator lhs_states_begin,
           InputIterator lhs_states_end, const state_t& rhs)
      : op_(op),
        lhs_states_(lhs_states_begin, lhs_states_end),
        rhs_(rhs) {
      //check_well_formed(op, lhs_states_, rhs);
    }
  private:
    friend const op_t& op(const rule_t& rule);
    friend const lhs_state_iterator lhs_states_begin(const rule_t& rule);
    friend const lhs_state_iterator lhs_states_end(const rule_t& rule);
    friend const state_t& rhs(const rule_t& rule);
    friend bool operator==(const rule_t& lhs, const rule_t& rhs);
    friend bool operator<(const rule_t& lhs, const rule_t& rhs);
    op_t op_;
    std::vector<state_t> lhs_states_;
    state_t rhs_;
  };
  inline
  const op_t& op(const rule_t& rule)  {
    return rule.op_;
  }
  inline
  const rule_t::lhs_state_iterator lhs_states_begin(const rule_t& rule) {
    return rule.lhs_states_.begin();
  }
  inline
  const rule_t::lhs_state_iterator lhs_states_end(const rule_t& rule) {
    return rule.lhs_states_.end();
  }
  inline
  const state_t& rhs(const rule_t& rule) {
    return rule.rhs_;
  }
  inline
  bool operator==(const rule_t& x, const rule_t& y) {
    return (op(x) == op(x))
        && (x.lhs_states_ == y.lhs_states_)
        && (rhs(x) == rhs(y));
  }
  inline
  bool operator!=(const rule_t& lhs, const rule_t& rhs) {
    return !(lhs == rhs);
  }
  inline
  bool operator<(const rule_t& x, const rule_t& y) {
    return (op(x)  < op(y))
        || (op(x) == op(y)) && (rhs(x)  < rhs(y))
        || (op(x) == op(y)) && (rhs(x) == rhs(y))
                            && (x.lhs_states_ < y.lhs_states_);
  }
  inline
  const state_t& lhs_state(const rule_t& rule, size_t i) {
    return lhs_states_begin(rule)[i];
  }
  inline
  size_t lhs_state_count(const rule_t& rule) {
    return std::distance(lhs_states_begin(rule), lhs_states_end(rule));
  }
  inline
  rule_t make_constant_rule(const op_t& lhs_op, const state_t& rhs) {
    const state_t* lhs_states = NULL;
    return rule_t(lhs_op, lhs_states, lhs_states, rhs);
  }
  inline
  rule_t make_unary_rule(const op_t& lhs_op, const state_t& lhs,
                         const state_t& rhs) {
    return rule_t(lhs_op, &lhs, &lhs + 1, rhs);
  }
  inline
  rule_t make_binary_rule(const op_t& lhs_op, const state_t& lhs1,
                          const state_t& lhs2, const state_t& rhs) {
    const state_t lhs_states[] = { lhs1, lhs2 };
    return rule_t(lhs_op, lhs_states, lhs_states + 2, rhs);
  }

  class ta_impl;

  class CETA_DSO_EXPORT ta_t {
  public:
    typedef std::set<state_t>::const_iterator state_iterator;
    typedef std::vector<erule_t>::const_iterator erule_iterator;
    typedef std::vector<rule_t>::const_iterator rule_iterator;
    ta_t(const theory_t& theory);
  private:
    friend const theory_t& theory(const ta_t& ta);
    friend bool member(const ta_t& theory, const state_t& state);
    friend const state_iterator states_begin(const ta_t& ta);
    friend const state_iterator states_end(const ta_t& ta);
    friend const state_iterator add_state(ta_t& ta, const state_t& state);
    friend const state_predicate_t&
            predicate(const ta_t& ta, const kind_t& kind);
    friend void set_predicate(ta_t& ta, const state_predicate_t& pred);
    friend const erule_iterator erules_begin(const ta_t& ta);
    friend const erule_iterator erules_end(const ta_t& ta);
    friend void add_erule(ta_t& ta, const erule_t& erule);
    friend const rule_iterator rules_begin(const ta_t& ta);
    friend const rule_iterator rules_end(const ta_t& ta);
    friend void add_rule(ta_t& ta, const rule_t& rule);
    boost::shared_ptr<ta_impl> impl_;
  };
  const theory_t& theory(const ta_t& ta) CETA_DSO_EXPORT;
  bool member(const ta_t& ta, const state_t& state) CETA_DSO_EXPORT;
  const ta_t::state_iterator states_begin(const ta_t& ta) CETA_DSO_EXPORT;
  const ta_t::state_iterator states_end(const ta_t& ta) CETA_DSO_EXPORT;
  const ta_t::state_iterator
    add_state(ta_t& ta, const state_t& state) CETA_DSO_EXPORT;
  const state_predicate_t&
    predicate(const ta_t& ta, const kind_t& kind) CETA_DSO_EXPORT;
  void set_predicate(ta_t& ta,
                     const state_predicate_t& pred) CETA_DSO_EXPORT;
  const ta_t::erule_iterator erules_begin(const ta_t& ta) CETA_DSO_EXPORT;
  const ta_t::erule_iterator erules_end(const ta_t& ta) CETA_DSO_EXPORT;
  void add_erule(ta_t& ta, const erule_t& erule) CETA_DSO_EXPORT;
  const ta_t::rule_iterator rules_begin(const ta_t& ta) CETA_DSO_EXPORT;
  const ta_t::rule_iterator rules_end(const ta_t& ta) CETA_DSO_EXPORT;
  void add_rule(ta_t& ta, const rule_t& rule) CETA_DSO_EXPORT;
  std::ostream& operator<<(std::ostream& o, const ta_t& ta) CETA_DSO_EXPORT;
  const ta_t operator!(const ta_t& ta) CETA_DSO_EXPORT;
  ta_t& operator&=(ta_t& lhs, const ta_t& rhs) CETA_DSO_EXPORT;
  ta_t& operator|=(ta_t& lhs, const ta_t& rhs) CETA_DSO_EXPORT;
  inline
  const ta_t operator&(const ta_t& lhs, const ta_t& rhs) {
    ta_t result = lhs;
    result &= rhs;
    return result;
  }
  inline
  const ta_t operator|(const ta_t& lhs, const ta_t& rhs) {
    ta_t result = lhs;
    result |= rhs;
    return result;
  }
}
#endif

---