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