Commit cc03baa7 authored by Joaquin Arias's avatar Joaquin Arias

Pretty print program+dual+nmr

parent 6c15727c
......@@ -10,7 +10,7 @@ scasp:
## sasp implemented in CIAO
sasp:
time casp -s0 queens_4.pl || true
time casp -s0 hanoi_8.pl || true
time casp -s0 hamcycle_one.pl || true
time casp -s0 hamcycle_two.pl || true
time sasp -s0 queens_4.pl || true
time sasp -s0 hanoi_8.pl || true
time sasp -s0 hamcycle_one.pl || true
time sasp -s0 hamcycle_two.pl || true
duration(load,D) :-
D .<. 23/3, D .>. 10/3.
duration(load,25).
duration(shoot,5).
duration(wait,36).
......@@ -28,6 +27,6 @@ transition(shoot, state(alive, loaded, PrevArmed), state(alive, unloaded, 0)) :-
spoiled(Armed) :- Armed .>. 35.
prohibited(shoot, T) :- T .<. 35.
?- T .<. 40, holds(T, state(dead,_,_), List).
?- T .<. 100, holds(T, state(dead,_,_), List).
#show holds/3.
duration(load,D) :-
D .<. 23/3, D .>. 10/3.
duration(shoot,5).
duration(wait,36).
holds(0,State,[]) :-
init(State).
holds(Time1, FinalState, [Action|As]) :-
Time1 .>. 0,
Time1 .=. Time + Duration,
duration(Action, Duration),
not prohibited(Action, Time1),
transition(Action, PrevState, FinalState),
holds(Time, PrevState, As).
init(state(alive, unloaded, 0)).
transition(load, state(alive, _, _), state(alive, loaded,FinalArmed)) :-
FinalArmed = 0.
transition(wait, state(alive, Gun, PrevArmed), state(alive, Gun, FinalArmed)) :-
duration(wait, D), FinalArmed .=. PrevArmed + D.
transition(shoot, state(alive, loaded, PrevArmed), state(dead, unloaded, 0)) :-
not spoiled(PrevArmed).
transition(shoot, state(alive, loaded, PrevArmed), state(alive, unloaded, 0)) :-
spoiled(PrevArmed).
spoiled(Armed) :- Armed .>. 35.
prohibited(shoot, T) :- T .<. 35.
?- T .<. 40, holds(T, state(dead,_,_), List).
#show holds/3.
% Given 3 birds, which can fly?
#pred penguin(X) :: '@(X) is a penguin'.
penguin(sam). % sam is a penguin
#pred wounded_bird(X) :: '@(X) is a wounded bird'.
wounded_bird(john). % john is wounded
bird(tweety). % tweety is just a bird
#pred bird(X) :: '@(X) is a bird'.
bird(tweety). % tweety is just a bird
% penguines and wounded birds are still birds
bird(X) :- penguin(X).
bird(X) :- wounded_bird(X).
#pred ab(X) :: '@(X:bird) is abnormal'.
% penguins and wounded birds are abnormal
ab(X) :- penguin(X).
ab(X) :- wounded_bird(X).
#pred flies(X) :: '@(X) can fly'.
% birds can fly if they are not abnormal
flies(X) :- bird(X), not ab(X).
#pred -flies(X) :: '@(X) can not fly'.
% explicit closed world assumptions
-flies(X) :- ab(X).
-flies(X) :- -bird(X).
......
......@@ -188,7 +188,7 @@ split_functor(P, N, -1) :- % no arity attached
create_unique_functor(Hi, C, Ho) :-
split_functor(Hi, Fc, A), % Strip the arity
number_chars(C, Cc),
append(Fc, ['.'], Fcc), % Add simbol '.' before the counter
append(Fc, ['_'], Fcc), % Add simbol '_' before the counter
append(Fcc, Cc, Fc2), % Add the counter
number_chars(A, Ac),
append(Fc2, ['_' | Ac], Fc3), % Add the arity back
......
......@@ -1246,13 +1246,13 @@ process_pr_pred_([C|Cs],[C|Rs],Var) :-
process_pr_pred_(Cs,Rs,Var).
process_pr_pred_var([':'|R0],Rs,VAc0,VAc1,NAc) :- !,
reverse(VAc0,VAc1),
process_pr_pred_name(R0,Rs,[],NAc).
process_pr_pred_name(R0,Rs,['\''],NAc).
process_pr_pred_var([')'|Rs],Rs,Ac0,Ac1,['\'','\'']) :- !,
reverse(Ac0,Ac1).
process_pr_pred_var([V0|R0],Rs,Ac0,Ac1,NVar) :-
process_pr_pred_var(R0,Rs,[V0|Ac0],Ac1,NVar).
process_pr_pred_name([')'|Rs],Rs,NAc0,NAc1) :- !,
reverse(NAc0,NAc1).
reverse(['\''|NAc0],NAc1).
process_pr_pred_name([NV0|R0],Rs,NAc0,NAc1) :-
process_pr_pred_name(R0,Rs,[NV0|NAc0],NAc1).
......
......@@ -92,8 +92,7 @@ main(Args) :-
parse_args(Args, Options, Sources),
set_options(Options),
load(Sources),
if_user_option(write_program, write_program),
if_user_option(write_program, halt),
if_user_option(write_program, ( write_program, halt )),
(
current_option(interactive, on) ->
main_loop
......@@ -521,6 +520,7 @@ check_CHS(Goal, I, co_failure) :-
check_CHS(Goal, I, co_failure) :-
predicate(Goal),
\+ table_predicate(Goal),
if_user_option(no_fail_loop, fail),
\+ \+ (
type_loop(Goal, I, fail_pos(S)),
if_user_option(check_calls, format('Positive loop, failling (Goal == ~w)\n',[Goal])),
......@@ -540,10 +540,18 @@ check_CHS(Goal, I, cont) :-
if(
(
predicate(Goal),
\+ ground(Goal),
\+ ground(Goal), %% the current goal is restricted
ground_neg_in_stack(Goal, I)
),
true,true
),
if(
(
predicate(Goal),
ground(Goal), %% the current goal restrict previous results
constrained_neg_in_stack(Goal, I)
),
true,true
).
%% check if the negation is in the stack -> coinductive failure
......@@ -562,12 +570,12 @@ neg_in_stack(Goal, [not(NegGoal)|_]) :-
instance(Goal, NegGoal),
instance(NegGoal, Goal), !,
if_user_option(warning,format("\nWARNING: Co-Failing in a negated loop due to a variant call (extension clp-disequality required).\n\tCurrent call:\t~p\n\tPrevious call:\t~p\n",[Goal,NegGoal])).
% neg_in_stack(not(Goal), [NegGoal|_]) :-
% Goal =.. [Name|ArgGoal],
% NegGoal =.. [Name|NegArgGoal],
% if_user_option(check_calls, format('\t\tCheck if not(~p) entails (is more particular than) ~p\n',[Goal,NegGoal])),
% entail_list(ArgGoal, NegArgGoal), !,
% if_user_option(check_calls, format('\t\tOK\n',[])).
%% neg_in_stack(not(Goal), [NegGoal|_]) :-
%% Goal =.. [Name|ArgGoal],
%% NegGoal =.. [Name|NegArgGoal],
%% if_user_option(check_calls, format('\t\tCheck if not(~p) entails (is more particular than) ~p\n',[Goal,NegGoal])),
%% entail_list(ArgGoal, NegArgGoal), !,
%% if_user_option(check_calls, format('\t\tOK\n',[])).
% neg_in_stack(Goal, [not(NegGoal)|_]) :-
% Goal =.. [Name|ArgGoal],
% NegGoal =.. [Name|NegArgGoal],
......@@ -629,6 +637,28 @@ ground_neg_in_stack_(Goal, [_|Ss], Intervening, MaxInter, Flag) :- !,
NewInter is Intervening + 1,
ground_neg_in_stack_(Goal, Ss, NewInter, NewMaxInter, Flag).
% restrict even more the constrained in the stack
constrained_neg_in_stack(_,[]).
constrained_neg_in_stack(not(Goal), [NegGoal|Ss]) :-
Goal =.. [Name|ArgGoal],
NegGoal =.. [Name|NegArgGoal],
if_user_option(check_calls, format('\t\tCheck if not(~p) is consistent with ~p\n',[Goal,NegGoal])), !,
loop_list(ArgGoal, NegArgGoal), !,
if_user_option(check_calls, format('\t\tOK\n',[])),
constrained_neg_in_stack(not(Goal), Ss).
constrained_neg_in_stack(Goal, [not(NegGoal)|Ss]) :-
Goal =.. [Name|ArgGoal],
NegGoal =.. [Name|NegArgGoal],
if_user_option(check_calls, format('\t\tCheck if not(~p) is consistent with ~p\n',[Goal,NegGoal])), !,
loop_list(ArgGoal, NegArgGoal), !,
if_user_option(check_calls, format('\t\tOK\n',[])),
constrained_neg_in_stack(Goal, Ss).
constrained_neg_in_stack(Goal, [_|Ss]) :-
constrained_neg_in_stack(Goal, Ss).
%% proved_in_stack
proved_in_stack(Goal, S) :-
proved_in_stack_(Goal, S, 0, -1),
......
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment