1/* 2* Copyright (c) 2016, University of Texas at Dallas 3* All rights reserved. 4* 5* Redistribution and use in source and binary forms, with or without 6* modification, are permitted provided that the following conditions are met: 7* * Redistributions of source code must retain the above copyright 8* notice, this list of conditions and the following disclaimer. 9* * Redistributions in binary form must reproduce the above copyright 10* notice, this list of conditions and the following disclaimer in the 11* documentation and/or other materials provided with the distribution. 12* * Neither the name of the University of Texas at Dallas nor the 13* names of its contributors may be used to endorse or promote products 14* derived from this software without specific prior written permission. 15* 16* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" 17* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE 18* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE 19* DISCLAIMED. IN NO EVENT SHALL THE UNIVERSITY OF TEXAS AT DALLAS BE LIABLE FOR 20* ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES 21* (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 22* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND 23* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 24* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS 25* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 26*/ 27 28:- module(scasp_program, 29 [ defined_rule/4, 30 defined_query/2, 31 defined_predicates/1, 32 defined_nmr_check/1, 33 defined_directive/1, 34 reserved_prefix/1, 35 has_prefix/2, 36 replace_prefix/4, % +FunctorIn,+OldPrefix,+NewPrefix,-Functor 37 non_printable/1, % +Name 38 assert_program/1, 39 assert_rule/1, 40 assert_nmr_check/1, 41 destroy_program/0 42 ]). 43 44/** <module> Input program access 45 46Allow access to input program rules and query by asserting them and exporting 47the resulting dynamic predicates. 48 49@author Kyle Marple 50@version 20170628 51@license BSD-3 52*/ 53 54:- use_module(library(lists)). 55:- use_module(library(apply)). 56:- use_module(library(debug)). 57 58:- use_module(common). 59:- use_module(variables). 60 61%! defined_rule(+Name:atom, +FullHead:compound, -Body:list, -Origin:compound) is nondet 62% 63% Dynamic predicate for asserted rules. 64% 65% @arg Head Head predicate has head/arity (no args). 66% @arg FullHead A predicate struct containing the head predicate with args. 67% @arg Body list of body goals. 68% @arg Origin A term describing the origin of this rule. For rules that are derived 69% from loaded clauses, Origin is set to `clause(ClauseRef)`; for compiler 70% generated rules, Origin is set to `generated(Why)` where `Why` is one 71% of `neg` for classical negation, `nmr` for NMR checks, and `dual` for dual rules; 72% for rules read directly as s(CASP) with e.g. `load_source_files/1`, Origin is set 73% to `source(Path, Pos)` where `Path` is the path of the source file, 74% and `Pos` is a term describing the postition and layout of the rule in the file. 75 76%! defined_query(-Goals:list, -SolCount:int) is det 77% 78% Dynamic predicate for query. 79% 80% @arg Goals List of goals in the query. 81% @arg SolCount The number of answer sets to compute. 82 83%! defined_predicates(-Predicates:list) is det 84% 85% Dynamic predicate for the list of predicate symbols defined in the 86% input program. 87% 88% @arg Predicates List of predicate structs. 89 90%! defined_nmr_check(+Subchecks:list) is det 91% 92% Dynamic predicate for the list of NMR sub-checks. 93% 94% @arg Subchecks The list of subcheck goals. 95 96% These predicates are filled by assert_program/1 from the output of the 97% parser. scasp_load/1 realizes the entire compilation chain. 98% Body terms contains variables as e.g. `'X'`. 99 100:- thread_local 101 defined_rule/4, % Name, Head, Body, Origin 102 defined_query/2, % Body, Count 103 defined_predicates/1, % list(Name) (1 clause) 104 defined_nmr_check/1, 105 defined_directive/1. % directive 106 107%! program(?ProgramStruct:compound, ?Rules:list, ?Directives:list, 108%! ?Query:compound) is det 109% 110% Convert a program structure into its components, or vice-versa. 111% 112% @arg ProgramStruct Program structure. 113% @arg Rules List of rules. 114% @arg Directives List of directives. 115% @arg Query Query structure. 116 117program(p(Rules, Directives, Query), Rules, Directives, Query). 118 119%! query(?QueryStruct:compound, ?Query:list, ?NMR_Check:list, 120%! ?SolutionCount:int) is det 121% 122% Convert a query structure to its components, or vice-versa. 123% NMR_Check will be unbound until after nmr_check:generate_nmr_check/0 124% has finished. 125% 126% @arg QueryStruct Query structure. 127% @arg Query List of query goals. 128% @arg NMR_Check List of NMR check goals (heads of NMR sub-checks). 129% @arg SolutionCount Hard-coded solution count. 130 131query(c(Q, Nmr_check, N), Q, Nmr_check, N). 132 133%! reserved_prefix(+Prefix:ground) is det 134% 135% Define reserved prefixes for predicates and compound terms. These 136% take the form of a single letter followed by an underscore. This 137% predicate just tests the letter. The dummy prefix (`o_`) is appended 138% to predicates and compound terms that either begin with an 139% underscore (legal in ASP but not Prolog) or with a reserved prefix. 140% It will be removed last before printing, and at most one copy will 141% be removed, ensuring that user-defined predicates starting with a 142% reserved prefix won't be processed the same as internally created 143% ones. 144% 145% @arg Prefix The letter portion of the prefix. 146 147reserved_prefix('c'). % classical negation 148reserved_prefix('n'). % dual rule prefix 149reserved_prefix('d'). % dummy prefix 150 151%! has_prefix(+Functor:atom, -Prefix:atom) is semidet. 152% 153% Succeed if Functor begins with a reserved prefix, returning the 154% character part of the (first) prefix. 155% 156% @arg Functor The functor to test. 157% @arg Prefix The character of the (first) reserved prefix of the 158% functor. 159 160has_prefix(F, C) :- 161 sub_atom(F, 1, _, _, '_'), 162 sub_atom(F, 0, 1, _, C), 163 reserved_prefix(C). % the letter is a reserved prefix 164 165%! replace_prefix(+FunctorIn, +OldPrefix, +NewPrefix, -Functor) 166 167replace_prefix(F0, P0, P, F) :- 168 string_concat(P0, B, F0), 169 atom_concat(P, B, F). 170 171%! non_printable(+Name) is semidet. 172% 173% True if Name should not be printed. This is true if it starts with 174% an underscore or has a normal prefix and then an underscore. 175 176non_printable(Name) :- 177 sub_atom(Name, 0, _, _, '_'), 178 !. 179non_printable(Name) :- 180 sub_atom(Name, 1, _, _, '__'), 181 !. 182 183 184%! assert_program(+Statements:list) is det 185% 186% Get rules, initial query and called predicates and assert them for 187% easy access. This fills the dynamic predicates 188% 189% - defined_predicates(List) with a list of predicate identifiers, 190% atoms encoded as <name>_<arity>, e.g., `parent_2` for parent/2. 191% - defined_rule(Name, Head, Body, Origin) where Name is the functor name 192% of Head and Body represents the conjunction of the body as a 193% list, and Origin denotes the source of the rule's definition. 194% - defined_query(List, Count) 195% List is like Body above, expressing the query and Count is the 196% number of answer sets to generate by default (based on the 197% `Count { Query }.` syntax. 198% - defined_nmr_check(List) 199% When defined, a list of one atom containing the rule name for the 200% NMR check. 201% 202% @arg Statements List of rules and compute statements produced by DCG. 203 204:- det(assert_program/1). 205 206assert_program(Stmts) :- 207 debug(scasp(compile), 'Converting program to internal format...', []), 208 format_program(Stmts, Program), 209 get_predicates(Program, Predicates), 210 assert_predicates(Predicates), 211 assert_program_struct(Program), 212 maplist(handle_classical_negation, Predicates). 213 214%! format_program(+Statements:list, -Program:compound) is det 215% 216% Convert the list of statements to a program structure containing a 217% list of rules and a single query. Queries are generated from compute 218% statements. Use the last compute statement encountered, or a default 219% one if no other is found. The default will always succeed during 220% execution, so the answer set returned will rely on the NMR check. 221% 222% @arg Statements List of rules and compute statements produced by DCG. 223% @arg Program Program data struct. 224 225format_program([], P) :- 226 !, % no program 227 predicate(G, '_false_0', []), 228 query(Q, [not(G)], _, 1), 229 program(P, [], [], Q). 230format_program(X, P) :- 231 predicate(G, '_false_0', []), 232 AScount = 1, 233 query(Q2, [not(G)], _, AScount), 234 sort_by_type(X, R, D, Q2, Q), 235 program(P, R, D, Q). 236 237%! sort_by_type(+Statements:list, -Rules:list, -Directives:list, 238%! +ComputeIn:compound, -ComputeOut:compound) is det 239% 240% Take a list of statements, return a list of rules and the last 241% compute statement encountered. Compute statement will be formatted 242% as a query. 243% 244% @arg Statements List of rules and compute statements produced by DCG. 245% @arg Rules extracted from Statements. Each rule is a term Head-Body. 246% @arg Directives is a list of plain directive terms (without # or :-) 247% @arg ComputeIn compute statement. @arg ComputeOut compute statement. 248% Only the final compute statement is kept. 249 250:- det(sort_by_type/5). 251 252sort_by_type([source(Ref, X)|T], [source(Ref, X)|R], D, Ci, Co) :- 253 c_rule(X, _, _), 254 !, 255 sort_by_type(T, R, D, Ci, Co). 256sort_by_type([source(_, X)|T], R, D, _, Co) :- 257 X = c(N, Q), 258 query(C, Q, _, N), 259 !, 260 sort_by_type(T, R, D, C, Co). 261sort_by_type([source(_, (:-(Directive)))|T], R, [Directive|D], C, Co) :- 262 !, 263 sort_by_type(T, R, D, C, Co). 264sort_by_type([], [], [], C, C). 265 266%! get_predicates(+Program:compound, -Predicates:list) is det 267% 268% Get a list of the predicate symbols used in the rules or query of 269% the program. This includes predicates that are called but not 270% defined. The internal-use predicate ``_false_0`` should be included 271% explictly, in case a hard-coded query overrode the default one. We 272% add ``_false_0`` as head of the query for that purpose. This both 273% gets the query in the shape of a rule and ensures ``_false_0`` is 274% included. 275% 276% @arg Program A program struct. 277% @arg Predicates A list of predicate symbols defined in the program. 278 279:- det(rule_predicates/2). 280 281get_predicates(P, Ps) :- 282 program(P, R, _, Q), 283 query(Q, Qs, _, _), 284 rules_predicates(['_false_0'-Qs|R], Ps). 285 286rules_predicates(Rules, Preds) :- 287 maplist(rule_predicates, Rules, Preds0), 288 append(Preds0, Preds1), 289 list_to_set(Preds1, Preds). 290 291rule_predicates(source(_, R), Preds) :- 292 !, 293 rule_predicates(R, Preds). 294rule_predicates(R, Preds) :- 295 c_rule(R, H, B), 296 atom_predicate(H, F), 297 convlist(atom_predicate, B, FB), 298 list_to_set([F|FB], Preds). 299 300atom_predicate(not(X), P) :- 301 atom_predicate(X, P). 302atom_predicate(X, F) :- 303 predicate(X, F, _). 304 305%! handle_classical_negation(+Predicate:atom) is det 306% 307% If Predicate is classically negated (in the source starts with '-'). 308% Assign the required number of variables, then create a rule of the 309% form 310% 311% :- -x, x. 312% 313% @arg Predicate is the name (atom) of a predicate 314 315handle_classical_negation(X) :- 316 has_prefix(X, 'c'), % classically negated literal 317 atom_concat(c_, Xn, X), % non-negated literal 318 defined_predicates(P), 319 memberchk(Xn, P), % only add constraint if non-negated literal is actually used. 320 !, 321 split_functor(X, _, N), % get arity 322 var_list(N, A), % get args, 323 X2 =.. [X|A], 324 Xn2 =.. [Xn|A], 325 predicate(H, '_false_0', []), % dummy head for headless rules 326 c_rule(R, H, [X2, Xn2]), 327 assert_rule(neg(R)). 328handle_classical_negation(_). 329 330%! assert_program_struct(+Program:compound) is det 331% 332% Assert rules and query from program struct. 333% 334% @arg Program A program struct. 335 336assert_program_struct(P) :- 337 program(P, R, D, Q), 338 maplist(assert_rule, R), 339 maplist(assert_directive, D), 340 assert_query(Q). 341 342%! assert_rule(+Rule:compound) is det 343% 344% Assert a program rule. 345% 346% @arg Rule A rule struct. 347 348:- det(assert_rule/1). 349 350assert_rule(Rule) :- 351 rule_origin(Rule, Origin, R), 352 assert_rule_(R, Origin). 353 354assert_rule_(Rule, Origin) :- 355 c_rule(Rule, H2, B), 356 predicate(H2, H, _), % get the head without args 357 assertz(defined_rule(H, H2, B, Origin)). 358 359rule_origin(source(Ref, Rule), Ref, Rule). 360rule_origin(neg(Rule), generated(neg), Rule). 361rule_origin(nmr(Rule), generated(nmr), Rule). 362rule_origin(dual(Rule), generated(dual), Rule). 363 364 365%! assert_directive(+Directive) is det 366% 367% Assert a directive 368% 369% @arg Directive is a term table(Pred), show(Pred) or pred(Pred) 370 371assert_directive(D) :- 372 assertz(defined_directive(D)). 373 374%! assert_query(+Query:compound) is det 375% 376% Assert the initial query. 377% 378% @arg Query A query struct. 379 380assert_query(Q) :- 381 query(Q, Qs, _, N), 382 assertz(defined_query(Qs, N)). 383 384%! assert_nmr_check(+NMR:list) is det 385% 386% Assert the NMR check. 387% 388% @arg NMR The list of goals in the NMR check. 389 390assert_nmr_check(NMR) :- 391 c_rule(R, '_nmr_check_0', NMR), 392 assert_rule(nmr(R)), 393 assertz(defined_nmr_check(['_nmr_check_0'])). 394 395%! assert_predicates(+Predicates:list) is det. 396% 397% Assert the list of defined predicate symbols. 398% 399% @arg Predicates A list of predicates. 400 401assert_predicates(Ps) :- 402 assertz(defined_predicates(Ps)). 403 404%! destroy_program 405% 406% Remove all asserted predicates to allow multiple funs with different 407% programs. 408 409destroy_program :- 410 retractall(defined_rule(_, _, _, _)), 411 retractall(defined_query(_, _)), 412 retractall(defined_predicates(_)), 413 retractall(defined_nmr_check(_)), 414 retractall(defined_directive(_))