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.h"

#include <vector>

namespace klee {
  class ConstraintManager;
  class Expr;
  class SolverImpl;

  struct Query {
  public:
    const ConstraintManager &constraints;
    ref<Expr> expr;

    Query(const ConstraintManager& _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::createNot(expr));
    }
  };

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

  class STPSolver : public Solver {
  public:
    STPSolver(bool useForkedSTP);

    
    
    char *getConstraintLog(const Query&);
    
    void setTimeout(double timeout);
  };

  /* *** */

  Solver *createValidatingSolver(Solver *s, Solver *oracle);

  Solver *createCachingSolver(Solver *s);

  Solver *createCexCachingSolver(Solver *s);

  Solver *createFastCexSolver(Solver *s);

  Solver *createIndependentSolver(Solver *s);
  
  Solver *createPCLoggingSolver(Solver *s, std::string path);

}

#endif