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

/*
 * 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
 */
#include "Lib/SkipList.hpp"
#include "Lib/DHMultiset.hpp"
#include "Lib/Int.hpp"
#include "Lib/DArray.hpp"

#include "Test/UnitTesting.hpp"

using namespace std;
using namespace Lib;

const int cnt=105000;

typedef int StoredType;

StoredType arr[cnt];

TEST_FUN(skiplist1)
{
  SkipList<StoredType, Int> sl1;
  SkipList<StoredType, Int> sl2;
  DArray<StoredType> darr(cnt);
  DHMultiset<StoredType> ms;

  for(int i=0;i<cnt;i++)
  {
    int num=(rand()%cnt)/100;
    ms.insert(num);
    sl1.insert(num);

    sl2.insert(num);
    darr[i]=num;
    arr[i]=num;
  }

  for(int i=0;i<cnt/2;i++)
  {
    ms.remove(arr[i]);
  }

  for(int i=0;i<cnt/2;i++)
  {
    sl1.remove(arr[i]);
  }

  std::sort(darr.begin(), darr.end());
  for(int i=0;i<cnt;i++)
  {
    ASS_EQ(sl2.pop(),darr[i]);
  }
}