You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 

91 lines
2.9 KiB

#include "src/solver/SmtratSmtSolver.h"
#include "src/utility/macros.h"
#include "src/exceptions/NotSupportedException.h"
#include "src/exceptions/InvalidStateException.h"
#ifdef STORM_HAVE_SMTRAT
#ifdef SMTRATDOESNTWORK // Does not compile with current version of smtrat.
#include "lib/smtrat.h"
namespace storm {
namespace solver {
SmtratSmtSolver::SmtratSmtSolver(storm::expressions::ExpressionManager& manager) : SmtSolver(manager)
{
// Construct the settingsManager.
//smtrat::RuntimeSettingsManager settingsManager;
// Construct solver.
smtrat::RatOne* solver = new smtrat::RatOne();
//std::list<std::pair<std::string, smtrat::RuntimeSettings*> > settingsObjects =
smtrat::addModules( solver );
// Introduce the settingsObjects from the modules to the manager.
//settingsManager.addSettingsObject( settingsObjects );
//settingsObjects.clear();
}
SmtratSmtSolver::~SmtratSmtSolver() {
delete solver;
}
void SmtratSmtSolver::push()
{
this->solver->push();
}
void SmtratSmtSolver::pop()
{
this->solver->pop();
}
void SmtratSmtSolver::pop(uint_fast64_t n)
{
this->solver->pop(static_cast<unsigned int>(n));
}
SmtSolver::CheckResult SmtratSmtSolver::check()
{
switch (this->solver->check()) {
case smtrat::Answer::True:
this->lastResult = SmtSolver::CheckResult::Sat;
break;
case smtrat::Answer::False:
this->lastResult = SmtSolver::CheckResult::Unsat;
break;
case smtrat::Answer::Unknown:
this->lastResult = SmtSolver::CheckResult::Unknown;
break;
default:
// maybe exit
this->lastResult = SmtSolver::CheckResult::Unknown;
break;
}
return this->lastResult;
}
void SmtratSmtSolver::add(const storm::RawPolynomial& pol, storm::CompareRelation cr) {
this->solver->add(smtrat::FormulaT(pol, cr));
}
template<>
smtrat::Model SmtratSmtSolver::getModel() const
{
return this->solver->model();
}
std::vector<smtrat::FormulasT> const& SmtratSmtSolver::getUnsatisfiableCores() const
{
return this->solver->infeasibleSubsets();
}
}
}
#endif
#endif