Skip to content

Commit 9497fe0

Browse files
NishEatsWafflezNishEatsWafflez
committed
Fixed str at negation - tiching did this one
1 parent 8d418d9 commit 9497fe0

2 files changed

Lines changed: 52 additions & 28 deletions

File tree

‎src/smt/parse.rs‎

Lines changed: 51 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -771,12 +771,6 @@ impl SmtParser {
771771
}
772772
false
773773
}
774-
fn is_substr_operation(&mut self, v: &Value) -> bool {
775-
if let Some((Value::Symbol(s), _tail)) = v.as_pair() {
776-
return **s == *"str.substr";
777-
}
778-
false
779-
}
780774

781775
fn parse_len_greater_than(
782776
&mut self,
@@ -1345,22 +1339,22 @@ impl SmtParser {
13451339
(IntToken::Var(v1), IntToken::Var(v2)) => {
13461340
let gre1 = GenRegex::create_gre_str_var(&v1);
13471341
let gre2 = GenRegex::create_gre_str_var(&v2);
1348-
return Ok(GenRegex::intersect(&gre1, &gre2));
1342+
Ok(GenRegex::intersect(&gre1, &gre2))
13491343
}
13501344
(IntToken::Var(v), IntToken::Val(num)) => {
13511345
let gre1 = GenRegex::create_gre_str_var(&v);
13521346
let gre2 = GenRegex::caret(num as u64, &Rc::new(GenRegex::Sigma));
1353-
return Ok(GenRegex::intersect(&gre1, &gre2));
1347+
Ok(GenRegex::intersect(&gre1, &gre2))
13541348
}
13551349
(IntToken::Val(num), IntToken::Var(v)) => {
13561350
let gre1 = GenRegex::create_gre_str_var(&v);
13571351
let gre2 = GenRegex::caret(num as u64, &Rc::new(GenRegex::Sigma));
1358-
return Ok(GenRegex::intersect(&gre1, &gre2));
1352+
Ok(GenRegex::intersect(&gre1, &gre2))
13591353
}
13601354
(IntToken::Val(num1), IntToken::Val(num2)) => {
13611355
let gre1 = GenRegex::caret(num1 as u64, &Rc::new(GenRegex::Sigma));
13621356
let gre2 = GenRegex::caret(num2 as u64, &Rc::new(GenRegex::Sigma));
1363-
return Ok(GenRegex::intersect(&gre1, &gre2));
1357+
Ok(GenRegex::intersect(&gre1, &gre2))
13641358
}
13651359
}
13661360
}
@@ -1874,17 +1868,17 @@ impl SmtParser {
18741868

18751869
let dot_i_s2_dot_j = GenRegex::complement(&GenRegex::concat(
18761870
&dot_i,
1877-
&GenRegex::concat(&string_gre, &dot_j),
1871+
&GenRegex::concat(string_gre, &dot_j),
18781872
));
18791873
let s1_case_1 = GenRegex::intersect(&big_string_gre, &dot_i_s2_dot_j);
1880-
let s2_case_1 = GenRegex::intersect(&string_gre, &dot_j);
1874+
let s2_case_1 = GenRegex::intersect(string_gre, &dot_j);
18811875
let s1_length_1 = GenRegex::intersect(
18821876
&big_string_gre,
18831877
&GenRegex::concat(&dot_i, &GenRegex::concat(&dot_j, &GenRegex::sigma_star())),
18841878
);
18851879
let case_1 = GenRegex::concat(&s1_case_1, &GenRegex::concat(&s2_case_1, &s1_length_1));
18861880

1887-
let dot_i_s2 = GenRegex::complement(&GenRegex::concat(&dot_i, &string_gre));
1881+
let dot_i_s2 = GenRegex::complement(&GenRegex::concat(&dot_i, string_gre));
18881882
let case_2_s1 = GenRegex::intersect(&big_string_gre, &dot_i_s2);
18891883
let dot_j_dot_star = GenRegex::concat(&dot_j, &GenRegex::sigma_star());
18901884
let s1_len_2 = GenRegex::concat(&dot_i, &GenRegex::complement(&dot_j_dot_star));
@@ -1895,7 +1889,7 @@ impl SmtParser {
18951889
let s1_len_3 =
18961890
GenRegex::intersect(&big_string_gre, &GenRegex::complement(&dot_i_dot_star));
18971891
let s2_case_3 =
1898-
GenRegex::intersect(&string_gre, &GenRegex::complement(&GenRegex::epsilon()));
1892+
GenRegex::intersect(string_gre, &GenRegex::complement(&GenRegex::epsilon()));
18991893
let case_3 = GenRegex::concat(&s1_len_3, &s2_case_3);
19001894

19011895
Ok(GenRegex::union(&GenRegex::union(&case_1, &case_2), &case_3))
@@ -1923,27 +1917,27 @@ impl SmtParser {
19231917

19241918
let dot_i_s2_dot_j = GenRegex::concat(
19251919
&dot_i,
1926-
&GenRegex::concat(&string_gre, &GenRegex::sigma_star()),
1920+
&GenRegex::concat(string_gre, &GenRegex::sigma_star()),
19271921
);
19281922
let s1_case_1 = GenRegex::intersect(&big_string_gre, &dot_i_s2_dot_j);
1929-
let s2_case_1 = GenRegex::intersect(&string_gre, &dot_j);
1923+
let s2_case_1 = GenRegex::intersect(string_gre, &dot_j);
19301924
let s1_length_1 = GenRegex::intersect(
19311925
&big_string_gre,
19321926
&GenRegex::concat(&dot_i, &GenRegex::concat(&dot_j, &GenRegex::sigma_star())),
19331927
);
19341928
let case_1 = GenRegex::concat(&s1_case_1, &GenRegex::concat(&s2_case_1, &s1_length_1));
19351929

1936-
let dot_i_s2 = GenRegex::concat(&dot_i, &string_gre);
1930+
let dot_i_s2 = GenRegex::concat(&dot_i, string_gre);
19371931
let case_2_s1 = GenRegex::intersect(&big_string_gre, &dot_i_s2);
19381932
let dot_j_dot_star = GenRegex::concat(&dot_j, &GenRegex::sigma_star());
19391933
let s1_len_2 = &GenRegex::complement(&dot_j_dot_star);
1940-
let s1_length_2 = GenRegex::intersect(&string_gre, &s1_len_2);
1934+
let s1_length_2 = GenRegex::intersect(string_gre, s1_len_2);
19411935
let case_2 = GenRegex::concat(&case_2_s1, &s1_length_2);
19421936

19431937
let dot_i_dot_star = GenRegex::concat(&dot_i, &GenRegex::sigma_star());
19441938
let s1_len_3 =
19451939
GenRegex::intersect(&big_string_gre, &GenRegex::complement(&dot_i_dot_star));
1946-
let s2_case_3 = GenRegex::intersect(&string_gre, &GenRegex::epsilon());
1940+
let s2_case_3 = GenRegex::intersect(string_gre, &GenRegex::epsilon());
19471941
let case_3 = GenRegex::concat(&s1_len_3, &s2_case_3);
19481942

19491943
Ok(GenRegex::union(&GenRegex::union(&case_1, &case_2), &case_3))
@@ -2383,23 +2377,53 @@ impl SmtParser {
23832377
found_str.clone(),
23842378
GenRegex::sigma_star(),
23852379
];
2386-
let string_constraint1 =
2387-
GenRegex::intersect(&string.clone(), &GenRegex::concat_many(&args));
2380+
let string_constraint1 =if self.not_flag {
2381+
GenRegex::intersect(&string.clone(), &GenRegex::complement(&GenRegex::concat_many(&args)))
2382+
} else {
2383+
GenRegex::intersect(&string.clone(), &GenRegex::concat_many(&args))
2384+
};
23882385
let constraint1 =
23892386
GenRegex::concat(&string_constraint1.clone(), &found_str_constraint1.clone());
23902387
println!("{}", constraint1);
2391-
let constraint2 = GenRegex::concat(
2388+
let constraint2 = if self.not_flag {
2389+
GenRegex::concat(
2390+
&GenRegex::intersect(
2391+
&string.clone(),
2392+
&GenRegex::complement(&GenRegex::concat(
2393+
&GenRegex::caret(index as u64, &GenRegex::create_sigma()),
2394+
&GenRegex::sigma_star(),
2395+
)),
2396+
),
2397+
&GenRegex::intersect(&found_str, &GenRegex::complement(&GenRegex::epsilon())),
2398+
)
2399+
} else {
2400+
GenRegex::concat(
23922401
&GenRegex::intersect(
23932402
&string.clone(),
23942403
&GenRegex::complement(&GenRegex::concat(
23952404
&GenRegex::caret(index as u64, &GenRegex::create_sigma()),
23962405
&GenRegex::sigma_star(),
23972406
)),
23982407
),
2399-
&GenRegex::intersect(&found_str, &GenRegex::epsilon()),
2400-
);
2408+
&GenRegex::intersect(&found_str, &GenRegex::epsilon()),
2409+
)
2410+
};
24012411
println!("{}", constraint2);
2402-
Ok(GenRegex::union(&constraint1, &constraint2))
2412+
if self.not_flag {
2413+
let constraint3=GenRegex::concat(
2414+
&GenRegex::intersect(
2415+
&string.clone(),
2416+
&GenRegex::concat(
2417+
&GenRegex::caret(index as u64, &GenRegex::create_sigma()),
2418+
&GenRegex::sigma_star(),
2419+
),
2420+
),
2421+
&GenRegex::intersect(&found_str, &GenRegex::complement(&GenRegex::create_sigma())),
2422+
);
2423+
Ok(GenRegex::union_many(&[constraint1,constraint2,constraint3]))
2424+
} else {
2425+
Ok(GenRegex::union(&constraint1, &constraint2))
2426+
}
24032427
}
24042428
/*
24052429
Parsing functions with output Int
@@ -2411,7 +2435,7 @@ impl SmtParser {
24112435
}
24122436
if let Some(name) = v.as_symbol() {
24132437
if self.int_var_names.contains(name) {
2414-
return Ok(IntToken::Var(name.to_string()));
2438+
Ok(IntToken::Var(name.to_string()))
24152439
} else {
24162440
Err(SmtParseError::BadLiteral(format!(
24172441
"{} is not found in declared variables, defined functions or let variables.",
@@ -2481,7 +2505,7 @@ impl SmtParser {
24812505
println!("{}", false_constraint);
24822506
let final_constraint = GenRegex::intersect(&true_constraint, &false_constraint);
24832507
println!("{}", final_constraint);
2484-
return Ok(GenRegex::intersect(&str1, &final_constraint));
2508+
Ok(GenRegex::intersect(&str1, &final_constraint))
24852509
}
24862510

24872511
/*

‎src/types/regex.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -230,7 +230,7 @@ impl GenRegex {
230230
pub fn make_equals(gre1: Rc<GenRegex>, gre2: Rc<GenRegex>) -> Rc<GenRegex> {
231231
let c1 = GenRegex::make_union(gre1.clone(), GenRegex::complement(&gre2.clone()));
232232
let c2 = GenRegex::make_union(gre2.clone(), GenRegex::complement(&gre1.clone()));
233-
return GenRegex::make_intersection(c1.clone(), c2.clone());
233+
GenRegex::make_intersection(c1.clone(), c2.clone())
234234
}
235235

236236
/*

0 commit comments

Comments
 (0)