/* Constraints.cpp -- C++ source file for KSI Constraint Graphs
*/
/*
 *
 * Copyright (c) 1996
 * Knowledge Science Institute, University of Calgary
 *
 * Permission to use, copy, modify, distribute and sell this software
 * and its documentation for any purpose is hereby granted without fee,
 * provided that the above copyright notice appear in all copies and
 * that both that copyright notice and this permission notice appear
 * in supporting documentation.  The Knowledge Science Institute makes no
 * representations about the suitability of this software for any
 * purpose.  It is provided "as is" without express or implied warranty.
 *
 */

#ifdef __BCPLUSPLUS__ //---Borland C++
#include 
#pragma hdrstop
#endif

#include "constraints.h"
#include 
#include 
#include 
#include 
#include 

#define DECL_PRIMITIVEVALIDATOR(className,applicable) \
class className : public Validator \
  { \
  public: \
    className() {} \
    className(const className& a) : Validator(a) {} \
    virtual Validator* clone() const {return new className(*this);} \
    virtual const string name() const {return string(#className);} \
    virtual bool operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags=0); \
    virtual unsigned long applicability() const {return applicable;} \
    virtual bool primitive() const {return true;} \
    virtual const string doc() const; \
    virtual const string spec() const; \
  };

ObjectLibrary* ConstraintLibrary = new ObjectLibrary();
ObjectLibrary* ConstraintTypeLibrary = new ObjectLibrary();

/******NOTE: Be sure to register all these function objects in
	     initConstraintLibrary() at the bottom of this file. */

/*------------------------------------------------------------------------------
				ConjunctionOfValidators
------------------------------------------------------------------------------*/
//this one (unlike most validators) is declared in the .h file

bool ConjunctionOfValidators::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  for (list >::iterator i(begin()); i!=end(); i++) {
    if (!(**i)(apply,owner,g,flags)) {
      if (!flags&silent)
        error(0,'W',"Validator '%s' failed for component %lu '%s' (validator in supertype component %lu '%s').\n%s\n\n%s",
                    (**i).name().c_str(),
		    apply.getID(), apply.getName().c_str(),
                    owner.getID(), owner.getName().c_str(),
                    (**i).doc().c_str(),
                    (**i).spec().c_str());
      return false;
      }
    }
  return true;
  }

const string ConjunctionOfValidators::doc() const
  {
  return "Return true only iff all contained validators are evaluate to true";
  }

const string ConjunctionOfValidators::spec() const
  {
  return
  "\t| ConjunctionOfValidators: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   ConjunctionOfValidators(apply,owner,g) =\n"
  "\t|     if (forall v:Validator | v in apply @ v(apply,t))\n"
  "\t|		then PASS\n"
  "\t|		else FAIL\n";
  }

int ConjunctionOfValidators::edit(unsigned long filter)
  {
  ConjunctionOfValidatorsDia dia(NULL,(ConjunctionOfValidators&)*this,filter);
  int stat = dia.Execute();
  return (stat==IDOK)?0:stat;
  }

ostream& ConjunctionOfValidators::printOn(ostream& o) const
  {
  Lexer::writeDelim(o,'(');
  bool first = true;
  for (list >::const_iterator i(begin()); i!=end(); i++) {
    if (first) first = false;
    else Lexer::writeDelim(o);
    Lexer::writeQuotedString(o,typeid(**i).name()); //usually the type is used, but in this case, the object's public name
    (**i).printOn(o);
    }
  Lexer::writeDelim(o,')');
  return o;
  }

istream& ConjunctionOfValidators::readFrom(istream& i)
  {
  erase(begin(),end());
  Lexer::readDelim(i,'(');
  do {
    string type;
    if (!Lexer::readQuotedString(i,type)) {
      Validator* v = ConstraintTypeLibrary->makeCopy(type);
      MASSERT(v);
      v->readFrom(i);
      push_back(Ref2(v,true));
      }
    } while(!Lexer::readDelim(i));
  Lexer::readDelim(i,')');
  return i;
  }

/*------------------------------------------------------------------------------
                                      NoArcBtwnArcs
------------------------------------------------------------------------------*/
/*
  Z spec*/

DECL_PRIMITIVEVALIDATOR(NoArcBtwnArcs,arc)

const string NoArcBtwnArcs::doc() const
  {
  return
  "Arcs between arcs are not allowed (except ARC itself and all ISA arcs).  "
  "Can be used at the ARC level to force first order graphs.\n\n";
  }

const string NoArcBtwnArcs::spec() const
  {
  return
  "\t| NoArcBtwnArcs: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   NoArcBtwnArcs(apply,owner,g) =\n"
  "\t|     if ((apply->g.ARC in g.isa0 /\ apply /= g.ARC /\ not(apply->g.ISA in g.isa0)) => (forall t:TERMINAL |\n"
  "\t|            t in ran (arc~(apply.Role)).Terminals @ t.Anchor->g.NODE in g.isa0))\n"
  "\t|		then PASS\n"
  "\t|		else FAIL";
  }

bool NoArcBtwnArcs::operator()(Component0& apply, Component0& owner, TypedGraph& t, unsigned long flags)
  {
  if (   (!(apply.getID() == t.getArcType()))
      && t.isa(apply.getID(),t.getArcType())
      && (!t.isa(apply.getID(),t.getIsaType()))) {
    ArcComponent* ac = dynamic_cast((Component0*)&apply);
    if (ac) {
      for (Arc0::terminals_type::size_type i = 0; igetTerminals()->size(); i++) {
        if (ac->getTerminalID(i))
          if (!t.isa(ac->getTerminalID(i),t.getNodeType()))
            return false;
        }
      }
    else error(0,'W',"NoArcBtwnArcs validator should only be applied to arcs");
    }
  return true;
  }

/*------------------------------------------------------------------------------
                                      NoConstAttrOverrides
------------------------------------------------------------------------------*/
/*
  Z spec*/

DECL_PRIMITIVEVALIDATOR(NoConstAttrOverrides,arc|node)

const string NoConstAttrOverrides::doc() const
  {
  return
  "A component cannot override a CONSTANT attribute in a supertype.";
  }

const string NoConstAttrOverrides::spec() const
  {
  return
  "\t| NoConstAttrOverrides: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   NoConstAttrOverrides(apply,owner,g) =\n"
  "\t|     if (forall a:apply.Attributes @\n"
  "\t|       not (exists c2:g.Contents | c2->apply in g.ancestorof0 @\n"
  "\t|         forall a2:c2.Attributes | a2.Name = a.Name @ CONSTANT in a2.Flags))\n"
  "\t|     then PASS\n"
  "\t|	 else FAIL";
  }

bool NoConstAttrOverrides::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  //if we used parentof() intead of ancestorof(), this alg would be more efficient
  for (TypedGraph::ContentsIterator c2=g.beginContents(); c2!=g.endContents(); c2++) {
    if (g.ancestorof((*c2).second->getID(),apply.getID())) {
      for (Component0::AttrIterator a2=(*c2).second->beginAttr(); a2!=(*c2).second->endAttr(); a2++) {
        if ((*a2)->getFlags()&Attribute::Constant) {
          for (Component0::AttrIterator a=apply.beginAttr(); a!=apply.endAttr(); a++) {
            if ((*a2)->getName()==(*a)->getName()) return false;
            }
          }
        }
      }
    }
  return true;
  }

/*------------------------------------------------------------------------------
			ArityEquals: this one takes a parameter, N
------------------------------------------------------------------------------*/
/*
  Z spec */

class ArityEquals : public EditableValidator
  {
  public:
    ArityEquals(int n) : N(n) {}
    ArityEquals(const ArityEquals& a) : EditableValidator(a), N(a.N) {}
    //clone will ask the user for a parameter if N = -1
    virtual Validator* clone() const;
    virtual bool operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags=0);
    virtual const string name() const;
    virtual const string specName() const {return "ArityEquals";}
    virtual const string doc() const;
    virtual const string spec() const;
    virtual int edit();
    virtual unsigned long applicability() const {return arc;}
    virtual bool primitive() const {return true;}
    virtual ostream& printOn(ostream& o) const;
    virtual istream& readFrom(istream& i);
  protected:
    int N;
  };

const string ArityEquals::name() const
  {
  char buf[6];
  if (N==-1) strcpy(buf,"n"); else sprintf(buf,"%d",N);
  return string("ArityEquals(")+buf+")";
  }

Validator* ArityEquals::clone() const
  {
  ArityEquals* ret = new ArityEquals(*this);
  /*
  if (N==-1) {
    if (!ret->edit()) return ret;
    else return NULL;
    }
  */
  return ret;
  }

int ArityEquals::edit()
  {
  char buf[3];
  int n;
  while (!askUser_string(name().c_str(),"Arity must be equal to (must be >0)",buf,3)) {
    if (sscanf(buf,"%d",&n) && n>0) {
      N = n;
      return 0;
      }
    }
  return -1;
  }

bool ArityEquals::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  ArcComponent* ac = dynamic_cast(&apply);
  if (ac)
    return ac->getTerminals()->size()==N;
  else {
    error(0,'W',"ArityEquals constraints should only be applied to ARCs");
    return true;
    }
  }

const string ArityEquals::doc() const
  {
  string ret =
  "The number of terminals (the arity) of this arc is restricted to ";
  ret += name() + ".";
  return ret;
  }

const string ArityEquals::spec() const
  {
  return
  "\t| ArityEquals: N1 --> VALIDATOR\n"
  "\t|---------------\n"
  "\t| forall n: N1 @\n"
  "\t|   ArityEquals(n) = (mu v:VALIDATOR |\n"
  "\t|     forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|       v(apply,owner,g) =\n"
  "\t|         if (#((arc~(apply.Role)).Terminals) = n)\n"
  "\t|		then PASS\n"
  "\t|		else FAIL)";
  }

ostream& ArityEquals::printOn(ostream& o) const
  {
  Lexer::writeLong(o,N);
  return o;
  }

istream& ArityEquals::readFrom(istream& i)
  {
  long x;
  Lexer::readLong(i,x);
  N = x;
  return i;
  }

/*------------------------------------------------------------------------------
			ArityLess: this one takes a parameter, N
------------------------------------------------------------------------------*/
/*
  Z spec */

class ArityLess : public EditableValidator
  {
  public:
    ArityLess(int n) : N(n) {}
    ArityLess(const ArityLess& a) : EditableValidator(a), N(a.N) {}
    virtual Validator* clone() const;
    virtual bool operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags=0);
    virtual const string name() const;
    virtual const string specName() const {return "ArityLess";}
    virtual const string doc() const;
    virtual const string spec() const;
    virtual int edit();
    virtual unsigned long applicability() const {return arc;}
    virtual ostream& printOn(ostream& o) const;
    virtual istream& readFrom(istream& i);
  protected:
    int N;
  };

const string ArityLess::name() const
  {
  char buf[6];
  if (N==-1) strcpy(buf,"n"); else sprintf(buf,"%d",N);
  return string("ArityLess(")+buf+")";
  }

Validator* ArityLess::clone() const
  {
  ArityLess* ret = new ArityLess(*this);
  /*
  if (N==-1) {
    if (!ret->edit()) return ret;
    else return NULL;
    }
  */
  return ret;
  }

int ArityLess::edit()
  {
  char buf[3];
  int n;
  while (!askUser_string(name().c_str(),"Arity should be less than (must be >1)",buf,3)) {
    if (sscanf(buf,"%d",&n) && n>1) {
      N = n;
      return 0;
      }
    }
  return -1;
  }

bool ArityLess::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  ArcComponent* ac = dynamic_cast(&apply);
  if (ac)
    return ac->getTerminals()->size() < N;
  else {
    error(0,'W',"ArityLess constraints should only be applied to ARCs");
    return true;
    }
  }

const string ArityLess::doc() const
  {
  string ret =
  "The number of terminals (the arity) of this arc is restricted to ";
  ret += name() + ".";
  return ret;
  }

const string ArityLess::spec() const
  {
  return
  "\t| ArityLess: N1 --> VALIDATOR\n"
  "\t|---------------\n"
  "\t| forall n: N1 @\n"
  "\t|   ArityLess(n) = (mu v:VALIDATOR |\n"
  "\t|     forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|       v(apply,owner,g) =\n"
  "\t|         if (#((arc~(apply.Role)).Terminals) = n)\n"
  "\t|		then PASS\n"
  "\t|		else FAIL)";
  }

ostream& ArityLess::printOn(ostream& o) const
  {
  Lexer::writeLong(o,N);
  return o;
  }

istream& ArityLess::readFrom(istream& i)
  {
  long x;
  Lexer::readLong(i,x);
  N = x;
  return i;
  }

/*------------------------------------------------------------------------------
			ArityGreater: this one takes a parameter, N
------------------------------------------------------------------------------*/
/*
  Z spec */

class ArityGreater : public EditableValidator
  {
  public:
    ArityGreater(int n) : N(n) {}
    ArityGreater(const ArityGreater& a) : EditableValidator(a), N(a.N) {}
    virtual Validator* clone() const;
    virtual bool operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags=0);
    virtual const string name() const;
    virtual const string specName() const {return "ArityGreater";}
    virtual const string doc() const;
    virtual const string spec() const;
    virtual int edit();
    virtual unsigned long applicability() const {return arc;}
    virtual ostream& printOn(ostream& o) const;
    virtual istream& readFrom(istream& i);
  protected:
    int N;
  };

const string ArityGreater::name() const
  {
  char buf[6];
  if (N==-1) strcpy(buf,"n"); else sprintf(buf,"%d",N);
  return string("ArityGreater(")+buf+")";
  }

Validator* ArityGreater::clone() const
  {
  ArityGreater* ret = new ArityGreater(*this);
  /*
  if (N==-1) {
    if (!ret->edit()) return ret;
    else return NULL;
    }
  */
  return ret;
  }

int ArityGreater::edit()
  {
  char buf[3];
  int n;
  while (!askUser_string(name().c_str(),"Arity should be greater than (must be >0)",buf,3)) {
    if (sscanf(buf,"%d",&n) && n>0) {
      N = n;
      return 0;
      }
    }
  return -1;
  }

bool ArityGreater::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  ArcComponent* ac = dynamic_cast(&apply);
  if (ac)
    return ac->getTerminals()->size()>N;
  else {
    if (!flags&silent) error(0,'W',"ArityGreater constraints should only be applied to ARCs");
    return true;
    }
  }

const string ArityGreater::doc() const
  {
  string ret =
  "The number of terminals (the arity) of this arc is restricted to ";
  ret += name() + ".";
  return ret;
  }

const string ArityGreater::spec() const
  {
  return
  "\t| ArityGreater: N1 --> VALIDATOR\n"
  "\t|---------------\n"
  "\t| forall n: N1 @\n"
  "\t|   ArityGreater(n) = (mu v:VALIDATOR |\n"
  "\t|     forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|       v(apply,owner,g) =\n"
  "\t|         if (#((arc~(apply.Role)).Terminals) = n)\n"
  "\t|		then PASS\n"
  "\t|		else FAIL)";
  }

ostream& ArityGreater::printOn(ostream& o) const
  {
  Lexer::writeLong(o,N);
  return o;
  }

istream& ArityGreater::readFrom(istream& i)
  {
  long x;
  Lexer::readLong(i,x);
  N = x;
  return i;
  }

/*------------------------------------------------------------------------------
                                      Directed
------------------------------------------------------------------------------*/
/*
  Z spec */

DECL_PRIMITIVEVALIDATOR(Directed,arc)

const string Directed::doc() const
  {
  return
  "The Directed VALIDATOR specifies a binary from-to arc.  This version automatically "
  "specializes any BOTH terminals to FROM and TO, respectively.";
  }

const string Directed::spec() const
  {
  return
  "\t| Directed: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   Directed(apply,owner,g) =\n"
  "\t|     if (ArityEquals(2)(apply,owner,g)=PASS	/\\\n"
  "\t|       GetTerminalDir(apply,1) = FROM	/\\\n"
  "\t|       GetTerminalDir(apply,2) = TO)\n"
  "\t|     then PASS\n"
  "\t|     else FAIL";
  }

bool Directed::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  bool ret=true;
  ArcComponent* a = dynamic_cast(&apply);
  if (a) {
    ret = ArityEquals(2)(*a,owner,g,flags);
    if (ret) {
      if (a->getTerminalDir(0)!=Terminal::FROM || a->getTerminalDir(1)!=Terminal::TO) {
        if (a->getTerminalDir(0)&Terminal::FROM && a->getTerminalDir(1)&Terminal::TO) {//OK, but have to specialize the directions
          a->setTerminalDir(0,Terminal::FROM);
          a->setTerminalDir(1,Terminal::TO);
          }
        else ret = false; //can't specialize, so fail
        }
      }
    }
  else {
    error(0,'W',"The Directed validator should be applied only to arcs");
    }
  return ret;
  }

/*------------------------------------------------------------------------------
                                      Upward
------------------------------------------------------------------------------*/
/*
  Z spec */

DECL_PRIMITIVEVALIDATOR(Upward,arc)

const string Upward::doc() const
  {
  return
  "The Upward VALIDATOR is a specialization of the Directed "
  "VALIDATOR that must be FROM an object at a level lower or equal to "
  "the the level of the TO side.  Also, the level of the isa arc itself must "
  "be the same as that of the FROM side.";
  }

const string Upward::spec() const
  {
  return
  "\t| Upward: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   Upward(apply,owner,g) =\n"
  "\t|     if (Directed(apply,owner,g)=PASS		/\\\n"
  "\t|       (GetTerminal(apply,1)).Level >=  (GetTerminal(apply,2)).Level /\\\n"
  "\t|       apply.Level <= (GetTerminal(apply,1)).Level)\n"
  "\t|     then PASS\n"
  "\t|     else FAIL";
  }

bool Upward::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  bool ret=true;
  ArcComponent* a = dynamic_cast(&apply);
  if (a) {
    ret = Directed()(*a,owner,g,flags);
    if (ret) {
      if (a->getTerminalID(0) && a->getTerminalID(1) &&
          (g[a->getTerminalID(0)].getLevel() < g[a->getTerminalID(1)].getLevel() ||
           a->getLevel() > g[a->getTerminalID(0)].getLevel()))
        ret = false;
      }
    }
  else {
    error(0,'W',"The Upward validator should be applied only to arcs");
    }
  return ret;
  }

/*------------------------------------------------------------------------------
                                      ConfinedToGraph
------------------------------------------------------------------------------*/
/*
  Z spec */

DECL_PRIMITIVEVALIDATOR(ConfinedToGraph,arc)

const string ConfinedToGraph::doc() const
  {
  return
  "An arc cannot refer to anything outside the graph it is contained in.  This validator\n"
  "is related to the NoDanglingTerminals validator, but this one allows dangling\n"
  "terminals and explicity checks for graph membership (NoDanglingTerminals doesn't).";
  }

const string ConfinedToGraph::spec() const
  {
  return
  "\t| ConfinedToGraph: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   ConfinedToGraph(apply,owner,g) =\n"
  "\t|     if (forall i:N | i<=#(arc~(apply.Role)).Terminals @\n"
  "\t|           GetTerminal(apply,i) in (g.Contents || {NULLCOMPONENT}))\n"
  "\t|     then PASS\n"
  "\t|     else FAIL";
  }

bool ConfinedToGraph::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  ArcComponent* ac = dynamic_cast(&apply);
  if (ac) {
    cerr << "(refs within graph only) ";
    for (Arc0::terminals_type::size_type i = 0; igetTerminals()->size(); i++) {
      if (ac->getTerminalID(i) && !g.contains(ac->getTerminalID(i)))
	return false;
      }
    }
  else {
    error(0,'W',"The ConfinedToGraph validator should be applied only to arcs");
    }
  return true;
  }

/*------------------------------------------------------------------------------
                                      NoDanglingTerminals
------------------------------------------------------------------------------*/
/*
  Z spec */

DECL_PRIMITIVEVALIDATOR(NoDanglingTerminals,arc)

const string NoDanglingTerminals::doc() const
  {
  return
  "An arc with the NoDanglingTerminals contraint must have all its terminals linked "
  "to a valid object in the graph (none must be uninstantiated or \"dangling\").  This "
  "constraint naturally applies to all isa arcs.  Note that this is related to the "
  "ConfinedToGraph validator, ConfinedToGraph allows dangling terminals while this "
  "one doesn't, and also doesn't explicitly check for membership in the graph.";
  }

const string NoDanglingTerminals::spec() const
  {
  return
  "\t| NoDanglingTerminals: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   NoDanglingTerminals(apply,owner,g) =\n"
  "\t|     if (forall i:N | i<=#(arc~(apply.Role)).Terminals @\n"
  "\t|           GetTerminal(apply,i) in g.Contents)\n"
  "\t|     then PASS\n"
  "\t|     else FAIL";
  }

bool NoDanglingTerminals::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  ArcComponent* ac = dynamic_cast(&apply);
  if (ac) {
    cerr << "(refs within graph only) ";
    for (Arc0::terminals_type::size_type i = 0; igetTerminals()->size(); i++) {
      if (!ac->getTerminalID(i)) return false;
      }
    }
  else {
    error(0,'W',"The NoDanglingTerminals validator should be applied only to arcs");
    }
  return true;
  }

/*------------------------------------------------------------------------------
                                      ArcConformance
------------------------------------------------------------------------------*/
/*
  Z spec */

DECL_PRIMITIVEVALIDATOR(ArcConformance,arc)

const string ArcConformance::doc() const
  {
  return
  "Arcs must conform to their parents' arcs; that is, the child's arity must be greater "
  "than or equal to the arity of the parent, and all terminating objects in the child "
  "must be sub-types (or equal) of the corresponding (and non-missing) types of "
  "the parent's terminating objects.\n"
  "NOTE: this version of ArcConformance will automatically patch the child arc "
  "if the only problem is the arities.";
  }

const string ArcConformance::spec() const
  {
  return
  "\t| ArcConformance: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   ArcConformance(apply,owner,g) =\n"
  "\t|     if (forall c2:ARC_COMPONENT | c2 in g.Contents /\\ c2->apply in g.ancestorof0 @\n"
  "\t|       % subtypes must have equal or more terminals\n"
  "\t|       #(arc~(c2.Role)).Terminals <= #(arc~(apply.Role)).Terminals /\\\n"
  "\t|       % subtypes must type-conform at each terminal\n"
  "\t|       (forall i:Z | i<=#(arc~(c2.Role)).Terminals @\n"
  "\t|	     GetTerminal(apply,i)->GetTerminal(c2,i) in g.isa0))\n"
  "\t|     then PASS\n"
  "\t|     else FAIL";
  }

bool ArcConformance::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  ArcComponent* ac = dynamic_cast(&apply);
  if (ac) {
    for (TypedGraph::ContentsIterator c2=g.beginContents(); c2!=g.endContents(); c2++) {
      ArcComponent* ac2 = dynamic_cast((Component0*)(*c2).second);
      if (ac2 && g.ancestorof(ac2->getID(),ac->getID())) {
	Arc0::terminals_type::size_type size1=ac->getTerminals()->size(),
                                        size2=ac2->getTerminals()->size(),
					minSize=min(size1,size2);
	//if (size2 > size1) return false; //this code is the strategy to just fail if arities aren't compatable
	for (Arc0::terminals_type::size_type i = 0; igetTerminalID(i) && ac2->getTerminalID(i) && (ac2->getTerminalID(i))!=g.getTopType()) {
            if (!g.isa(ac->getTerminalID(i),ac2->getTerminalID(i))) return false;
	    }
	  }
	while (size2 > size1) { //this code is the strategy to patch up the arc if only the arities are incompatable
	  ac->putAnchor(size1,ac2->getTerminalID(size1),ac2->getTerminalDir(size1));
	  size1++;
	  }
	}
      }
    }
  else {
    error(0,'W',"The ArcConformance validator should be applied only to arcs");
    }
  return true;
  }

/*------------------------------------------------------------------------------
                                      NoSelfReference
------------------------------------------------------------------------------*/
/*
  Z spec */

DECL_PRIMITIVEVALIDATOR(NoSelfReference,arc)

const string NoSelfReference::doc() const
  {
  return
  "No arc may refer to itself.  This rule will be added to the definition of an ARC.";
  }

const string NoSelfReference::spec() const
  {
  return
  "\t| NoSelfReference: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   NoSelfReference(apply,owner,g) =\n"
  "\t|     if (forall t:second(| (arc~(apply.Role)).Terminals |) @\n"
  "\t|                apply /= t.Anchor)\n"
  "\t| 	 then PASS\n"
  "\t|	 else FAIL";
  }

bool NoSelfReference::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  ArcComponent* ac = dynamic_cast(&apply);
  if (ac) {
    for (Arc0::terminals_type::size_type i = 0; igetTerminals()->size(); i++) {
      if (ac->getTerminalID(i) == ac->getID()) return false;
      }
    }
  else {
    error(0,'W',"The NoSelfReference validator should be applied only to arcs");
    }
  return true;
  }

/*------------------------------------------------------------------------------
                                      NoMixin
------------------------------------------------------------------------------*/
/*
  Z spec */

DECL_VALIDATOR(NoMixin,node|arc)

const string NoMixin::doc() const
  {
  return
  "Nothing that has an ancestor with the NoMixin validator has more than one direct parent.";
  }

const string NoMixin::spec() const
  {
  return
  "\t| NoMixin: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   NoMixin(apply,owner,g) =\n"
  "\t|     if (apply /= owner => (exists1 c:g.Contents @ c->apply in g.parentof0))\n"
  "\t| 	 then PASS\n"
  "\t|	 else FAIL";
  }

bool NoMixin::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  int one = false;
  for (TypedGraph::ContentsIterator i(g.beginContents()); i!=g.endContents(); i++) {
    if (apply.getID()!=owner.getID() && (*(*i).second).getLevel()>1 && g.parentof((*i).first,apply.getID())) {
      if (one) return false;
      else     one = true;
      }
    }
  return true;
  }

/*------------------------------------------------------------------------------
                                      ParentOfIndividual
------------------------------------------------------------------------------*/
/*
  Z spec */

DECL_VALIDATOR(ParentOfIndividual,node|arc)

const string ParentOfIndividual::doc() const
  {
  return
  "Nothing that has an ancestor with the ParentOfIndividual validator can have ";
  "any subtypes: it is an \"object\" in the traditional sense of the word.";
  }

const string ParentOfIndividual::spec() const
  {
  return
  "\t| ParentOfIndividual: VALIDATOR\n"
  "\t|--------------\n"
  "\t| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @\n"
  "\t|   ParentOfIndividual(apply,owner,g) =\n"
  "\t|     if (apply /= owner => not (exists c:g.Contents @ (apply->c in g.ancestorof0)))\n"
  "\t| 	 then PASS\n"
  "\t|	 else FAIL";
  }

bool ParentOfIndividual::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  for (TypedGraph::ContentsIterator i(g.beginContents()); i!=g.endContents(); i++) {
    if (apply.getID()!=owner.getID() && (*(*i).second).getLevel()>1 && g.ancestorof(apply.getID(),(*i).first))
      return false;
    }
  return true;
  }

/*------------------------------------------------------------------------------
			NameRegularExpression: this one takes a parameter, N
------------------------------------------------------------------------------*/
/*
  Z spec */

class NameRegularExpression : public EditableValidator
  {
  public:
    NameRegularExpression(string re="") : REs(re) {}
    NameRegularExpression(const NameRegularExpression& a) : EditableValidator(a), REs(a.REs) {}
    virtual Validator* clone() const {return new NameRegularExpression(*this);}
    virtual bool operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags=0);
    virtual const string name() const {return "NameRegularExpression";}
    virtual const string doc() const;
    virtual const string spec() const;
    virtual int edit();
    virtual unsigned long applicability() const {return arc|node;}
    virtual ostream& printOn(ostream& o) const;
    virtual istream& readFrom(istream& i);
  protected:
    string REs;
  };

int NameRegularExpression::edit()
  {
  RegExpsDia dia(NULL,REs);
  int stat = dia.Execute();
  return (stat==IDOK)?0:stat;
  }

bool NameRegularExpression::operator()(Component0& apply, Component0& owner, TypedGraph& g, unsigned long flags)
  {
  bool ret = false;
  size_t pos = 0;
  size_t pos2;
  string name = apply.getName();
  TRegexp regexp("");
  size_t end = REs.length();
  while (posinsert(v->name(),v); \
  ConstraintTypeLibrary->insert(x); \
  }


void initConstraintLibrary() {
  //Note: make sure to register in both ConstraintLibrary and ConstraintTypeLibrary
  put(new NoArcBtwnArcs());
  put(new NoConstAttrOverrides());
  put(new ArityEquals(-1));
  put(new ArityLess(-1));
  put(new ArityGreater(-1));
  put(new Directed());
  put(new Upward());
  put(new ConfinedToGraph());
  put(new NoDanglingTerminals());
  put(new ArcConformance());
  put(new NoSelfReference());
  put(new NoMixin());
  put(new ParentOfIndividual());
  put(new NameRegularExpression());
  }

/*


*/