1 2 /* 3 * File SAT2FO.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 SAT2FO.hpp 21 * Defines class SAT2FO. 22 */ 23 24 #ifndef __SAT2FO__ 25 #define __SAT2FO__ 26 27 #include "Forwards.hpp" 28 29 #include "Lib/Numbering.hpp" 30 31 #include "Kernel/Inference.hpp" 32 33 namespace SAT { 34 35 using namespace Lib; 36 using namespace Kernel; 37 38 /** 39 * Performs conversion between SAT and first-order literals 40 * assuming it is a one-to-one relation 41 * 42 * Also has other utility functions related to the correspondence 43 * between SAT and first-order literals 44 */ 45 class SAT2FO { 46 public: 47 SATLiteral toSAT(Literal* l); 48 SATClause* toSAT(Clause* cl); 49 Literal* toFO(SATLiteral sl) const; 50 51 unsigned createSpareSatVar(); 52 53 void collectAssignment(SATSolver& solver, LiteralStack& res) const; 54 SATClause* createConflictClause(LiteralStack& unsatCore, InferenceRule rule=InferenceRule::THEORY_TAUTOLOGY_SAT_CONFLICT); 55 maxSATVar() const56 unsigned maxSATVar() const { return _posMap.getNumberUpperBound(); } 57 reset()58 void reset(){ _posMap.reset(); } 59 private: 60 typedef Numbering<Literal *, 1 /* variables start from 1 */ > TwoWayMap; 61 TwoWayMap _posMap; 62 }; 63 64 } 65 66 #endif // __SAT2FO__ 67