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