forked from vprover/vampire
-
Notifications
You must be signed in to change notification settings - Fork 0
/
FallbackSolverWrapper.cpp
94 lines (79 loc) · 2.13 KB
/
FallbackSolverWrapper.cpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
/*
* File FallbackSolverWrapper.cpp.
*
* This file is part of the source code of the software program
* Vampire. It is protected by applicable
* copyright laws.
*
* This source code is distributed under the licence found here
* https://vprover.github.io/license.html
* and in the source directory
*
* In summary, you are allowed to use Vampire for non-commercial
* purposes but not allowed to distribute, modify, copy, create derivatives,
* or use in competitions.
* For other uses of Vampire please contact developers for a different
* licence, which we will make an effort to provide.
*/
/**
* @file FallbackSolverWrapper.cpp
* Implements class FallbackSolverWrapper.
*/
#include "Lib/Environment.hpp"
#include "Shell/Statistics.hpp"
#include "Debug/RuntimeStatistics.hpp"
#include "SAT/SATClause.hpp"
#include "FallbackSolverWrapper.hpp"
namespace SAT
{
FallbackSolverWrapper::FallbackSolverWrapper(SATSolver* inner,SATSolver* fallback)
: _inner(inner), _fallback(fallback), _usingFallback(false), _varCnt(0)
{
CALL("FallbackSolverWrapper::FallbackSolverWrapper");
}
/**
* Add a clause to sat solver
*
* @author Giles
*/
void FallbackSolverWrapper::addClause(SATClause* cl)
{
CALL("FallbackSolverWrapper::addClause");
_inner->addClause(cl);
_fallback->addClause(cl);
}
/**
*
* @author Giles
*/
SATSolver::Status FallbackSolverWrapper::solve(unsigned conflictCountLimit)
{
CALL("FallbackSolverWrapper::solve");
// Currently always run the _inner solver to see if we can use it
Status status = _inner->solve(conflictCountLimit);
// Check if we need to use _fallback
if(status == Status::UNKNOWN){
status = _fallback->solve(conflictCountLimit);
_usingFallback = true;
ASS(status != Status::UNKNOWN);
env.statistics->smtFallbacks++;
}
else{
_usingFallback = false;
}
return status;
}
/**
*
* @author Giles
*/
SATSolver::VarAssignment FallbackSolverWrapper::getAssignment(unsigned var)
{
CALL("FallbackSolverWrapper::getAssignment");
ASS_G(var,0); ASS_LE(var,_varCnt);
if(_usingFallback){
return _fallback->getAssignment(var);
}
return _inner->getAssignment(var);
}
}