vampire-sys 0.5.2

Low-level FFI bindings to the Vampire theorem prover (use the 'vampire' crate instead)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

/*
 * This file is part of the source code of the software program
 * Vampire. It is protected by applicable
 * copyright laws.
 *
 * This source code is distributed under the licence found here
 * https://vprover.github.io/license.html
 * and in the source directory
 */
/**
 * @file StringUtils.hpp
 * Defines class StringUtils.
 */

#ifndef __StringUtils__
#define __StringUtils__

#include <cstdlib>
#include <sstream>

#include "Forwards.hpp"
#include "Lib/Output.hpp"

namespace Lib {


template<class A> struct StringParser;

class StringUtils {
public:
  static std::string replaceChar(std::string str, char src, char target);
  static std::string sanitizeSuffix(std::string str);
  static bool isPositiveInteger(std::string str);
  static bool isPositiveDecimal(std::string str);
  static void replaceAll(std::string& where, const std::string& from, const std::string& to);

  static bool starts_with(const std::string& str, const std::string& what) {
    return str.rfind(what,0) == 0;
  }
  static void splitStr(const char* str, char delimiter, Stack<std::string>& strings);
  static void dropEmpty(Stack<std::string>& strings);
  static bool readEquality(const char* str, char eqChar, std::string& lhs, std::string& rhs);
  static bool readEqualities(const char* str, char delimiter, char eqChar, DHMap<std::string,std::string>& pairs);
  template<class A>
  static A parse(std::string const& str)
  { return StringParser<A>{}(str); }

  static size_t distance(const std::string &s1, const std::string &s2);
};

template<> struct StringParser<int>
{
  int operator()(std::string const& str)
  { return atoi(str.c_str()); }
};


template<> struct StringParser<float>
{
  float operator()(std::string const& str)
  { return atof(str.c_str()); }
};

template<class... Cs>
std::string outputToString(Cs const&... xs) {
  std::stringstream out;
  out << Kernel::Output::cat(xs...);
  return out.str();
}

// TODO deprecate
template<class A>
std::string toString(A const& a) {
  std::stringstream out;
  out << a;
  return out.str();
}


} // namespace Lib

#endif // __StringUtils__