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