QuAPI/test/test_supplied_solver.cpp at stable · maximaximal/QuAPI · GitHub

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
#include "util.hpp"
#include <catch.hpp>
#include <cstdlib>
#include <quapi/quapi.h>

TEST_CASE("User-Supplied SAT solver from env SOLVER_SAT", "[user]") {
  const char* path = std::getenv("SOLVER_SAT");
  if(!path)
    return;

  REQUIRE(file_exists(path));

  QuAPISolver S(quapi_init(path, NULL, NULL, 2, 2, 1, NULL, NULL));
  quapi_solver* s = S.get();

  // Code from the example without quantify.

  quapi_add(s, 1), quapi_add(s, -2), quapi_add(s, 0);
  quapi_add(s, -1), quapi_add(s, 2), quapi_add(s, 0);
  quapi_assume(s, 1);
  int status = quapi_solve(s);
  REQUIRE(status == 10);
  quapi_assume(s, -1);
  status = quapi_solve(s);
  REQUIRE(status == 10);
}

TEST_CASE("User-Supplied QBF solver from env SOLVER_QBF", "[user]") {
  const char* path = std::getenv("SOLVER_QBF");
  if(!path)
    return;

  REQUIRE(file_exists(path));

  QuAPISolver S(quapi_init(path, NULL, NULL, 2, 2, 1, NULL, NULL));
  quapi_solver* s = S.get();

  // Code from the example.

  quapi_quantify(s, -1);
  quapi_quantify(s, 2);
  quapi_add(s, 1), quapi_add(s, -2), quapi_add(s, 0);
  quapi_add(s, -1), quapi_add(s, 2), quapi_add(s, 0);
  quapi_assume(s, 1);
  int status = quapi_solve(s);
  REQUIRE(status == 10);
  quapi_assume(s, -1);
  status = quapi_solve(s);
  REQUIRE(status == 10);
}