/**
 * This file is part of sally.
 * Copyright (C) 2015 SRI International.
 *
 * Sally 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.
 *
 * Sally 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 sally.  If not, see <http://www.gnu.org/licenses/>.
 */

#include "system/transition_system.h"

#include <iostream>

namespace sally {
namespace system {

transition_system::transition_system(const state_type* state_type, state_formula* initial_states, transition_formula* transition_relation)
: d_state_type(state_type)
, d_initial_states(initial_states)
, d_transition_relation(transition_relation)
{
  d_trace_helper = new trace_helper(state_type);
  d_invariant = new state_formula(state_type->tm(), state_type, state_type->tm().mk_boolean_constant(true));
}

void transition_system::to_stream(std::ostream& out) const {
  out << "[" << std::endl;
  out << "type: " << *d_state_type << std::endl;
  out << "I: " << d_initial_states->get_formula() << std::endl;
  out << "T: " << d_transition_relation->get_formula() << std::endl;
  out << "Inv: " << d_invariant->get_formula() << std::endl;
  out << "]";
}

std::ostream& operator << (std::ostream& out, const transition_system& T) {
  T.to_stream(out);
  return out;
}

expr::term_ref transition_system::get_transition_relation() const {
  std::vector<expr::term_ref> transitions;
  transitions.push_back(d_transition_relation->get_formula());
  expr::term_ref transition = d_state_type->tm().mk_or(transitions);
  if (has_state_assumptions()) {
    expr::term_ref A = get_state_assumption();
    expr::term_ref A_next = d_state_type->change_formula_vars(state_type::STATE_CURRENT, state_type::STATE_NEXT, A);
    transition = d_state_type->tm().mk_term(expr::TERM_AND, transition, A, A_next);
  }
  if (has_transition_assumptions()) {
    expr::term_ref T = get_transition_assumption();
    transition = d_state_type->tm().mk_term(expr::TERM_AND, transition, T);
  }
  expr::term_ref Inv = get_invariant();
  expr::term_ref Inv_next = d_state_type->change_formula_vars(state_type::STATE_CURRENT, state_type::STATE_NEXT, Inv);
  transition = d_state_type->tm().mk_term(expr::TERM_AND, transition, Inv, Inv_next);
  return transition;
}

expr::term_ref transition_system::get_initial_states() const {
  expr::term_ref I = d_initial_states->get_formula();
  if (has_state_assumptions()) {
    I = d_state_type->tm().mk_term(expr::TERM_AND, I, get_state_assumption());
  }
  expr::term_ref Inv = get_invariant();
  I = d_state_type->tm().mk_term(expr::TERM_AND, I, Inv);
  return I;
}

void transition_system::add_assumption(state_formula* assumption) {
  d_assumptions_state.push_back(assumption);
}

void transition_system::add_assumption(transition_formula* assumption) {
  d_assumptions_transition.push_back(assumption);
}

void transition_system::add_invariant(state_formula* invariant) {
  expr::term_ref Inv = d_invariant->get_formula();
  expr::term_ref Inv_new = invariant->get_formula();
  expr::term_ref combined = d_state_type->tm().mk_term(expr::TERM_AND, Inv, Inv_new);
  state_formula* new_invariant = new system::state_formula(d_state_type->tm(), d_state_type, combined);
  delete d_invariant; 
  d_invariant = new_invariant;
}

expr::term_ref transition_system::get_invariant() const {
  return d_invariant->get_formula();
}

expr::term_ref transition_system::get_state_assumption() const {
  std::vector<expr::term_ref> assumption_terms;
  for (size_t i = 0; i < d_assumptions_state.size(); ++ i) {
    assumption_terms.push_back(d_assumptions_state[i]->get_formula());
  }
  return d_state_type->tm().mk_and(assumption_terms);
}

expr::term_ref transition_system::get_transition_assumption() const {
  std::vector<expr::term_ref> assumption_terms;
  for (size_t i = 0; i < d_assumptions_transition.size(); ++ i) {
    assumption_terms.push_back(d_assumptions_transition[i]->get_formula());
  }
  return d_state_type->tm().mk_and(assumption_terms);
}

trace_helper* transition_system::get_trace_helper() const {
  return d_trace_helper;
}

transition_system::~transition_system() {
  for (size_t i = 0; i < d_assumptions_state.size(); ++ i) {
    delete d_assumptions_state[i];
  }
  delete d_initial_states;
  delete d_transition_relation;
  delete d_invariant;
  delete d_trace_helper;
}

}
}
