1 
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4 
5 --*/
6 
7 using System;
8 using System.Collections.Generic;
9 using System.Linq;
10 using System.Text;
11 using System.Threading;
12 using Microsoft.Z3;
13 
14 namespace Microsoft.SolverFoundation.Plugin.Z3
15 {
16     /// <summary>
17     /// Thread that will wait until the query abort function returns true or
18     /// the stop method is called. If the abort function returns true at some
19     /// point it will issue a softCancel() call to Z3.
20     /// </summary>
21     internal class AbortWorker
22     {
23         #region Private Members
24 
25         /// <summary>The Z3 solver</summary>
26         private Microsoft.Z3.Context _context;
27         /// <summary>The abort function to use to check if we are aborted</summary>
28         private Func<bool> _QueryAbortFunction;
29         /// <summary>Flag indicating that worker should stop</summary>
30         private bool _stop = false;
31         /// <summary>Flag indicating that we have been sent an abort signal</summary>
32         private bool _aborted = false;
33 
34         #endregion Private Members
35 
36         #region Construction
37 
38         /// <summary>
39         /// Worker constructor taking a Z3 instance and a function to periodically
40         /// check for aborts.
41         /// </summary>
42         /// <param name="z3">Z3 instance</param>
43         /// <param name="queryAbortFunction">method to call to check for aborts</param>
AbortWorker(Context context, Func<bool> queryAbortFunction)44         public AbortWorker(Context context, Func<bool> queryAbortFunction)
45         {
46             _context = context;
47             _QueryAbortFunction = queryAbortFunction;
48         }
49 
50         #endregion Construction
51 
52         #region Public Methods
53 
54         /// <summary>
55         /// Stop the abort worker.
56         /// </summary>
Stop()57         public void Stop()
58         {
59             _stop = true;
60         }
61 
62         /// <summary>
63         /// Is true if we have been aborted.
64         /// </summary>
65         public bool Aborted
66         {
67             get
68             {
69                 return _aborted;
70             }
71         }
72 
73         /// <summary>
74         /// Starts the abort worker. The worker checks the abort method
75         /// periodically until either it is stopped by a call to the Stop()
76         /// method or it gets an abort signal. In the latter case it will
77         /// issue a soft abort signal to Z3.
78         /// </summary>
Start()79         public void Start()
80         {
81             // We go until someone stops us
82             _stop = false;
83             while (!_stop && !_QueryAbortFunction())
84             {
85                 // Wait for a while
86                 Thread.Sleep(10);
87             }
88             // If we were stopped on abort, cancel z3
89             if (!_stop)
90             {
91                 _context.Interrupt();
92                 _aborted = true;
93             }
94         }
95 
96         #endregion Public Methods
97     }
98 }
99