Solver.h

Go to the documentation of this file.

//===-- Solver.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_SOLVER_H
#define KLEE_SOLVER_H
 
#include "klee/Expr/Expr.h"
#include "klee/System/Time.h"
#include "klee/Solver/SolverCmdLine.h"
 
#include <vector>
 
namespace klee {
  class ConstraintSet;
  class Expr;
  class SolverImpl;
 
  struct SolverQueryMetaData {
    time::Span queryCost;
  };
 
  struct Query {
  public:
    const ConstraintSet &constraints;
    ref<Expr> expr;
 
    Query(const ConstraintSet& _constraints, ref<Expr> _expr)
      : constraints(_constraints), expr(_expr) {
    }
 
    Query withExpr(ref<Expr> _expr) const {
      return Query(constraints, _expr);
    }
 
    Query withFalse() const {
      return Query(constraints, ConstantExpr::alloc(0, Expr::Bool));
    }
 
    Query negateExpr() const {
      return withExpr(Expr::createIsZero(expr));
    }
 
    void dump() const ;
  };
 
  class Solver {
    // DO NOT IMPLEMENT.
    Solver(const Solver&);
    void operator=(const Solver&);
 
  public:
    enum Validity {
      True = 1,
      False = -1,
      Unknown = 0
    };
  
  public:
    static const char *validity_to_str(Validity v);
 
  public:
    SolverImpl *impl;
 
  public:
    Solver(SolverImpl *_impl) : impl(_impl) {}
    virtual ~Solver();
 
    bool evaluate(const Query&, Validity &result);
  
    bool mustBeTrue(const Query&, bool &result);
 
    bool mustBeFalse(const Query&, bool &result);
 
    bool mayBeTrue(const Query&, bool &result);
 
    bool mayBeFalse(const Query&, bool &result);
 
    bool getValue(const Query&, ref<ConstantExpr> &result);
 
    //
    // FIXME: This API is lame. We should probably just provide an API which
    // returns an Assignment object, then clients can get out whatever values
    // they want. This also allows us to optimize the representation.
    bool getInitialValues(const Query&, 
                          const std::vector<const Array*> &objects,
                          std::vector< std::vector<unsigned char> > &result);
 
    //
    // FIXME: This should go into a helper class, and should handle failure.
    virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&);
    
    virtual char *getConstraintLog(const Query& query);
    virtual void setCoreSolverTimeout(time::Span timeout);
  };
 
  /* *** */
 
  Solver *createValidatingSolver(Solver *s, Solver *oracle);
 
  Solver *createAssignmentValidatingSolver(Solver *s);
 
  Solver *createCachingSolver(Solver *s);
 
  Solver *createCexCachingSolver(Solver *s);
 
  Solver *createFastCexSolver(Solver *s);
 
  Solver *createIndependentSolver(Solver *s);
  
  Solver *createKQueryLoggingSolver(Solver *s, std::string path,
                                    time::Span minQueryTimeToLog,
                                    bool logTimedOut);
 
  Solver *createSMTLIBLoggingSolver(Solver *s, std::string path,
                                    time::Span minQueryTimeToLog,
                                    bool logTimedOut);
 
 
  Solver *createDummySolver();
 
  // Create a solver based on the supplied ``CoreSolverType``.
  Solver *createCoreSolver(CoreSolverType cst);
}
 
#endif /* KLEE_SOLVER_H */