1 
2 /*
3  * File BFNTMainLoop.hpp.
4  *
5  * This file is part of the source code of the software program
6  * Vampire. It is protected by applicable
7  * copyright laws.
8  *
9  * This source code is distributed under the licence found here
10  * https://vprover.github.io/license.html
11  * and in the source directory
12  *
13  * In summary, you are allowed to use Vampire for non-commercial
14  * purposes but not allowed to distribute, modify, copy, create derivatives,
15  * or use in competitions.
16  * For other uses of Vampire please contact developers for a different
17  * licence, which we will make an effort to provide.
18  */
19 /**
20  * @file BFNTMainLoop.hpp
21  * Defines class BFNTMainLoop.
22  */
23 
24 #ifndef __BFNTMainLoop__
25 #define __BFNTMainLoop__
26 
27 #include "Lib/Portability.hpp"
28 
29 #include "Forwards.hpp"
30 
31 #include "Lib/SmartPtr.hpp"
32 
33 #include "Kernel/MainLoop.hpp"
34 
35 #include "BFNT.hpp"
36 #include "Options.hpp"
37 
38 namespace Shell {
39 
40 using namespace Lib;
41 using namespace Kernel;
42 
43 class BFNTMainLoop : public MainLoop {
44 public:
45   CLASS_NAME(BFNTMainLoop);
46   USE_ALLOCATOR(BFNTMainLoop);
47 
48   BFNTMainLoop(Problem& prb, const Options& opt);
49 
50 protected:
51   virtual void init();
52   virtual MainLoopResult runImpl();
53 
54 private:
55 
56   /** If problem has sorts, we set this to true and just terminate with unknown
57    * (at least until we have proper handling of sorts in BFNT) */
58   bool _hasSorts;
59 
60   void runChild(size_t modelSize) __attribute__((noreturn));
61   MainLoopResult spawnChild(size_t modelSize);
62 
63   Options _childOpts;
64   /** the input transformer */
65   BFNT _bfnt;
66 };
67 
68 }
69 
70 #endif // __BFNTMainLoop__
71