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(tools),[start_ms_timer/1, stop_ms_timer_with_msg/2, stop_ms_timer_with_debug_msg/2]).
25		:- use_module(probsrc(debug),[debug_format/3]).
26		:- use_module(probsrc(error_manager),[add_error/3, add_internal_error/2]).
27		:- use_module(b_to_cnf).
28
29		:- use_module(library(lists), [maplist/2,maplist/3,exclude/3]).
30
31		foreign_resource('satsolver', [new_solver,solve,delete_solver,
32		add_clause,assign_model,get_model,toDimacs]).
33
34		foreign(new_solver, c, new_solver([-integer])).
35		foreign(solve, c, solve(+integer)).
36		foreign(delete_solver, c, delete_solver(+integer)).
37		foreign(add_clause, c, add_clause(+integer,+term)).
38		foreign(assign_model, c, assign_model(+integer,+term)).
39		foreign(get_model, c, get_model(+integer,+term)).
40		foreign(toDimacs, c, toDimacs(+integer,+string)).
41
42		:- dynamic is_initialised/0.
43
44		init_satsolver :- is_initialised,!.
45		init_satsolver :-
46		catch(load_foreign_resource(library(satsolver)),E,
47		(add_error(satsolver,'Loading satsolver library failed, be sure to have satsolver.bundle/so/dll in the lib folder of ProB:',E),
48		fail)),
49		assertz(is_initialised).
50
51
52