Implement formula parsing
This commit is contained in:
parent
1b9654f44f
commit
dcf12d45eb
GPG Key ID:
05F3611E97A70ABF
597
src/lib.rs
597
src/lib.rs
@ -123,7 +123,7 @@ impl std::fmt::Display for VariableDeclaration
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn term_precedence(term: &Term) -> u64
|
pub fn term_precedence(term: &Term) -> u64
|
||||||
{
|
{
|
||||||
match term
|
match term
|
||||||
{
|
{
|
||||||
@ -134,17 +134,17 @@ fn term_precedence(term: &Term) -> u64
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn formula_precedence(formula: &Formula) -> u64
|
pub fn formula_precedence(formula: &Formula) -> u64
|
||||||
{
|
{
|
||||||
match formula
|
match formula
|
||||||
{
|
{
|
||||||
Formula::Predicate(_) | Formula::Boolean(_) | Formula::Less(_, _) | Formula::LessOrEqual(_, _) | Formula::Greater(_, _) | Formula::GreaterOrEqual(_, _) | Formula::Equal(_, _) | Formula::NotEqual(_, _) => 0,
|
Formula::Predicate(_) | Formula::Boolean(_) | Formula::Less(_, _) | Formula::LessOrEqual(_, _) | Formula::Greater(_, _) | Formula::GreaterOrEqual(_, _) | Formula::Equal(_, _) | Formula::NotEqual(_, _) => 0,
|
||||||
Formula::Not(_) => 1,
|
Formula::Exists(_) | Formula::ForAll(_) => 1,
|
||||||
Formula::And(_) => 2,
|
Formula::Not(_) => 2,
|
||||||
Formula::Or(_) => 3,
|
Formula::And(_) => 3,
|
||||||
Formula::Implies(_, _) => 4,
|
Formula::Or(_) => 4,
|
||||||
Formula::Biconditional(_, _) => 5,
|
Formula::Implies(_, _) => 5,
|
||||||
Formula::Exists(_) | Formula::ForAll(_) => 6,
|
Formula::Biconditional(_, _) => 6,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -440,7 +440,7 @@ fn is_lowercase_alphanumeric(c: char) -> bool
|
|||||||
|
|
||||||
fn symbolic_identifier(i: &str) -> IResult<&str, String>
|
fn symbolic_identifier(i: &str) -> IResult<&str, String>
|
||||||
{
|
{
|
||||||
map
|
let (i, symbolic_identifier) = map
|
||||||
(
|
(
|
||||||
pair
|
pair
|
||||||
(
|
(
|
||||||
@ -448,7 +448,9 @@ fn symbolic_identifier(i: &str) -> IResult<&str, String>
|
|||||||
take_while(char::is_alphanumeric)
|
take_while(char::is_alphanumeric)
|
||||||
),
|
),
|
||||||
|(s0, s1)| format!("{}{}", s0, s1)
|
|(s0, s1)| format!("{}{}", s0, s1)
|
||||||
)(i)
|
)(i)?;
|
||||||
|
|
||||||
|
Ok((i, symbolic_identifier))
|
||||||
}
|
}
|
||||||
|
|
||||||
fn symbolic(i: &str) -> IResult<&str, Term>
|
fn symbolic(i: &str) -> IResult<&str, Term>
|
||||||
@ -489,7 +491,7 @@ fn program_variable_identifier(i: &str) -> IResult<&str, String>
|
|||||||
preceded
|
preceded
|
||||||
(
|
(
|
||||||
tag("X"),
|
tag("X"),
|
||||||
take_while1(char::is_alphanumeric)
|
take_while(char::is_alphanumeric)
|
||||||
),
|
),
|
||||||
multispace0
|
multispace0
|
||||||
),
|
),
|
||||||
@ -507,7 +509,7 @@ fn integer_variable_identifier(i: &str) -> IResult<&str, String>
|
|||||||
preceded
|
preceded
|
||||||
(
|
(
|
||||||
tag("N"),
|
tag("N"),
|
||||||
take_while1(char::is_alphanumeric)
|
take_while(char::is_alphanumeric)
|
||||||
),
|
),
|
||||||
multispace0
|
multispace0
|
||||||
),
|
),
|
||||||
@ -597,9 +599,14 @@ fn predicate_n_ary(i: &str) -> IResult<&str, Formula>
|
|||||||
delimited(multispace0, symbolic_identifier, multispace0),
|
delimited(multispace0, symbolic_identifier, multispace0),
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
tag("("),
|
multispace0,
|
||||||
separated_list(tag(","), term),
|
delimited
|
||||||
tag(")")
|
(
|
||||||
|
tag("("),
|
||||||
|
separated_list(tag(","), term),
|
||||||
|
tag(")")
|
||||||
|
),
|
||||||
|
multispace0
|
||||||
)
|
)
|
||||||
),
|
),
|
||||||
|(name, arguments)| Formula::Predicate(
|
|(name, arguments)| Formula::Predicate(
|
||||||
@ -643,10 +650,96 @@ fn boolean(i: &str) -> IResult<&str, Formula>
|
|||||||
)(i)
|
)(i)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn less(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
map
|
||||||
|
(
|
||||||
|
pair
|
||||||
|
(
|
||||||
|
term,
|
||||||
|
preceded(tag("<"), term)
|
||||||
|
),
|
||||||
|
|(left, right)| Formula::Less(left, right)
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn less_or_equal(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
map
|
||||||
|
(
|
||||||
|
pair
|
||||||
|
(
|
||||||
|
term,
|
||||||
|
preceded(tag("<="), term)
|
||||||
|
),
|
||||||
|
|(left, right)| Formula::LessOrEqual(left, right)
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn greater(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
map
|
||||||
|
(
|
||||||
|
pair
|
||||||
|
(
|
||||||
|
term,
|
||||||
|
preceded(tag(">"), term)
|
||||||
|
),
|
||||||
|
|(left, right)| Formula::Greater(left, right)
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn greater_or_equal(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
map
|
||||||
|
(
|
||||||
|
pair
|
||||||
|
(
|
||||||
|
term,
|
||||||
|
preceded(tag(">="), term)
|
||||||
|
),
|
||||||
|
|(left, right)| Formula::GreaterOrEqual(left, right)
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn equal(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
map
|
||||||
|
(
|
||||||
|
pair
|
||||||
|
(
|
||||||
|
term,
|
||||||
|
preceded(tag("="), term)
|
||||||
|
),
|
||||||
|
|(left, right)| Formula::Equal(left, right)
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn not_equal(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
map
|
||||||
|
(
|
||||||
|
pair
|
||||||
|
(
|
||||||
|
term,
|
||||||
|
preceded(tag("!="), term)
|
||||||
|
),
|
||||||
|
|(left, right)| Formula::NotEqual(left, right)
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn comparison(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
alt
|
||||||
|
((
|
||||||
|
less,
|
||||||
|
less_or_equal,
|
||||||
|
greater,
|
||||||
|
greater_or_equal,
|
||||||
|
equal,
|
||||||
|
not_equal
|
||||||
|
))(i)
|
||||||
|
}
|
||||||
|
|
||||||
fn term_parenthesized(i: &str) -> IResult<&str, Term>
|
fn term_parenthesized(i: &str) -> IResult<&str, Term>
|
||||||
{
|
{
|
||||||
@ -751,11 +844,197 @@ fn term_precedence_3(i: &str) -> IResult<&str, Term>
|
|||||||
Ok((i, fold_terms(initial, remainder)))
|
Ok((i, fold_terms(initial, remainder)))
|
||||||
}
|
}
|
||||||
|
|
||||||
fn term(i: &str) -> IResult<&str, Term>
|
pub fn term(i: &str) -> IResult<&str, Term>
|
||||||
{
|
{
|
||||||
term_precedence_3(i)
|
term_precedence_3(i)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn formula_parenthesized(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
delimited
|
||||||
|
(
|
||||||
|
multispace0,
|
||||||
|
delimited
|
||||||
|
(
|
||||||
|
tag("("),
|
||||||
|
formula,
|
||||||
|
tag(")")
|
||||||
|
),
|
||||||
|
multispace0
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn formula_precedence_0(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
alt
|
||||||
|
((
|
||||||
|
predicate,
|
||||||
|
boolean,
|
||||||
|
comparison,
|
||||||
|
formula_parenthesized
|
||||||
|
))(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn exists(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
map
|
||||||
|
(
|
||||||
|
delimited
|
||||||
|
(
|
||||||
|
multispace0,
|
||||||
|
preceded
|
||||||
|
(
|
||||||
|
tag("exists "),
|
||||||
|
pair
|
||||||
|
(
|
||||||
|
separated_list
|
||||||
|
(
|
||||||
|
tag(","),
|
||||||
|
variable_declaration
|
||||||
|
),
|
||||||
|
formula_precedence_1
|
||||||
|
)
|
||||||
|
),
|
||||||
|
multispace0
|
||||||
|
),
|
||||||
|
|(parameters, argument)| Formula::Exists(
|
||||||
|
Exists
|
||||||
|
{
|
||||||
|
parameters: parameters,
|
||||||
|
argument: Box::new(argument),
|
||||||
|
})
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn for_all(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
map
|
||||||
|
(
|
||||||
|
delimited
|
||||||
|
(
|
||||||
|
multispace0,
|
||||||
|
preceded
|
||||||
|
(
|
||||||
|
tag("forall "),
|
||||||
|
pair
|
||||||
|
(
|
||||||
|
separated_list
|
||||||
|
(
|
||||||
|
tag(","),
|
||||||
|
variable_declaration
|
||||||
|
),
|
||||||
|
formula_precedence_1
|
||||||
|
)
|
||||||
|
),
|
||||||
|
multispace0
|
||||||
|
),
|
||||||
|
|(parameters, argument)| Formula::ForAll(
|
||||||
|
ForAll
|
||||||
|
{
|
||||||
|
parameters: parameters,
|
||||||
|
argument: Box::new(argument),
|
||||||
|
})
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn formula_precedence_1(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
alt
|
||||||
|
((
|
||||||
|
exists,
|
||||||
|
for_all,
|
||||||
|
formula_precedence_0
|
||||||
|
))(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn formula_precedence_2(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
alt
|
||||||
|
((
|
||||||
|
map
|
||||||
|
(
|
||||||
|
delimited
|
||||||
|
(
|
||||||
|
multispace0,
|
||||||
|
preceded(tag("not "), formula_precedence_1),
|
||||||
|
multispace0
|
||||||
|
),
|
||||||
|
|argument| Formula::Not(Box::new(argument))
|
||||||
|
),
|
||||||
|
formula_precedence_1
|
||||||
|
))(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn formula_precedence_3(i: &str) -> IResult<&str, 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(Formula::And(arguments)),
|
||||||
|
}
|
||||||
|
),
|
||||||
|
formula_precedence_2
|
||||||
|
))(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn formula_precedence_4(i: &str) -> IResult<&str, 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(Formula::Or(arguments)),
|
||||||
|
}
|
||||||
|
),
|
||||||
|
formula_precedence_3
|
||||||
|
))(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn formula_precedence_5(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
let (i, left) = formula_precedence_4(i)?;
|
||||||
|
|
||||||
|
match preceded(tag("->"), formula_precedence_4)(i)
|
||||||
|
{
|
||||||
|
Ok((i, right)) => Ok((i, Formula::Implies(Box::new(left), Box::new(right)))),
|
||||||
|
Err(_) => Ok((i, left)),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn formula_precedence_6(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
let (i, left) = formula_precedence_5(i)?;
|
||||||
|
|
||||||
|
match preceded(tag("<->"), formula_precedence_5)(i)
|
||||||
|
{
|
||||||
|
Ok((i, right)) => Ok((i, Formula::Biconditional(Box::new(left), Box::new(right)))),
|
||||||
|
Err(_) => Ok((i, left)),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn formula(i: &str) -> IResult<&str, Formula>
|
||||||
|
{
|
||||||
|
formula_precedence_6(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn formulas(i: &str) -> IResult<&str, Vec<Formula>>
|
||||||
|
{
|
||||||
|
many0(formula)(i)
|
||||||
|
}
|
||||||
|
|
||||||
#[cfg(test)]
|
#[cfg(test)]
|
||||||
mod tests
|
mod tests
|
||||||
{
|
{
|
||||||
@ -768,8 +1047,8 @@ mod tests
|
|||||||
#[test]
|
#[test]
|
||||||
fn parse_variable_declaration()
|
fn parse_variable_declaration()
|
||||||
{
|
{
|
||||||
assert_eq!(crate::variable_declaration("X5"), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()})));
|
assert_eq!(crate::variable_declaration(" X5 "), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()})));
|
||||||
assert_eq!(crate::variable_declaration("NX3"), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()})));
|
assert_eq!(crate::variable_declaration(" NX3 "), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()})));
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
@ -870,9 +1149,9 @@ mod tests
|
|||||||
#[test]
|
#[test]
|
||||||
fn parse_predicate()
|
fn parse_predicate()
|
||||||
{
|
{
|
||||||
assert_eq!(crate::predicate("p"), Ok(("", crate::Formula::Predicate(crate::Predicate{declaration: crate::PredicateDeclaration{name: "p".to_string(), arity: 0}, arguments: vec![]}))));
|
assert_eq!(crate::predicate(" p "), Ok(("", crate::Formula::Predicate(crate::Predicate{declaration: crate::PredicateDeclaration{name: "p".to_string(), arity: 0}, arguments: vec![]}))));
|
||||||
|
|
||||||
assert_eq!(crate::predicate_n_ary("p(5, 6, 7)"), Ok(("",
|
assert_eq!(crate::predicate_n_ary(" p(5, 6, 7) "), Ok(("",
|
||||||
crate::Formula::Predicate
|
crate::Formula::Predicate
|
||||||
(
|
(
|
||||||
crate::Predicate
|
crate::Predicate
|
||||||
@ -889,11 +1168,11 @@ mod tests
|
|||||||
crate::Term::Integer(5),
|
crate::Term::Integer(5),
|
||||||
crate::Term::Integer(6),
|
crate::Term::Integer(6),
|
||||||
crate::Term::Integer(7),
|
crate::Term::Integer(7),
|
||||||
]
|
],
|
||||||
}
|
}
|
||||||
))));
|
))));
|
||||||
|
|
||||||
assert_eq!(crate::predicate("p(1, 3+4*5+6, \"test\")"), Ok(("",
|
assert_eq!(crate::predicate(" p(1, 3+4*5+6, \"test\") "), Ok(("",
|
||||||
crate::Formula::Predicate
|
crate::Formula::Predicate
|
||||||
(
|
(
|
||||||
crate::Predicate
|
crate::Predicate
|
||||||
@ -922,7 +1201,281 @@ mod tests
|
|||||||
Box::new(crate::Term::Integer(6)),
|
Box::new(crate::Term::Integer(6)),
|
||||||
),
|
),
|
||||||
crate::Term::String("test".to_string()),
|
crate::Term::String("test".to_string()),
|
||||||
|
],
|
||||||
|
}
|
||||||
|
))));
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn parse_comparison()
|
||||||
|
{
|
||||||
|
assert_eq!(crate::comparison("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::comparison("#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)),
|
||||||
|
),
|
||||||
|
))));
|
||||||
|
}
|
||||||
|
|
||||||
|
#[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)),
|
||||||
|
]
|
||||||
|
)),
|
||||||
|
}
|
||||||
|
)),
|
||||||
}
|
}
|
||||||
))));
|
))));
|
||||||
}
|
}
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user