--  Programmed by Jedidiah Barber
--  Licensed under the Sunset License v1.0

--  See license.txt for further details


--  Taken from Algebra 1, Glencoe/McGraw-Hill, New York, New York, 1998
--  pg. 411, Problem 56:

--  There are 8 houses on McArthur St, all in a row. These houses
--  are numbered from 1 to 8.

--  Allison, whose house number is greater than 2, lives next door
--  to her best friend, Adrienne. Belinda, whose house number is
--  greater than 5, lives 2 doors away from her boyfriend, Benito.
--  Cheri, whose house number is greater than Benito's, lives
--  three doors away from her piano teacher, Mr. Crawford. Daryl,
--  whose house number is less than 4, lives 4 doors from his
--  teammate, Don.

--  Who lives in each house?


with

    Ada.Text_IO,
    Kompsos.Math,
    Kompsos.Pretty_Print;


procedure Houses is

    package TIO renames Ada.Text_IO;


    --  Only using the Math subpackage so no need for anything fancier than Boolean.
    package BKomp is new Kompsos (Boolean);
    use BKomp;

    package Math is new BKomp.Math (False, True);


    --  Since the following subprograms are procedures, they cannot be used
    --  with Conjunct. Some don't take a Term_Array for inputs either.

    --  But that's alright because we aren't conjuncting things here anyway.

    procedure Unique
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        if Inputs'Length <= 1 then
            return;
        end if;
        for Index in Inputs'First + 1 .. Inputs'Last loop
            This := Disjunct
               (Math.LT (This, Inputs (Inputs'First) & Inputs (Index)),
                Math.GT (This, Inputs (Inputs'First) & Inputs (Index)));
        end loop;
        Unique (This, Inputs (Inputs'First + 1 .. Inputs'Last));
    end Unique;


    procedure Within_Range
           (This             : in out Goal;
            Value, Low, High : in     Term) is
    begin
        Math.GTE (This, Value & Low);
        Math.LTE (This, Value & High);
    end Within_Range;


    procedure Doors_From
           (This                     : in out Goal;
            Person_A, Diff, Person_B : in     Term) is
    begin
        This := Disjunct
           (Math.Add (This, Person_A & Diff & Person_B),
            Math.Subtract (This, Person_A & Diff & Person_B));
    end Doors_From;


    One   : constant Term := Math.Build (1);
    Two   : constant Term := Math.Build (2);
    Three : constant Term := Math.Build (3);
    Four  : constant Term := Math.Build (4);
    Five  : constant Term := Math.Build (5);
    Six   : constant Term := Math.Build (6);
    Seven : constant Term := Math.Build (7);
    Eight : constant Term := Math.Build (8);


    Relation : Goal := Empty_Goal;

    Allison     : constant Term := Relation.Fresh;
    Adrienne    : constant Term := Relation.Fresh;
    Belinda     : constant Term := Relation.Fresh;
    Benito      : constant Term := Relation.Fresh;
    Cheri       : constant Term := Relation.Fresh;
    Mr_Crawford : constant Term := Relation.Fresh;
    Daryl       : constant Term := Relation.Fresh;
    Don         : constant Term := Relation.Fresh;

    Result : State;

begin

    Within_Range (Relation, Allison, Three, Eight);
    Within_Range (Relation, Adrienne, One, Eight);
    Within_Range (Relation, Belinda, Six, Eight);
    Within_Range (Relation, Benito, One, Eight);
    Within_Range (Relation, Cheri, Two, Eight);
    Within_Range (Relation, Mr_Crawford, One, Eight);
    Within_Range (Relation, Daryl, One, Three);
    Within_Range (Relation, Don, One, Eight);

    Unique (Relation, Allison & Adrienne & Belinda & Benito & Cheri & Mr_Crawford & Daryl & Don);

    Doors_From (Relation, Allison, One, Adrienne);
    Doors_From (Relation, Belinda, Two, Benito);
    Doors_From (Relation, Cheri, Three, Mr_Crawford);
    Doors_From (Relation, Daryl, Four, Don);

    Math.GT (Relation, Cheri & Benito);

    Result := Relation.Run;

    TIO.Put_Line ("Allison:"     & Integer'Image (Math.Value (Allison.Resolve (Result))));
    TIO.Put_Line ("Adrienne:"    & Integer'Image (Math.Value (Adrienne.Resolve (Result))));
    TIO.Put_Line ("Belinda:"     & Integer'Image (Math.Value (Belinda.Resolve (Result))));
    TIO.Put_Line ("Benito:"      & Integer'Image (Math.Value (Benito.Resolve (Result))));
    TIO.Put_Line ("Cheri:"       & Integer'Image (Math.Value (Cheri.Resolve (Result))));
    TIO.Put_Line ("Mr Crawford:" & Integer'Image (Math.Value (Mr_Crawford.Resolve (Result))));
    TIO.Put_Line ("Daryl:"       & Integer'Image (Math.Value (Daryl.Resolve (Result))));
    TIO.Put_Line ("Don:"         & Integer'Image (Math.Value (Don.Resolve (Result))));

end Houses;