1 2 /* 3 * File CPAInterpolator.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 CPAInterpolator.hpp 21 * Defines class CPAInterpolator. 22 */ 23 24 #ifndef __CPAInterpolator__ 25 #define __CPAInterpolator__ 26 27 #include "Forwards.hpp" 28 29 #include "Kernel/Problem.hpp" 30 #include "Kernel/Sorts.hpp" 31 32 namespace VUtils { 33 34 using namespace Lib; 35 using namespace Kernel; 36 37 38 class CPAInterpolator { 39 public: 40 int perform(unsigned argc, char** argv); 41 private: 42 void printUsageAndExit(unsigned argc, char** argv); 43 void declareColors(); 44 void loadFormulas(); 45 void doProving(); 46 void displayResult(); 47 48 void loadFormula(vstring fname); 49 50 typedef pair<vstring,unsigned> FuncSpec; 51 typedef DHSet<FuncSpec> FuncSet; 52 typedef DHMap<FuncSpec,BaseType*> FuncTypeMap; 53 54 void collectSMTLIBFileFunctions(vstring fname, FuncSet& acc); 55 56 57 Stack<vstring> _leftFNames; 58 Stack<vstring> _rightFNames; 59 60 FuncTypeMap _funcTypes; 61 62 Problem _prb; 63 UnitList* _forms; 64 UnitList* _defs; 65 66 private: 67 //slicing 68 69 typedef DHSet<vstring> StrategySet; 70 typedef Stack<vstring> Schedule; 71 72 bool runSchedule(Schedule& schedule,StrategySet& ss,bool fallback); 73 bool runSlice(vstring slice, unsigned ds); 74 bool runSlice(Options& opt); 75 void childRun(Options& opt); 76 77 bool tryMakeAdmissibleStrategy(Options& opt); 78 79 }; 80 81 82 } 83 84 #endif // __CPAInterpolator__ 85