1 
2 /*
3  * File InterpretedEvaluation.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 InterpretedEvaluation.hpp
21  * Defines class InterpretedEvaluation.
22  */
23 
24 
25 #ifndef __InterpretedEvaluation__
26 #define __InterpretedEvaluation__
27 
28 #include "Forwards.hpp"
29 
30 #include "Lib/DHMap.hpp"
31 
32 #include "Kernel/InterpretedLiteralEvaluator.hpp"
33 #include "Kernel/Theory.hpp"
34 
35 #include "InferenceEngine.hpp"
36 
37 namespace Inferences {
38 
39 class InterpretedEvaluation
40 : public ImmediateSimplificationEngine
41 {
42 public:
43   CLASS_NAME(InterpretedEvaluation);
44   USE_ALLOCATOR(InterpretedEvaluation);
45 
46   InterpretedEvaluation(bool doNormalize, Ordering& ordering);
47   virtual ~InterpretedEvaluation();
48 
49   Clause* simplify(Clause* cl);
50 private:
51   bool simplifyLiteral(Literal* lit, bool& constant, Literal*& res, bool& constantTrue,Stack<Literal*>& sideConditions);
52 
53   InterpretedLiteralEvaluator* _simpl;
54   Ordering& _ordering;
55 };
56 
57 };
58 
59 #endif /* __InterpretedEvaluation__ */
60