ts_engines.h

Go to the documentation of this file.

#pragma once
 
#include <transition-system/transition_system.h>
#include <solvers/smt/smt_conv.h>
 
#include <cstdint>
#include <memory>

class ts_enginet
{
public:
  ts_enginet(
    const transition_systemt &ts,
    const namespacet &ns,
    optionst &options,
    bool incremental = true);

  int bmc(uint64_t max_k, bool push_pop);

  smt_resultt solve_bound(unsigned k);
  smt_resultt solve_prefix();
 
protected:
  const transition_systemt &ts;
  const namespacet &ns;
  std::unique_ptr<smt_convt> solver;
 
  expr2tc bad_literal(unsigned step) const;
  bool check_prefix();
  void assume_prefix();
  void add_step(unsigned step);
  void close_step(unsigned step);
  smt_resultt solve_bad(unsigned step, bool push_pop);
  void report_counterexample(unsigned step);
};