Skip to content

Commit

Permalink
Add some options
Browse files Browse the repository at this point in the history
  • Loading branch information
sthiele committed Apr 30, 2024
1 parent e72b700 commit e199024
Show file tree
Hide file tree
Showing 2 changed files with 67 additions and 113 deletions.
33 changes: 25 additions & 8 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,19 @@ use std::io::Write;

#[derive(Serialize, Deserialize)]
pub struct Config {
break_after_head: bool,
break_after_body_atom: bool,
break_after_colon: bool,
soft_flush_limit: usize,
}
impl Default for Config {
fn default() -> Self {
Self { soft_flush_limit: 60 }
Self {
break_after_head: true,
break_after_body_atom: false,
break_after_colon: false,
soft_flush_limit: 60,
}
}
}

Expand Down Expand Up @@ -111,7 +119,7 @@ pub fn format_program(
source_code: &[u8],
out: &mut dyn Write,
debug: bool,
config: &Config,
config: &Config,
) -> Result<()> {
let mut formatter = Formatter {
out,
Expand Down Expand Up @@ -163,7 +171,7 @@ pub fn format_program(
"statement" => {
let mut buf = Vec::new();
let stmt_type =
format_statement(&node, source_code, &mut buf, debug,config)?;
format_statement(&node, source_code, &mut buf, debug, config)?;

formatter.process_statement(stmt_type, &buf)?;
short_cut = true;
Expand Down Expand Up @@ -233,7 +241,7 @@ fn format_statement(
source_code: &[u8],
out: &mut dyn Write,
debug: bool,
config: &Config,
config: &Config,
) -> Result<StatementType> {
let mut buf: Vec<u8> = vec![];
let mut soft_flush = false;
Expand Down Expand Up @@ -430,9 +438,15 @@ fn format_statement(
"COLON" => {
if state.in_theory_atom_definition | state.is_show {
write!(buf, " ")?;
} else if state.in_conjunction | state.in_optcondition {
} else if config.break_after_colon
&& (state.in_conjunction | state.in_optcondition)
{
mindent_level += 1;
flush = true;
} else {
write!(buf, " ")?;
mindent_level += 1;
soft_flush = true;
}
}
"LBRACE" => {
Expand All @@ -444,20 +458,23 @@ fn format_statement(
}
}
"COMMA" => {
if state.in_termvec == 0 && !state.is_show {
if config.break_after_body_atom && state.in_termvec == 0 && !state.is_show {
flush = true;
} else {
write!(buf, " ")?;
soft_flush = true;
}
soft_flush = true;
}
"IF" => {
state.has_if = true;
mindent_level += 1; // decrease after bodydot
if !state.has_head_like {
write!(buf, " ")?;
} else {
} else if config.break_after_head {
flush = true;
} else {
write!(buf, " ")?;
soft_flush = true;
}
}
_ => {}
Expand Down
147 changes: 42 additions & 105 deletions src/tests.rs
Original file line number Diff line number Diff line change
@@ -1,19 +1,17 @@
use super::*;
const CONFIG : Config = Config{
soft_flush_limit: 60,
};

/// function to simplify tests
fn fmt_and_cmp(source_code: &str, res: &str) {

let mut buf = Vec::new();
let mut parser = tree_sitter::Parser::new();
parser
.set_language(&tree_sitter_clingo::language())
.expect("Error loading clingo grammar");

let tree = parser.parse(&source_code, None).unwrap();
let config = Config::default();

format_program(&tree, source_code.as_bytes(), &mut buf, false,&CONFIG).unwrap();
format_program(&tree, source_code.as_bytes(), &mut buf, false, &config).unwrap();
let parse_res = std::str::from_utf8(&buf).unwrap();
assert_eq!(parse_res, res)
}
Expand Down Expand Up @@ -210,139 +208,89 @@ sel_vat(H, V) :- sel_vat(N,W) : cons(Identifier,var(N,W));
"#;
let result = r#"% Derive (varying) atoms
atom(A) :-
model(M),
true(M, A).
model(M), true(M, A).
vary(A) :-
model(M),
atom(A),
not true(M, A).
model(M), atom(A), not true(M, A).
% Derive lower bound LB and upper bound UB for size of prime implicants
% - LB: minimum number of varying atoms s.t. interpretations don't exceed models
% - UB: minimum of number of varying atoms and number of non-models
varies(X) :-
X = #count {
A :
vary(A)
A : vary(A)
}.
models(Y) :-
Y = #count {
M :
model(M)
M : model(M)
}.
:- models(0).
% must have some model
minsize(Y, 2**X, 0) :-
varies(X),
models(Y),
1 < Y.
varies(X), models(Y), 1 < Y.
% nothing varies if one model
minsize(Y, Z/2, L+1) :-
minsize(Y, Z, L),
Y < Z.
minsize(Y, Z, L), Y < Z.
bounds(L, (X+F- | X-F | )/2) :-
varies(X),
minsize(Y, Z, L),
not minsize(Y, Z/2, L+1),
F = 2**X-Y.
varies(X), minsize(Y, Z, L), not minsize(Y, Z/2, L+1), F = 2**X-Y.
% Select literals for prime implicant
select(A, 1) :-
atom(A),
not vary(A).
atom(A), not vary(A).
{
select(A, 0..1)
} < 2 :-
vary(A),
not bounds(0, 0).
vary(A), not bounds(0, 0).
selected(A) :-
select(A, V),
vary(A).
select(A, V), vary(A).
% Check lower and upper bounds via "Sinz counter" on selected varying atoms
index(A, I) :-
vary(A),
I = #count {
B :
vary(B),
B <= A
},
not bounds(0, 0).
vary(A), I = #count {
B : vary(B), B <= A
}, not bounds(0, 0).
counter(I, 1) :-
index(A, I),
bounds(L, U),
L <= I,
selected(A).
index(A, I), bounds(L, U), L <= I, selected(A).
counter(I, C+1) :-
index(A, I),
bounds(L, U),
C < U,
selected(A),
counter(I+1, C).
index(A, I), bounds(L, U), C < U, selected(A), counter(I+1,
C).
counter(I, C) :-
index(A, I),
bounds(L, U),
L < C+I,
counter(I+1, C).
index(A, I), bounds(L, U), L < C+I, counter(I+1, C).
:- bounds(L, U),
0 < L,
not counter(1, L).
:- bounds(L, U), 0 < L, not counter(1, L).
:- bounds(L, U),
index(A, I),
selected(A),
counter(I+1, U).
:- bounds(L, U), index(A, I), selected(A), counter(I+1, U).
% Derive models excluded by (some) selected literal
exclude(M, A) :-
model(M),
select(A, 0),
true(M, A).
model(M), select(A, 0), true(M, A).
exclude(M, A) :-
model(M),
select(A, 1),
not true(M, A).
model(M), select(A, 1), not true(M, A).
excluded(M) :-
exclude(M, A).
% Check that all interpretations extending prime implicant are models
:- bounds(L, U),
varies(X),
models(Y),
#sum {
2**(X-Z) :
Z = L+1..X,
not counter(1, Z);
1, M :
excluded(M)
:- bounds(L, U), varies(X), models(Y), #sum {
2**(X-Z) : Z = L+1..X, not counter(1, Z);
1, M : excluded(M)
} >= Y.
% Check that removing any literal of prime implicant yields some non-model
:- bounds(L, U),
varies(X),
models(Y),
index(A, I),
#sum {
2**(X-Z) :
Z = L..X,
not counter(1, Z+1);
1, M :
exclude(M, B),
B != A
:- bounds(L, U), varies(X), models(Y), index(A, I), #sum {
2**(X-Z) : Z = L..X, not counter(1, Z+1);
1, M : exclude(M, B), B != A
} < Y.
% Display literals of prime implicant
Expand All @@ -355,24 +303,19 @@ n(s). bb(x).
output(@fmt(("The @fmt() function is flexible enough to take multi-line ",
"strings containing many placeholders: {} and ",
"{} and {} outputs"), (X, Y, Z))) :-
num(X),
string(Y),
constant(Z).
num(X), string(Y), constant(Z).
sel_vat(H, V) :-
sel_vat(N, W) :
cons(Identifier, var(N, W));
subgraph(N) :
cons(Identifier, has_x("strong", N))%*jjj*%;
sel_vat(N, W) : cons(Identifier, var(N, W));
subgraph(N) : cons(Identifier, has_x("strong", N))%*jjj*%;
%c1
has_con(F, T, Na, Index)%c0
%c01
:
cons(Identifier, has_con("strong", F, T, Na, Index));
: cons(Identifier, has_con("strong", F, T, Na, Index));
%c2
%c3
not has_con(F, _, Na, Index) :
cons(Identifier, has_con("weak", F, Na, Index));
not has_con(F, _, Na, Index) : cons(Identifier, has_con("weak",
F, Na, Index));
%* c2
sss *%cons(Identifier, tail(H, V)).
Expand All @@ -381,33 +324,28 @@ bla%aa
:-
%aa
%bb
varies(X),
#sum %aa
varies(X), #sum %aa
%bb
{
%aa
%bb
2**(X-Z)%aa
%bb
:
%aa
: %aa
%bb
Z = L+1..X,
%aa
Z = L+1..X, %aa
%bb
not counter(1, Z);
%aa
%bb
1, M :
excluded(M)
1, M : excluded(M)
}%aa
%bb
>= %aa
%bb
Y%aa
%bb
,
models(Y).
, models(Y).
:- bla(1, 2).
Expand All @@ -420,8 +358,7 @@ bla%aa
}.
#maximise {
X :
ccc(X)
X : ccc(X)
}.
#include "fail1.lp".
Expand Down

0 comments on commit e199024

Please sign in to comment.