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

#include "../../src/cadical.hpp"
#include <iostream>
#ifdef NDEBUG
#undef NDEBUG
#endif
#include <cassert>
using namespace std;
int main () {
  CaDiCaL::Solver solver;
  solver.add (1);
  solver.add (0);
  int res = solver.solve ();
  cout << "solver.solve () = " << res << endl << flush;
  assert (res == 10);
  res = solver.val (1);
  cout << "solver.val (1) = " << res << endl << flush;
  cout << "solver.val (-1) = " << solver.val (-1) << endl << flush;
  cout << "solver.val (2) = " << solver.val (2) << endl << flush;
  cout << "solver.val (3) = " << solver.val (3) << endl << flush;
  assert (res > 0);
  return 0;
}