/**
 * 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 "value.h"
#include "expr/term_manager.h"
#include "utils/exception.h"

#include <iostream>
#include <cassert>

namespace sally {
namespace expr {

value::value()
: d_type(VALUE_NONE)
, d_b(false)
{
}

value::value(bool b)
: d_type(VALUE_BOOL)
, d_b(b)
{
}

value::value(const value& v)
: d_type(v.d_type)
, d_b(v.d_b)
, d_bv(v.d_bv)
, d_q(v.d_q)
, d_a(v.d_a)
, d_ev(v.d_ev)
{
}

value::value(const rational& q)
: d_type(VALUE_RATIONAL)
, d_b(false)
, d_q(q)
{
}

value::value(const algebraic_number& a)
: d_type(VALUE_ALGEBRAIC)
, d_b(false)
, d_a(a)
{
}


value::value(const bitvector& bv)
: d_type(VALUE_BITVECTOR)
, d_b(false)
, d_bv(bv)
{
}

value::value(const enum_value& ev)
: d_type(VALUE_ENUM)
, d_b(false)
, d_ev(ev)
{}

value::value(const term_manager& tm, term_ref t)
: d_type(VALUE_NONE)
, d_b(false)
{
  const expr::term& t_term = tm.term_of(t);
  expr::term_op op = t_term.op();
  switch (op) {
  case CONST_BOOL:
    d_b = tm.get_boolean_constant(t_term);
    d_type = VALUE_BOOL;
    break;
  case CONST_BITVECTOR:
    d_bv = tm.get_bitvector_constant(t_term);
    d_type = VALUE_BITVECTOR;
    break;
  case CONST_RATIONAL:
    d_q = tm.get_rational_constant(t_term);
    d_type = VALUE_RATIONAL;
    break;
  case CONST_ENUM:
    d_ev = tm.get_enum_constant(t_term);
    d_type = VALUE_ENUM;
    break;
  default:
    assert(false);
  }
}

value& value::operator = (const value& v) {
  if (this != &v) {
    d_type = v.d_type;
    d_b = v.d_b;
    d_bv = v.d_bv;
    d_q = v.d_q;
    d_a = v.d_a;
    d_ev = v.d_ev;
  }
  return *this;
}

bool value::operator == (const value& v) const {

  if (is_arithmetic() && v.is_arithmetic()) {
    return cmp(v) == 0;
  }

  if (d_type != v.d_type) {
    return false;
  }

  switch (d_type) {
  case VALUE_NONE:
    return true;
  case VALUE_BOOL:
    return d_b == v.d_b;
  case VALUE_BITVECTOR:
    return d_bv == v.d_bv;
  case VALUE_ENUM:
    return d_ev == v.d_ev;
  default:
    assert(false);
    return false;
  }
}

bool value::operator != (const value& v) const {
  return !(*this == v);
}

size_t value::hash() const {
  switch (d_type) {
  case VALUE_NONE:
    return 0;
  case VALUE_BOOL:
    return d_b;
  case VALUE_BITVECTOR:
    return d_bv.hash();
  case VALUE_RATIONAL:
    return d_q.hash();
  case VALUE_ALGEBRAIC:
    return d_a.hash();
  case VALUE_ENUM:
    return d_ev.hash();
  default:
    return 0;
  }
}

void value::to_stream(std::ostream& out) const {
  switch (d_type) {
  case VALUE_NONE:
    out << "VALUE_NONE";
    break;
  case VALUE_BOOL:
    out << (d_b ? "true" : "false");
    break;
  case VALUE_BITVECTOR:
    out << d_bv;
    break;
  case VALUE_RATIONAL:
    out << d_q;
    break;
  case VALUE_ALGEBRAIC:
    out << d_a;
    break;
  case VALUE_ENUM:
    out << d_ev;
    break;
  }
}

bool value::get_bool() const {
  assert(is_bool());
  return d_b;
}

const bitvector& value::get_bitvector() const {
  assert(is_bitvector());
  return d_bv;
}

const rational& value::get_rational() const {
  assert(is_rational());
  return d_q;
}

const algebraic_number& value::get_algebraic() const {
  assert(is_algebraic());
  return d_a;
}

const enum_value& value::get_enum_value() const {
  assert(is_enum_value());
  return d_ev;
}

term_ref value::to_term(term_manager& tm) const {
  switch (d_type) {
  case VALUE_NONE:
    return term_ref();
  case VALUE_BOOL:
    return tm.mk_boolean_constant(d_b);
  case VALUE_BITVECTOR:
    return tm.mk_bitvector_constant(d_bv);
  case VALUE_RATIONAL:
    return tm.mk_rational_constant(d_q);
  case VALUE_ALGEBRAIC:
    throw exception("Cannot create algebraic numbers as terms");
  case VALUE_ENUM:
    return tm.mk_enum_constant(d_ev);
  }
  return term_ref();
}

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

class value_upcast {

  const value* x_to_use;
  const value* y_to_use;

  value tmp;

public:

  value_upcast(const value& x, const value& y)
  : x_to_use(0)
  , y_to_use(0)
  {
    if (x.value_type() == y.value_type()) {
      x_to_use = &x;
      y_to_use = &y;
    } else {
      if (x.value_type() == value::VALUE_RATIONAL) {
        tmp = value(algebraic_number(x.get_rational()));
        x_to_use = &tmp;
        y_to_use = &y;
      } else {
        tmp = value(algebraic_number(y.get_rational()));
        x_to_use = &x;
        y_to_use = &tmp;
      }
    }
  }

  const value& x() { return *x_to_use; }
  const value& y() { return *y_to_use; }

  value::type value_type() const { return x_to_use->value_type(); }
};

value value::operator + (const value& other) const {
  value_upcast cast(*this, other);
  switch (cast.value_type()) {
  case VALUE_RATIONAL:
    return value(cast.x().get_rational() + cast.y().get_rational());
  case VALUE_ALGEBRAIC:
    return value(cast.x().get_algebraic() + cast.y().get_algebraic());
  default:
    assert(false);
    break;
  }
  return value();
}

value& value::operator += (const value& other) {
  value_upcast cast(*this, other);
  switch (cast.value_type()) {
  case VALUE_RATIONAL:
    return *this = value(cast.x().get_rational() + cast.y().get_rational());
  case VALUE_ALGEBRAIC:
    return *this = value(cast.x().get_algebraic() + cast.y().get_algebraic());
  default:
    assert(false);
    break;
  }
  return *this;
}

value value::operator - () const {
  switch (value_type()) {
  case VALUE_RATIONAL:
    return value(get_rational().invert());
  case VALUE_ALGEBRAIC:
    return value(get_algebraic().invert());
  default:
    assert(false);
  }
  return value();
}

value value::operator - (const value& other) const {
  value_upcast cast(*this, other);
  switch (cast.value_type()) {
  case VALUE_RATIONAL:
    return value(cast.x().get_rational() - cast.y().get_rational());
  case VALUE_ALGEBRAIC:
    return value(cast.x().get_algebraic() - cast.y().get_algebraic());
  default:
    assert(false);
    break;
  }
  return value();
}

value& value::operator -= (const value& other) {
  value_upcast cast(*this, other);
  switch (cast.value_type()) {
  case VALUE_RATIONAL:
    return *this = value(cast.x().get_rational() - cast.y().get_rational());
  case VALUE_ALGEBRAIC:
    return *this = value(cast.x().get_algebraic() - cast.y().get_algebraic());
  default:
    assert(false);
    break;
  }
  return *this;
}

value value::operator * (const value& other) const {
  value_upcast cast(*this, other);
  switch (cast.value_type()) {
  case VALUE_RATIONAL:
    return value(cast.x().get_rational() * cast.y().get_rational());
  case VALUE_ALGEBRAIC:
    return value(cast.x().get_algebraic() * cast.y().get_algebraic());
  default:
    assert(false);
    break;
  }
  return value();
}

value& value::operator *= (const value& other) {
  value_upcast cast(*this, other);
  switch (cast.value_type()) {
  case VALUE_RATIONAL:
    return *this = value(cast.x().get_rational() * cast.y().get_rational());
  case VALUE_ALGEBRAIC:
    return *this = value(cast.x().get_algebraic() * cast.y().get_algebraic());
  default:
    assert(false);
    break;
  }
  return *this;
}

value value::operator / (const value& other) const {
  value_upcast cast(*this, other);
  switch (cast.value_type()) {
  case VALUE_RATIONAL:
    return value(cast.x().get_rational() / cast.y().get_rational());
  case VALUE_ALGEBRAIC:
    return value(cast.x().get_algebraic() / cast.y().get_algebraic());
  default:
    assert(false);
    break;
  }
  return value();
}

value& value::operator /= (const value& other) {
  value_upcast cast(*this, other);
  switch (cast.value_type()) {
  case VALUE_RATIONAL:
    return *this = value(cast.x().get_rational() / cast.y().get_rational());
  case VALUE_ALGEBRAIC:
    return *this = value(cast.x().get_algebraic() / cast.y().get_algebraic());
  default:
    assert(false);
    break;
  }
  return *this;
}

bool value::operator < (const value& other) const {
  return cmp(other) < 0;
}

bool value::operator <= (const value& other) const {
  return cmp(other) <= 0;
}

bool value::operator > (const value& other) const {
  return cmp(other) > 0;
}

bool value::operator >= (const value& other) const {
  return cmp(other) >= 0;
}

int value::cmp(const value& other) const {
  value_upcast cast(*this, other);
  switch (cast.value_type()) {
  case VALUE_RATIONAL:
    return cast.x().get_rational().cmp(cast.y().get_rational());
  case VALUE_ALGEBRAIC:
    return cast.x().get_algebraic().cmp(cast.y().get_algebraic());
  default:
    assert(false);
    break;
  }
  return false;
}

value value::floor() const {
  switch (value_type()) {
  case VALUE_RATIONAL:
    return value(get_rational().floor());
  case VALUE_ALGEBRAIC:
    return value(get_algebraic().floor());
  default:
    assert(false);
  }
  return false;
}

bool value::is_integer() const {
  switch (value_type()) {
  case VALUE_RATIONAL:
    return get_rational().is_integer();
  case VALUE_ALGEBRAIC:
    return get_algebraic().is_integer();
  default:
    assert(false);
  }
  return false;
}

}
}
