SolverImpl.h

Go to the documentation of this file.

//===-- SolverImpl.h --------------------------------------------*- C++ -*-===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
 
#ifndef KLEE_SOLVERIMPL_H
#define KLEE_SOLVERIMPL_H
 
#include "klee/System/Time.h"
#include "Solver.h"
 
#include <vector>
 
namespace klee {
  class Array;
  class ExecutionState;
  class Expr;
  struct Query;
 
  class SolverImpl {
    // DO NOT IMPLEMENT.
    SolverImpl(const SolverImpl&);
    void operator=(const SolverImpl&);
    
  public:
    SolverImpl() {}
    virtual ~SolverImpl();
 
    enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE,
                           SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE,
                           SOLVER_RUN_STATUS_FAILURE,
                           SOLVER_RUN_STATUS_TIMEOUT,
                           SOLVER_RUN_STATUS_FORK_FAILED,
                           SOLVER_RUN_STATUS_INTERRUPTED,
                           SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE,
                           SOLVER_RUN_STATUS_WAITPID_FAILED };
 
    virtual bool computeValidity(const Query& query, Solver::Validity &result);
    
    virtual bool computeTruth(const Query& query, bool &isValid) = 0;
 
    virtual bool computeValue(const Query& query, ref<Expr> &result) = 0;
    
    virtual bool computeInitialValues(const Query& query,
                                      const std::vector<const Array*> 
                                        &objects,
                                      std::vector< std::vector<unsigned char> > 
                                        &values,
                                      bool &hasSolution) = 0;
    
    virtual SolverRunStatus getOperationStatusCode() = 0;
 
    static const char* getOperationStatusString(SolverRunStatus statusCode);
 
    virtual char *getConstraintLog(const Query& query)  {
        // dummy
        return nullptr;
    }
 
    virtual void setCoreSolverTimeout(time::Span timeout) {};
};
 
}
 
#endif /* KLEE_SOLVERIMPL_H */