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_compile, 29 [ scasp_load/2, % :Sources, +Options 30 scasp_compile/2, % :Terms, +Options 31 scasp_compile_query/3, % :Goal,-Query,+Options 32 scasp_query/1, % :Query 33 scasp_query/3 % :Query, -Bindings, +Options 34 ]). 35:- use_module(library(error)). 36:- use_module(library(lists)). 37:- use_module(library(option)). 38:- use_module(library(prolog_code)). 39:- use_module(predicates). 40:- use_module(common). 41 42/** <module> s(ASP) Ungrounded Stable Models Solver 43 44Read in a normal logic program. Compute dual rules and the NMR check. Execute 45the modified program according to the stable model semantics and output the 46results. 47 48@author Kyle Marple 49@version 20170127 50@license BSD-3 51*/ 52 53:- use_module(input). 54:- use_module(program). 55:- use_module(comp_duals). 56:- use_module(nmr_check). 57:- use_module(pr_rules). 58:- use_module(variables). 59 60:- meta_predicate 61 scasp_load(:, +), 62 scasp_compile(:, +), 63 scasp_query(:), 64 scasp_query(:, -, +), 65 scasp_compile_query(:, -, +). 66 67%! scasp_load(:Sources, +Options) 68% 69% Load the files from Sources. Steps taken: 70% 71% - Parse input and assert in dynamic predicates with 72% program.pl (defined_rule/4, etc,) 73% - Enrich the program in the same format (comp_duals/0, 74% generate_nmr_check/0). 75% - Transform into _pr_ rules (generate_pr_rules/1) 76% - Destroy the program dynamic predicates. 77% 78% @arg Sources A list of paths of input files. 79 80:- det(scasp_load/2). 81scasp_load(M:Spec, Options) :- 82 to_list(Spec, Sources), 83 call_cleanup( 84 scasp_load_guarded(M:Sources, Options), 85 destroy_program). 86 87to_list(List, List) :- 88 is_list(List), 89 !. 90to_list(One, [One]). 91 92scasp_load_guarded(M:Sources, Options) :- 93 clean_pr_program(M), 94 load_source_files(Sources), 95 comp_duals, 96 generate_nmr_check(M), 97 generate_pr_rules(M:Sources, Options). 98 99%! scasp_compile(:Terms, +Options) is det. 100% 101% Create an sCASP program from Terms. 102 103scasp_compile(M:Terms, Options) :- 104 call_cleanup( 105 scasp_compile_guarded(M:Terms, Options), 106 destroy_program). 107 108scasp_compile_guarded(M:Terms, Options) :- 109 clean_pr_program(M), 110 scasp_load_terms(Terms, Options), 111 comp_duals, 112 generate_nmr_check(M), 113 generate_pr_rules(M:_Sources, Options). % ignored anyway 114 115%! scasp_compile_query(:Goal, -Query, +Options) is det. 116 117scasp_compile_query(M:Goal, M:Query, Options) :- 118 conj_to_list(Goal, Q0), 119 maplist(intern_negation, Q0, Q1), 120 add_nmr(Q1, Query, Options), 121 maplist(check_existence(M), Query). 122 123conj_to_list(true, []) :- 124 !. 125conj_to_list(Conj, List) :- 126 comma_list(Conj, List). 127 128add_nmr(Q0, Q, Options) :- 129 option(nmr(false), Options), 130 Q = Q0. 131add_nmr(Q0, Q, _Options) :- 132 append(Q0, [o_nmr_check], Q). 133 134check_existence(M, G) :- 135 shown_predicate(M:G), 136 !. 137check_existence(_,G) :- 138 prolog_builtin(G), 139 !. 140check_existence(_,G) :- 141 clp_builtin(G), 142 !. 143check_existence(_,G) :- 144 clp_interval(G), 145 !. 146check_existence(_,_ is _) :- 147 !. 148check_existence(_, G) :- 149 scasp_pi(G, PI), 150 existence_error(scasp_predicate, PI). 151 152scasp_pi(not(G), PI) :- 153 !, 154 scasp_pi(G, PI). 155scasp_pi(G, PI) :- 156 pi_head(PI, G). 157 158%! scasp_query(:Query) is det. 159% 160% True when Query is the (last) sCASP query that is part of the 161% program. 162% 163% @error existence_error(scasp_query, Module) 164 165scasp_query(M:_Query) :- 166 M:pr_query([not(o_false)]), !, 167 existence_error(scasp_query, M). 168scasp_query(M:Query) :- 169 M:pr_query(Query). 170 171%! scasp_query(:Query, -Bindings, +Options) is det. 172% 173% True when Query is the s(CASP) query as a list that includes the NMR 174% check if required. Bindings is a list of `Name=Var` terms expressing 175% the names of the variables. 176 177scasp_query(M:Query, Bindings, Options) :- 178 scasp_query(M:Query0), 179 process_query(M:Query0, _, M:Query, Bindings, Options), 180 maplist(check_existence(M), Query). 181 182process_query(M:Q, M:Query, M:TotalQuery, VarNames, Options) :- 183 revar(Q, A, VarNames), 184 ( is_list(A) 185 -> Query = A 186 ; comma_list(A, Query) 187 ), 188 ( option(nmr(false), Options) 189 -> TotalQuery = Query 190 ; append(Query, [o_nmr_check], TotalQuery) 191 )