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
8		:- module(satsolver, [init_satsolver/0, sat/1, sat/2, bt_sat/1, multi_sat/3, b_sat/2]).
9
10		:- use_module('../../src/module_information.pl').
11		:- module_info(group,experimental).
12		:- module_info(description,'This is the interface between ProB and the Glucose SAT solver').
13
14		:- use_module(b_to_cnf).
15
16		:- use_module(library(lists), [maplist/2,maplist/3]).
17
18		foreign_resource('satsolver', [new_solver,solve,delete_solver,
19		add_clause,assign_model,get_model]).
20
21		foreign(new_solver, c, new_solver([-integer])).
22		foreign(solve, c, solve(+integer)).
23		foreign(delete_solver, c, delete_solver(+integer)).
24		foreign(add_clause, c, add_clause(+integer,+term)).
25		foreign(assign_model, c, assign_model(+integer,+term)).
26		foreign(get_model, c, get_model(+integer,+term)).
27
28		:- dynamic is_initialised/0.
29
30		init_satsolver :- is_initialised,!.
31		init_satsolver :-
32		catch(load_foreign_resource(library(satsolver)),_,(print('*** LOADING satsolver library failed'),nl,fail)),
33		assert(is_initialised).
34
35		b_sat(BFormula,State) :-
36		init_satsolver,
37		b_to_cnf(BFormula,State,CNF),!,
38		bt_sat(CNF).
39
40		sat(CNF):-
41		sat(CNF,Solved),!,
42		Solved=1.
43
44		sat([],1):-!.
45		sat([[]],0):-!.
46		sat(F,Solved):-
47		new_solver(SolverID),
48		setup_solver(SolverID),
49		(addCnf2Solver(SolverID,F,FVars)
50		-> (solve(SolverID)
51		-> assign_model(SolverID,[1|FVars]), Solved = 1
52		; Solved = 0)
53		; Solved=0),
54		delete_solver(SolverID),!.
55
56		bt_sat(F) :-
57		new_solver(SolverID),
58		bt_sat_aux(SolverID,F).
59
60		bt_sat_aux(SolverID,F) :-
61		setup_solver(SolverID),
62		addCnf2Solver(SolverID,F,FVars),
63		solve(SolverID),
64		get_model(SolverID,[_|Model]),
65		bt_sat(SolverID,FVars,Model).
66		bt_sat_aux(SolverID,_) :-
67		delete_solver(SolverID), fail.
68
69		bt_sat(SolverID,FVars,_Model) :-
70		assign_model(SolverID,[1|FVars]).
71		bt_sat(SolverID,FVars,Model) :-
72		add_negated_model(SolverID,Model),
73		solve(SolverID),
74		get_model(SolverID,[_|NewModel]),
75		bt_sat(SolverID,FVars,NewModel).
76
77		multi_sat([],_,1):-!.
78		multi_sat([[]],_,0):-!.
79		multi_sat(F,MaxSols,SolCount):-
80		new_solver(SolverID),
81		setup_solver(SolverID),
82		(addCnf2Solver(SolverID,F,FVars)
83		-> satMultiModels(SolverID,MaxSols,Models),
84		delete_solver(SolverID),!,
85		length(Models,SolCount),
86		(SolCount == 0 ; assignMultiSols(Models,FVars))
87		; delete_solver(SolverID),!,SolCount=0),!.
88
89		satMultiModels(SolverID,MaxSols,Models):-
90		MaxSols > 0,!,
91		(solve(SolverID)
92		-> get_model(SolverID,[_|Model]),
93		Models=[Model|MoreModels],
94		MaxSols1 is MaxSols - 1,
95		((MaxSols1 > 0, add_negated_model(SolverID,Model))
96		-> satMultiModels(SolverID,MaxSols1,MoreModels)
97		; MoreModels=[])
98		; Models=[]).
99		satMultiModels(_,_,[]):-!.
100
101		add_negated_model(SolverID,Model):-
102		maplist(neg,Model,NoAsgn),
103		add_clause(SolverID,NoAsgn).
104
105		neg(V,VN) :- VN is -V.
106
107		assignMultiSols(Models,FVars):-!,
108		length(FVars,VarLen),
109		length(SoFar,VarLen),
110		maplist(=([]),SoFar),!,
111		assignMultiSols(Models,SoFar,FVars).
112
113		assignMultiSols([],SoFar,SoFar):-!.
114		assignMultiSols([M|Models],SoFar,Vars):-!,
115		addModel2Vars(M,SoFar,NVars),!,
116		assignMultiSols(Models,NVars,Vars).
117
118		addModel2Vars([],[],[]).
119		addModel2Vars([M|Ms],[V|Vs],[[NV|V]|NVs]):-
120		(M>0 -> NV=1 ; NV= -1),
121		addModel2Vars(Ms,Vs,NVs).
122
123		addCnf2Solver(SolverID,Cnf,FVars):-
124		term_variables(Cnf,FVars),!,
125		\+ \+ (bind2index(FVars,3,FN),
126		add_cnf_clauses(Cnf,SolverID),
127		neg(FN,FNeg),
128		add_cnf_clauses([[FN,FNeg]],SolverID)).
129
130		add_cnf_clauses([Cl|Cls],SolverID):-!,
131		maplist(to_minisat_cl,Cl,MiniSatCl),
132		add_clause(SolverID,MiniSatCl),
133		add_cnf_clauses(Cls,SolverID).
134		add_cnf_clauses([],_):-!.
135
136		setup_solver(SolverID) :-
137		add_clause(SolverID,[1]), % true
138		add_clause(SolverID,[-2]).
139
140		to_minisat_cl(pred_true,1) :- !.
141		to_minisat_cl(pred_false,2) :- !.
142		to_minisat_cl(X,X).
143
144		bind2index([N|Ns],N,FN) :- N1 is N+1, bind2index(Ns,N1,FN).
145		bind2index([],N,FN):-!, FN is N - 1.