cprover
smt1_dec.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_SMT1_SMT1_DEC_H
11 #define CPROVER_SOLVERS_SMT1_SMT1_DEC_H
12 
13 #include <fstream>
14 
15 #include "smt1_conv.h"
16 
18 {
19 public:
22 
23 protected:
24  std::ofstream temp_out;
26 };
27 
30 class smt1_dect:protected smt1_temp_filet, public smt1_convt
31 {
32 public:
34  const namespacet &_ns,
35  const std::string &_benchmark,
36  const std::string &_source,
37  const std::string &_logic,
38  solvert _solver):
40  smt1_convt(_ns, _benchmark, _source, _logic, _solver, temp_out),
41  logic(_logic),
42  dec_solve_was_called(false)
43  {
44  }
45 
46  virtual resultt dec_solve();
47  virtual std::string decision_procedure_text() const;
48 
49 protected:
50  std::string logic;
52 
53  resultt read_result_boolector(std::istream &in);
54  resultt read_result_cvc3(std::istream &in);
55  resultt read_result_opensmt(std::istream &in);
56  resultt read_result_mathsat(std::istream &in);
57  resultt read_result_yices(std::istream &in);
58  resultt read_result_z3(std::istream &in);
59 
60  bool string_to_expr_z3(
61  const typet &type,
62  const std::string &value, exprt &e) const;
63 
64  std::string mathsat_value(const std::string &src);
65 
66  struct valuet
67  {
68  // map from array index to value
69  typedef std::map<std::string, std::string> index_value_mapt;
70  index_value_mapt index_value_map;
71  std::string value;
72  };
73 };
74 
75 #endif // CPROVER_SOLVERS_SMT1_SMT1_DEC_H
The type of an expression.
Definition: type.h:20
index_value_mapt index_value_map
Definition: smt1_dec.h:70
std::string value
Definition: smt1_dec.h:71
smt1_dect(const namespacet &_ns, const std::string &_benchmark, const std::string &_source, const std::string &_logic, solvert _solver)
Definition: smt1_dec.h:33
std::string temp_out_filename
Definition: smt1_dec.h:25
std::ofstream temp_out
Definition: smt1_dec.h:24
std::map< std::string, std::string > index_value_mapt
Definition: smt1_dec.h:69
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Decision procedure interface for various SMT 1.x solvers.
Definition: smt1_dec.h:30
Base class for all expressions.
Definition: expr.h:46
SMT Version 1 Backend.
std::string logic
Definition: smt1_dec.h:50
std::string temp_result_filename
Definition: smt1_dec.h:25
bool dec_solve_was_called
Definition: smt1_dec.h:51