/* File: sm_int.P ** Author(s): Castro, Swift ** Contact: xsb-contact@cs.sunysb.edu ** ** Copyright (C) The Research Foundation of SUNY, 1986, 1993-1998 ** Copyright (C) ECRC, Germany, 1990 ** ** XSB is free software; you can redistribute it and/or modify it under the ** terms of the GNU Library General Public License as published by the Free ** Software Foundation; either version 2 of the License, or (at your option) ** any later version. ** ** XSB is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS ** FOR A PARTICULAR PURPOSE. See the GNU Library General Public License for ** more details. ** ** You should have received a copy of the GNU Library General Public License ** along with XSB; if not, write to the Free Software Foundation, ** Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. ** ** $Id: sm_int.P,v 1.1 2003/02/21 16:57:22 lfcastro Exp $ ** */ :- compiler_options([ciao_directives]). :- comment(module,"This interface allows efficient access from XSB to the C-level Smodels API. When using the interface, Smodels can be linked to XSB so that it can be used to evaluate combinatorial or satisfiability problems that may be difficult or inefficient to do directly in XSB. This interface contains two levels: the @em{cooked} level and the @em{raw} level. The cooked level interns rules in an XSB @em{clause store}, and translates general weight constraint rules @cite{SiNS02} into a @em{normal form} that the Smodels engine can evaluate. When the programmer has determined that enough clauses have been added to the store to form a semantically complete sub-program, the program is @em{committed}. This means that information in the clauses is copied to Smodels and interned using Smodels data structures so that stable models of the clauses can be computed and examined. By convention, the cooked interface ensures that the atom @tt{true} is present in all stable models, and the atom @tt{false} is false in all stable models. The raw level models closely the Smodels API, and demands, among other things, that each atom in a stable sub-program has been translated into a unique integer. The raw level also does not provide translation of arbitrary weight constraint rules into the normal form requried by the SModels engine. As a result, the raw level is significantly more difficult to directly use than the cooked level. While we make public the APIs for both the raw and cooked level, we provide support only for users of the cooked interface. As mentioned above Smodels extends normal programs to allow weight constraints, which can be useful for combinatorial problems. However, the syntax used by Smodels for weight constraints does not follow ISO Prolog syntax so that the XSB syntax for weight constraints differs in some respects from that of SModels. Our syntax is defined as follows, where @em{A} is a Prolog atom, @em{N} a non-negative integer, and @em{I} an arbitrary integer. @begin{itemize} @item @em{GeneralLiteral ::= WeightConstraint | Literal } @item @em{WeightConstraint ::= weightConst(Bound,WeightList,Bound)} @item @em{WeightList ::= ""List of WeightLiterals""} @item @em{WeightLiteral ::= Literal | weight(Literal,N)} @item @em{Literal ::= A | not(A)} @item @em{Bound ::== I | undef} @end{itemize} Thus an example of a weight constraint might be: @begin{itemize} weightConst(1,[weight(a,1),weight(not(b),1)],2) @end{itemize} We note that if a user does not wish to put an upper or lower bound on a weight constraint, she may simply set the bound to @tt{undef} or to an integer less than @tt{0}. The intuitive semantics of a weight constraint @tt{weightConst(Lower,WeightList,Upper)}, in which @tt{List} is is list of @em{WeightLiterals} that it is true in a model @em{M} whenever the sum of the weights of the literals in the constraint that are true in @em{M} is between the lower @tt{Lower} and @tt{Upper}. Any literal in a @em{WeightList} that does not have a weight explicitly attached to it is taken to have a weight of @em{1}. In a typical session, a user will initialize the Smodels interface, add rules to the clause store until it contains a semantically meaningful sub-problem. He can then specify a compute statement if needed, commit the rules, and compute and examine stable models via backtracking. If desired, the user can then re-initialize the interface, and add rules to or retract rules from the clause store until another semantically meaningful sub-program is defined; and then commit, compute and examine another stable model @footnote{Currently, only normal rules can be retracted.}. Neither the raw nor the cooked interface currently supports explicit negation. The process of adding information to a store and periodically evaluating it is vaguely reminiscent of the Constraint Logic Programming (CLP) paradigm, but there are important differences. In CLP, constraints are part of the object language of a Prolog program: constraints are added to or projected out of a constraint store upon forward execution, removed upon backwards execution, and iteratively checked. When using this interface, on the other hand, an XSB program essentially acts as a compiler for the clause store, which is treated as a target language. Clauses must be explicitly added or removed from the store, and stable model computation cannot occur incrementally -- it must wait until all clauses have been added to the store. We note in passing that the @tt{xnmr} module provides an elegant but specialized alternative. @tt{xnmr} integrates stable models into the object language of XSB, by computing ""relevant"" stable models from the the residual answers produced by query evaluation. It does not however, support the weighted constriant rules, compute statements and so on that this module supports. "). %------------------ retract_clause_store:- retractall('$sm_pos_compute'(_)), retractall('$sm_neg_compute'(_)), retractall('$sm_atomnum'(_,_)), retractall('$sm_basicrule'(_,_,_)), retractall('$sm_weightrule'(_,_,_,_)), retractall('$sm_constraintrule'(_,_,_,_)), retractall('$sm_choicerule'(_,_,_)). :- comment(smcInit/0,"Initializes the XSB clause store and the Smodels API. This predicate must be executed before building up a clause store for the first time. The corresponding raw predicate, @pred{smrInit(Num)}, initializes the Smodels API assuming that it will require at most @tt{Num} atoms."). smcInit:- smodelsInit, retract_clause_store, conset('$sm_atomnum', 0), % false is 0, true is conset(sm_gennum_val, 0), smcAddRule(true,[]), translate_atom(false,_Num), smcSetCompute([not(false)]). :- comment(smcReInit/0,"Reinitializes the Smodels API, but does @em{not} affect the XSB clause store. This predicate is provided so that a user can reuse rules in a clause store in the context of more than one sub-program."). smcReInit:- smodelsInit. :- comment(hide,smrInit/1). smrInit(NumAtoms):- smodelsInit, smodelsNumAtoms(NumAtoms). %----------------------------------------------------------- % Adding Rules %----------------------------------------------------------- :- comment(smcAddRule/2,"@tt{smcAddRule(Head,Body)} interns a ground rule into the XSB clause store. @tt{Head} must be a @em{GeneralLiteral} as defined at the beginning of this section, and @tt{Body} must be a list of @em{GeneralLiterals}. Upon interning, the rule is translated into a normal form, if necessary, and atoms are translated to unique integers. The corresponding raw predicates, @pred{smrAddBasicRule/3}, @pred{smrAddChoiceRule/3}, @pred{smrAddConstraintRule/4}, and @pred{smrAddWeightRule/3} can be used to add raw predicates immediately into the SModels API. "). smcAddRule(Head,Body):- (member(weightConst(_,_,_),[Head|Body]) -> smcAddGeneralRule(Head,Body) ; smcAddBasicRule(Head,Body) ). %---------------- smcAddGeneralRule(Head,Body):- translateWCHead(Head,NewHead,LowH,UpH), translateWCBody(Body,NBdy), (is_list(NewHead) -> smcAddChoiceRule(NewHead,NBdy), (LowH \== undef -> smcAddBasicRule(false,[not(LowH)|NBdy]) ; true), (UpH \== undef -> smcAddBasicRule(false,[UpH|NBdy]) ; true) ; smcAddBasicRule(NewHead,NBdy) ). translateWCHead(weightConst(Lower,Literals,Upper), LitsOut, LowH, UpH):- !, translateWC(weightConst(Lower,Literals,Upper), LitsOut, LowH, UpH). translateWCHead(Head,Head,undef,undef):- atomic(Head). translateWCBody([],[]). translateWCBody([weightConst(Lower,Literals,Upper)|R],Lits):- !, translateWC(weightConst(Lower,Literals,Upper),_,LowH,UpH), (UpH \== undef -> Lits = [not(UpH)|Lits1] ; Lits = Lits1), (LowH \== undef -> Lits1 = [LowH|Lits2] ; Lits1 = Lits2), translateWCBody(R,Lits2). translateWCBody([H|R],[H|R1]):- translateWCBody(R,R1). translateWC(weightConst(Lower,Literals,Upper),Litsout,LowHead,UpHead):- extract_literals(Literals,Litsout,Has_weights), (is_undef(Lower) -> LowHead = undef ; sm_gensym(lower, LowHead), (nonvar(Has_weights) -> smcAddWeightRule(LowHead,Literals,Lower) ; smcAddConstraintRule(LowHead,Literals,Lower) ) ), (is_undef(Upper) -> UpHead = undef ; sm_gensym(upper, UpHead), Upper1 is Upper + 1, (nonvar(Has_weights) -> smcAddWeightRule(UpHead,Literals,Upper1) ; smcAddConstraintRule(UpHead,Literals,Upper1) ) ). is_undef(undef):-!. is_undef(N):- number(N),N < 0. extract_literals([],[],_). extract_literals([weight(not(_L),_W)|R],R1,1):- !, extract_literals(R,R1,1). extract_literals([weight(L,_W)|R],[L|R1],1):- !, extract_literals(R,R1,1). extract_literals([not(_L)|R],R1,Has_weights):- extract_literals(R,R1,Has_weights). extract_literals([L|R],[L|R1],Has_weights):- extract_literals(R,R1,Has_weights). sm_gensym(Root, Sym) :- (atom(Root),var(Sym) -> sm_gennum(N), number_codes(N,NLst), atom_codes(NAtm, NLst), str_cat(Root, NAtm, Sym) ; abort('Wrong type argument in gensym/2') ). sm_gennum(N) :- conget(sm_gennum_val, O), N is O + 1, conset(sm_gennum_val, N). %---------------- smcAddChoiceRule(Head,Body):- translate_choice_head(Head,A), translate_body(Body,Pos,Neg), assert( '$sm_choicerule'(A,Pos,Neg) ). translate_choice_head([],[]). translate_choice_head([H|T],[Num|NT]):- (H = not(_) -> abort(('negative literal in head of choice rule'(H))) ; true), translate_atom(H,Num), translate_choice_head(T,NT). %---------------- smcAddConstraintRule(Head,Body,Bound):- translate_atom(Head,A), translate_body(Body,Pos,Neg), assert( '$sm_constraintrule'(A,Pos,Neg,Bound) ). %---------------- smcAddWeightRule(Head,Body,Bound):- translate_atom(Head,A), translate_weight_body(Body,Pos,Neg), assert('$sm_weightrule'(A,Pos,Neg,Bound) ). translate_weight_body([],[],[]). translate_weight_body([weight(not(A),W)|R],PR,[weight(N,W)|NR]):- !, translate_atom(A,N), translate_weight_body(R,PR,NR). translate_weight_body([weight(A,W)|R],[weight(N,W)|PR],NR):- !, translate_atom(A,N), translate_weight_body(R,PR,NR). translate_weight_body([not(A)|R],PR,[weight(N,1)|NR]):- !, translate_atom(A,N), translate_weight_body(R,PR,NR). translate_weight_body([A|R],[weight(N,1)|PR],NR):- !, translate_atom(A,N), translate_weight_body(R,PR,NR). %---------------- smcAddBasicRule(Head,Body):- translate_atom(Head,A), translate_body(Body,Pos,Neg), assert( '$sm_basicrule'(A,Pos,Neg) ). translate_atom(Atom,Num):- ('$sm_atomnum'(Atom,Num) -> true ; smNewAtomNum(Num), assert('$sm_atomnum'(Atom,Num)) ). translate_body([],[],[]). translate_body([not(A)|R],PR,[N|NR]):- !, translate_atom(A,N), translate_body(R,PR,NR). translate_body([A|R],[N|PR],NR):- !, translate_atom(A,N), translate_body(R,PR,NR). %---------------- :- comment(hide,smrAddBasicRule/3). smrAddBasicRule(Head,Pos,Neg) :- smodelsBeginBasicRule, smodelsAddHead(Head), smAddPositives(Pos), smAddNegatives(Neg), smodelsEndRule. smAddPositives([]). smAddPositives([Pos|LPos]) :- smodelsAddPosBody(Pos), smAddPositives(LPos). smAddNegatives([]). smAddNegatives([Neg|LNeg]) :- smodelsAddNegBody(Neg), smAddNegatives(LNeg). %---------------- :- comment(hide,smrAddChoiceRule/3). smrAddChoiceRule(HeadList,Pos,Neg) :- smodelsBeginChoiceRule, smrAddHeadList(HeadList), smAddPositives(Pos), smAddNegatives(Neg), smodelsEndRule. smrAddHeadList([]). smrAddHeadList([H|T]):- smodelsAddHead(H), smrAddHeadList(T). %---------------- :- comment(hide,smrAddConstraintRule/4). smrAddConstraintRule(Head,Pos,Neg,Weight) :- smodelsBeginConstraintRule, smodelsAddHead(Head), smAddPositives(Pos), smAddNegatives(Neg), smodelsSetBody(Weight), smodelsEndRule. %------------------ :- comment(hide,smrAddWeightRule/4). smrAddWeightRule(Head,Pos,Neg,Weight) :- smodelsBeginWeightRule, smodelsAddHead(Head), smAddWPositives(Pos), smAddWNegatives(Neg), smodelsSetWeight(Weight), smodelsEndRule. smAddWPositives([]). smAddWPositives([weight(Pos,W)|LPos]) :- smodelsAddWPosBody(Pos,W), smAddWPositives(LPos). smAddWPositives([Pos|LPos]) :- smodelsAddWPosBody(Pos,1), smAddWPositives(LPos). smAddWNegatives([]). smAddWNegatives([weight(Pos,W)|LPos]) :- smodelsAddWNegBody(Pos,W), smAddWNegatives(LPos). smAddWNegatives([Pos|LPos]) :- smodelsAddWNegBody(Pos,1), smAddWNegatives(LPos). %----------------------------------------------------------- % Retracting Rules %----------------------------------------------------------- :- comment(smcRetractRule/2,"@tt{smcRetractBasicRule(Head,Body)} retracts a ground (basic) rule from the XSB clause store. Currently, this predicate cannot retract rules with weight constraints: @tt{Head} must be a @em{Literal} as defined at the beginning of this section, and @tt{Body} must be a list of @em{GeneralLiterals}. "). smcRetractRule(Head,Body):- '$sm_atomnum'(Head,A), retranslate_body(Body,Pos,Neg), retractall( '$sm_basicrule'(A,Pos,Neg) ). retranslate_body([],[],[]). retranslate_body([not(A)|R],PR,[N|NR]):- !, '$sm_atomnum'(A,N), retranslate_body(R,PR,NR). retranslate_body([A|R],[N|PR],NR):- !, '$sm_atomnum'(A,N), retranslate_body(R,PR,NR). %----------------------------------------------------------- % Compute statements %----------------------------------------------------------- :- comment(smcSetCompute/1,"@pred{smcSetCompute(+List)} requires that @tt{List} be a list of literals -- i.e. atoms or the default negation of atoms). This predicate ensures that each literal in @tt{List} is present in the stable models returned by Smodels. By convention the cooked interface ensures that @tt{true} is present and @tt{false} absent in all stable models. After translating a literal it calls the raw interface predicates @pred{smrSetPosCompute/1} and @pred{smrSetNegCompute/1}"). smcSetCompute([]). smcSetCompute([L|T]):- smcSetCompute_1(L), smcSetCompute(T). smcSetCompute_1(not(A)):- !, '$sm_atomnum'(A,N), assert('$sm_neg_compute'(N)). smcSetCompute_1(A):- '$sm_atomnum'(A,N), assert('$sm_pos_compute'(N)). :- comment(hide,smrSetPosCompute/1). smrSetPosCompute(N):- smodelsSetPosCompute(N). :- comment(hide,smrSetNegCompute/1). smrSetNegCompute(N):- smodelsSetNegCompute(N). %----------------------------------------------------------- % Computing Models %----------------------------------------------------------- :- comment(smcCommitProgram/0,"This predicate translates all of the clauses from the XSB clause store into the data structures of the Smodels API. It then signals to the API that all clauses have been added, and initializes the Smodels computation. The corresponding raw predicate, @pred{smrCommitProgram}, performs only the last two of these features."). smcCommitProgram :- conget('$sm_atomctr', N), smodelsNumAtoms(N), translate_rules_to_smodels, translate_compute_statements, smodelsCommitRules. /* Data structures: '$sm_basicrule'(Head,Poslist,Neglist). '$sm_choicerule'(Headlist,Poslist,Neglist). '$sm_constraintrule'(Head,Lower,Poslist,Neglist). '$sm_generaterule'(Headlist,Poslist,Neglist). */ translate_rules_to_smodels:- '$sm_basicrule'(Head,Pos,Neg), smrAddBasicRule(Head,Pos,Neg), fail. translate_rules_to_smodels:- '$sm_choicerule'(HeadList,Pos,Neg), smrAddChoiceRule(HeadList,Pos,Neg), fail. translate_rules_to_smodels:- '$sm_constraintrule'(Head,Pos,Neg,Bound), smrAddConstraintRule(Head,Pos,Neg,Bound), fail. translate_rules_to_smodels:- '$sm_weightrule'(Head,Pos,Neg,Bound), smrAddWeightRule(Head,Pos,Neg,Bound), fail. translate_rules_to_smodels. translate_compute_statements:- '$sm_pos_compute'(N), smodelsSetPosCompute(N), fail. translate_compute_statements:- '$sm_neg_compute'(N), smodelsSetNegCompute(N), fail. translate_compute_statements. :- comment(hide,smrCommitProgram/0). smrCommitProgram :- smodelsCommitRules. %------------------ :- comment(smComputeModel/0,"This predicate calls Smodels to compute a stable model, and succeeds if a stable model can be computed. Upon backtracking, the predicate will continue to succeed until all stable models for a given program cache have been computed. @pred{smComputeModel/0} is used by both the raw and the cooked levels."). smComputeModel:- smodelsExistsModel(Var),Var =\= 0, smComputeModel1. smComputeModel1. smComputeModel1:- smComputeModel. :- comment(smcExamineModel/1,"@pred{smcExamineModel/(-Atoms)} returns the list of atoms that are true in the most recently computed stable model. To examine the truth values of particular literals, use @pred{smcExamineModel/2}."). smcExamineModel(Pos):- conget('$sm_atomctr', N), raw_literals_in_model(N,PosNums), translate_atomlist(PosNums,Pos). translate_atomlist([],[]). translate_atomlist([N|NR],[A|AR]):- '$sm_atomnum'(A,N), translate_atomlist(NR,AR). :- comment(smcExamineModel/2,"@pred{smcExamineModel/(+List,-Atoms)} filters the literals in @tt{List} to determine which are true in the most recently computed stable model. These true literals are returned in the list @tt{Atoms}. @pred{smrExamineModel(+N,-Atoms)} provides the corresponding raw interface in which integers from @tt{0} to @tt{N}, true in the most recently computed stable model, are input and output."). smcExamineModel(List,Pos):- literals_in_model(List,Pos). literals_in_model([],[]). literals_in_model([not(A)|R],Pos):- !, ('$sm_atomnum'(A,Num) -> true ; abort(('smcExamineModel/2: ',A, ' is not a valid literal in the smodels cache'))), smodelsCheckAtom(Num,Var), (Var == 0 -> Pos = [not(A)|P] ; Pos = P), literals_in_model(R,P). literals_in_model([A|R],Pos):- ('$sm_atomnum'(A,Num) -> true ; abort(('smcExamineModel/2: ',A, ' is not a valid literal in the smodels cache'))), smodelsCheckAtom(Num,Var), (Var \== 0 -> Pos = [A|P] ; Pos = P), literals_in_model(R,P). :- comment(hide,smrExamineModel/2). smrExamineModel(N,Pos):- raw_literals_in_model(N,Pos). raw_literals_in_model(0,[]):-!. raw_literals_in_model(N,Pos):- smodelsCheckAtom(N,Var), (Var \== 0 -> Pos = [N|P] ; Pos = P), N1 is N - 1, raw_literals_in_model(N1,P). :- comment(smEnd/0,"Reclaims all resources consumed by Smodels and the various APIs. This predicate is used by both the cooked and the raw interfaces."). smEnd :- retract_clause_store, conset('$sm_atomctr', 1), smodelsClose. %----------------------------------------------------------- smNewAtomNum(N1) :- conget('$sm_atomctr', N), N1 is N + 1, conset('$sm_atomctr', N1). :- comment(print_cache/0,"This predicate can be used to examine the XSB clause store, and may be useful for debugging."). print_cache:- '$sm_basicrule'(N,Pos,Neg), '$sm_atomnum'(A,N), translate_poslitlist(Pos,Posatom), translate_neglitlist(Neg,Negatom), writeln(basicrule(A,[Posatom,Negatom])), fail. print_cache:- '$sm_constraintrule'(N,Pos,Neg,Bound), '$sm_atomnum'(A,N), translate_poslitlist(Pos,Posatom), translate_neglitlist(Neg,Negatom), writeln(constrrule(A,weightConst(Bound,[Posatom,Negatom]),undef)), fail. print_cache:- '$sm_choicerule'(Nlist,Pos,Neg), translate_poslitlist(Nlist,Hlist), translate_poslitlist(Pos,Posatom), translate_neglitlist(Neg,Negatom), writeln(choicerule(Hlist,[Posatom,Negatom])), fail. print_cache:- '$sm_weightrule'(N,Pos,Neg,Bound), '$sm_atomnum'(A,N), translate_poslitlist(Pos,Posatom), translate_neglitlist(Neg,Negatom), writeln(weightrule(A,weightConst(Bound,[Posatom,Negatom]),undef)), fail. print_cache. translate_neglitlist([],[]). translate_neglitlist([weight(N,W)|NR],[not(A)=W|AR]):- !, '$sm_atomnum'(A,N), translate_neglitlist(NR,AR). translate_neglitlist([N|NR],[not(A)|AR]):- '$sm_atomnum'(A,N), translate_neglitlist(NR,AR). translate_poslitlist([],[]). translate_poslitlist([weight(N,W)|NR],[A=W|AR]):- !, '$sm_atomnum'(A,N), translate_poslitlist(NR,AR). translate_poslitlist([N|NR],[A|AR]):- '$sm_atomnum'(A,N), translate_poslitlist(NR,AR). end_of_file.