Symbolic solver: add a timeout feature

pmderodat · raph-amiard · commit e90d03f90f7a · 2022-03-30T14:23:21.000Z
TN: SB20-024
diff --git a/support/langkit_support-adalog-generic_main_support.adb b/support/langkit_support-adalog-generic_main_support.adb
@@ -71,7 +71,7 @@ package body Langkit_Support.Adalog.Generic_Main_Support is
    -- Solve_All --
    ---------------
 
-   procedure Solve_All (Rel : Relation) is
+   procedure Solve_All (Rel : Relation; Timeout : Natural := 0) is
 
       type Var_And_Val is record
          Var     : Refs.Logic_Var;
@@ -203,10 +203,12 @@ package body Langkit_Support.Adalog.Generic_Main_Support is
 
       procedure Run_Solve (Opts : Solve_Options_Type) is
       begin
-         Solve (Rel, Solution_Callback'Access, Opts);
+         Solve (Rel, Solution_Callback'Access, Opts, Timeout);
       exception
          when Early_Binding_Error =>
             Put_Line ("Resolution failed with Early_Binding_Error");
+         when Timeout_Error =>
+            Put_Line ("Resolution failed with Timeout_Error");
          when Exc : others =>
             Put_Line ("  -> " & Exception_Name (Exc)
                       & ": " & Exception_Message (Exc));
diff --git a/support/langkit_support-adalog-generic_main_support.ads b/support/langkit_support-adalog-generic_main_support.ads
@@ -113,7 +113,7 @@ package Langkit_Support.Adalog.Generic_Main_Support is
    function Logic_False return Relation is (+Create_False);
    function Logic_True return Relation is (+Create_True);
 
-   procedure Solve_All (Rel : Relation);
+   procedure Solve_All (Rel : Relation; Timeout : Natural := 0);
 
    procedure Run_Main (Main : access procedure);
    procedure Setup_Traces;
diff --git a/support/langkit_support-adalog-solver.adb b/support/langkit_support-adalog-solver.adb
@@ -310,8 +310,12 @@ package body Langkit_Support.Adalog.Solver is
       Timeout           : Natural := 0) is
    begin
       case Self.Kind is
-         when Symbolic => Sym_Solve.Solve
-              (Self.Symbolic_Relation, Solution_Callback, Solve_Options);
+         when Symbolic =>
+            Sym_Solve.Solve
+              (Self.Symbolic_Relation,
+               Solution_Callback,
+               Solve_Options,
+               Timeout);
          when State_Machine =>
             while Abstract_Relation.Solve (Self.SSM_Relation, Timeout) loop
                declare
@@ -354,7 +358,7 @@ package body Langkit_Support.Adalog.Solver is
       case Self.Kind is
          when Symbolic =>
             return Sym_Solve.Solve_First
-              (Self.Symbolic_Relation, Solve_Options);
+              (Self.Symbolic_Relation, Solve_Options, Timeout);
          when State_Machine =>
             return Abstract_Relation.Solve (Self.SSM_Relation, Timeout);
          when None => raise Constraint_Error with "Cannot solve No_Relation";
diff --git a/support/langkit_support-adalog-solver.ads b/support/langkit_support-adalog-solver.ads
@@ -79,8 +79,10 @@ package Langkit_Support.Adalog.Solver is
    --  process.
    --
    --  For the state machine solver, ``Timeout`` determines the maximum number
-   --  of solving step to run before aborting the solver. If left to 0 or for
-   --  the symbolic solver, no timeout applies.
+   --  of solving step to run before aborting the solver. For the symbolic
+   --  solver, ``Timeout`` determines the maximum of times we evaluate atoms
+   --  before aborting the solver. In both cases, if left to 0, no timeout
+   --  applies.
 
    function Solve_First
      (Self          : Relation;
@@ -91,8 +93,10 @@ package Langkit_Support.Adalog.Solver is
    --  way to configure the resolution process.
    --
    --  For the state machine solver, ``Timeout`` determines the maximum number
-   --  of solving step to run before aborting the solver. If left to 0 or for
-   --  the symbolic solver, no timeout applies.
+   --  of solving step to run before aborting the solver. For the symbolic
+   --  solver, ``Timeout`` determines the maximum of times we evaluate atoms
+   --  before aborting the solver. In both cases, if left to 0, no timeout
+   --  applies.
 
    ---------------------------
    -- Relation constructors --
diff --git a/support/langkit_support-adalog-symbolic_solver.adb b/support/langkit_support-adalog-symbolic_solver.adb
@@ -186,22 +186,6 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
    --  ``Has_Orphan`` is set to whether at least one atom is an "orphan", that
    --  is to say it is not part of the resulting sorted collection.
 
-   function Evaluate_Atoms
-     (Sorted_Atoms : Atomic_Relation_Vectors.Elements_Array) return Boolean;
-   --  Evaluate the given sequence of sorted atoms (see ``Topo_Sort``) and
-   --  return whether they are all satisfied: if they are, the logic variables
-   --  are assigned values, so it is possible to invoke the user callback for
-   --  solutions.
-
-   function Has_Contradiction
-     (Atoms, Unifies : Atomic_Relation_Vector;
-      Vars           : Logic_Var_Array;
-      Sort_Ctx       : in out Sort_Context) return Boolean;
-   --  Return whether the given sequence of atoms contains a contradiction,
-   --  i.e. if two or more of its atoms make each other unsatisfied. This
-   --  function works even for incomplete sequences, for instance when one atom
-   --  uses a variable that no atom defines.
-
    type Solving_Context is record
       Cb : Callback_Type;
       --  User callback, to be called when a solution is found. Returns whether
@@ -232,6 +216,10 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
       Anys : Any_Relation_Vector;
       --  Remaining list of ``Any`` relations to traverse
 
+      Timeout : Natural;
+      --  Number of times left we allow ourselves to evaluate an atom before
+      --  aborting the solver. If 0, no timeout applies.
+
       Cut_Dead_Branches : Boolean := False;
       --  Optimization that will cut branches that necessarily contain falsy
       --  solutions.
@@ -263,6 +251,23 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
    procedure Destroy (Ctx : in out Solving_Context);
    --  Destroy a solving context, and associated data
 
+   function Evaluate_Atoms
+     (Ctx          : in out Solving_Context;
+      Sorted_Atoms : Atomic_Relation_Vectors.Elements_Array) return Boolean;
+   --  Evaluate the given sequence of sorted atoms (see ``Topo_Sort``) and
+   --  return whether they are all satisfied: if they are, the logic variables
+   --  are assigned values, so it is possible to invoke the user callback for
+   --  solutions.
+
+   function Has_Contradiction
+     (Atoms, Unifies : Atomic_Relation_Vector;
+      Vars           : Logic_Var_Array;
+      Ctx            : in out Solving_Context) return Boolean;
+   --  Return whether the given sequence of atoms contains a contradiction,
+   --  i.e. if two or more of its atoms make each other unsatisfied. This
+   --  function works even for incomplete sequences, for instance when one atom
+   --  uses a variable that no atom defines.
+
    function Solve_Compound
      (Self : Compound_Relation; Ctx : in out Solving_Context) return Boolean;
    --  Look for valid solutions in ``Self`` & ``Ctx``. Return whether to
@@ -829,13 +834,60 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
       return Sorted_Atoms (1 .. Last_Atom_Index);
    end Topo_Sort;
 
+   -------------
+   -- Destroy --
+   -------------
+
+   procedure Destroy (Sort_Ctx : in out Sort_Context) is
+   begin
+      Sort_Ctx.N_Preds.Destroy;
+      Sort_Ctx.Working_Set.Destroy;
+      for Atoms of Sort_Ctx.Using_Atoms.all loop
+         Atoms.Destroy;
+      end loop;
+      Free (Sort_Ctx.Using_Atoms);
+   end Destroy;
+
+   -------------
+   -- Destroy --
+   -------------
+
+   procedure Destroy (Ctx : in out Solving_Context) is
+   begin
+      Ctx.Unifies.Destroy;
+      Ctx.Atoms.Destroy;
+      Ctx.Anys.Destroy;
+      Destroy (Ctx.Sort_Ctx);
+
+      --  Cleanup logic vars for future solver runs using them. Note that no
+      --  aliasing information is supposed to be left at this stage.
+
+      for V of Ctx.Vars.all loop
+         Reset (V);
+         Set_Id (V, 0);
+      end loop;
+      Free (Ctx.Vars);
+   end Destroy;
+
    --------------------
    -- Evaluate_Atoms --
    --------------------
 
    function Evaluate_Atoms
-     (Sorted_Atoms : Atomic_Relation_Vectors.Elements_Array) return Boolean is
+     (Ctx          : in out Solving_Context;
+      Sorted_Atoms : Atomic_Relation_Vectors.Elements_Array) return Boolean is
    begin
+      --  If we have a timeout, apply it
+
+      if Ctx.Timeout > 0 then
+         if Sorted_Atoms'Length > Ctx.Timeout then
+            raise Timeout_Error;
+         end if;
+         Ctx.Timeout := Ctx.Timeout - Sorted_Atoms'Length;
+      end if;
+
+      --  Evaluate each individual atom
+
       for Atom of Sorted_Atoms loop
          if not Solve_Atomic (Atom) then
             if Solv_Trace.Is_Active then
@@ -856,28 +908,28 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
    function Has_Contradiction
      (Atoms, Unifies : Atomic_Relation_Vector;
       Vars           : Logic_Var_Array;
-      Sort_Ctx       : in out Sort_Context) return Boolean
+      Ctx            : in out Solving_Context) return Boolean
    is
       Had_Exception : Boolean := False;
       Exc           : Exception_Occurrence;
 
       Result : Boolean;
    begin
-      Sort_Ctx.Has_Contradiction_Counter :=
-        Sort_Ctx.Has_Contradiction_Counter + 1;
+      Ctx.Sort_Ctx.Has_Contradiction_Counter :=
+        Ctx.Sort_Ctx.Has_Contradiction_Counter + 1;
 
       if Solv_Trace.Is_Active then
          Solv_Trace.Increase_Indent
            ("Looking for a contradiction (number"
-            & Sort_Ctx.Has_Contradiction_Counter'Image & ")");
+            & Ctx.Sort_Ctx.Has_Contradiction_Counter'Image & ")");
          Solv_Trace.Trace (Image (Atoms));
       end if;
 
       declare
          use Atomic_Relation_Vectors;
          Dummy        : Boolean;
          Sorted_Atoms : constant Elements_Array :=
-           Topo_Sort (Atoms, Unifies, Vars, Sort_Ctx, Dummy);
+           Topo_Sort (Atoms, Unifies, Vars, Ctx.Sort_Ctx, Dummy);
       begin
          if Solv_Trace.Is_Active then
             Solv_Trace.Trace ("After partial topo sort");
@@ -897,7 +949,7 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
          --  the order in which the solver finds solutions.
 
          begin
-            Result := not Evaluate_Atoms (Sorted_Atoms);
+            Result := not Evaluate_Atoms (Ctx, Sorted_Atoms);
          exception
             when E : others =>
                Save_Occurrence (Exc, E);
@@ -927,41 +979,6 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
       end;
    end Has_Contradiction;
 
-   -------------
-   -- Destroy --
-   -------------
-
-   procedure Destroy (Sort_Ctx : in out Sort_Context) is
-   begin
-      Sort_Ctx.N_Preds.Destroy;
-      Sort_Ctx.Working_Set.Destroy;
-      for Atoms of Sort_Ctx.Using_Atoms.all loop
-         Atoms.Destroy;
-      end loop;
-      Free (Sort_Ctx.Using_Atoms);
-   end Destroy;
-
-   -------------
-   -- Destroy --
-   -------------
-
-   procedure Destroy (Ctx : in out Solving_Context) is
-   begin
-      Ctx.Unifies.Destroy;
-      Ctx.Atoms.Destroy;
-      Ctx.Anys.Destroy;
-      Destroy (Ctx.Sort_Ctx);
-
-      --  Cleanup logic vars for future solver runs using them. Note that no
-      --  aliasing information is supposed to be left at this stage.
-
-      for V of Ctx.Vars.all loop
-         Reset (V);
-         Set_Id (V, 0);
-      end loop;
-      Free (Ctx.Vars);
-   end Destroy;
-
    --------------
    -- Used_Var --
    --------------
@@ -1140,7 +1157,7 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
 
             --  Once the topological sort has been done, we just have to solve
             --  every relation in order. Abort if one doesn't solve.
-            if not Evaluate_Atoms (Sorted_Atoms) then
+            if not Evaluate_Atoms (Ctx, Sorted_Atoms) then
                return Cleanup (True);
             end if;
 
@@ -1351,7 +1368,7 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
 
             Create_Aliases;
             if Has_Contradiction
-              (Ctx.Atoms, Ctx.Unifies, Ctx.Vars.all, Ctx.Sort_Ctx)
+              (Ctx.Atoms, Ctx.Unifies, Ctx.Vars.all, Ctx)
             then
                if Solv_Trace.Active then
                   Solv_Trace.Trace ("Aborting due to exp res optim");
@@ -1426,7 +1443,8 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
      (Self              : Relation;
       Solution_Callback : access function
         (Vars : Logic_Var_Array) return Boolean;
-      Solve_Options     : Solve_Options_Type := Default_Options)
+      Solve_Options     : Solve_Options_Type := Default_Options;
+      Timeout           : Natural)
    is
       PRel   : Prepared_Relation;
       Rel    : Relation renames PRel.Rel;
@@ -1454,6 +1472,7 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
 
       PRel := Prepare_Relation (Self);
       Ctx := Create (Solution_Callback'Unrestricted_Access.all, PRel.Vars);
+      Ctx.Timeout := Timeout;
       Ctx.Cut_Dead_Branches := Solve_Options.Cut_Dead_Branches;
 
       declare
@@ -1506,7 +1525,8 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
 
    function Solve_First
      (Self          : Relation;
-      Solve_Options : Solve_Options_Type := Default_Options) return Boolean
+      Solve_Options : Solve_Options_Type := Default_Options;
+      Timeout       : Natural) return Boolean
    is
       Ret : Boolean := False;
 
@@ -1550,7 +1570,7 @@ package body Langkit_Support.Adalog.Symbolic_Solver is
       end Callback;
 
    begin
-      Solve (Self, Callback'Access, Solve_Options);
+      Solve (Self, Callback'Access, Solve_Options, Timeout);
       if Tracked_Vars /= null then
          for TV of Tracked_Vars.all loop
             if TV.Defined then
diff --git a/support/langkit_support-adalog-symbolic_solver.ads b/support/langkit_support-adalog-symbolic_solver.ads
@@ -57,19 +57,27 @@ package Langkit_Support.Adalog.Symbolic_Solver is
      (Self              : Relation;
       Solution_Callback : access function
         (Vars : Logic_Var_Array) return Boolean;
-      Solve_Options     : Solve_Options_Type := Default_Options);
+      Solve_Options     : Solve_Options_Type := Default_Options;
+      Timeout           : Natural);
    --  Run the solver on the ``Self`` relation. For every solution found, call
    --  ``Solution_Callback`` with the variables involved in ``Self``, and
    --  continue looking for other solutions iff it returns True. See
    --  ``Solve_Options Type`` for the available way to configure the resolution
    --  process.
+   --
+   --  ``Timeout`` determines the maximum of times we evaluate atoms before
+   --  aborting the solver. If left to 0, no timeout applies.
 
    function Solve_First
      (Self          : Relation;
-      Solve_Options : Solve_Options_Type := Default_Options) return Boolean;
+      Solve_Options : Solve_Options_Type := Default_Options;
+      Timeout       : Natural) return Boolean;
    --  Run the solver on the ``Self`` relation. Return whether there is at
    --  least one valid solution. See ``Solve_Options Type`` for the available
    --  way to configure the resolution process.
+   --
+   --  ``Timeout`` determines the maximum of times we evaluate atoms before
+   --  aborting the solver. If left to 0, no timeout applies.
 
    function Image (Self : Relation) return String;
    --  Return a textual representation of ``Self`` as a multi-line string
diff --git a/testsuite/tests/adalog/timeout/main.adb b/testsuite/tests/adalog/timeout/main.adb
diff --git a/testsuite/tests/adalog/timeout/test.out b/testsuite/tests/adalog/timeout/test.out
diff --git a/testsuite/tests/adalog/timeout/test.yaml b/testsuite/tests/adalog/timeout/test.yaml
