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 |