this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2
3/*
4 * Main authors:
5 * Jip J. Dekker <jip.dekker@monash.edu>
6 */
7
8/* This Source Code Form is subject to the terms of the Mozilla Public
9 * License, v. 2.0. If a copy of the MPL was not distributed with this
10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
11
12#include <minizinc/c_interface.h>
13#include <minizinc/interpreter.hh>
14#include <minizinc/interpreter/primitives.hh>
15#include <minizinc/solver.hh>
16#include <minizinc/solvers/gecode_solverinstance.hh>
17
18#include <cstdarg>
19#include <iostream>
20
21using namespace MiniZinc;
22
23class Instance {
24public:
25 Instance(std::string file, std::string data_file, std::string solver)
26 : slv({"--solver", solver, file, data_file}){};
27
28 MznSolver slv;
29 std::string result;
30};
31
32void set_rnd_seed(int seed) {
33 dynamic_cast<BytecodePrimitives::Uniform*>(primitiveMap()[PrimitiveMap::UNIFORM])->setSeed(seed);
34}
35
36MZNInstance minizinc_instance_init(const char* mza_file, const char* data_file,
37 const char* solver) {
38 auto inst = new Instance(mza_file, data_file, solver);
39 return reinterpret_cast<MZNInstance>(inst);
40}
41
42void minizinc_instance_destroy(MZNInstance _inst) {
43 auto inst = reinterpret_cast<Instance*>(_inst);
44 delete inst;
45}
46
47void minizinc_add_call(MZNInstance _inst, const char* call, ...) {
48 auto inst = reinterpret_cast<Instance*>(_inst);
49 auto it = inst->slv.resolve_call.find(call);
50 assert(it != inst->slv.resolve_call.end());
51
52 std::vector<Val> args;
53 va_list my_args;
54 va_start(my_args, call);
55 for (int i = 0; i < it->second.second; ++i) {
56 int num = va_arg(my_args, int);
57 args.emplace_back(num);
58 }
59
60 inst->slv.interpreter->call(it->second.first, std::move(args));
61}
62
63void minizinc_set_solution(MZNInstance _inst, int def, int sol) {
64 auto inst = reinterpret_cast<Instance*>(_inst);
65 auto it = inst->slv.interpreter->solutions.emplace(def, sol);
66}
67
68void minizinc_output_dict(MZNInstance _inst, bool b) {
69 auto inst = reinterpret_cast<Instance*>(_inst);
70 inst->slv.output_dict = b;
71}
72
73void minizinc_push_state(MZNInstance _inst) {
74 auto inst = reinterpret_cast<Instance*>(_inst);
75 inst->slv.interpreter->trail.save_state(inst->slv.interpreter);
76 inst->slv.pushToSolver();
77}
78void minizinc_pop_state(MZNInstance _inst) {
79 auto inst = reinterpret_cast<Instance*>(_inst);
80 inst->slv.interpreter->trail.untrail(inst->slv.interpreter);
81 inst->slv.popFromSolver();
82}
83
84void minizinc_print_hedge(MZNInstance _inst) {
85 auto inst = reinterpret_cast<Instance*>(_inst);
86 inst->slv.interpreter->dumpState(std::cerr);
87}
88
89void minizinc_set_limit(MZNInstance _inst, int limit) {
90 auto inst = reinterpret_cast<Instance*>(_inst);
91 auto opt = static_cast<GecodeOptions*>(inst->slv.getSI_OPT());
92 opt->nodes = limit;
93}
94
95std::string status_to_string(SolverInstance::Status s) {
96 switch (s) {
97 case SolverInstance::OPT:
98 return "OPT";
99 case SolverInstance::SAT:
100 return "SAT";
101 case SolverInstance::UNSAT:
102 return "UNSAT";
103 case SolverInstance::UNBND:
104 return "UNBND";
105 case SolverInstance::UNSATorUNBND:
106 return "UNSATorUNBND";
107 case SolverInstance::UNKNOWN:
108 return "UNKNOWN";
109 case SolverInstance::ERROR:
110 return "ERROR";
111 case SolverInstance::NONE:
112 return "NONE";
113 }
114}
115
116const char* minizinc_solve(MZNInstance _inst) {
117 auto inst = reinterpret_cast<Instance*>(_inst);
118 auto result = inst->slv.run();
119
120 std::stringstream ss;
121 ss << "{";
122 ss << "\"status\": \"" << status_to_string(result.first) << "\",";
123 if (result.first == MiniZinc::SolverInstance::SAT ||
124 result.first == MiniZinc::SolverInstance::OPT) {
125 ss << "\"solution\": " << result.second;
126 } else {
127 ss << R"("solution": "")";
128 }
129 ss << "}";
130
131 inst->result = ss.str();
132 return inst->result.c_str();
133}