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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128

/*
 * 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 "Test/UnitTesting.hpp"
#include "Test/SyntaxSugar.hpp"
#include "Inferences/PushUnaryMinus.hpp"

#include "Test/SyntaxSugar.hpp"
#include "Test/TestUtils.hpp"
#include "Test/SimplificationTester.hpp"

using namespace std;
using namespace Kernel;
using namespace Inferences;
using namespace Test;

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
////// TEST UNIT INITIALIZATION
/////////////////////////////////////

/** 
 * NECESSARY: We need a subclass of SimplificationTester
 */
class PumSimplTester : public Test::Simplification::SimplificationTester
{
public:

  virtual Kernel::Clause* simplify(Kernel::Clause* in) override 
  {
    PushUnaryMinus pum;
    return pum.simplify(in);
  }

  virtual bool eq(Kernel::Clause* lhs, Kernel::Clause* rhs) const  override
  { return TestUtils::eqModAC(lhs, rhs); }
};

REGISTER_SIMPL_TESTER(PumSimplTester)

#define MY_SYNTAX_SUGAR                                                                                       \
  NUMBER_SUGAR(Real)                                                                                          \
  DECL_DEFAULT_VARS                                                                                           \
  DECL_CONST(a, Real)                                                                                         \
  DECL_CONST(b, Real)                                                                                         \
  DECL_FUNC(f, {Real}, Real)                                                                                  \
  DECL_PRED(p, {Real})                                                                                        \
  DECL_PRED(q, {Real})                                                                                        \

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
////// TEST CASES
/////////////////////////////////////

TEST_SIMPLIFY(test_1,
    Simplification::Success()
      .input(    clause({  p(-(a + b))  }))
      .expected( clause({  p(-a + -b)  }))
    )

TEST_SIMPLIFY(test_2,
    Simplification::NotApplicable()
      .input( clause({ p(-a + -b) }))
    )

TEST_SIMPLIFY(test_3,
    Simplification::NotApplicable()
      .input( clause({ p(a) }))
    )

TEST_SIMPLIFY(test_4,
    Simplification::Success()
      .input(    clause({  p(-(a + b)), p(a)  }))
      .expected( clause({  p(-a + -b), p(a)  }))
    )

TEST_SIMPLIFY(test_5,
    Simplification::Success()
      .input(    clause({  p(a), p(-(a + b))  }))
      .expected( clause({  p(a), p(-a + -b)  }))
    )

// TEST_SIMPLIFY(test_3,
//     Simplification::Success()
//       .input(    clause({  3 * x != 6, x < x  }))
//       .expected( clause({  /* 2 < 2 */  }))
//     )
//
//   // 2x + y = x + y ==> 0 = 2x + y - x - y ==> 0 = x
// TEST_SIMPLIFY(test_4,
//     Simplification::Success()
//       .input(    clause({  2 * x + y != x + y, p(x) }))
//       .expected( clause({  p(0)  }))
//     )
//
// TEST_SIMPLIFY(test_uninterpreted,
//     Simplification::Success()
//       .input(    clause({  3 * f(x) != y, x < y  }))
//       .expected( clause({  x < 3 * f(x)  }))
//     )
//
//   // x!=4 \/ x+y != 5 \/ C[x]
//   //         4+y != 5 \/ C[4]
//   //                     C[4]
// TEST_SIMPLIFY(test_multiplesteps_1,
//     Simplification::Success()
//       .input(    clause({  x != 4, x + y != 5, x < f(x)  }))
//       .expected( clause({  4 < f(4)  }))
//     )
//
//   // x!=4 \/ x+y != 5 \/ C[x,y]
//   //         4+y != 5 \/ C[4,y]
//   //                     C[4,1]
// TEST_SIMPLIFY(test_multiplesteps_2,
//     Simplification::Success()
//       .input(    clause({  x != 4, x + y !=  5, x < f(y)  }))
//       .expected( clause({  4 < f(1)  }))
//     )
//
// TEST_SIMPLIFY(test_div,
//     Simplification::Success()
//       .input(    clause({  x / 3 != 4, p(x)  }))
//       .expected( clause({  p(12)  }))
//     )