// variable reference class -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "Variable.h"
#include "Valuation.h"
#include "Value.h"
#include "VariableDefinition.h"
#include "VariableSet.h"
#include "Constant.h"
#include "Substitution.h"
#include "Printer.h"
#include "Transition.h"
#include "util.h"
#include "Printer.h"

#include <assert.h>

/** @file Variable.C
 * Variable reference
 */

/* Copyright  1998-2002 Marko Mkel (msmakela@tcs.hut.fi).

   This file is part of MARIA, a reachability analyzer and model checker
   for high-level Petri nets.

   MARIA 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, or (at your option)
   any later version.

   MARIA 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.

   The GNU General Public License is often shipped with GNU software, and
   is generally kept in a file called COPYING or LICENSE.  If you do not
   have a copy of the license, write to the Free Software Foundation,
   59 Temple Place, Suite 330, Boston, MA 02111 USA. */

Variable::Variable (const class VariableDefinition& variable,
		    bool pred) :
  Expression (),
  myVariable (&variable), myPred (pred)
{
  setType (myVariable->getType ());
  assert (!pred || myVariable->getFather ());
}

Variable::~Variable ()
{
}

void
Variable::setType (const class Type& type)
{
  assert (myVariable->getType ().isAlwaysAssignable (type));
  Expression::setType (type);
}

class Value*
Variable::do_eval (const class Valuation& valuation) const
{
  const class Value* v = valuation.getValue (*myVariable);
  myVariable->flagReferenced (true);
  assert (!v || v->getType ().isAssignable (*getType ()));
  if (v)
    return constrain (valuation, v->copy ());
  else {
    valuation.flag (errVar, *this);
    return NULL;
  }
}

class Expression*
Variable::ground (const class Valuation& valuation,
		  class Transition* transition,
		  bool declare)
{
  if (myVariable->isAggregate ()) {
    const class Value* v = valuation.getValue (*myVariable);
    assert (!v || v->getType ().isAssignable (*getType ()));
    return v ? (new class Constant (*v->copy ()))->cse () : copy ();
  }
  else if (const class VariableDefinition* father = myVariable->getFather ()) {
    if (!transition)
      return 0;
    if (const class Value* v = valuation.getValue (*father)) {
      class StringBuffer buf;
      buf.append (myVariable->getName ());
      buf.append ("[");
      class Printer printer;
      printer.setOutput (&buf);
      if (myPred) {
	class Value* vp = v->copy ();
	vp->decrement ();
	vp->display (printer);
	delete vp;
      }
      else
	v->display (printer);
      buf.append ("]");
      const char* name = buf.getString ();
      if (const class VariableDefinition* var =
	  transition->getVariable (name)) {
	if (&var->getType () != getType ())
	  return 0;
	return (new class Variable (*var))->cse ();
      }
      else if (declare)
	return (new class Variable (transition->addVariable
				    (newString (name), *getType (),
				     false, false)))->cse ();
      else
	return 0;
    }
  }
  return copy ();
}

class Expression*
Variable::substitute (class Substitution& substitution)
{
  class Expression* e = substitution.getExpr (*myVariable);
  assert (!e || e->isAssignable (*getType ()));

  return e ? e : copy ();
}

bool
Variable::depends (const class VariableSet& vars,
		   bool complement) const
{
  return vars.contains (*myVariable) ? !complement : complement;
}

bool
Variable::forVariables (bool (*operation)
			(const class Expression&,void*),
			void* data) const
{
  return operation (*this, data);
}

bool
Variable::isCompatible (const class Value& value,
			const class Valuation& valuation) const
{
  assert (&value.getType () == getType ());
  if (const class Value* v = valuation.getValue (*myVariable))
    return *v == value;
  else
    return true;
}

void
Variable::getLvalues (const class Value& value,
		      class Valuation& valuation,
		      const class VariableSet& vars) const
{
  assert (&value.getType () == getType ());
  if (vars.contains (*myVariable) &&
      !valuation.getValue (*myVariable))
    valuation.setValue (*myVariable, *value.copy ());
}

void
Variable::getLvalues (const class VariableSet& rvalues,
		      class VariableSet*& lvalues) const
{
  if (!rvalues.contains (*myVariable)) {
    if (!lvalues)
      lvalues = new class VariableSet;
    lvalues->insert (*myVariable);
  }
}

#ifdef EXPR_COMPILE
# include "CExpression.h"

void
Variable::compileLvalue (class CExpression& cexpr,
			 unsigned indent,
			 const class VariableSet& vars,
			 const char* lvalue) const
{
  assert (myVariable->getNumber () && lvalue);
  if (!vars.contains (*myVariable))
    return;
  class StringBuffer& out = cexpr.getOut ();
  if (myVariable->isUndefined ()) {
    out.indent (indent);
    out.append ("ASSIGN (vars, ");
    out.append (myVariable->getNumber () - 1);
    out.append (");\n");
  }
  char* name;
  cexpr.getVariable (*this, name);
  out.indent (indent);
  out.append (name);
  out.append ("=");
  out.append (lvalue);
  out.append (";\n");
  delete[] name;
}

void
Variable::compileCompatible (class CExpression& cexpr,
			     unsigned indent,
			     const class VariableSet& vars,
			     const char* value) const
{
  if (!vars.contains (*myVariable))
    return;
  class StringBuffer& out = cexpr.getOut ();
  out.indent (indent);
  out.append ("if (");
  if (myVariable->isUndefined ()) {
    out.append ("ASSIGNED (");
    out.append (cexpr.getValuation ());
    out.append (", ");
    out.append (myVariable->getNumber () - 1);
    out.append (")&&\n");
  }
  char* name;
  cexpr.getVariable (*this, name);
  if (!getType ()->compileEqual (out, indent + 4, name, value,
				 false, !myVariable->isUndefined (),
				 true, false))
    out.append ("0");
  out.append (")\n");
  cexpr.compileError (indent + 2, errComp);
}

void
Variable::compile (class CExpression& cexpr,
		   unsigned indent,
		   const char* lvalue,
		   const class VariableSet* vars) const
{
  class StringBuffer& out = cexpr.getOut ();
  char* rvalue = cexpr.isIterator (*myVariable);
  if (rvalue) goto gotName;
  assert (myVariable->getNumber ());
  if (!vars || vars->contains (*myVariable)) {
    if (myVariable->isUndefined ()) {
      out.indent (indent);
      out.append ("if (!ASSIGNED (");
      out.append (cexpr.getValuation ());
      out.append (", ");
      out.append (myVariable->getNumber () - 1);
      out.append ("))\n");
      cexpr.compileError (indent + 2, errVar);
    }
    cexpr.getVariable (*this, rvalue);
  gotName:
    if (strcmp (lvalue, rvalue)) {
      out.indent (indent);
      out.append (lvalue);
      out.append ("=");
      out.append (rvalue);
      out.append (";\n");
    }
    delete[] rvalue;
  }
  else
    cexpr.compileError (indent, errVar);
}

#endif // EXPR_COMPILE

void
Variable::display (const class Printer& printer) const
{
  if (const class VariableDefinition* father = myVariable->getFather ()) {
    printer.delimiter (myPred ? ':' : '.');
    printer.print (myVariable->getName ());
    printer.delimiter (' ');
    printer.print (father->getName ());
  }
  else
    printer.print (myVariable->getName ());
}