This commit is contained in:
Patrick Lühne 2020-02-05 02:47:21 +01:00
parent 75356d2972
commit 02481ae4fd
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
4 changed files with 1 additions and 50 deletions

2
.gitignore vendored
View File

@ -1,3 +1,3 @@
/Cargo.lock
/target
**/*.rs.bk
Cargo.lock

View File

@ -3,6 +3,3 @@ name = "foliage"
version = "0.1.0"
authors = ["Patrick Lühne <patrick@luehne.de>"]
edition = "2018"
[dependencies]
nom = "5.0"

View File

@ -1,20 +0,0 @@
#![feature(test)]
extern crate test;
#[cfg(test)]
mod tests
{
#[bench]
fn anthem_example_2(b: &mut test::Bencher)
{
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)))";
b.iter(||
{
let (i, _) = foliage::formulas(formulas).unwrap();
assert_eq!(i, "");
});
}
}

View File

@ -1,26 +0,0 @@
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) = foliage::formulas(formulas).unwrap();
assert_eq!(i, "");
for formula in formulas
{
println!("{}", formula);
}
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) = foliage::formulas(formulas).unwrap();
assert_eq!(i, "");
for formula in formulas
{
println!("{}", formula);
}
Ok(())
}