#ifndef VLMINTERM_HEADER
#define VLMINTERM_HEADER 1
/////////////////////////////////////////////////////////
//! file="amma/Logic/Basic/LMinTerm.hh"
//! lib=VLBasic
//! author="Charles Galambos"
//! date="14/5/1996"
//! docentry="Logic.Basic"
//! rcsid="$Id: LMinTerm.hh,v 1.19 2000/07/14 14:30:09 ees1cg Exp $"

#include "amma/Logic2/LSymb.hh"
#include "amma/Logic2/LSymbSet.hh"
#include "amma/DList.hh"
//#include "amma/DLIter.hh"
//#include "amma/CDLIter.hh"

// This is a small object !

class VLSpace;
class VLBindLst;
class VLSymbIter;
class VLMinTermSOP;
class VLSubstBase;
class VLMinTermC; // The handle class.
class VLRule;

//! userlevel=Develop
//: Logical min-term.
// this contains two sets of symbols.
// this first set must be all true, and the second all false.

class VLMinTerm 
  : public VLSymb 
{
public:
  inline VLMinTerm();
  //: Constuctor, default.
  
  VLMinTerm(VLSymbSet &PC,VLSymbSet &NC);
  //: Constuctor from sets.
  
  VLMinTerm(VLSymbSet &PC);
  //: Constuctor from positive set only.
  
  inline VLMinTerm(const VLMinTerm &Oth);
  // Copy constructor.
  
  inline VLMinTerm(const VLSymb &PosSymb);
  // VLSymb -> VLMinTerm conversion.
  
  inline VLMinTerm(BooleanT Negate,const VLSymb &ASymb);
  // Constructor.

  inline VLMinTerm(BooleanT Negate,const VLSymbC &ASymb);
  // Constructor.
  
  virtual VLSymbC SymbCopy(void) const;
  // Make a copy of this object on the heap.
  
  inline VLMinTerm &operator=(const VLMinTerm &Oth);
  // Assigment to another minterm.
  
  inline BooleanT operator==(const VLMinTerm &Oth) const;
  // Comparison to another VLMinTerm.
  
  inline BooleanT operator!=(const VLMinTerm &Oth) const;
  // Comparison to another VLMinTerm.
  
  virtual BooleanT IsSimple(void) const { return !Vars; }
  // Does this minterm contain any Variables ? (True == No).
  
  void Invert(void);
  // Invert condition in-place. Swap Neg & Pos.
  
  DListC<VLMinTermC> Inverse(void) const;
  // Get inverse of min term, put it in result.
  
  void Empty(void);
  // Clear all contents.
  
  VLSymbSetC &GetPos(void) {  return Pos; }
  // Get set of positive Symbols.
  
  VLSymbSetC &GetNeg(void) { return Neg; }
  // Get set of negative Symbols.
  
  const VLSymbSetC &GetPos(void) const { return Pos; }
  // Get set of positive Symbols.
  
  const VLSymbSetC &GetNeg(void) const { return Neg; }
  // Get set of negative Symbols.
  
  BooleanT AddPosCond(const VLSymb &Symb);
  // False if contradiction.
  
  BooleanT AddNegCond(const VLSymb &Symb);
  // False if contradiction.

  BooleanT AddPosCond(const VLSymbC &Symb);
  // False if contradiction.
  
  BooleanT AddNegCond(const VLSymbC &Symb);
  // False if contradiction.
  
  BooleanT AndAdd(const VLMinTerm &Oth);
  // False if causes contradiction.
  
  BooleanT Covers(const VLMinTerm &Oth) const ; 
  // Check if '*this' is true in all states that 'Oth' is.
  // Setwise only.
  
  BooleanT Covers(const VLMinTerm &Oth,VLBindLst &Bnds) const ; 
  // Check if '*this' is true in all states that 'Oth' is.
  // Unifying version.
  
  BooleanT Covers(const VLSymb &Oth) const ; 
  // Check if '*this' is true in all states that 'Oth' is.
  
  BooleanT CoveredBy(const VLSymb &Oth) const;
  // Check if Oth->Covers(*this);
  
  void Intersect(const VLMinTerm &Oth,VLMinTerm &Result) const; 
  // Get intersection of *this & Oth.
  
  int Size(void) const { return Pos.Size() + Neg.Size(); }
  // Get number of terms in condition.
  
  virtual BooleanT IsEqual(const VLSymb &Other) const;
  // Is this equal to another Symbol ?
  
  BooleanT Unify(const VLSymb &Other,VLBindLst &SF,BooleanT NegateSymb) const;
  // Unify this with another Symbol.
  // This will succeed as long as there's no direct contradiction.
  // If there are more than one way to create a successfull binding,
  // the first found will be used.
  
  virtual BooleanT Unify(const VLSymb &Other,VLBindLst &SF) const;
  // Unify this with another Symbol.
  // This will succeed as long as there's no direct contradiction.
  // If there are more than one way to create a successfull binding,
  // the first found will be used.
  
  BooleanT Unify(const VLMinTerm &Other,VLBindLst &SF) const;
  // Unify with another, MinTerm.
  
  virtual BooleanT Test(const VLSpace &State,VLBindLst &Bnd,VLSymbIterC &Iter) const; 
  // Test if this MinTerm is true in 'State' with binding 'Bnd', if there are
  // more than one set of matching bindings use 'Iter' to iterate through them.
  // See VLSymb::Test(...) for more info.
  
  VLSymbC Subst(const VLBindLst &Bnds) const;
  //: Substitue binds.
  // Allocates a new body.
  
  virtual VLSymbC Subst(const VLSubstBaseC &Subs) const;
  // Substitute one set of symbols for another.
  
  VLMinTermC NewVarDupD(VLSubstBaseC &Subst) const;
  // Create subsitutions for variables as needed.
  
  virtual StringC GetName(StringC Buff = StringC()) const;
  // Get name of MinTerm. (Name of its contents.)
  
  virtual void Dump(void) const;
  // Dump it to stdout.

  virtual unsigned int Hash() const;
  //: Calculate hash value.
  
private:
  VLSymbSetC Pos; // Things that must be true.
  VLSymbSetC Neg; // Things that must be false.
  BooleanT Vars;   // Contains any vars ?
};

typedef DListC<VLMinTermC> VLMinTermLstC;     
typedef DLIterC<VLMinTermC> VLMinTermLstIterC;
typedef ConstDLIterC<VLMinTermC> VLMinTermLstCIterC;

//////////////////////////////////////////////////////////////

//! userlevel=Normal
//: Logical min-term.
// this contains two sets of symbols.
// this first set must be all true, and the second all false.

class VLMinTermC 
  : public VLSymbC 
{
public:
  inline VLMinTermC();
  //: Default constructor.
  // Creates an InValid refrence.
  
  inline VLMinTermC(const VLMinTermC &oth);
  //: Copy constructor.
  
  inline VLMinTermC(const VLSymbC &oth);
  //: Attempt to construct from a general symbol. 
  // If symbol is an
  // a minterm then this object will become a handle to that minterm
  // otherwise a new minterm will be constructed with the symbol as
  // a positive condition.
  
  inline VLMinTermC(BooleanT invert,const VLSymbC &oth) 
    : VLSymbC(*new VLMinTerm(invert,oth))
    {}
  //: Construct from a symbol
  // True value is inverted if invert is TRUE.
  
  inline VLMinTermC(BooleanT /*filled*/) 
    : VLSymbC(*new VLMinTerm())
    {}
  //: Construct an empty minterm.
  
  VLMinTermC(VLSymbSet &PC,VLSymbSet &NC)
    : VLSymbC(*new VLMinTerm(PC,NC))
    {}
  //: Constuctor from positive and negative sets.
  
  VLMinTermC(VLSymbSet &PC)
    : VLSymbC(*new VLMinTerm(PC))
    {}
  //: Constuctor from positive set only.
  
  inline VLMinTerm &Body() 
    { return static_cast<VLMinTerm &>(VLSymbC::Body()); }
  // Access expression.
  
  inline const VLMinTerm &Body() const 
    { return static_cast<const VLMinTerm &>(VLSymbC::Body()); }
  // Constant access to expression.
  
  inline VLMinTermC(VLMinTerm &oth) 
    : VLSymbC(oth) 
    {}
  //: Body constructor.
  
  inline static BooleanT IsMinTerm(const VLSymbC &oth)
    { return (dynamic_cast<const VLMinTerm *>(&oth.Body()) != 0); }
  //: Test if 'oth' is an expression.
  
  inline VLMinTermC Copy() const 
    { return VLMinTermC(Body().SymbCopy()); }
  // Copy MinTerm.
  
  inline BooleanT operator==(const VLMinTermC &Oth) const 
    { return Body().operator==(Oth.Body()); }
  // Comparison to another VLMinTerm.
  
  inline BooleanT operator!=(const VLMinTermC &Oth) const 
    { return Body().operator!=(Oth.Body()); }
  // Comparison to another VLMinTerm.
  
  inline BooleanT Covers(const VLMinTermC &Oth) const 
    { return Body().Covers(Oth.Body()); }
  // Check if '*this' is true in all states that 'Oth' is.
  // Setwise only.
  
  inline BooleanT Covers(const VLMinTermC &Oth,VLBindLst &Bnds) const 
    { return Body().Covers(Oth.Body(),Bnds); }
  // Check if '*this' is true in all states that 'Oth' is.
  // Unifying version.
  
  inline BooleanT Covers(const VLSymbC &Oth) const 
    { return Body().Covers(Oth.Body()); }
  // Check if '*this' is true in all states that 'Oth' is.
  
  inline BooleanT CoveredBy(const VLSymbC &Oth) const 
    { return Body().CoveredBy(Oth.Body()); }
  //: Check if Oth->Covers(*this);
  
  inline BooleanT AddPosCond(const VLSymbC &Symb) 
    { return Body().AddPosCond(Symb.Body()); }
  //: Add positive condition
  // False if contradiction.
  
  inline BooleanT AddNegCond(const VLSymbC &Symb) 
    { return Body().AddNegCond(Symb.Body()); }
  //: Add negative condition
  // False if contradiction.
  
  inline BooleanT AndAdd(const VLMinTermC &Oth) { return Body().AndAdd(Oth.Body()); }
  //: False if causes contradiction.
  
  inline BooleanT operator*= (const VLMinTermC &Oth) { return Body().AndAdd(Oth.Body()); }
  //: And another minterm.
  
  inline BooleanT operator*= (const VLSymbC &Oth) { return Body().AddPosCond(Oth.Body()); }
  //: And positive condition.
  
  inline BooleanT operator/= (const VLSymbC &Oth) { return Body().AddNegCond(Oth.Body()); }
  //: And negative condition.

  inline BooleanT operator+= (const VLSymbC &Oth) { return Body().AddPosCond(Oth.Body()); }
  //: And positive condition.
  
  inline BooleanT operator-= (const VLSymbC &Oth) { return Body().AddNegCond(Oth.Body()); }
  //: And negative condition.
  
  inline void Empty(void) 
    { Body().Empty(); }
  //: Clear all contents.
  
  inline void Invert(void) 
    { Body().Invert(); } 
  //: Invert condition in-place. Swap Neg & Pos.
  
  DListC<VLMinTermC> Inverse(void) const
    { return Body().Inverse(); } 
  //: Get inverse of min term, put it in result.
  
  inline VLMinTermC Intersect(const VLMinTermC &Oth) const;
  //: Get intersection of *this & Oth.
  
  inline BooleanT Unify(const VLMinTermC &Other,VLBindLst &SF) const 
    { return Body().Unify(Other.Body(),SF); } 
  //: Unify with another, MinTerm.
  
  inline BooleanT Unify(const VLSymbC &Other,VLBindLst &SF,BooleanT NegateSymb = FALSE) const     
    { return Body().Unify(Other.Body(),SF,NegateSymb); }
  //: Unify this with another Symbol.
  // This will succeed as long as there's no direct contradiction.
  // If there are more than one way to create a successfull binding,
  // the first found will be used.
  
  inline const VLSymbSetC &Pos() const 
    { return Body().GetPos(); }
  //: Access positive condition set.
  
  inline const VLSymbSetC &Neg() const 
    { return Body().GetNeg(); }
  //: Access negative condition set.
  
  int Size(void) const 
    { return Body().Size(); }
  // Get number of terms in condition.
  
  friend class VLMinTermSOP;
  friend class VLRule;
};

///////////////////
// Constuctor, default.

inline VLMinTerm::VLMinTerm() 
  : Vars(False)
{}

///////////////////
// Copy constructor.

inline VLMinTerm::VLMinTerm(const VLMinTerm &Oth)
  : Pos(Oth.Pos.Copy()),
    Neg(Oth.Neg.Copy()),
    Vars(Oth.Vars) 
{}

///////////////////
// VLSymb -> VLMinTerm conversion.

inline 
VLMinTerm::VLMinTerm(const VLSymb &PosSymb) 
  : Vars(False)
{ AddPosCond(PosSymb); }

///////////////////
// Constuctor.

inline 
VLMinTerm::VLMinTerm(BooleanT Negate,const VLSymb &ASymb) 
  : Vars(False)
{ 
  if(!Negate)
    AddPosCond(ASymb); 
  else
    AddNegCond(ASymb); 
}

inline 
VLMinTerm::VLMinTerm(BooleanT Negate,const VLSymbC &ASymb)
  : Vars(False)
{
  if(!Negate)
    AddPosCond(ASymb); 
  else
    AddNegCond(ASymb); 
}

/////////////////////////////////
// Assigment to another minterm.

inline VLMinTerm &VLMinTerm::operator=(const VLMinTerm &Oth) 
{ 
  assert(IsNotConst());
  Pos = Oth.Pos; 
  Neg = Oth.Neg; 
  Vars = Oth.Vars; 
  return *this;
}

///////////////////////////
// Comparison of conditions.

inline 
BooleanT VLMinTerm::operator==(const VLMinTerm &Oth) const 
{ 
  if(Pos != Oth.Pos)
    return False;
  return (Neg == Oth.Neg);
}

inline 
BooleanT VLMinTerm::operator!=(const VLMinTerm &Oth) const 
{ return !operator==(Oth); }


///////////////////////////////////////

inline 
VLMinTermC::VLMinTermC() 
{}

inline 
VLMinTermC::VLMinTermC(const VLMinTermC &oth) 
  : VLSymbC(oth) 
{}

inline 
VLMinTermC::VLMinTermC(const VLSymbC &oth) 
  : VLSymbC(oth)
{
  if(oth.IsValid()) {
    if(dynamic_cast<const VLMinTerm *>(&oth.Body()) == 0)
      (*this) = VLMinTermC(*new VLMinTerm(oth.Body()));
  }
}

inline 
VLMinTermC VLMinTermC::Intersect(const VLMinTermC &Oth) const 
{ 
  VLMinTermC ret(TRUE); 
  Body().Intersect(Oth.Body(),ret.Body());
  return ret;
}

#endif