pub(in crate::proving) fn is_always_false(_assertion: &str) -> bool {
false
}
pub(in crate::proving) fn is_always_true(_assertion: &str) -> bool {
false
}
pub(in crate::proving) fn find_conditional_counterexample(
_antecedent: &str,
_consequent: &str,
) -> Option<String> {
None
}
pub(in crate::proving) fn find_universal_counterexample(_assertion: &str) -> Option<String> {
None
}
pub(in crate::proving) fn find_existential_witness(_assertion: &str) -> Option<String> {
None
}
pub(in crate::proving) fn evaluate_expression(expr: &str) -> Option<f64> {
expr.parse::<f64>()
.ok()
.or_else(|| try_binary_operation(expr))
}
fn try_binary_operation(expr: &str) -> Option<f64> {
try_operation(expr, '+', |a, b| a + b)
.or_else(|| try_operation(expr, '-', |a, b| a - b))
.or_else(|| try_operation(expr, '*', |a, b| a * b))
}
fn try_operation<F>(expr: &str, op: char, compute: F) -> Option<f64>
where
F: Fn(f64, f64) -> f64,
{
if !expr.contains(op) {
return None;
}
let parts: Vec<&str> = expr.split(op).collect();
if parts.len() != 2 {
return None;
}
let left = evaluate_expression(parts[0].trim())?;
let right = evaluate_expression(parts[1].trim())?;
Some(compute(left, right))
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_is_always_false() {
assert!(!is_always_false("true"));
assert!(!is_always_false("some assertion"));
}
#[test]
fn test_is_always_true() {
assert!(!is_always_true("false"));
assert!(!is_always_true("some assertion"));
}
#[test]
fn test_find_conditional_counterexample() {
let result = find_conditional_counterexample("a", "b");
assert!(result.is_none());
}
#[test]
fn test_find_universal_counterexample() {
let result = find_universal_counterexample("forall x, x > 0");
assert!(result.is_none());
}
#[test]
fn test_find_existential_witness() {
let result = find_existential_witness("exists x, x > 0");
assert!(result.is_none());
}
#[test]
fn test_evaluate_expression_number() {
assert_eq!(evaluate_expression("42"), Some(42.0));
assert_eq!(evaluate_expression("3.14"), Some(3.14));
assert_eq!(evaluate_expression("-5"), Some(-5.0));
}
#[test]
fn test_evaluate_expression_addition() {
assert_eq!(evaluate_expression("2 + 3"), Some(5.0));
assert_eq!(evaluate_expression("10 + 5"), Some(15.0));
}
#[test]
fn test_evaluate_expression_subtraction() {
assert_eq!(evaluate_expression("5 - 3"), Some(2.0));
assert_eq!(evaluate_expression("10 - 15"), Some(-5.0));
}
#[test]
fn test_evaluate_expression_multiplication() {
assert_eq!(evaluate_expression("4 * 3"), Some(12.0));
assert_eq!(evaluate_expression("2 * 5"), Some(10.0));
}
#[test]
fn test_evaluate_expression_invalid() {
assert!(evaluate_expression("abc").is_none());
assert!(evaluate_expression("x + y").is_none());
}
#[test]
fn test_try_binary_operation_add() {
assert_eq!(try_binary_operation("1 + 2"), Some(3.0));
}
#[test]
fn test_try_binary_operation_sub() {
assert_eq!(try_binary_operation("5 - 2"), Some(3.0));
}
#[test]
fn test_try_binary_operation_mul() {
assert_eq!(try_binary_operation("3 * 4"), Some(12.0));
}
#[test]
fn test_try_operation_no_operator() {
let result = try_operation("42", '+', |a, b| a + b);
assert!(result.is_none());
}
#[test]
fn test_try_operation_too_many_parts() {
let result = try_operation("1 + 2 + 3", '+', |a, b| a + b);
assert!(result.is_none());
}
#[test]
fn test_try_operation_invalid_operands() {
let result = try_operation("a + b", '+', |a, b| a + b);
assert!(result.is_none());
}
}