1		/*
2		* Exposes Glucose API to SICStus Prolog
3		*
4		* Based on SWI Prolog Minisat Integration by
5		* Michael Codish, Vitaly Lagoon, Peter J. Stuckey
6
7		* initial integration into ProB by Sebastian Krings
8		* extensions (b_to_cnf, card support,...) and full integration by Michael Leuschel
9		*/
10
11		:- module(satsolver, [init_satsolver/0,
12		new_solver/1,
13		solve/1,
14		delete_solver/1,
15		add_clause/2,
16		assign_model/2,
17		get_model/2,
18		toDimacs/2]).
19
20		:- use_module('../../src/module_information.pl').
21		:- module_info(group,experimental).
22		:- module_info(description,'This is the interface between ProB and the Glucose SAT solver').
23
24		:- use_module(probsrc(error_manager),[add_error/3]).
25
26		foreign_resource('satsolver', [new_solver,solve,delete_solver,
27		add_clause,assign_model,get_model,toDimacs]).
28
29		foreign(new_solver, c, new_solver([-integer])).
30		foreign(solve, c, solve(+integer)).
31		foreign(delete_solver, c, delete_solver(+integer)).
32		foreign(add_clause, c, add_clause(+integer,+term)).
33		foreign(assign_model, c, assign_model(+integer,+term)).
34		foreign(get_model, c, get_model(+integer,+term)).
35		foreign(toDimacs, c, toDimacs(+integer,+string)).
36
37		:- dynamic is_initialised/0.
38
39		init_satsolver :- is_initialised,!.
40		init_satsolver :-
41		catch(load_foreign_resource(library(satsolver)),E,
42		(add_error(satsolver,'Loading satsolver library failed, be sure to have satsolver.bundle/so/dll in the lib folder of ProB:',E),
43		fail)),
44		assertz(is_initialised).
45
46
47