synthphonia/parser/
check.rs

1
2
3use itertools::Itertools;
4use pest::{iterators::Pair, Parser};
5use regex::Regex;
6
7use crate::{expr::{ops::{Op1Enum, Op2Enum, Op3Enum}, Expr}, galloc::AllocForAny, utils::TryRetain, value::{ConstValue, Type}};
8use derive_more::Display;
9
10use super::{config::Config, ioexamples::IOExamples, problem::{new_custom_error_span, Error, FunSig, ProblemParser, Rule}};
11
12
13impl Expr {
14    /// Parses an expression from a parsed `Pair` using an optional function signature and returns a static lifetime reference to an `Expr`, or an error. 
15    pub fn parse(pair: Pair<'_, Rule>, sig: Option<&FunSig>) -> Result<&'static Expr, Error> {
16        let mut vec = pair.into_inner().collect_vec();
17        let mut config = Config::new();
18        vec.try_retain(|x| {
19            if x.as_rule() == Rule::config {
20                config.merge(Config::parse(x.clone())?);
21                Ok(false)
22            } else { Ok(true) }
23        })?;
24        if vec.len() == 1 {
25            let [value]: [_; 1] = vec.try_into().unwrap();
26            match value.as_rule() {
27                Rule::value => Ok(Self::Const(ConstValue::parse(value)?).galloc()),
28                Rule::symbol => {
29                    let regex1 = Regex::new(r"^<[0-9]>$".to_string().as_str()).unwrap();
30                    if let Some(v) = sig.and_then(|x| x.index(value.as_str())) {
31                        Ok(Self::Var(v as _).galloc())
32                    } else if regex1.is_match(value.as_str()) {
33                        Ok(Self::Var(value.as_str()[1..2].parse::<_>().unwrap()).galloc())
34                    } else {
35                        return Err(new_custom_error_span("Not an input variable".into(), value.as_span()));
36                    }
37                }
38                _ => panic!("should not reach here"),
39            }
40        } else {
41            match vec.as_slice() {
42                [op, a1] => {
43                    let op = Op1Enum::from_name(op.as_str(), &config);
44                    Ok(Self::Op1(op.galloc(), Expr::parse(a1.clone(), sig)?).galloc())
45                }
46                [op, a1, a2] => {
47                    let op = Op2Enum::from_name(op.as_str(), &config);
48                    Ok(Self::Op2(op.galloc(), Expr::parse(a1.clone(), sig)?, Expr::parse(a2.clone(), sig)?).galloc())
49                }
50                [op, a1, a2, a3] => {
51                    let op = Op3Enum::from_name(op.as_str(), &config);
52                    Ok(Self::Op3(op.galloc(), Expr::parse(a1.clone(), sig)?, Expr::parse(a2.clone(), sig)?, Expr::parse(a3.clone(), sig)?).galloc())
53                }
54                _ => panic!("should not reach here"),
55            }
56        }
57    }
58}
59
60#[derive(Debug, Display, Clone)]
61#[display(fmt = "(define-fun {} {})", "sig", "expr.format(&sig)")]
62/// A struct that encapsulates the definition of a function in the synthesis problem. 
63/// 
64/// It contains two fields: `sig`, which holds the function's signature defined by the `FunSig` type, describing the function's name, return type, and its parameters; and `expr`, a reference to a static expression represented by the `Expr` type, which defines the body or implementation of the function. 
65/// This structure forms a crucial part of representing function definitions within the synthesis process, linking the declared signature with its corresponding executable expression.
66/// 
67pub struct DefineFun {
68    pub sig: FunSig,
69    pub expr: &'static Expr,
70}
71
72impl DefineFun {
73    /// Parses a `DefineFun` instance from a sequence of parsed pairs. 
74    pub fn parse<'i>(pairs: Pair<'_, Rule>) -> Result<DefineFun, Error> {
75        let [name, arglist, typ, expr]: [_; 4] = pairs.into_inner().collect_vec().try_into().unwrap();
76        let args: Vec<(String, Type)> = arglist
77            .into_inner()
78            .map(|x| {
79                let [name, typ]: [_; 2] = x.into_inner().collect_vec().try_into().unwrap();
80                Ok((name.as_str().to_owned(), Type::parse(typ)?))
81            })
82            .try_collect()?;
83        let rettype = Type::parse(typ)?;
84        let sig = FunSig{name: name.as_str().into(), args, rettype};
85        
86        let expr = Expr::parse(expr, Some(&sig))?;
87        Ok(Self{sig, expr})
88    }
89}
90
91#[derive(Debug, Clone)]
92/// A struct representing a problem to be checked for synthesis validity. 
93/// 
94/// This structure comprises essential components required for verifying the correctness of a synthesis problem in the string synthesis module. 
95/// 
96/// 
97/// It includes a logical representation of the synthesis context as a `String`, which outlines the constraints and specifications relevant to the synthesis task. 
98/// Furthermore, it contains a `DefineFun` element, which likely encapsulates the definition of the function(s) or grammar that need to be synthesized. 
99/// Additionally, it has an `IOExamples` member, supplying input/output examples that serve as benchmarks or validation points to corroborate the synthesized solutions against given expectations or specifications. 
100/// This combination ensures comprehensive representation and validation capacity for synthesis problems.
101pub struct CheckProblem {
102    pub logic: String,
103    pub definefun: DefineFun,
104    pub examples: IOExamples,
105}
106
107impl CheckProblem {
108    /// Parses the input string to create a `CheckProblem` instance. 
109    pub fn parse(input: &str) -> Result<CheckProblem, Error> {
110        let [file]: [_; 1] = ProblemParser::parse(Rule::smtfile, input)?.collect_vec().try_into().unwrap();
111        let [_, logic, definefun, examples, checksat]: [_; 5] = file.into_inner().collect_vec().try_into().unwrap();
112        let [logic]: [_; 1] = logic.into_inner().collect_vec().try_into().unwrap();
113        let definefun = DefineFun::parse(definefun)?;
114        let examples = IOExamples::parse(examples, &definefun.sig, false)?;
115
116        Ok(CheckProblem {
117            logic: logic.as_str().to_owned(),
118            definefun,
119            examples,
120        })
121    }
122}
123
124#[cfg(test)]
125mod tests {
126    use std::fs;
127    use super::CheckProblem;
128
129    #[test]
130    fn test() {
131        let s = fs::read_to_string("test/a.smt2").unwrap();
132        let a = CheckProblem::parse(s.as_str()).unwrap();
133        println!("{:?}", a);
134    }
135}
synthphonia/parser/check.rs

synthphonia/parser/
check.rs
