Skip to content

Commit 15c9cb6

Browse files
tichingkaotichingkao
committed
Added concrete int and indexof support
1 parent 4b6add3 commit 15c9cb6

3 files changed

Lines changed: 209 additions & 31 deletions

File tree

‎Cargo.lock‎

Lines changed: 19 additions & 13 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎src/smt/parse.rs‎

Lines changed: 184 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -100,8 +100,9 @@ impl Error for SmtParseError {}
100100
enum TokenTypes {
101101
ReTok(RegexToken),
102102
StrTok(StringToken),
103+
IntTok(IntToken),
103104
Assertion(Rc<GenRegex>, Rc<GenRegex>),
104-
Other,
105+
Other(Value),
105106
}
106107

107108
#[derive(Debug)]
@@ -432,6 +433,12 @@ enum StringToken {
432433
},
433434
}
434435

436+
#[derive(Debug)]
437+
enum IntToken {
438+
Var(String),
439+
Val(i64),
440+
}
441+
435442
/*
436443
Top-level S-expression parsing functions
437444
*/
@@ -486,6 +493,7 @@ pub struct SmtParser {
486493
found_check_sat: bool,
487494
str_var_names: HashSet<String>,
488495
// TODO: eventually this should be replaced by StringToken
496+
int_var_names: HashSet<String>,
489497
func_names: HashMap<String, String>,
490498
// And this by RegexToken probably
491499
re_var_names: HashMap<String, Option<Rc<GenRegex>>>,
@@ -500,6 +508,7 @@ impl SmtParser {
500508
found_assert: false,
501509
found_check_sat: false,
502510
str_var_names: HashSet::new(),
511+
int_var_names: HashSet::new(),
503512
func_names: HashMap::new(),
504513
re_var_names: HashMap::new(),
505514
let_vars: HashMap::new(),
@@ -565,7 +574,7 @@ impl SmtParser {
565574
}
566575
}
567576
fn parse_declare_fun(&mut self, v: &Value) -> Result<(), SmtParseError> {
568-
// Syntax: (define-fun [fun name] () String )
577+
// Syntax: (define-fun [fun name] () [Type] )
569578
let args = self.get_args(v)?;
570579
if args.len() != 3 {
571580
return Err(SmtParseError::unrecog(v));
@@ -577,17 +586,16 @@ impl SmtParser {
577586
Value::Cons(_) => return Err(SmtParseError::unsupported(params)),
578587
_ => return Err(SmtParseError::unrecog(params)),
579588
};
589+
println!("declar_fun found {}", ret_type);
580590
match ret_type
581591
.as_symbol()
582592
.ok_or(SmtParseError::unrecog(ret_type))?
583593
{
584-
"String" => (),
594+
"String" => self.str_var_names.insert(name.to_string()),
595+
"Int" => self.int_var_names.insert(name.to_string()),
585596
"RegLan" => return Err(SmtParseError::unsupported(ret_type)),
586597
_ => return Err(SmtParseError::unrecog(ret_type)),
587598
};
588-
589-
//Parses the function definition and inserts into HashMap
590-
self.str_var_names.insert(name.to_string());
591599
Ok(())
592600
}
593601

@@ -600,17 +608,17 @@ impl SmtParser {
600608
let (var_name, tail) = v.as_pair().ok_or(SmtParseError::unrecog(v))?;
601609
let (var_type, tail) = tail.as_pair().ok_or(SmtParseError::unrecog(v))?;
602610
expect_null(tail)?;
611+
println!("declar_const found {}", var_type);
603612
match var_type.as_symbol().ok_or(SmtParseError::unrecog(v))? {
604-
"String" => {
605-
self.str_var_names.insert(var_name.to_string());
606-
Ok(())
607-
}
608-
"RegLan" => {
609-
self.re_var_names.insert(var_name.to_string(), None);
610-
Ok(())
611-
}
612-
_ => Err(SmtParseError::unrecog(v)),
613-
}
613+
"String" => self.str_var_names.insert(var_name.to_string()),
614+
"Int" => self.int_var_names.insert(var_name.to_string()),
615+
"RegLan" => self
616+
.re_var_names
617+
.insert(var_name.to_string(), None)
618+
.is_none(),
619+
_ => return Err(SmtParseError::unrecog(v)),
620+
};
621+
Ok(())
614622
}
615623

616624
fn parse_assert(&mut self, v: &Value) -> Result<(), SmtParseError> {
@@ -1116,6 +1124,11 @@ impl SmtParser {
11161124
//println!("called parse_equals_tok_type: str return");
11171125
return Ok(TokenTypes::StrTok(str_tok));
11181126
}
1127+
let try_int = self.parse_int_expr(arg);
1128+
if let Ok(int_tok) = try_int {
1129+
println!("called parse_equals_tok_type: int return");
1130+
return Ok(TokenTypes::IntTok(int_tok));
1131+
}
11191132
let saved_not_flag = self.not_flag;
11201133
self.not_flag = false;
11211134
let try_assert = self.parse_assert_arg(arg);
@@ -1125,8 +1138,8 @@ impl SmtParser {
11251138
//println!("called parse_equals_tok_type: assertion return");
11261139
return Ok(TokenTypes::Assertion(assert, assert_neg));
11271140
}
1128-
//println!("called parse_equals_tok_type: other return");
1129-
Ok(TokenTypes::Other)
1141+
println!("called parse_equals_tok_type: other return");
1142+
Ok(TokenTypes::Other(arg.clone()))
11301143
}
11311144

11321145
fn parse_equals(&mut self, v: &Value) -> Result<Rc<GenRegex>, SmtParseError> {
@@ -1327,6 +1340,30 @@ impl SmtParser {
13271340
}
13281341
}
13291342
}
1343+
(TokenTypes::IntTok(int_token1), TokenTypes::IntTok(int_token2)) => {
1344+
match (int_token1, int_token2) {
1345+
(IntToken::Var(v1), IntToken::Var(v2)) => {
1346+
let gre1 = GenRegex::create_gre_str_var(&v1);
1347+
let gre2 = GenRegex::create_gre_str_var(&v2);
1348+
return Ok(GenRegex::intersect(&gre1, &gre2));
1349+
}
1350+
(IntToken::Var(v), IntToken::Val(num)) => {
1351+
let gre1 = GenRegex::create_gre_str_var(&v);
1352+
let gre2 = GenRegex::caret(num as u64, &Rc::new(GenRegex::Sigma));
1353+
return Ok(GenRegex::intersect(&gre1, &gre2));
1354+
}
1355+
(IntToken::Val(num), IntToken::Var(v)) => {
1356+
let gre1 = GenRegex::create_gre_str_var(&v);
1357+
let gre2 = GenRegex::caret(num as u64, &Rc::new(GenRegex::Sigma));
1358+
return Ok(GenRegex::intersect(&gre1, &gre2));
1359+
}
1360+
(IntToken::Val(num1), IntToken::Val(num2)) => {
1361+
let gre1 = GenRegex::caret(num1 as u64, &Rc::new(GenRegex::Sigma));
1362+
let gre2 = GenRegex::caret(num2 as u64, &Rc::new(GenRegex::Sigma));
1363+
return Ok(GenRegex::intersect(&gre1, &gre2));
1364+
}
1365+
}
1366+
}
13301367
(
13311368
TokenTypes::Assertion(assert1, assert1_neg),
13321369
TokenTypes::Assertion(assert2, assert2_neg),
@@ -1343,6 +1380,18 @@ impl SmtParser {
13431380
))
13441381
}
13451382
}
1383+
(TokenTypes::IntTok(int_token), TokenTypes::Other(val))
1384+
| (TokenTypes::Other(val), TokenTypes::IntTok(int_token)) => {
1385+
let IntToken::Val(num) = int_token else {
1386+
return Err(SmtParseError::unsupported_note("Ints must be concrete."));
1387+
};
1388+
let (head, tail) = val.as_pair().ok_or(SmtParseError::unrecog(&val))?;
1389+
let cmd = head.as_symbol().ok_or(SmtParseError::unrecog(head))?;
1390+
match cmd {
1391+
"str.indexof" => self.parse_indexof(tail, num as u64),
1392+
_ => Err(SmtParseError::unrecog(head)),
1393+
}
1394+
}
13461395
// TODO: remove exhaustive fallback pattern
13471396
_ => {
13481397
if arg1.is_number() && self.is_length_operation(arg2) {
@@ -2008,6 +2057,16 @@ impl SmtParser {
20082057
}
20092058
}
20102059

2060+
fn strtok_to_re(s: &StringToken) -> Result<Rc<GenRegex>, SmtParseError> {
2061+
let retok = Self::strtok_to_retok(s)?;
2062+
match retok {
2063+
RegexToken::Val(gen_regex) => Ok(gen_regex),
2064+
RegexToken::Conditional { .. } => todo!(),
2065+
//StringToken should never result to a Regex variables
2066+
RegexToken::Var(_) => unreachable!(),
2067+
}
2068+
}
2069+
20112070
fn parse_str_to_re(&mut self, v: &Value) -> Result<RegexToken, SmtParseError> {
20122071
// (str.to_re "String")
20132072
let (str, tail) = v.as_pair().ok_or(SmtParseError::unrecog(v))?;
@@ -2286,6 +2345,113 @@ impl SmtParser {
22862345
}
22872346
}
22882347

2348+
/*
2349+
Parsing functions with output Int
2350+
*/
2351+
2352+
fn parse_int_expr(&mut self, v: &Value) -> Result<IntToken, SmtParseError> {
2353+
if let Some(num) = v.as_i64() {
2354+
return Ok(IntToken::Val(num));
2355+
}
2356+
if let Some(name) = v.as_symbol() {
2357+
if self.int_var_names.contains(name) {
2358+
return Ok(IntToken::Var(name.to_string()));
2359+
} else {
2360+
Err(SmtParseError::BadLiteral(format!(
2361+
"{} is not found in declared variables, defined functions or let variables.",
2362+
name
2363+
)))
2364+
}
2365+
} else {
2366+
Err(SmtParseError::unrecog(v))
2367+
}
2368+
}
2369+
2370+
fn parse_indexof(
2371+
&mut self,
2372+
args: &Value,
2373+
found_index: u64,
2374+
) -> Result<Rc<GenRegex>, SmtParseError> {
2375+
println!("We made it to indexof!!!");
2376+
let arg_vec = self.get_args(args)?;
2377+
if arg_vec.len() != 3 {
2378+
return Err(SmtParseError::unexpected(args, "3 arguments for indexof"));
2379+
}
2380+
let str1 = Self::strtok_to_re(&self.parse_string_expr(arg_vec[0])?)?;
2381+
let str2 = Self::strtok_to_re(&self.parse_string_expr(arg_vec[1])?)?;
2382+
let IntToken::Val(offset) = self.parse_int_expr(arg_vec[2])? else {
2383+
return Err(SmtParseError::unsupported(arg_vec[2]));
2384+
};
2385+
println!("{},{},{}", str1, str2, offset);
2386+
let offset_re = GenRegex::caret(offset as u64, &Rc::new(GenRegex::Sigma));
2387+
let found_index_re = GenRegex::caret(found_index, &Rc::new(GenRegex::Sigma));
2388+
let concat_list = [
2389+
offset_re.clone(),
2390+
found_index_re.clone(),
2391+
str2.clone(),
2392+
GenRegex::sigma_star(),
2393+
];
2394+
let true_constraint = if self.not_flag {
2395+
GenRegex::complement(&GenRegex::concat_many(&concat_list))
2396+
} else {
2397+
GenRegex::concat_many(&concat_list)
2398+
};
2399+
println!("{}", true_constraint);
2400+
let concat_list = [offset_re.clone(), str2.clone(), GenRegex::sigma_star()];
2401+
let mut false_constraint = if self.not_flag {
2402+
GenRegex::concat_many(&concat_list)
2403+
} else {
2404+
GenRegex::complement(&GenRegex::concat_many(&concat_list))
2405+
};
2406+
println!("{}", false_constraint);
2407+
for i in 1..found_index {
2408+
let found_index_re = GenRegex::caret(i, &Rc::new(GenRegex::Sigma));
2409+
let concat_list = [
2410+
offset_re.clone(),
2411+
found_index_re.clone(),
2412+
str2.clone(),
2413+
GenRegex::sigma_star(),
2414+
];
2415+
if self.not_flag {
2416+
false_constraint =
2417+
GenRegex::intersect(&false_constraint, &GenRegex::concat_many(&concat_list));
2418+
} else {
2419+
false_constraint = GenRegex::intersect(
2420+
&false_constraint,
2421+
&GenRegex::complement(&GenRegex::concat_many(&concat_list)),
2422+
);
2423+
}
2424+
}
2425+
println!("{}", false_constraint);
2426+
let final_constraint = GenRegex::intersect(&true_constraint, &false_constraint);
2427+
println!("{}", final_constraint);
2428+
return Ok(GenRegex::intersect(&str1, &final_constraint));
2429+
}
2430+
2431+
/*
2432+
fn parse_indexof(&mut self, args: &Value) -> Result<IntToken,SmtParseError> {
2433+
let arg_vec=self.get_args(args)?;
2434+
if arg_vec.len()!=3{
2435+
return Err(SmtParseError::unrecog(args));
2436+
}
2437+
let (str1, str2, num)=(arg_vec[0],arg_vec[1],arg_vec[2]);
2438+
let str1=Self::strtok_to_re(&self.parse_string_expr(str1)?)?;
2439+
let str2=Self::strtok_to_re(&self.parse_string_expr(str2)?)?;
2440+
let IntToken::Val(num)=self.parse_int_expr(num)? else{
2441+
return Err(SmtParseError::unsupported(args));
2442+
};
2443+
let offset_re=GenRegex::caret(num as u64-1, &Rc::new(GenRegex::Sigma));
2444+
let make_indexof = move |num:i64| -> Rc<GenRegex>{
2445+
let found_index=num as u64;
2446+
let found_index_re=GenRegex::caret(num as u64, &Rc::new(GenRegex::Sigma));
2447+
let concat_list=[offset_re,found_index_re,str2,GenRegex::sigma_star()];
2448+
let true_constraint=GenRegex::concat_many(&concat_list);
2449+
true_constraint
2450+
};
2451+
return make_indexof;
2452+
}
2453+
*/
2454+
22892455
/*
22902456
Helper Functions
22912457
*/

‎src/types/regex.rs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -227,6 +227,12 @@ impl GenRegex {
227227
}
228228
}
229229

230+
pub fn make_equals(gre1: Rc<GenRegex>, gre2: Rc<GenRegex>) -> Rc<GenRegex> {
231+
let c1 = GenRegex::make_union(gre1.clone(), GenRegex::complement(&gre2.clone()));
232+
let c2 = GenRegex::make_union(gre2.clone(), GenRegex::complement(&gre1.clone()));
233+
return GenRegex::make_intersection(c1.clone(), c2.clone());
234+
}
235+
230236
/*
231237
Helper for regex length
232238
*/

0 commit comments

Comments
 (0)