/////////////////////////type declarations start/////////////////////////////

type = { Wall, Door, Other }

//////////////////////////type declarations end///////////////////////////////


////////////////////////////predicate declarations start///////////////////////

////////////////////////////discrete predicates start//////////////////////////

// The segment is of the type (query predicate); 
"!" means types are mutually exclusive and exhaustive
SegType(seg,type!)
 
// The line is of the type
LineType(line,type!)
 
// The segment is part of the line (query)
PartOf(seg, line)
 
// The segment is the start of a line (query)
StartLine(seg,line) 

// The segment is the end of a line (query)
EndLine(seg,line)
 
// There are segments aligned to this segment and preceding it (evidence)
PreviousAligned(seg)

// There are segments aligned to this segment and following it (evidence)
NextAligned(seg)

// The angle between two segments is below some threshold, 
// and so is the perpendicular distance between them (evidence)
Aligned(seg,seg)

// The distance between the nearest end points of 
// two segments is below some threshold (evidence)
Neighbors(seg,seg)

// There is no other segment's initial point between 
// the initial points of the two segments (evidence)
Consecutive(seg,seg)

// The angle between the segment and the average line it belongs to 
// is below some threshold (evidence)
SingleAligned(seg)
  
// The distance between the segment and its neighbor is below some threshold,
// and it is almost perpendicular to the average line (evidence)
SharpTurn(seg)

////////////////////////////discrete predicates end///////////////////////////


////////////////////////////numeric properties start//////////////////////////

// The x,y coordinates of the initial point of the segment (evidence)
X_si(seg) 
Y_si(seg)

// The x,y coordinates of the final point of the segment (evidence)
X_sf(seg)
Y_sf(seg)

// The x,y coordinates of the initial point of the line (query)
X_li(line)
Y_li(line)

// The x,y coordinates of the final point of the line (query)
X_lf(line)
Y_lf(line)

// The length of the segment (evidence)
Length(seg)

// The depth of the segment, i.e., the signed 
// perpendicular distance of the segment's midpoint to the nearest line (evidence)
Depth(seg)

// The angle between the segment and the nearest line
Angle(seg)

////////////////////////////numeric properties end////////////////////////////

/////////////////////////predicate declarations end///////////////////////////


//////////////////////////////formulas start//////////////////////////////////

//////////////////////////discrete formulas start/////////////////////////////

// All unit clauses are added to the MLN by default

// Unit clause for the prior probability of each type; 
// The "+t" notation directs Alchemy to learn a separate weight 
// for each grounding of t
SegType(s, +t) 

// All lines are walls in the current setting
LineType(l, Wall).

// Each wall segment is part of exactly one wall line
SegType(s,Wall) => (Exist l PartOf(s,l) ^ LineType(l,Wall))
SegType(s,Wall) ^ PartOf(s,l) ^ (l != l') => !PartOf(s,l')

// Each line consists of at least one segment
Exist s PartOf(s,l)

// Only Wall segments can be part of Wall lines
PartOf(s,l) => LineType(l,Wall) ^ SegType(s,Wall)

// Aligned wall segments tend to be part of the same wall line
SegType(s,Wall) ^ SegType(s',Wall) ^ Aligned(s,s') ^ PartOf(s,l) => PartOf(s',l)

// A segment's type is predictive of the next segment's type
SegType(s,+t) ^ Consecutive(s,s') => SegType(s',+t')

// Segments that are in sequence and aligned tend to be of the same type
SegType(s,t) ^ Consecutive(s,s') ^ Aligned(s,s') => SegType(s',t)

// A door segment's neighboring segment tends not to be a door segment
SegType(s,Door) ^ Neighbors(s,s') => !SegType(s',Door)

// If the segment is in a sharp turn, it is of type "Other"
SharpTurn(s) => SegType(s,Other)

// Single aligned segments are likely to be wall segments
SingleAligned(s) => SegType(s,Wall)

// A segment is the initial segment in the line it belongs to
// if and only if it has no previous aligned segment
PartOf(s,l) => (!PreviousAligned(s) <=> StartLine(s,l))

// A segment is the final segment in the line it belongs to 
// if and only if it has no next aligned segment
PartOf(s,l) => (!NextAligned(s) <=> EndLine(s,l))

/////////////////////////////discrete formulas end///////////////////////////


/////////////////////////////hybrid formulas start///////////////////////////

// Typical lengths and depths of door and wall segments
SegType(s, Door) * (Length(s) = 0.127)
SegType(s, Door) * (Depth(s) = 0.0233)
SegType(s, Wall) * (Length(s) = 0.345)
SegType(s, Wall) * (Depth(s) = 0.00114)

// If a segment is shorter than the typical minimum length of wall segments, 
// then it's not a wall segment; this rule is hard
(Length(s) < 0.132) => !SegType(s,Wall).

// If a segment is too long or too short for a door segment, 
// then it is not a door segment; these rules are hard
(Length(s) < 0.00218) => !SegType(s,Door).
(Length(s) > 0.317) => !SegType(s,Door).

// If a segment is too deep, it is of type "Other"
SegType(s,Other) * (Depth(s) > 0.0589)

// If a segment is too far away from a wall line at the negative side, 
// then it is of type "Other"
SegType(s,Other) * (Depth(s) < 0.000439)

// If the angle of the segment is larger than some threshold, it is of type 
// "Other"; this is a hard rule
(Angle(s) > MaxAngle) => SegType(s,Other).

// If the segment s is the start or end segment of line l then l's 
// initial/final point has the same x and y coordinates as s's.
StartLine(s,l) * [(X_si(s) = X_li(l)) + (Y_si(s) = Y_li(l))]
EndLine(s,l) * [(X_sf(s) = X_lf(l)) + (Y_sf(s) = Y_lf(l))]

// If a segment s belongs to a line l, the slope of s should be the same as 
// the slope of a line connecting the initial points of s and l, 
// and similarly for their final points.
PartOf(s,l) * [((Y_si(s) - Y_li(l))*(X_si(s) - X_sf(s)) = (Y_si(s) - Y_sf(s))*(X_si(s) - X_li(l))) + ((Y_sf(s) - Y_lf(l))*(X_si(s) - X_sf(s)) = (Y_si(s) - Y_sf(s))*(X_sf(s) - X_lf(l)))]
/////////////////////////////////hybrid formulas end/////////////////////////

/////////////////////////////formulas end////////////////////////////////////