1 2 /* 3 * File FallbackSolverWrapper.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 FallbackSolverWrapper.hpp 21 * Defines class FallbackSolverWrapper. 22 * 23 * The idea is to run two solvers next to each other 'falling back' to one if the first isn't giving 24 * us an answer. The intended setting is where the main solver is a SMT solver that can return Unknown 25 * and the fallback solver is a SAT solver that cannot 26 * 27 * @author Giles 28 */ 29 30 #ifndef __FallbackSolverWrapper__ 31 #define __FallbackSolverWrapper__ 32 33 #include "Forwards.hpp" 34 35 #include "Lib/DArray.hpp" 36 #include "Lib/DHMap.hpp" 37 #include "Lib/DHSet.hpp" 38 #include "Lib/ScopedPtr.hpp" 39 #include "Lib/Stack.hpp" 40 41 #include "SATSolver.hpp" 42 43 namespace SAT { 44 45 using namespace Lib; 46 47 class FallbackSolverWrapper : public SATSolver { 48 public: 49 CLASS_NAME(FallbackSolverWrapper); 50 USE_ALLOCATOR(FallbackSolverWrapper); 51 52 FallbackSolverWrapper(SATSolver* inner,SATSolver* fallback); 53 getRefutation()54 virtual SATClause* getRefutation() override { 55 if(_usingFallback){ 56 return _fallback->getRefutation(); 57 } 58 return _inner->getRefutation(); 59 } getRefutationPremiseList()60 virtual SATClauseList* getRefutationPremiseList() override { 61 if(_usingFallback){ 62 return _fallback->getRefutationPremiseList(); 63 } 64 return _inner->getRefutationPremiseList(); 65 } randomizeForNextAssignment(unsigned maxVar)66 virtual void randomizeForNextAssignment(unsigned maxVar) override { 67 _fallback->randomizeForNextAssignment(maxVar); 68 _inner->randomizeForNextAssignment(maxVar); 69 } 70 71 virtual void addClause(SATClause* cl) override; 72 virtual Status solve(unsigned conflictCountLimit) override; 73 virtual VarAssignment getAssignment(unsigned var) override; 74 isZeroImplied(unsigned var)75 virtual bool isZeroImplied(unsigned var) override { 76 CALL("FallbackSolverWrapper::isZeroImplied"); 77 ASS_G(var,0); ASS_LE(var,_varCnt); 78 79 if(_usingFallback){ 80 return _fallback->isZeroImplied(var); 81 } 82 83 // alternatively, we could directly refer to _inner, it must handle variables up to _varCnt as well 84 return _inner->isZeroImplied(var); 85 } collectZeroImplied(SATLiteralStack & acc)86 virtual void collectZeroImplied(SATLiteralStack& acc) override { 87 if(_usingFallback){ 88 _fallback->collectZeroImplied(acc); 89 return; 90 } 91 _inner->collectZeroImplied(acc); 92 } 93 getZeroImpliedCertificate(unsigned var)94 virtual SATClause* getZeroImpliedCertificate(unsigned var) override { 95 if(_usingFallback){ 96 return _fallback->getZeroImpliedCertificate(var); 97 } 98 return _inner->getZeroImpliedCertificate(var); 99 } 100 ensureVarCount(unsigned newVarCnt)101 virtual void ensureVarCount(unsigned newVarCnt) override { 102 _inner->ensureVarCount(newVarCnt); 103 _fallback->ensureVarCount(newVarCnt); 104 _varCnt=max(_varCnt,newVarCnt); 105 } 106 107 newVar()108 virtual unsigned newVar() override { 109 CALL("FallbackSolverWrapper::newVar"); 110 111 ALWAYS(_inner->newVar() == ++_varCnt); 112 ALWAYS(_fallback->newVar() == _varCnt); 113 return _varCnt; 114 } 115 suggestPolarity(unsigned var,unsigned pol)116 virtual void suggestPolarity(unsigned var,unsigned pol) override { 117 _inner->suggestPolarity(var,pol); 118 _fallback->suggestPolarity(var,pol); 119 } recordSource(unsigned var,Literal * lit)120 virtual void recordSource(unsigned var, Literal* lit) override { 121 _inner->recordSource(var,lit); 122 _fallback->recordSource(var,lit); 123 } 124 125 private: 126 127 SATSolverSCP _inner; 128 SATSolverSCP _fallback; 129 130 bool _usingFallback; 131 132 unsigned _varCnt; 133 134 }; 135 136 } 137 138 #endif // __FallbackSolverWrapper__ 139