1000 lines
20 KiB
Rust
1000 lines
20 KiB
Rust
mod helpers;
|
|
mod names;
|
|
mod terms;
|
|
|
|
pub(crate) use helpers::word_boundary;
|
|
pub use names::{function_name, predicate_name, variable_name};
|
|
pub use terms::{integer, special_integer, string};
|
|
|
|
/*
|
|
use nom::
|
|
{
|
|
IResult,
|
|
bytes::complete::{take_while, take_while_m_n, is_not},
|
|
character::complete::{digit1, multispace0},
|
|
sequence::{preceded, delimited, pair},
|
|
combinator::{map, map_res},
|
|
multi::{many0, separated_list},
|
|
branch::alt,
|
|
bytes::complete::tag,
|
|
};
|
|
|
|
struct Declarations
|
|
{
|
|
//function_declarations:,
|
|
//predicate_declarations:,
|
|
//variable_declaration_stack: VariableDeclarationStack,
|
|
}
|
|
|
|
enum TermOperator
|
|
{
|
|
Add,
|
|
Subtract,
|
|
Multiply,
|
|
}
|
|
|
|
fn variable_declaration<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::VariableDeclaration>
|
|
{
|
|
map
|
|
(
|
|
|i| variable_identifier(i, declarations),
|
|
|s| crate::VariableDeclaration{name: s},
|
|
)(i)
|
|
}*/
|
|
|
|
/*
|
|
fn program_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
|i| program_variable_identifier(i, declarations),
|
|
|s|
|
|
{
|
|
let declaration = declarations.variable_declaration_stack.get(s.as_ref());
|
|
|
|
crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program})
|
|
},
|
|
)(i)
|
|
}
|
|
|
|
fn integer_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
|i| integer_variable_identifier,
|
|
|s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer}),
|
|
)(i)
|
|
}
|
|
|
|
fn variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
|i| program_variable(i, declarations),
|
|
|i| integer_variable(i, declarations),
|
|
))(i)
|
|
}
|
|
|
|
fn predicate_0_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
delimited(multispace0, symbolic_identifier, multispace0),
|
|
|name| crate::Formula::Predicate(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: name,
|
|
arity: 0,
|
|
},
|
|
arguments: vec![],
|
|
})
|
|
)(i)
|
|
}
|
|
|
|
fn predicate_n_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
delimited(multispace0, symbolic_identifier, multispace0),
|
|
delimited
|
|
(
|
|
multispace0,
|
|
delimited
|
|
(
|
|
tag("("),
|
|
separated_list(tag(","), term),
|
|
tag(")")
|
|
),
|
|
multispace0
|
|
)
|
|
),
|
|
|(name, arguments)| crate::Formula::Predicate(
|
|
crate::Predicate
|
|
{
|
|
declaration:
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: name,
|
|
arity: arguments.len(),
|
|
},
|
|
arguments: arguments,
|
|
})
|
|
)(i)
|
|
}
|
|
|
|
fn predicate<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
predicate_n_ary,
|
|
predicate_0_ary
|
|
))(i)
|
|
}
|
|
|
|
fn boolean<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
multispace0,
|
|
alt
|
|
((
|
|
map(tag("#true"), |_| true),
|
|
map(tag("#false"), |_| false)
|
|
)),
|
|
multispace0
|
|
),
|
|
|value| crate::Formula::Boolean(value)
|
|
)(i)
|
|
}
|
|
|
|
fn less<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag("<"), term)
|
|
),
|
|
|(left, right)| crate::Formula::Less(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn less_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag("<="), term)
|
|
),
|
|
|(left, right)| crate::Formula::LessOrEqual(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn greater<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag(">"), term)
|
|
),
|
|
|(left, right)| crate::Formula::Greater(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn greater_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag(">="), term)
|
|
),
|
|
|(left, right)| crate::Formula::GreaterOrEqual(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag("="), term)
|
|
),
|
|
|(left, right)| crate::Formula::Equal(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn not_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
term,
|
|
preceded(tag("!="), term)
|
|
),
|
|
|(left, right)| crate::Formula::NotEqual(left, right)
|
|
)(i)
|
|
}
|
|
|
|
fn comparison<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
less,
|
|
less_or_equal,
|
|
greater,
|
|
greater_or_equal,
|
|
equal,
|
|
not_equal
|
|
))(i)
|
|
}
|
|
*/
|
|
|
|
/*fn term_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
delimited
|
|
(
|
|
multispace0,
|
|
delimited
|
|
(
|
|
tag("("),
|
|
term,
|
|
tag(")")
|
|
),
|
|
multispace0
|
|
)(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<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
infimum,
|
|
supremum,
|
|
integer,
|
|
symbolic,
|
|
string,
|
|
variable,
|
|
term_parenthesized
|
|
))(i)
|
|
}
|
|
|
|
fn term_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
multispace0,
|
|
preceded(tag("-"), term_precedence_0),
|
|
multispace0
|
|
),
|
|
|term| crate::Term::Negative(Box::new(term))
|
|
),
|
|
term_precedence_0
|
|
))(i)
|
|
}
|
|
|
|
fn term_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a 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<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a 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<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
term_precedence_3(i)
|
|
}
|
|
*/
|
|
|
|
/*
|
|
fn formula_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
delimited
|
|
(
|
|
multispace0,
|
|
delimited
|
|
(
|
|
tag("("),
|
|
formula,
|
|
tag(")")
|
|
),
|
|
multispace0
|
|
)(i)
|
|
}
|
|
|
|
fn formula_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
comparison,
|
|
predicate,
|
|
boolean,
|
|
formula_parenthesized
|
|
))(i)
|
|
}
|
|
|
|
fn exists<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
multispace0,
|
|
preceded
|
|
(
|
|
tag("exists "),
|
|
pair
|
|
(
|
|
separated_list
|
|
(
|
|
tag(","),
|
|
variable_declaration
|
|
),
|
|
formula_precedence_1
|
|
)
|
|
),
|
|
multispace0
|
|
),
|
|
|(parameters, argument)| crate::Formula::Exists(
|
|
crate::Exists
|
|
{
|
|
parameters: parameters,
|
|
argument: Box::new(argument),
|
|
})
|
|
)(i)
|
|
}
|
|
|
|
fn for_all<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
multispace0,
|
|
preceded
|
|
(
|
|
tag("forall "),
|
|
pair
|
|
(
|
|
separated_list
|
|
(
|
|
tag(","),
|
|
variable_declaration
|
|
),
|
|
formula_precedence_1
|
|
)
|
|
),
|
|
multispace0
|
|
),
|
|
|(parameters, argument)| crate::Formula::ForAll(
|
|
crate::ForAll
|
|
{
|
|
parameters: parameters,
|
|
argument: Box::new(argument),
|
|
})
|
|
)(i)
|
|
}
|
|
|
|
fn formula_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
exists,
|
|
for_all,
|
|
formula_precedence_0
|
|
))(i)
|
|
}
|
|
|
|
fn formula_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
multispace0,
|
|
preceded(tag("not "), formula_precedence_1),
|
|
multispace0
|
|
),
|
|
|argument| crate::Formula::Not(Box::new(argument))
|
|
),
|
|
formula_precedence_1
|
|
))(i)
|
|
}
|
|
|
|
fn formula_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a 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<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a 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<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a 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)))),
|
|
Err(_) => Ok((i, left)),
|
|
}
|
|
}
|
|
|
|
fn formula_precedence_6<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a 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<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
formula_precedence_6(i)
|
|
}
|
|
|
|
pub fn formulas<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a 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)),
|
|
]
|
|
)),
|
|
}
|
|
)),
|
|
}
|
|
))));
|
|
}
|
|
}
|
|
*/
|