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 <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();

    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;  
};

}

#endif