1132 lines
21 KiB
Rust
1132 lines
21 KiB
Rust
use nom::
|
|
{
|
|
IResult,
|
|
bytes::complete::{take_while, take_while_m_n, is_not},
|
|
character::complete::{digit1, multispace0, space1, not_line_ending, line_ending},
|
|
sequence::{preceded, delimited, pair, terminated},
|
|
combinator::{map, map_res, recognize},
|
|
multi::{many0, many0_count, separated_list},
|
|
branch::alt,
|
|
bytes::complete::tag,
|
|
};
|
|
|
|
enum TermOperator
|
|
{
|
|
Add,
|
|
Subtract,
|
|
Multiply,
|
|
}
|
|
|
|
fn comment(i: &str) -> IResult<&str, &str>
|
|
{
|
|
terminated
|
|
(
|
|
preceded
|
|
(
|
|
tag("%"),
|
|
not_line_ending,
|
|
),
|
|
line_ending,
|
|
)(i)
|
|
}
|
|
|
|
pub fn whitespace0(i: &str) -> IResult<&str, ()>
|
|
{
|
|
let (i, _) = preceded
|
|
(
|
|
multispace0,
|
|
many0_count
|
|
(
|
|
preceded
|
|
(
|
|
comment,
|
|
multispace0,
|
|
)
|
|
),
|
|
)(i)?;
|
|
|
|
Ok((i, ()))
|
|
}
|
|
|
|
pub fn whitespace_single(i: &str) -> IResult<&str, ()>
|
|
{
|
|
let (i, _) = alt
|
|
((
|
|
space1,
|
|
line_ending,
|
|
))(i)?;
|
|
|
|
Ok((i, ()))
|
|
}
|
|
|
|
fn infimum(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
delimited(whitespace0, tag("#inf"), whitespace0),
|
|
|_| crate::Term::Infimum
|
|
)(i)
|
|
}
|
|
|
|
fn supremum(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
delimited(whitespace0, tag("#sup"), whitespace0),
|
|
|_| crate::Term::Supremum
|
|
)(i)
|
|
}
|
|
|
|
fn integer(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
map_res
|
|
(
|
|
delimited(whitespace0, digit1, whitespace0),
|
|
std::str::FromStr::from_str
|
|
),
|
|
crate::Term::Integer
|
|
)(i)
|
|
}
|
|
|
|
fn is_lowercase_alphanumeric(c: char) -> bool
|
|
{
|
|
c.is_alphanumeric() && c.is_lowercase()
|
|
}
|
|
|
|
fn is_uppercase_alphanumeric(c: char) -> bool
|
|
{
|
|
c.is_alphanumeric() && c.is_uppercase()
|
|
}
|
|
|
|
pub fn symbolic_identifier(i: &str) -> IResult<&str, String>
|
|
{
|
|
let (i, symbolic_identifier) = map
|
|
(
|
|
pair
|
|
(
|
|
take_while_m_n(1, 1, is_lowercase_alphanumeric),
|
|
take_while(char::is_alphanumeric)
|
|
),
|
|
|(s0, s1)| format!("{}{}", s0, s1)
|
|
)(i)?;
|
|
|
|
Ok((i, symbolic_identifier))
|
|
}
|
|
|
|
fn symbolic(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
delimited(whitespace0, symbolic_identifier, whitespace0),
|
|
crate::Term::Symbolic
|
|
)(i)
|
|
}
|
|
|
|
fn string(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
whitespace0,
|
|
delimited
|
|
(
|
|
tag("\""),
|
|
is_not("\""),
|
|
tag("\""),
|
|
),
|
|
whitespace0
|
|
),
|
|
|s: &str| crate::Term::String(s.to_string())
|
|
)(i)
|
|
}
|
|
|
|
fn variable_identifier(i: &str) -> IResult<&str, String>
|
|
{
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
whitespace0,
|
|
recognize
|
|
(
|
|
pair
|
|
(
|
|
take_while_m_n(1, 1, is_uppercase_alphanumeric),
|
|
take_while(char::is_alphanumeric)
|
|
)
|
|
),
|
|
whitespace0
|
|
),
|
|
|s: &str| s.to_string()
|
|
)(i)
|
|
}
|
|
|
|
fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
|
|
{
|
|
map
|
|
(
|
|
variable_identifier,
|
|
|name|
|
|
{
|
|
let domain = match name.chars().next()
|
|
{
|
|
Some('X') | Some('Y') | Some('Z') => crate::Domain::Program,
|
|
Some('I') | Some('J') | Some('K') | Some('L') | Some('M') | Some('N') => crate::Domain::Integer,
|
|
Some(other) => panic!("variable “{}” starts with character “{}”, which is not allowed", name, other),
|
|
None => panic!("unexpected variable name, please report to bug tracker"),
|
|
};
|
|
|
|
crate::VariableDeclaration{name, domain}
|
|
}
|
|
)(i)
|
|
}
|
|
|
|
fn variable(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
variable_declaration,
|
|
|variable_declaration| crate::Term::Variable(variable_declaration)
|
|
)(i)
|
|
}
|
|
|
|
fn predicate_0_ary(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
delimited(whitespace0, symbolic_identifier, whitespace0),
|
|
|name| crate::Formula::Predicate(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: name,
|
|
arity: 0,
|
|
},
|
|
arguments: vec![],
|
|
})
|
|
)(i)
|
|
}
|
|
|
|
fn predicate_n_ary(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
delimited(whitespace0, symbolic_identifier, whitespace0),
|
|
delimited
|
|
(
|
|
whitespace0,
|
|
delimited
|
|
(
|
|
tag("("),
|
|
separated_list(tag(","), term),
|
|
tag(")")
|
|
),
|
|
whitespace0
|
|
)
|
|
),
|
|
|(name, arguments)| crate::Formula::Predicate(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: name,
|
|
arity: arguments.len(),
|
|
},
|
|
arguments: arguments,
|
|
})
|
|
)(i)
|
|
}
|
|
|
|
fn predicate(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
predicate_n_ary,
|
|
predicate_0_ary
|
|
))(i)
|
|
}
|
|
|
|
fn boolean(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
whitespace0,
|
|
alt
|
|
((
|
|
map(tag("#true"), |_| true),
|
|
map(tag("#false"), |_| false)
|
|
)),
|
|
whitespace0
|
|
),
|
|
|value| crate::Formula::Boolean(value)
|
|
)(i)
|
|
}
|
|
|
|
fn less(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag("<"), term)
|
|
),
|
|
|(left, right)| crate::Formula::Less(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn less_or_equal(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag("<="), term)
|
|
),
|
|
|(left, right)| crate::Formula::LessOrEqual(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn greater(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag(">"), term)
|
|
),
|
|
|(left, right)| crate::Formula::Greater(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn greater_or_equal(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag(">="), term)
|
|
),
|
|
|(left, right)| crate::Formula::GreaterOrEqual(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn equal(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag("="), term)
|
|
),
|
|
|(left, right)| crate::Formula::Equal(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn not_equal(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag("!="), term)
|
|
),
|
|
|(left, right)| crate::Formula::NotEqual(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn comparison(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
less,
|
|
less_or_equal,
|
|
greater,
|
|
greater_or_equal,
|
|
equal,
|
|
not_equal
|
|
))(i)
|
|
}
|
|
|
|
fn term_parenthesized(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
delimited
|
|
(
|
|
whitespace0,
|
|
delimited
|
|
(
|
|
tag("("),
|
|
term,
|
|
tag(")")
|
|
),
|
|
whitespace0
|
|
)(i)
|
|
}
|
|
|
|
fn fold_terms(initial: crate::Term, remainder: Vec<(TermOperator, crate::Term)>) -> crate::Term
|
|
{
|
|
remainder.into_iter().fold(initial,
|
|
|accumulator, pair|
|
|
{
|
|
let (term_operator, term) = pair;
|
|
|
|
match term_operator
|
|
{
|
|
TermOperator::Add => crate::Term::Add(Box::new(accumulator), Box::new(term)),
|
|
TermOperator::Subtract => crate::Term::Subtract(Box::new(accumulator), Box::new(term)),
|
|
TermOperator::Multiply => crate::Term::Multiply(Box::new(accumulator), Box::new(term)),
|
|
}
|
|
})
|
|
}
|
|
|
|
fn term_precedence_0(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
infimum,
|
|
supremum,
|
|
integer,
|
|
symbolic,
|
|
string,
|
|
variable,
|
|
term_parenthesized
|
|
))(i)
|
|
}
|
|
|
|
fn term_precedence_1(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
whitespace0,
|
|
preceded(tag("-"), term_precedence_0),
|
|
whitespace0
|
|
),
|
|
|term| crate::Term::Negative(Box::new(term))
|
|
),
|
|
term_precedence_0
|
|
))(i)
|
|
}
|
|
|
|
fn term_precedence_2(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
let (i, initial) = term_precedence_1(i)?;
|
|
let (i, remainder) =
|
|
many0
|
|
(
|
|
|i|
|
|
{
|
|
let (i, term) = preceded(tag("*"), term_precedence_1)(i)?;
|
|
Ok((i, (TermOperator::Multiply, term)))
|
|
}
|
|
)(i)?;
|
|
|
|
Ok((i, fold_terms(initial, remainder)))
|
|
}
|
|
|
|
fn term_precedence_3(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
let (i, initial) = term_precedence_2(i)?;
|
|
let (i, remainder) =
|
|
many0
|
|
(
|
|
alt
|
|
((
|
|
|i|
|
|
{
|
|
let (i, term) = preceded(tag("+"), term_precedence_2)(i)?;
|
|
Ok((i, (TermOperator::Add, term)))
|
|
},
|
|
|i|
|
|
{
|
|
let (i, term) = preceded(tag("-"), term_precedence_2)(i)?;
|
|
Ok((i, (TermOperator::Subtract, term)))
|
|
}
|
|
))
|
|
)(i)?;
|
|
|
|
Ok((i, fold_terms(initial, remainder)))
|
|
}
|
|
|
|
pub fn term(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
term_precedence_3(i)
|
|
}
|
|
|
|
fn formula_parenthesized(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
delimited
|
|
(
|
|
whitespace0,
|
|
delimited
|
|
(
|
|
tag("("),
|
|
formula,
|
|
tag(")")
|
|
),
|
|
whitespace0
|
|
)(i)
|
|
}
|
|
|
|
fn formula_precedence_0(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
comparison,
|
|
predicate,
|
|
boolean,
|
|
formula_parenthesized
|
|
))(i)
|
|
}
|
|
|
|
fn exists(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
whitespace0,
|
|
preceded
|
|
(
|
|
terminated
|
|
(
|
|
tag("exists"),
|
|
whitespace_single,
|
|
),
|
|
pair
|
|
(
|
|
separated_list
|
|
(
|
|
tag(","),
|
|
variable_declaration
|
|
),
|
|
formula_precedence_2
|
|
)
|
|
),
|
|
whitespace0
|
|
),
|
|
|(parameters, argument)| crate::Formula::Exists(
|
|
crate::Exists
|
|
{
|
|
parameters: parameters,
|
|
argument: Box::new(argument),
|
|
})
|
|
)(i)
|
|
}
|
|
|
|
fn for_all(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
whitespace0,
|
|
preceded
|
|
(
|
|
terminated
|
|
(
|
|
tag("forall"),
|
|
whitespace_single,
|
|
),
|
|
pair
|
|
(
|
|
separated_list
|
|
(
|
|
tag(","),
|
|
variable_declaration
|
|
),
|
|
formula_precedence_2
|
|
)
|
|
),
|
|
whitespace0
|
|
),
|
|
|(parameters, argument)| crate::Formula::ForAll(
|
|
crate::ForAll
|
|
{
|
|
parameters: parameters,
|
|
argument: Box::new(argument),
|
|
})
|
|
)(i)
|
|
}
|
|
|
|
fn formula_precedence_1(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
exists,
|
|
for_all,
|
|
formula_precedence_0
|
|
))(i)
|
|
}
|
|
|
|
fn formula_precedence_2(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
whitespace0,
|
|
preceded
|
|
(
|
|
terminated
|
|
(
|
|
tag("not"),
|
|
whitespace_single,
|
|
),
|
|
formula_precedence_1
|
|
),
|
|
whitespace0
|
|
),
|
|
|argument| crate::Formula::Not(Box::new(argument))
|
|
),
|
|
formula_precedence_1
|
|
))(i)
|
|
}
|
|
|
|
fn formula_precedence_3(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
map_res
|
|
(
|
|
separated_list(tag("and"), map(formula_precedence_2, |argument| Box::new(argument))),
|
|
|arguments|
|
|
match arguments.len()
|
|
{
|
|
// TODO: improve error handling
|
|
0 | 1 => Err(nom::Err::Error("")),
|
|
_ => Ok(crate::Formula::And(arguments)),
|
|
}
|
|
),
|
|
formula_precedence_2
|
|
))(i)
|
|
}
|
|
|
|
fn formula_precedence_4(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
map_res
|
|
(
|
|
separated_list(tag("or"), map(formula_precedence_3, |argument| Box::new(argument))),
|
|
|arguments|
|
|
match arguments.len()
|
|
{
|
|
// TODO: improve error handling
|
|
0 | 1 => Err(nom::Err::Error("")),
|
|
_ => Ok(crate::Formula::Or(arguments)),
|
|
}
|
|
),
|
|
formula_precedence_3
|
|
))(i)
|
|
}
|
|
|
|
fn formula_precedence_5(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
let (i, left) = formula_precedence_4(i)?;
|
|
|
|
match preceded(tag("->"), formula_precedence_4)(i)
|
|
{
|
|
Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right), crate::ImplicationDirection::LeftToRight))),
|
|
Err(_) => match preceded(tag("<-"), formula_precedence_4)(i)
|
|
{
|
|
Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right), crate::ImplicationDirection::RightToLeft))),
|
|
Err(_) => Ok((i, left)),
|
|
},
|
|
}
|
|
}
|
|
|
|
fn formula_precedence_6(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
let (i, left) = formula_precedence_5(i)?;
|
|
|
|
match preceded(tag("<->"), formula_precedence_5)(i)
|
|
{
|
|
Ok((i, right)) => Ok((i, crate::Formula::Biconditional(Box::new(left), Box::new(right)))),
|
|
Err(_) => Ok((i, left)),
|
|
}
|
|
}
|
|
|
|
pub fn formula(i: &str) -> IResult<&str, crate::Formula>
|
|
{
|
|
formula_precedence_6(i)
|
|
}
|
|
|
|
pub fn formulas(i: &str) -> IResult<&str, Vec<crate::Formula>>
|
|
{
|
|
many0(formula)(i)
|
|
}
|
|
|
|
#[cfg(test)]
|
|
mod tests
|
|
{
|
|
#[test]
|
|
fn parse_integer()
|
|
{
|
|
assert_eq!(crate::term("12345"), Ok(("", crate::Term::Integer(12345))));
|
|
}
|
|
|
|
#[test]
|
|
fn parse_variable_declaration()
|
|
{
|
|
assert_eq!(crate::term(" X5 "), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()}))));
|
|
assert_eq!(crate::term(" NX3 "), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()}))));
|
|
}
|
|
|
|
#[test]
|
|
fn parse_variable()
|
|
{
|
|
assert_eq!(crate::term("X5"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()}))));
|
|
assert_eq!(crate::term("NX3"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()}))));
|
|
}
|
|
|
|
#[test]
|
|
fn parse_string()
|
|
{
|
|
assert_eq!(crate::term(" \"foobar\" "), Ok(("", crate::Term::String("foobar".to_string()))));
|
|
}
|
|
|
|
#[test]
|
|
fn parse_boolean()
|
|
{
|
|
assert_eq!(crate::formula(" #true "), Ok(("", crate::Formula::Boolean(true))));
|
|
assert_eq!(crate::formula(" #false "), Ok(("", crate::Formula::Boolean(false))));
|
|
}
|
|
|
|
#[test]
|
|
fn parse_term()
|
|
{
|
|
assert_eq!(crate::term(" 5 + 3"), Ok(("",
|
|
crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Integer(5)),
|
|
Box::new(crate::Term::Integer(3)),
|
|
))));
|
|
|
|
assert_eq!(crate::term(" -5"), Ok(("",
|
|
crate::Term::Negative
|
|
(
|
|
Box::new(crate::Term::Integer(5))
|
|
)
|
|
)));
|
|
|
|
assert_eq!(crate::term(" 5+3 * -(9+ 1) + 2 "), Ok(("",
|
|
crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Integer(5)),
|
|
Box::new(crate::Term::Multiply
|
|
(
|
|
Box::new(crate::Term::Integer(3)),
|
|
Box::new(crate::Term::Negative
|
|
(
|
|
Box::new(crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Integer(9)),
|
|
Box::new(crate::Term::Integer(1)),
|
|
))
|
|
)),
|
|
)),
|
|
)),
|
|
Box::new(crate::Term::Integer(2)),
|
|
))));
|
|
|
|
assert_eq!(crate::term(" 5 + a "), Ok(("",
|
|
crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Integer(5)),
|
|
Box::new(crate::Term::Symbolic("a".to_string())),
|
|
))));
|
|
|
|
assert_eq!(crate::term(" 5 + #sup "), Ok(("",
|
|
crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Integer(5)),
|
|
Box::new(crate::Term::Supremum),
|
|
))));
|
|
|
|
assert_eq!(crate::term(" 5 + #inf "), Ok(("",
|
|
crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Integer(5)),
|
|
Box::new(crate::Term::Infimum),
|
|
))));
|
|
|
|
assert_eq!(crate::term(" 5 + \" text \" "), Ok(("",
|
|
crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Integer(5)),
|
|
Box::new(crate::Term::String(" text ".to_string())),
|
|
))));
|
|
|
|
assert_eq!(crate::term(" 5 + X1 "), Ok(("",
|
|
crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Integer(5)),
|
|
Box::new(crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "1".to_string()})),
|
|
))));
|
|
}
|
|
|
|
#[test]
|
|
fn parse_predicate()
|
|
{
|
|
assert_eq!(crate::formula(" p "), Ok(("", crate::Formula::Predicate(crate::Predicate{declaration: crate::PredicateDeclaration{name: "p".to_string(), arity: 0}, arguments: vec![]}))));
|
|
|
|
assert_eq!(crate::formula(" p(5, 6, 7) "), Ok(("",
|
|
crate::Formula::Predicate
|
|
(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: "p".to_string(),
|
|
arity: 3,
|
|
},
|
|
arguments:
|
|
vec!
|
|
[
|
|
crate::Term::Integer(5),
|
|
crate::Term::Integer(6),
|
|
crate::Term::Integer(7),
|
|
],
|
|
}
|
|
))));
|
|
|
|
assert_eq!(crate::formula(" p(1, 3+4*5+6, \"test\") "), Ok(("",
|
|
crate::Formula::Predicate
|
|
(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: "p".to_string(),
|
|
arity: 3,
|
|
},
|
|
arguments:
|
|
vec!
|
|
[
|
|
crate::Term::Integer(1),
|
|
crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Integer(3)),
|
|
Box::new(crate::Term::Multiply
|
|
(
|
|
Box::new(crate::Term::Integer(4)),
|
|
Box::new(crate::Term::Integer(5)),
|
|
)),
|
|
)),
|
|
Box::new(crate::Term::Integer(6)),
|
|
),
|
|
crate::Term::String("test".to_string()),
|
|
],
|
|
}
|
|
))));
|
|
}
|
|
|
|
#[test]
|
|
fn parse_comparison()
|
|
{
|
|
assert_eq!(crate::formula("5 + 9 < #sup"), Ok(("",
|
|
crate::Formula::Less
|
|
(
|
|
crate::Term::Add
|
|
(
|
|
Box::new(crate::Term::Integer(5)),
|
|
Box::new(crate::Term::Integer(9)),
|
|
),
|
|
crate::Term::Supremum,
|
|
))));
|
|
|
|
assert_eq!(crate::formula("#inf != 6 * 9"), Ok(("",
|
|
crate::Formula::NotEqual
|
|
(
|
|
crate::Term::Infimum,
|
|
crate::Term::Multiply
|
|
(
|
|
Box::new(crate::Term::Integer(6)),
|
|
Box::new(crate::Term::Integer(9)),
|
|
),
|
|
))));
|
|
|
|
assert_eq!(crate::formula("n = 5"), Ok(("",
|
|
crate::Formula::Equal
|
|
(
|
|
crate::Term::Symbolic("n".to_string()),
|
|
crate::Term::Integer(5),
|
|
))));
|
|
}
|
|
|
|
#[test]
|
|
fn formula()
|
|
{
|
|
assert_eq!(crate::formula("p(1, a) or q(2)"), Ok(("",
|
|
crate::Formula::Or
|
|
(
|
|
vec!
|
|
[
|
|
Box::new(crate::Formula::Predicate
|
|
(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: "p".to_string(),
|
|
arity: 2,
|
|
},
|
|
arguments:
|
|
vec!
|
|
[
|
|
crate::Term::Integer(1),
|
|
crate::Term::Symbolic("a".to_string()),
|
|
],
|
|
}
|
|
)),
|
|
Box::new(crate::Formula::Predicate
|
|
(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: "q".to_string(),
|
|
arity: 1,
|
|
},
|
|
arguments:
|
|
vec!
|
|
[
|
|
crate::Term::Integer(2),
|
|
],
|
|
}
|
|
)),
|
|
]
|
|
))));
|
|
|
|
assert_eq!(crate::formula("#inf < 5 and p(1, a) or q(2)"), Ok(("",
|
|
crate::Formula::Or
|
|
(
|
|
vec!
|
|
[
|
|
Box::new(crate::Formula::And
|
|
(
|
|
vec!
|
|
[
|
|
Box::new(crate::Formula::Less
|
|
(
|
|
crate::Term::Infimum,
|
|
crate::Term::Integer(5),
|
|
)),
|
|
Box::new(crate::Formula::Predicate
|
|
(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: "p".to_string(),
|
|
arity: 2,
|
|
},
|
|
arguments:
|
|
vec!
|
|
[
|
|
crate::Term::Integer(1),
|
|
crate::Term::Symbolic("a".to_string()),
|
|
],
|
|
}
|
|
)),
|
|
]
|
|
)),
|
|
Box::new(crate::Formula::Predicate
|
|
(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: "q".to_string(),
|
|
arity: 1,
|
|
},
|
|
arguments:
|
|
vec!
|
|
[
|
|
crate::Term::Integer(2),
|
|
],
|
|
}
|
|
)),
|
|
]
|
|
))));
|
|
|
|
assert_eq!(crate::formula("#inf < 5 and p(1, a) or q(2) -> #false"), Ok(("",
|
|
crate::Formula::Implies
|
|
(
|
|
Box::new(crate::Formula::Or
|
|
(
|
|
vec!
|
|
[
|
|
Box::new(crate::Formula::And
|
|
(
|
|
vec!
|
|
[
|
|
Box::new(crate::Formula::Less
|
|
(
|
|
crate::Term::Infimum,
|
|
crate::Term::Integer(5),
|
|
)),
|
|
Box::new(crate::Formula::Predicate
|
|
(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: "p".to_string(),
|
|
arity: 2,
|
|
},
|
|
arguments:
|
|
vec!
|
|
[
|
|
crate::Term::Integer(1),
|
|
crate::Term::Symbolic("a".to_string()),
|
|
],
|
|
}
|
|
)),
|
|
]
|
|
)),
|
|
Box::new(crate::Formula::Predicate
|
|
(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: "q".to_string(),
|
|
arity: 1,
|
|
},
|
|
arguments:
|
|
vec!
|
|
[
|
|
crate::Term::Integer(2),
|
|
],
|
|
}
|
|
)),
|
|
]
|
|
)),
|
|
Box::new(crate::Formula::Boolean(false)),
|
|
))));
|
|
|
|
assert_eq!(crate::formula(" not #true"), Ok(("",
|
|
crate::Formula::Not(Box::new(crate::Formula::Boolean(true))))));
|
|
|
|
assert_eq!(crate::formula("exists X forall N1 p(1, 2) and #false"), Ok(("",
|
|
crate::Formula::And
|
|
(
|
|
vec!
|
|
[
|
|
Box::new(crate::Formula::Exists
|
|
(
|
|
crate::Exists
|
|
{
|
|
parameters: vec![crate::VariableDeclaration{name: "".to_string(), domain: crate::Domain::Program}],
|
|
argument:
|
|
Box::new(crate::Formula::ForAll
|
|
(
|
|
crate::ForAll
|
|
{
|
|
parameters: vec![crate::VariableDeclaration{name: "1".to_string(), domain: crate::Domain::Integer}],
|
|
argument:
|
|
Box::new(crate::Formula::Predicate
|
|
(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: "p".to_string(),
|
|
arity: 2,
|
|
},
|
|
arguments:
|
|
vec!
|
|
[
|
|
crate::Term::Integer(1),
|
|
crate::Term::Integer(2),
|
|
],
|
|
}
|
|
)),
|
|
}
|
|
)),
|
|
}
|
|
)),
|
|
Box::new(crate::Formula::Boolean(false)),
|
|
]
|
|
))));
|
|
|
|
assert_eq!(crate::formula("exists X forall N1 (p(1, 2) and #false)"), Ok(("",
|
|
crate::Formula::Exists
|
|
(
|
|
crate::Exists
|
|
{
|
|
parameters: vec![crate::VariableDeclaration{name: "".to_string(), domain: crate::Domain::Program}],
|
|
argument:
|
|
Box::new(crate::Formula::ForAll
|
|
(
|
|
crate::ForAll
|
|
{
|
|
parameters: vec![crate::VariableDeclaration{name: "1".to_string(), domain: crate::Domain::Integer}],
|
|
argument:
|
|
Box::new(crate::Formula::And
|
|
(
|
|
vec!
|
|
[
|
|
Box::new(crate::Formula::Predicate
|
|
(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: "p".to_string(),
|
|
arity: 2,
|
|
},
|
|
arguments:
|
|
vec!
|
|
[
|
|
crate::Term::Integer(1),
|
|
crate::Term::Integer(2),
|
|
],
|
|
}
|
|
)),
|
|
Box::new(crate::Formula::Boolean(false)),
|
|
]
|
|
)),
|
|
}
|
|
)),
|
|
}
|
|
))));
|
|
}
|
|
}
|