Add example
This commit is contained in:
parent
dcf12d45eb
commit
48b18b9354
15
examples/test.rs
Normal file
15
examples/test.rs
Normal file
@ -0,0 +1,15 @@
|
|||||||
|
fn main() -> Result<(), Box<dyn std::error::Error>>
|
||||||
|
{
|
||||||
|
let formulas = "forall XV1 (p(XV1) <-> (exists XU1 (exists X1, X2 (X1 = XU1 and exists N1, N2, N3 (N1 = 0 and N2 = n and N1 <= N3 and N3 <= N2 and X2 = N3) and X1 = X2) and exists X3, X4 (exists N4, N5 (X3 = (N4 * N5) and N4 = XU1 and N5 = XU1) and X4 = n and X3 <= X4) and XV1 = XU1)))
|
||||||
|
forall XV2 (q(XV2) <-> (exists XU2 (exists X5 (X5 = XU2 and p(X5)) and exists X6 (exists N6, N7 (X6 = (N6 + N7) and N6 = XU2 and N7 = 1) and not p(X6)) and XV2 = XU2)))";
|
||||||
|
|
||||||
|
let (i, formulas) = fol_parser::formulas(formulas).unwrap();
|
||||||
|
assert_eq!(i, "");
|
||||||
|
|
||||||
|
for formula in formulas
|
||||||
|
{
|
||||||
|
println!("{}", formula);
|
||||||
|
}
|
||||||
|
|
||||||
|
Ok(())
|
||||||
|
}
|
Loading…
Reference in New Issue
Block a user