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