/*
  This Formula specificatin models a problem in graph theory. It tries to find 
  a Eulerian walk within a specified graph. The problem is to find a walk through 
  the graph with the following properties:
  
  - all edges in the graph must be used
  - every edge must be used only once
  
  A well known example of this problem is the so called German "Das-ist-das-Haus-vom-Nikolaus"
  problem, which is modeled within this file.
*/

domain EulerWay
{
  primitive BaseEdge ::= (x:PosInteger, y:PosInteger).
  primitive SolutionEdge ::= (pos:PosInteger, x : PosInteger, y : PosInteger).
  
  // Make sure we have used all BaseEdge terms in the solution
  usedBaseEdge ::= (x:PosInteger, y:PosInteger).
  usedBaseEdge(x,y) :- BaseEdge(x,y), SolutionEdge(_,x,y).
  usedBaseEdge(x,y) :- BaseEdge(x,y), SolutionEdge(_,y,x).
  unusedBaseEdge := BaseEdge(x,y), fail usedBaseEdge(x,y).

  // Make sure our index values are one based and not bigger than the number of base edges
  indexTooBig := SolutionEdge(x,_,_), x > count(BaseEdge(_,_)).
 
  // Make sure that no index is used twice
  doubleIndex := s1 is SolutionEdge, s2 is SolutionEdge, s1 != s2, s1.pos = s2.pos.
  
  // Exclude edges that don't line up
  //wrongSequence := SolutionEdge(x, Edge(_,b)), SolutionEdge(y, Edge(c,_)), y = x + 1, b != c.
  wrongSequence := SolutionEdge(pos1,_,y1), SolutionEdge(pos2,x2,_), pos2 = pos1 + 1, y1 != x2.
  
  // Avoid using edges twice
  doubleEdge := SolutionEdge(pos1,x,y), SolutionEdge(pos2,x,y), pos1 != pos2.
  
  // Exclude mirrors of already used edges
  mirrorEdge := SolutionEdge(_,x,y), SolutionEdge(_,y,x).
  
  conforms := !unusedBaseEdge & !indexTooBig & !doubleIndex & !wrongSequence & !doubleEdge & !mirrorEdge.
}

/*
   Nikolaus graph:

     5
    / \
   3---4
   |\ /|
   | X |
   |/ \|
   1---2
*/

partial model nikolaus2 of EulerWay
{
    BaseEdge(1,2)
    BaseEdge(1,3)
    BaseEdge(1,4)
    BaseEdge(2,4)
    BaseEdge(2,3)
    BaseEdge(3,4)
    BaseEdge(3,5)
    BaseEdge(4,5)
    SolutionEdge(1,_,_)
    SolutionEdge(2,_,_)
    SolutionEdge(3,_,_)
    SolutionEdge(4,_,_)
    SolutionEdge(5,_,_)
    SolutionEdge(6,_,_)
    SolutionEdge(7,_,_)
    SolutionEdge(8,_,_)
}