From 42089014bd8337dfcb288db3e68f308b9eaadf0b Mon Sep 17 00:00:00 2001 From: Vinicius Gomes Date: Thu, 27 Jun 2024 20:52:19 -0300 Subject: [PATCH] Add String length core rules and extend PolyeqComparator for String comparisons --- carcara/src/ast/polyeq.rs | 180 +++++++++++++++- carcara/src/checker/mod.rs | 4 + carcara/src/checker/rules/strings.rs | 305 ++++++++++++++++++++++++++- 3 files changed, 485 insertions(+), 4 deletions(-) diff --git a/carcara/src/ast/polyeq.rs b/carcara/src/ast/polyeq.rs index b7f7dce9..2064ae25 100644 --- a/carcara/src/ast/polyeq.rs +++ b/carcara/src/ast/polyeq.rs @@ -10,9 +10,15 @@ use super::{ AnchorArg, BindingList, Operator, ProofArg, ProofCommand, ProofStep, Rc, Sort, Subproof, Term, }; -use crate::utils::HashMapStack; +use crate::{ast::Constant, utils::HashMapStack}; use std::time::{Duration, Instant}; +#[derive(Debug, Clone)] +enum Concat { + Constant(String), + Term(Rc), +} + /// A trait that represents objects that can be compared for equality modulo reordering of /// equalities or alpha equivalence. pub trait Polyeq { @@ -266,6 +272,138 @@ impl PolyeqComparator { self.compare_assoc(op, left_tail, right_tail) } + + fn remainder(&mut self, a: Vec, b: Vec) -> (Vec, Vec) { + fn to_concat(args: &[Rc]) -> Vec { + args.iter() + .map(|arg| match arg.as_ref() { + Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), + _ => Concat::Term(arg.clone()), + }) + .collect() + } + + match (a.first(), b.first()) { + (None | Some(_), None) | (None, Some(_)) => (a, b), + (Some(a_head), Some(b_head)) => match (a_head, b_head) { + (Concat::Constant(a_constant), Concat::Constant(b_constant)) => { + let prefix_length = std::cmp::min(a_constant.len(), b_constant.len()); + for i in 0..prefix_length { + if a_constant.chars().nth(i).unwrap() != b_constant.chars().nth(i).unwrap() + { + return (a, b); + } + } + let a_const_rem = &a_constant[prefix_length..]; + let b_const_rem = &b_constant[prefix_length..]; + let mut new_a = a[1..].to_vec(); + let mut new_b = b[1..].to_vec(); + if !a_const_rem.is_empty() { + new_a.insert(0, Concat::Constant(a_const_rem.to_owned())); + } + if !b_const_rem.is_empty() { + new_b.insert(0, Concat::Constant(b_const_rem.to_owned())); + } + self.remainder(new_a, new_b) + } + (Concat::Constant(constant), Concat::Term(term)) => match term.as_ref() { + Term::Op(Operator::StrConcat, args) => { + let concat_args: Vec = to_concat(args); + let (constant_rem, concat_rem) = self.remainder(a.clone(), concat_args); + let mut new_b = b[1..].to_vec(); + for c in concat_rem.iter().rev() { + new_b.insert(0, c.clone()); + } + self.remainder(constant_rem, new_b) + } + _ => { + if constant.is_empty() { + return self.remainder(a[1..].to_vec(), b); + } + (a, b) + } + }, + (Concat::Term(term), Concat::Constant(constant)) => match term.as_ref() { + Term::Op(Operator::StrConcat, args) => { + let concat_args: Vec = to_concat(args); + let (concat_rem, constant_rem) = self.remainder(concat_args, b.clone()); + let mut new_a = a[1..].to_vec(); + for c in concat_rem.iter().rev() { + new_a.insert(0, c.clone()); + } + self.remainder(new_a, constant_rem) + } + _ => { + if constant.is_empty() { + return self.remainder(a, b[1..].to_vec()); + } + (a, b) + } + }, + (Concat::Term(a_term), Concat::Term(b_term)) => { + match (a_term.as_ref(), b_term.as_ref()) { + ( + Term::Op(Operator::StrConcat, a_args), + Term::Op(Operator::StrConcat, b_args), + ) => { + let concat_a_args: Vec = to_concat(a_args); + let concat_b_args: Vec = to_concat(b_args); + let (concat_a_rem, concat_b_rem) = + self.remainder(concat_a_args, concat_b_args); + let mut new_a = a[1..].to_vec(); + let mut new_b = b[1..].to_vec(); + for c in concat_a_rem.iter().rev() { + new_a.insert(0, c.clone()); + } + for c in concat_b_rem.iter().rev() { + new_b.insert(0, c.clone()); + } + self.remainder(new_a, new_b) + } + (Term::Op(Operator::StrConcat, a_args), _) => { + if Polyeq::eq(self, &a_args[0], b_term) { + let concat_a_rem: Vec = to_concat(&a_args[1..]); + let mut new_a = a[1..].to_vec(); + for c in concat_a_rem.iter().rev() { + new_a.insert(0, c.clone()); + } + let new_b = b[1..].to_vec(); + self.remainder(new_a, new_b) + } else { + (a, b) + } + } + (_, Term::Op(Operator::StrConcat, b_args)) => { + if Polyeq::eq(self, &b_args[0], a_term) { + let new_a = a[1..].to_vec(); + let concat_b_rem: Vec = to_concat(&b_args[1..]); + let mut new_b = b[1..].to_vec(); + for c in concat_b_rem.iter().rev() { + new_b.insert(0, c.clone()); + } + self.remainder(new_a, new_b) + } else { + (a, b) + } + } + _ => { + if Polyeq::eq(self, a_term, b_term) { + let new_a = a[1..].to_vec(); + let new_b = b[1..].to_vec(); + self.remainder(new_a, new_b) + } else { + (a, b) + } + } + } + } + }, + } + } + + fn compare_strings(&mut self, a: Vec, b: Vec) -> bool { + matches!(self.remainder(a, b), (rem_a, rem_b) if rem_a.is_empty() && rem_b.is_empty()) + } } impl Polyeq for Rc { @@ -328,6 +466,46 @@ impl Polyeq for Term { args: args_b, }, ) => op_a == op_b && op_args_a == op_args_b && Polyeq::eq(comp, args_a, args_b), + (Term::Op(Operator::StrConcat, args_a), Term::Op(Operator::StrConcat, args_b)) => { + let concat_args_a: Vec = args_a + .iter() + .map(|arg| match arg.as_ref() { + Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), + _ => Concat::Term(arg.clone()), + }) + .collect(); + let concat_args_b: Vec = args_b + .iter() + .map(|arg| match arg.as_ref() { + Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), + _ => Concat::Term(arg.clone()), + }) + .collect(); + comp.compare_strings(concat_args_a, concat_args_b) + } + (Term::Op(Operator::StrConcat, args_a), Term::Const(Constant::String(b))) => { + let concat_args_a: Vec = args_a + .iter() + .map(|arg| match arg.as_ref() { + Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), + _ => Concat::Term(arg.clone()), + }) + .collect(); + let concat_args_b = vec![Concat::Constant(b.clone())]; + comp.compare_strings(concat_args_a, concat_args_b) + } + (Term::Const(Constant::String(a)), Term::Op(Operator::StrConcat, args_b)) => { + let concat_args_a = vec![Concat::Constant(a.clone())]; + let concat_args_b: Vec = args_b + .iter() + .map(|arg| match arg.as_ref() { + Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), + _ => Concat::Term(arg.clone()), + }) + .collect(); + comp.compare_strings(concat_args_a, concat_args_b) + } + (Term::Op(op_a, args_a), Term::Op(op_b, args_b)) => { comp.compare_op(*op_a, args_a, *op_b, args_b) } diff --git a/carcara/src/checker/mod.rs b/carcara/src/checker/mod.rs index e28b6893..943050d0 100644 --- a/carcara/src/checker/mod.rs +++ b/carcara/src/checker/mod.rs @@ -557,6 +557,10 @@ impl<'c> ProofChecker<'c> { "concat_lprop_prefix" => strings::concat_lprop_prefix, "concat_lprop_suffix" => strings::concat_lprop_suffix, + "string_decompose" => strings::string_decompose, + "string_length_pos" => strings::string_length_pos, + "string_length_non_empty" => strings::string_length_non_empty, + // Special rules that always check as valid, and are used to indicate holes in the // proof. "hole" => |_| Ok(()), diff --git a/carcara/src/checker/rules/strings.rs b/carcara/src/checker/rules/strings.rs index eb6cb9e8..ad1879da 100644 --- a/carcara/src/checker/rules/strings.rs +++ b/carcara/src/checker/rules/strings.rs @@ -2,7 +2,10 @@ use super::{ assert_clause_len, assert_eq, assert_num_args, assert_num_premises, assert_polyeq_expected, get_premise_term, RuleArgs, RuleResult, }; -use crate::{ast::*, checker::error::CheckerError}; +use crate::{ + ast::*, + checker::{error::CheckerError, rules::assert_polyeq}, +}; use std::{cmp, time::Duration}; /// A function that takes an `Rc` and returns a vector corresponding to @@ -726,6 +729,90 @@ pub fn concat_lprop_suffix( assert_eq(&expected, &expanded) } +pub fn string_decompose( + RuleArgs { + premises, + args, + conclusion, + pool, + polyeq_time, + .. + }: RuleArgs, +) -> RuleResult { + assert_num_premises(premises, 1)?; + assert_num_args(args, 1)?; + assert_clause_len(conclusion, 1)?; + + let term = get_premise_term(&premises[0])?; + let rev = args[0].as_term()?.as_bool_err()?; + let (t, n) = match_term_err!((>= (strlen t) n) = term)?; + + match_term_err!( + (and + (= t x) + (= (strlen y) n) + ) = &conclusion[0] + )?; + + let w_1 = build_skolem_prefix(pool, t.clone(), n.clone()); + let w_2 = build_skolem_suffix_rem(pool, t.clone(), n.clone()); + let len_term = if rev { w_2.clone() } else { w_1.clone() }; + + let expanded = build_term!( + pool, + (and + (= {t.clone()} (strconcat {w_1.clone()} {w_2.clone()})) + (= (strlen {len_term.clone()}) {n.clone()}) + ) + ); + + assert_polyeq(&conclusion[0], &expanded, polyeq_time) +} + +pub fn string_length_pos(RuleArgs { args, conclusion, polyeq_time, .. }: RuleArgs) -> RuleResult { + assert_num_args(args, 1)?; + assert_clause_len(conclusion, 1)?; + + let t = args[0].as_term()?; + let (((t_1, _), (t_2, _)), (t_3, _)) = match_term_err!( + (or + (and + (= (strlen t) 0) + (= t "") + ) + (> (strlen t) 0) + ) = &conclusion[0] + )?; + + assert_polyeq(t_1, t, polyeq_time)?; + assert_polyeq(t_2, t, polyeq_time)?; + assert_polyeq(t_3, t, polyeq_time)?; + + Ok(()) +} + +pub fn string_length_non_empty( + RuleArgs { + premises, conclusion, polyeq_time, .. + }: RuleArgs, +) -> RuleResult { + assert_num_premises(premises, 1)?; + assert_clause_len(conclusion, 1)?; + + let term = get_premise_term(&premises[0])?; + let (t, _) = match_term_err!((not (= t "")) = term)?; + + let (t_conc, _) = match_term_err!( + (not + (= (strlen t) 0) + ) = &conclusion[0] + )?; + + assert_polyeq(t_conc, t, polyeq_time)?; + + Ok(()) +} + mod tests { #[test] fn concat_eq() { @@ -1192,7 +1279,7 @@ mod tests { (define-fun r_skolem () String (ite (>= (str.len "a") (str.len (str.++ "a" c))) (str.substr "a" (str.len (str.++ "a" c)) (- (str.len "a") (str.len (str.++ "a" c)))) (str.substr (str.++ "a" c) (str.len "a") (- (str.len (str.++ "a" c)) (str.len "a"))))) (step t1 (cl (and (or (= "a" (str.++ "a" c r_skolem)) (= (str.++ "a" c) (str.++ "a" r_skolem))) (not (= r_skolem "")) (> (str.len r_skolem) 0))) :rule concat_split_prefix :premises (h1 h2))"#: false, } - r#"Conclusion term is not of the form (and (or (= x y) (= z w)) (not (= r "")) (> (str.len r) 0))"# { + "Conclusion term is not of the form (and (or (= x y) (= z w)) (not (= r \"\")) (> (str.len r) 0))" { r#"(assume h1 (= (str.++ a b c) (str.++ c d e))) (assume h2 (not (= (str.len (str.++ a b)) (str.len c)))) (define-fun r_skolem () String (ite (>= (str.len (str.++ a b)) (str.len c)) (str.substr (str.++ a b) (str.len c) (- (str.len (str.++ a b)) (str.len c))) (str.substr c (str.len (str.++ a b)) (- (str.len c) (str.len (str.++ a b)))))) @@ -1277,7 +1364,7 @@ mod tests { (define-fun r_skolem () String (ite (>= (str.len (str.++ "b" b)) (str.len c)) (str.substr (str.++ "b" b) 0 (- (str.len (str.++ "b" b)) (str.len c))) (str.substr c 0 (- (str.len c) (str.len (str.++ "b" b)))))) (step t1 (cl (and (or (= (str.++ "b" b) (str.++ r_skolem c)) (= c (str.++ r_skolem (str.++ "b" b)))) (not (= r_skolem "")) (> (str.len r_skolem) 0))) :rule concat_split_suffix :premises (h1 h2))"#: false, } - r#"Conclusion term is not of the form (and (or (= x y) (= z w)) (not (= r "")) (> (str.len r) 0))"# { + "Conclusion term is not of the form (and (or (= x y) (= z w)) (not (= r \"\")) (> (str.len r) 0))" { r#"(assume h1 (= (str.++ a b c d) (str.++ b c d e))) (assume h2 (not (= (str.len (str.++ c d)) (str.len (str.++ c d e))))) (define-fun r_skolem () String (ite (>= (str.len (str.++ c d)) (str.len (str.++ c d e))) (str.substr (str.++ c d) 0 (- (str.len (str.++ c d)) (str.len (str.++ c d e)))) (str.substr (str.++ c d e) 0 (- (str.len (str.++ c d e)) (str.len (str.++ c d)))))) @@ -1465,4 +1552,216 @@ mod tests { } } } + + #[test] + fn string_decompose() { + test_cases! { + definitions = " + (declare-fun a () String) + (declare-fun b () String) + (declare-fun c () String) + (declare-fun d () String) + ", + "Simple working examples" { + r#"(assume h1 (>= (str.len "ab") 2)) + (define-fun w_1 () String (str.substr "ab" 0 2)) + (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2))) + (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args (false))"#: true, + r#"(assume h1 (>= (str.len (str.++ "d" "c")) 1)) + (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1)) + (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1))) + (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_1 w_2)) (= (str.len w_1) 1))) :rule string_decompose :premises (h1) :args (false))"#: true, + r#"(assume h1 (>= (str.len (str.++ a (str.++ "b" c))) 0)) + (define-fun w_1 () String (str.substr (str.++ a (str.++ "b" c)) 0 0)) + (define-fun w_2 () String (str.substr (str.++ a (str.++ "b" c)) 0 (- (str.len (str.++ a (str.++ "b" c))) 0))) + (step t1 (cl (and (= (str.++ a (str.++ "b" c)) (str.++ w_1 w_2)) (= (str.len w_1) 0))) :rule string_decompose :premises (h1) :args (false))"#: true, + r#"(assume h1 (>= (str.len "ab") 2)) + (define-fun w_1 () String (str.substr "ab" 0 2)) + (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2))) + (step t1 (cl (and (= (str.++ "a" "b") (str.++ w_1 w_2)) (= (str.len w_2) 2))) :rule string_decompose :premises (h1) :args (true))"#: true, + + } + "Reverse argument set to true" { + r#"(assume h1 (>= (str.len "ab") 2)) + (define-fun w_1 () String (str.substr "ab" 0 2)) + (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2))) + (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_2) 2))) :rule string_decompose :premises (h1) :args (true))"#: true, + r#"(assume h1 (>= (str.len (str.++ "d" "c")) 1)) + (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1)) + (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1))) + (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_1 w_2)) (= (str.len w_2) 1))) :rule string_decompose :premises (h1) :args (true))"#: true, + } + "Invalid argument type" { + r#"(assume h1 (>= (str.len "ab") 2)) + (define-fun w_1 () String (str.substr "ab" 0 2)) + (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2))) + (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args (1))"#: false, + r#"(assume h1 (>= (str.len "ab") 2)) + (define-fun w_1 () String (str.substr "ab" 0 2)) + (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2))) + (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args (1.5))"#: false, + r#"(assume h1 (>= (str.len "ab") 2)) + (define-fun w_1 () String (str.substr "ab" 0 2)) + (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2))) + (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args ((- 1)))"#: false, + r#"(assume h1 (>= (str.len "ab") 2)) + (define-fun w_1 () String (str.substr "ab" 0 2)) + (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2))) + (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args ("teste"))"#: false, + r#"(assume h1 (>= (str.len "ab") 2)) + (define-fun w_1 () String (str.substr "ab" 0 2)) + (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2))) + (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args (d))"#: false, + } + "Premise term \"t\" is not the same in the conclusion" { + r#"(assume h1 (>= (str.len "ab") 2)) + (define-fun w_1 () String (str.substr "ab" 0 2)) + (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2))) + (step t1 (cl (and (= "ba" (str.++ w_1 w_2)) (= (str.len w_2) 2))) :rule string_decompose :premises (h1) :args (true))"#: false, + r#"(assume h1 (>= (str.len "ba") 2)) + (define-fun w_1 () String (str.substr "ba" 0 2)) + (define-fun w_2 () String (str.substr "ba" 2 (- (str.len "ba") 2))) + (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_2) 2))) :rule string_decompose :premises (h1) :args (true))"#: false, + r#"(assume h1 (>= (str.len (str.++ "a" (str.++ b "c"))) 2)) + (define-fun w_1 () String (str.substr (str.++ "a" (str.++ b "c")) 0 2)) + (define-fun w_2 () String (str.substr (str.++ "a" (str.++ b "c")) 2 (- (str.len (str.++ "a" (str.++ b "c"))) 2))) + (step t1 (cl (and (= (str.++ a (str.++ b "c")) (str.++ w_1 w_2)) (= (str.len w_2) 2))) :rule string_decompose :premises (h1) :args (true))"#: false, + } + "Switched skolems in the conclusion" { + r#"(assume h1 (>= (str.len (str.++ "d" "c")) 1)) + (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1)) + (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1))) + (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_2 w_1)) (= (str.len w_1) 1))) :rule string_decompose :premises (h1) :args (false))"#: false, + } + "" {} + "Premise is not of the form (>= (str.len t) n)" { + r#"(assume h1 (< (str.len (str.++ "d" "c")) 1)) + (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1)) + (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1))) + (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_1 w_2)) (= (str.len w_2) 1))) :rule string_decompose :premises (h1) :args (true))"#: false, + r#"(assume h1 (>= (str.to_code (str.++ "d" "c")) 1)) + (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1)) + (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1))) + (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_1 w_2)) (= (str.len w_2) 1))) :rule string_decompose :premises (h1) :args (true))"#: false, + } + "Conclusion term is not of the form (and (= t x) (= (str.len y) 0))" { + r#"(assume h1 (>= (str.len (str.++ a (str.++ "b" c))) 0)) + (define-fun w_1 () String (str.substr (str.++ a (str.++ "b" c)) 0 0)) + (define-fun w_2 () String (str.substr (str.++ a (str.++ "b" c)) 0 (- (str.len (str.++ a (str.++ "b" c))) 0))) + (step t1 (cl (or (= (str.++ a (str.++ "b" c)) (str.++ w_1 w_2)) (= (str.len w_1) 0))) :rule string_decompose :premises (h1) :args (false))"#: false, + r#"(assume h1 (>= (str.len (str.++ a (str.++ "b" c))) 0)) + (define-fun w_1 () String (str.substr (str.++ a (str.++ "b" c)) 0 0)) + (define-fun w_2 () String (str.substr (str.++ a (str.++ "b" c)) 0 (- (str.len (str.++ a (str.++ "b" c))) 0))) + (step t1 (cl (and (not (= (str.++ a (str.++ "b" c)) (str.++ w_1 w_2))) (= (str.len w_1) 0))) :rule string_decompose :premises (h1) :args (false))"#: false, + r#"(assume h1 (>= (str.len (str.++ a (str.++ "b" c))) 0)) + (define-fun w_1 () String (str.substr (str.++ a (str.++ "b" c)) 0 0)) + (define-fun w_2 () String (str.substr (str.++ a (str.++ "b" c)) 0 (- (str.len (str.++ a (str.++ "b" c))) 0))) + (step t1 (cl (and (= (str.++ a (str.++ "b" c)) (str.++ w_1 w_2)) (not (= (str.len w_1) 0)))) :rule string_decompose :premises (h1) :args (false))"#: false, + r#"(assume h1 (>= (str.len (str.++ a (str.++ "b" c))) 0)) + (define-fun w_1 () String (str.substr (str.++ a (str.++ "b" c)) 0 0)) + (define-fun w_2 () String (str.substr (str.++ a (str.++ "b" c)) 0 (- (str.len (str.++ a (str.++ "b" c))) 0))) + (step t1 (cl (and (= (str.++ a (str.++ "b" c)) (str.++ w_1 w_2)) (= (str.to_code w_1) 0))) :rule string_decompose :premises (h1) :args (false))"#: false, + } + "Inverted argument value" { + r#"(assume h1 (>= (str.len "ab") 2)) + (define-fun w_1 () String (str.substr "ab" 0 2)) + (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2))) + (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args (true))"#: false, + r#"(assume h1 (>= (str.len (str.++ "d" "c")) 1)) + (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1)) + (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1))) + (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_1 w_2)) (= (str.len w_2) 1))) :rule string_decompose :premises (h1) :args (false))"#: false, + } + } + } + + #[test] + fn string_length_pos() { + test_cases! { + definitions = " + (declare-fun a () String) + (declare-fun b () String) + (declare-fun c () String) + (declare-fun d () String) + ", + "Simple working examples" { + r#"(step t1 (cl (or (and (= (str.len "ab") 0) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: true, + r#"(step t1 (cl (or (and (= (str.len (str.++ "a" (str.++ b "c"))) 0) (= (str.++ "a" (str.++ b "c")) "")) (> (str.len (str.++ "a" (str.++ b "c"))) 0))) :rule string_length_pos :args ((str.++ "a" (str.++ b "c"))))"#: true, + r#"(step t1 (cl (or (and (= (str.len a) 0) (= a "")) (> (str.len a) 0))) :rule string_length_pos :args (a))"#: true, + r#"(step t1 (cl (or (and (= (str.len (str.++ a "b")) 0) (= (str.++ a "b") "")) (> (str.len (str.++ a "b")) 0))) :rule string_length_pos :args ((str.++ a "b")))"#: true, + r#"(step t1 (cl (or (and (= (str.len (str.++ "a" "b")) 0) (= (str.++ "a" "b") "")) (> (str.len (str.++ "a" "b")) 0))) :rule string_length_pos :args ("ab"))"#: true, + } + "Argument term \"t\" and the conclusion term \"t\" is not the same" { + r#"(step t1 (cl (or (and (= (str.len (str.++ a "b")) 0) (= (str.++ a "b") "")) (> (str.len (str.++ a "b")) 0))) :rule string_length_pos :args ((str.++ "a" b)))"#: false, + r#"(step t1 (cl (or (and (= (str.len (str.++ "a" b)) 0) (= (str.++ "a" b) "")) (> (str.len (str.++ "a" b)) 0))) :rule string_length_pos :args ((str.++ a "b")))"#: false, + r#"(step t1 (cl (or (and (= (str.len (str.++ "b" a)) 0) (= (str.++ a "b") "")) (> (str.len (str.++ a "b")) 0))) :rule string_length_pos :args ((str.++ a "b")))"#: false, + r#"(step t1 (cl (or (and (= (str.len (str.++ a "b")) 0) (= a "")) (> (str.len (str.++ a "b")) 0))) :rule string_length_pos :args ((str.++ a "b")))"#: false, + r#"(step t1 (cl (or (and (= (str.len (str.++ a "b")) 0) (= (str.++ a "b") "")) (> (str.len (str.++ b d)) 0))) :rule string_length_pos :args ((str.++ a "b")))"#: false, + } + "Conclusion is not of the form (or (and (= (str.len t) 0) (= t \"\")) (> (str.len t) 0))" { + r#"(step t1 (cl (and (and (= (str.len "ab") 0) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false, + r#"(step t1 (cl (or (or (= (str.len "ab") 0) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false, + r#"(step t1 (cl (or (and (not (= (str.len "ab") 0)) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false, + r#"(step t1 (cl (or (and (= (str.to_code "ab") 0) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false, + r#"(step t1 (cl (or (and (= (str.len "ab") 1) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false, + r#"(step t1 (cl (or (and (= (str.len "ab") 0) (not (= "ab" ""))) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false, + r#"(step t1 (cl (or (and (= (str.len "ab") 0) (= "ab" "a")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false, + r#"(step t1 (cl (or (and (= (str.len "ab") 0) (= "ab" "")) (< (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false, + r#"(step t1 (cl (or (and (= (str.len "ab") 0) (= "ab" "")) (> (str.to_code "ab") 0))) :rule string_length_pos :args ("ab"))"#: false, + r#"(step t1 (cl (or (and (= (str.len "ab") 0) (= "ab" "")) (> (str.len "ab") 1))) :rule string_length_pos :args ("ab"))"#: false, + } + } + } + + #[test] + fn string_length_non_empty() { + test_cases! { + definitions = " + (declare-fun a () String) + (declare-fun b () String) + (declare-fun c () String) + (declare-fun d () String) + ", + "Simple working examples" { + r#"(assume h1 (not (= "ab" ""))) + (step t1 (cl (not (= (str.len "ab") 0))) :rule string_length_non_empty :premises (h1))"#: true, + r#"(assume h1 (not (= (str.++ "a" (str.++ "b" "c")) ""))) + (step t1 (cl (not (= (str.len (str.++ "a" (str.++ "b" "c"))) 0))) :rule string_length_non_empty :premises (h1))"#: true, + r#"(assume h1 (not (= d ""))) + (step t1 (cl (not (= (str.len d) 0))) :rule string_length_non_empty :premises (h1))"#: true, + r#"(assume h1 (not (= (str.++ b c) ""))) + (step t1 (cl (not (= (str.len (str.++ b c)) 0))) :rule string_length_non_empty :premises (h1))"#: true, + r#"(assume h1 (not (= (str.++ "b" "c") ""))) + (step t1 (cl (not (= (str.len "bc") 0))) :rule string_length_non_empty :premises (h1))"#: true, + } + "Premise term is not an inequality of the form (not (= t \"\"))" { + r#"(assume h1 (= (str.++ "a" (str.++ "b" "c")) "")) + (step t1 (cl (not (= (str.len (str.++ "a" (str.++ "b" "c"))) 0))) :rule string_length_non_empty :premises (h1))"#: false, + r#"(assume h1 (not (= (str.++ "a" (str.++ "b" "c")) "ab"))) + (step t1 (cl (not (= (str.len (str.++ "a" (str.++ "b" "c"))) 0))) :rule string_length_non_empty :premises (h1))"#: false, + r#"(assume h1 (not (= (str.++ "a" (str.++ "b" "c")) a))) + (step t1 (cl (not (= (str.len (str.++ "a" (str.++ "b" "c"))) 0))) :rule string_length_non_empty :premises (h1))"#: false, + r#"(assume h1 (not (= (str.++ "a" (str.++ "b" "c")) (str.++ a b)))) + (step t1 (cl (not (= (str.len (str.++ "a" (str.++ "b" "c"))) 0))) :rule string_length_non_empty :premises (h1))"#: false, + } + "Shared term \"t\" between the premise and the conclusion is not the same" { + r#"(assume h1 (not (= (str.++ b c) ""))) + (step t1 (cl (not (= (str.len (str.++ c b)) 0))) :rule string_length_non_empty :premises (h1))"#: false, + r#"(assume h1 (not (= (str.++ b c) ""))) + (step t1 (cl (not (= (str.len (str.++ "b" "c")) 0))) :rule string_length_non_empty :premises (h1))"#: false, + r#"(assume h1 (not (= (str.++ "b" c) ""))) + (step t1 (cl (not (= (str.len (str.++ b c)) 0))) :rule string_length_non_empty :premises (h1))"#: false, + } + "Conclusion term is not an inequality of the form (not (= (str.len t) 0))" { + r#"(assume h1 (not (= "ab" ""))) + (step t1 (cl (= (str.len "ab") 0)) :rule string_length_non_empty :premises (h1))"#: false, + r#"(assume h1 (not (= "ab" ""))) + (step t1 (cl (not (= (str.to_code "ab") 0))) :rule string_length_non_empty :premises (h1))"#: false, + r#"(assume h1 (not (= "ab" ""))) + (step t1 (cl (not (> (str.len "ab") 0))) :rule string_length_non_empty :premises (h1))"#: false, + r#"(assume h1 (not (= "ab" ""))) + (step t1 (cl (not (= (str.len "ab") 1))) :rule string_length_non_empty :premises (h1))"#: false, + } + } + } }