using System;
using System.Collections;

namespace Omega
{
	public class Relation
	{
		protected int h;

		protected Relation (int h)
		{
			this.h = h;
		}

		public Relation (Variable[] s, AST.Node b)
		{
			h = DllInterface.Relation_Create1(s.Length);

			for (int k = 0; k < s.Length; k++)
			{
				if (s[k].Name != null)
					DllInterface.Relation_NameSetVariable(h, k + 1, s[k].Name);

				s[k].Initialize(DllInterface.Relation_GetSetVariable(h, k + 1));
			}

			Build(DllInterface.Relation_AddAnd(h), (AST.Expression)b);
		}

		public Relation (Variable[] i, Variable[] o, AST.Node b)
		{
			h = DllInterface.Relation_Create2(i.Length, o.Length);

			for (int k = 0; k < i.Length; k++)
			{
				if (i[k].Name != null)
					DllInterface.Relation_NameInputVariable(h, k + 1, i[k].Name);

				i[k].Initialize(DllInterface.Relation_GetInputVariable(h, k + 1));
			}
			
			for (int k = 0; k < o.Length; k++)
			{
				if (o[k].Name != null)
					DllInterface.Relation_NameOutputVariable(h, k + 1, o[k].Name);

				o[k].Initialize(DllInterface.Relation_GetOutputVariable(h, k + 1));
			}

			Build(DllInterface.Relation_AddAnd(h), (AST.Expression)b);
		}

		public VariableTuple Tuple
		{
			get
			{
				return new VariableTuple(new VariableTuple.GetVariableDelegate(GetSetVariable));
			}
		}

		public VariableTuple Input
		{
			get
			{
				return new VariableTuple(new VariableTuple.GetVariableDelegate(GetInputVariable));
			}
		}

		public VariableTuple Output
		{
			get
			{
				return new VariableTuple(new VariableTuple.GetVariableDelegate(GetOutputVariable));
			}
		}

		protected int GetSetVariable (int i)
		{
			if (i == 0)
				return DllInterface.Relation_GetSetCount(h);
			else
				return DllInterface.Relation_GetSetVariable(h, i);
		}

		protected int GetInputVariable (int i)
		{
			if (i == 0)
				return DllInterface.Relation_GetInputCount(h);
			else
				return DllInterface.Relation_GetInputVariable(h, i);
		}

		protected int GetOutputVariable (int i)
		{
			if (i == 0)
				return DllInterface.Relation_GetOutputCount(h);
			else
				return DllInterface.Relation_GetOutputVariable(h, i);
		}

		protected void Build (int h, AST.Node n)
		{
			if (n is AST.And)
			{
				AST.Binary x = (AST.Binary)n;

				Build(DllInterface.Formula_AddAnd(h), x.Left);
				Build(DllInterface.Formula_AddAnd(h), x.Right);
			}
			else if (n is AST.Or)
			{
				AST.Binary x = (AST.Binary)n;

				int h1 = DllInterface.Formula_AddOr(h);

				Build(DllInterface.Formula_AddAnd(h1), x.Left);
				Build(DllInterface.Formula_AddAnd(h1), x.Right);
			}
			else if (n is AST.Not)
				Build(DllInterface.Formula_AddAnd(DllInterface.Formula_AddNot(h)), ((AST.Not)n).Expression);
			else if (n is AST.Relation)
			{
				AST.Relation r = (AST.Relation)n;

				int h1 = r.IsGEQ ? DllInterface.FAnd_AddGEQ(h) : DllInterface.FAnd_AddEQ(h);

				Build(h1, r.Coefficients);

				DllInterface.Constraint_DeleteHandle(h1);
			}
			else if (n is AST.Coefficients)
			{
				AST.Coefficients c = (AST.Coefficients)n;

				DllInterface.Constraint_UpdateConstant(h, c.Constant);
			
				foreach (Variable v in c.Variables)
				{
					Variable t = v.Global ? GetLocal(v) : v;

					DllInterface.Constraint_UpdateCoefficient(h, (int)t, c[v]);
				}
			}
			else
				throw new ArgumentException();
		}

		public void Print ()
		{
			DllInterface.Relation_Print(h);
		}

		public void Finalize ()
		{
			DllInterface.Relation_Finalize(h);
		}

		public void Simplify ()
		{
			DllInterface.Relation_Simplify(h, 2, 4);
		}

		public static Relation operator * (Relation r1, Relation r2)
		{
			return new Relation(DllInterface.Relation_Intersection(r1.h, r2.h));
		}

		public static Relation operator + (Relation r1, Relation r2)
		{
			return new Relation(DllInterface.Relation_Union(r1.h, r2.h));
		}

		public Relation this [Relation r]
		{
			get
			{
				return new Relation(DllInterface.Relation_Composition(h, r.h));
			}
		}

		unsafe public int[] Conjuncts 
		{
			get
			{
				int *c = DllInterface.Relation_GetConjuncts(h);

				int[] r = new int[c[0]];

				for (int i = 0; i < c[0]; i++)
					r[i] = c[i + 1];

				return r;
			}
		}

		public Variable GetLocal (Variable v)
		{
			return new Variable(DllInterface.Relation_GetLocal(h, (int)v));
		}

		public static void GetVariableBounds (int c, Variable v, out int lb, out int ub)
		{
			lb = DllInterface.Conjunct_QueryVariableLowerBound(c, (int)v);
			ub = DllInterface.Conjunct_QueryVariableUpperBound(c, (int)v);
		}
	}
}