aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/TimingSolver.h6
-rw-r--r--lib/Solver/CachingSolver.cpp10
-rw-r--r--lib/Solver/CexCachingSolver.cpp10
-rw-r--r--lib/Solver/IncompleteSolver.cpp9
-rw-r--r--lib/Solver/IndependentSolver.cpp10
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp7
-rw-r--r--lib/Solver/QueryLoggingSolver.h3
-rw-r--r--lib/Solver/Solver.cpp28
8 files changed, 76 insertions, 7 deletions
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index b13879df..2684e071 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -42,7 +42,11 @@ namespace klee {
}
void setTimeout(double t) {
- stpSolver->setTimeout(t);
+ stpSolver->setCoreSolverTimeout(t);
+ }
+
+ char *getConstraintLog(const Query& query) {
+ return solver->getConstraintLog(query);
}
bool evaluate(const ExecutionState&, ref<Expr>, Solver::Validity &result);
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 5911bbf3..674d4627 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -85,6 +85,8 @@ public:
hasSolution);
}
SolverRunStatus getOperationStatusCode();
+ char *getConstraintLog(const Query&);
+ void setCoreSolverTimeout(double timeout);
};
/** @returns the canonical version of the given query. The reference
@@ -244,6 +246,14 @@ SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode() {
return solver->impl->getOperationStatusCode();
}
+char *CachingSolver::getConstraintLog(const Query& query) {
+ return solver->impl->getConstraintLog(query);
+}
+
+void CachingSolver::setCoreSolverTimeout(double timeout) {
+ solver->impl->setCoreSolverTimeout(timeout);
+}
+
///
Solver *klee::createCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index b38df672..df7fffc5 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -83,6 +83,8 @@ public:
std::vector< std::vector<unsigned char> > &values,
bool &hasSolution);
SolverRunStatus getOperationStatusCode();
+ char *getConstraintLog(const Query& query);
+ void setCoreSolverTimeout(double timeout);
};
///
@@ -350,6 +352,14 @@ SolverImpl::SolverRunStatus CexCachingSolver::getOperationStatusCode() {
return solver->impl->getOperationStatusCode();
}
+char *CexCachingSolver::getConstraintLog(const Query& query) {
+ return solver->impl->getConstraintLog(query);
+}
+
+void CexCachingSolver::setCoreSolverTimeout(double timeout) {
+ solver->impl->setCoreSolverTimeout(timeout);
+}
+
///
Solver *klee::createCexCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index 7bc8058d..dc2c9fd4 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -138,3 +138,12 @@ StagedSolverImpl::computeInitialValues(const Query& query,
SolverImpl::SolverRunStatus StagedSolverImpl::getOperationStatusCode() {
return secondary->impl->getOperationStatusCode();
}
+
+char *StagedSolverImpl::getConstraintLog(const Query& query) {
+ return secondary->impl->getConstraintLog(query);
+}
+
+void StagedSolverImpl::setCoreSolverTimeout(double timeout) {
+ secondary->impl->setCoreSolverTimeout(timeout);
+}
+
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index b3ef1e57..d9fc77dc 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -285,6 +285,8 @@ public:
hasSolution);
}
SolverRunStatus getOperationStatusCode();
+ char *getConstraintLog(const Query&);
+ void setCoreSolverTimeout(double timeout);
};
bool IndependentSolver::computeValidity(const Query& query,
@@ -318,6 +320,14 @@ SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() {
return solver->impl->getOperationStatusCode();
}
+char *IndependentSolver::getConstraintLog(const Query& query) {
+ return solver->impl->getConstraintLog(query);
+}
+
+void IndependentSolver::setCoreSolverTimeout(double timeout) {
+ solver->impl->setCoreSolverTimeout(timeout);
+}
+
Solver *klee::createIndependentSolver(Solver *s) {
return new Solver(new IndependentSolver(s));
}
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 245ad3bf..e7187fc3 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -183,4 +183,11 @@ SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() {
return solver->impl->getOperationStatusCode();
}
+char *QueryLoggingSolver::getConstraintLog(const Query& query) {
+ return solver->impl->getConstraintLog(query);
+}
+
+void QueryLoggingSolver::setCoreSolverTimeout(double timeout) {
+ solver->impl->setCoreSolverTimeout(timeout);
+}
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 527d075b..2c7d80e8 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -70,7 +70,8 @@ public:
std::vector< std::vector<unsigned char> > &values,
bool &hasSolution);
SolverRunStatus getOperationStatusCode();
-
+ char *getConstraintLog(const Query&);
+ void setCoreSolverTimeout(double timeout);
};
#endif /* KLEE_QUERYLOGGINGSOLVER_H */
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index b3d1613d..3414cda2 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -101,6 +101,14 @@ Solver::~Solver() {
delete impl;
}
+char *Solver::getConstraintLog(const Query& query) {
+ return impl->getConstraintLog(query);
+}
+
+void Solver::setCoreSolverTimeout(double timeout) {
+ impl->setCoreSolverTimeout(timeout);
+}
+
bool Solver::evaluate(const Query& query, Validity &result) {
assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
@@ -307,6 +315,8 @@ public:
std::vector< std::vector<unsigned char> > &values,
bool &hasSolution);
SolverRunStatus getOperationStatusCode();
+ char *getConstraintLog(const Query&);
+ void setCoreSolverTimeout(double timeout);
};
bool ValidatingSolver::computeTruth(const Query& query,
@@ -408,6 +418,14 @@ SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() {
return solver->impl->getOperationStatusCode();
}
+char *ValidatingSolver::getConstraintLog(const Query& query) {
+ return solver->impl->getConstraintLog(query);
+}
+
+void ValidatingSolver::setCoreSolverTimeout(double timeout) {
+ solver->impl->setCoreSolverTimeout(timeout);
+}
+
Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) {
return new Solver(new ValidatingSolver(s, oracle));
}
@@ -466,9 +484,9 @@ private:
public:
STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
~STPSolverImpl();
-
+
char *getConstraintLog(const Query&);
- void setTimeout(double _timeout) { timeout = _timeout; }
+ void setCoreSolverTimeout(double _timeout) { timeout = _timeout; }
bool computeTruth(const Query&, bool &isValid);
bool computeValue(const Query&, ref<Expr> &result);
@@ -532,11 +550,11 @@ STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
}
char *STPSolver::getConstraintLog(const Query &query) {
- return static_cast<STPSolverImpl*>(impl)->getConstraintLog(query);
+ return impl->getConstraintLog(query);
}
-void STPSolver::setTimeout(double timeout) {
- static_cast<STPSolverImpl*>(impl)->setTimeout(timeout);
+void STPSolver::setCoreSolverTimeout(double timeout) {
+ impl->setCoreSolverTimeout(timeout);
}
/***/
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-21 16:54:10 +0000