CASP Program

%%
%% LIA theory langauge specifications
%%
%%

#theory lp {
    lin_term {
    - : 2, unary;
    * : 1, binary, left;
    + : 0, binary, left;
    - : 0, binary, left
    };
    bounds{
    - : 4, unary;
    * : 3, binary, left;
    / : 2, binary, left;
    + : 1, binary, left;
    - : 1, binary, left;
    .. : 0, binary, left
    };
    &dom/0 : bounds, {=}, lin_term, head;
    &sum/0   : lin_term, {<=,>=,>,<,=,!=}, bounds, any
}.

%%
%% Encoding TS Problem
%%

road(Y,X):-road(X,Y).
cost(Y,X,C):-cost(X,Y,C).

1{route(X,Y): road(X,Y)}1:-city(X).
1{route(X,Y): road(X,Y)}1:-city(Y).

reached(X):-initial(X).
reached(Y):-reached(X), route(X,Y).

:-city(X), not reached(X).

&dom {0..C} = c(X,Y) :- cost(X,Y,C).
&sum {c(X,Y)} =0 :-cost(X,Y,C), not route(X,Y).
&sum {c(X,Y)} =C :-cost(X,Y,C), route(X,Y).
:- &sum {c(X,Y):cost(X,Y,C)} > W, maxCost(W).

%%
%% Instance TS Problem
%%

city(a). city(b). city(c). city(d).
initial(a).
road(a,b).   road(b,c).   road(c,d).
cost(a,b,1). cost(b,c,1). cost(c,d,1).
road(d,a).   road(a,c).   road(b,d).
cost(d,a,1). cost(a,c,2). cost(b,d,2).
maxCost(4).

CASP Program

EZSMT Output