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