IncompleteSolver.h

Go to the documentation of this file.

//===-- IncompleteSolver.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_INCOMPLETESOLVER_H
#define KLEE_INCOMPLETESOLVER_H
 
#include "klee/Solver/Solver.h"
#include "klee/Solver/SolverImpl.h"
 
namespace klee {
 
class IncompleteSolver {
public:
  enum PartialValidity {
    MustBeTrue = 1,
 
    MustBeFalse = -1,
 
    MayBeTrue = 2,
 
    MayBeFalse = -2,
 
    TrueOrFalse = 0,
 
    None = 3
  };
 
  static PartialValidity negatePartialValidity(PartialValidity pv);
 
public:
  IncompleteSolver() {}
  virtual ~IncompleteSolver() {}
 
  virtual IncompleteSolver::PartialValidity computeValidity(const Query&);
 
  virtual IncompleteSolver::PartialValidity computeTruth(const Query&) = 0;
  
  virtual bool computeValue(const Query&, ref<Expr> &result) = 0;
 
  virtual bool computeInitialValues(const Query&,
                                    const std::vector<const Array*> 
                                      &objects,
                                    std::vector< std::vector<unsigned char> > 
                                      &values,
                                    bool &hasSolution) = 0;
};
 
class StagedSolverImpl : public SolverImpl {
private:
  IncompleteSolver *primary;
  Solver *secondary;
  
public:
  StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary);
  ~StagedSolverImpl();
    
  bool computeTruth(const Query&, bool &isValid);
  bool computeValidity(const Query&, Solver::Validity &result);
  bool computeValue(const Query&, ref<Expr> &result);
  bool computeInitialValues(const Query&,
                            const std::vector<const Array*> &objects,
                            std::vector< std::vector<unsigned char> > &values,
                            bool &hasSolution);
  SolverRunStatus getOperationStatusCode();
  char *getConstraintLog(const Query&);
  void setCoreSolverTimeout(time::Span timeout);
};
 
}
 
#endif /* KLEE_INCOMPLETESOLVER_H */