synthphonia/
main.rs

1#![allow(unused_imports)] 
2#![allow(unused_mut)] 
3#![feature(int_roundings)]
4#![feature(thread_local)]
5#![feature(map_try_insert)]
6#![feature(hash_raw_entry)]
7#![feature(cell_update)]
8#![feature(trait_alias)]
9
10/// Global allocation 
11pub mod galloc;
12
13/// Logging
14pub mod log;
15
16/// Utility functions
17pub mod utils;
18
19/// SyGuS-IF parsing
20pub mod parser;
21
22/// Representing Value
23pub mod value;
24
25/// Representing Expression
26pub mod expr;
27
28/// Forward enumerator
29/// 
30/// Provides an `Executor` struct that manages the enumeration process, including the `enumerate` function for generating expressions based on the provided grammar and context.
31pub mod forward;
32
33/// Backward Deducer
34/// 
35/// Provides a `DeducerEnum` enum that represents different deduction strategies, including `Enumeration`, `ACS`, and `TopBlocked`.
36pub mod backward;
37
38/// Decision Tree Learning
39pub mod tree_learning;
40
41/// Acumulative case-splitting solutions.
42pub mod solutions;
43
44/// Handle special text objects.
45pub mod text;
46use std::{borrow::BorrowMut, cell::Cell, cmp::min, fs, os, process::exit};
47
48use clap::Parser;
49use expr::{cfg::Cfg, context::Context, Expr};
50use forward::executor::{Executor, STOP_SIGNAL};
51use futures::{stream::FuturesUnordered, StreamExt};
52use galloc::AllocForAny;
53use itertools::Itertools;
54use mapped_futures::mapped_futures::MappedFutures;
55use parser::check::CheckProblem;
56use solutions::{new_thread, CONDITIONS};
57use tokio::task::JoinHandle;
58use value::ConstValue;
59
60use crate::{backward::Problem, expr::cfg::{NonTerminal, ProdRule}, parser::{check::DefineFun, problem::PBEProblem}, solutions::{cond_search_thread, Solutions}, value::Type};
61#[derive(Debug, Parser)]
62#[command(name = "synthphonia")]
63/// A command-line interface configuration providing options for controlling a string synthesis process. 
64/// 
65/// The struct fields represent various parameters that users can configure, such as logging verbosity, file paths for grammar configurations, and the thread count for execution. 
66/// It includes options to enable or disable the use of the `ite` operator and deduction mode, which involves Enumeration and ACS. 
67/// Users can also choose to enable a separate all-example thread to optimize processing or extract constants when needed. 
68/// The input file path is required and can be in enriched sygus-if or smt2 format depending on whether synthesis or result-checking is required. 
69/// Additional debugging options are available, allowing for more verbose output, viewing examples, or simply printing the signature of a synthesis problem without solving it.
70/// 
71struct Cli {
72    /// Log level
73    #[arg(short, long, action = clap::ArgAction::Count)]
74    verbose: u8,
75    /// Path to the context-free grammar configuration (enriched sygus-if)
76    #[arg(short, long)]
77    cfg: Option<String>,
78    
79    /// Number of threads
80    #[arg(short='j', long, default_value_t=4)]
81    thread: usize,
82    
83    /// No ITE Mode: Generate results without `ite` operator
84    #[arg(long)]
85    no_ite: bool,
86    
87    /// Set the rate limit of ITE (in milliseconds), i.e., how much time (without new solutions) does it take for the `ite_limit` to increment by one.
88    #[arg(long, default_value_t=4000)]
89    ite_limit_rate: usize,
90    
91    /// Disable deduction, i.e., Enumeration + ACS.
92    #[arg(long, default_value_t=false)]
93    no_deduction: bool,
94    
95    /// Enable all-example thread (Using one thread for all-example thread)
96    #[arg(long)]
97    with_all_example_thread: bool,
98
99    /// Enable constant extraction.
100    #[arg(long)]
101    extract_constants: bool,
102    
103    /// Path to the input file: enriched sygus-if (.sl) for synthesis or smt2 (.smt2) to check the result.
104    path: String,
105    
106    /// Debug Mode (More assertions)
107    #[arg(short, long)]
108    debug: bool,
109        
110    /// Show examples (debugging)
111    #[arg(long)]
112    showex: bool,
113
114    /// Show Signature (Just Print the signature without solving)
115    #[arg(long)]
116    sig: bool
117}
118
119#[thread_local]
120/// No longer used
121pub static DEBUG: Cell<bool> = Cell::new(false);
122
123/// no longer used
124pub static COUNTER: spin::Mutex<[usize; 6]> = spin::Mutex::new([0usize; 6]);
125
126#[tokio::main(flavor = "multi_thread")]
127/// Executes the main asynchronous function for processing string synthesis problems using a command-line interface. 
128/// 
129/// First, it parses command-line arguments to configure logging levels and debug settings. 
130/// If the `--sig` flag is specified, it reads and parses a synthesis problem from the input file and prints the function signature. 
131/// If the input file ends with `.smt2`, it handles an expression checking problem by parsing it, evaluating its expression in the context of provided examples, and comparing the result with expected outputs, printing the correctness count.
132/// 
133/// For other input files, it reads and parses a programming-by-example problem, creating a context-free grammar configuration from the synthesized function. 
134/// Optional configurations are applied through an external file, and context enrichment is based on example detection. 
135/// If constant extraction is enabled, constants from examples are added to grammar rules. 
136/// The configuration is logged, and examples are optionally shown. 
137/// The function adjusts for deduction settings and either solves the synthesis problem using top-blocked search without `ite` or sets up multi-threaded search loops to find solutions, outputting the derived function. 
138/// Finally, it ensures threads complete gracefully before exiting. 
139/// 
140async fn main() -> Result<(), Box<dyn std::error::Error>>{
141    let args = Cli::parse();
142    log::set_log_level(args.verbose + 2);
143    DEBUG.set(args.debug);
144    if args.sig {
145        let s = fs::read_to_string(args.path).unwrap();
146        let problem = PBEProblem::parse(s.as_str()).unwrap();
147        
148        println!("{}", problem.synthfun().sig)
149    } else if args.path.ends_with(".smt2") {
150        let s = fs::read_to_string(args.path).unwrap();
151        let problem = CheckProblem::parse(s.as_str()).unwrap();
152        let ctx = Context::from_examples(&problem.examples);
153        info!("Expression: {:?}", problem.definefun.expr);
154        info!("Examples: {:?}", problem.examples);
155        let result = problem.definefun.expr.eval(&ctx);
156        info!("Result: {:?}", result);
157        println!("{}", result.eq_count(&problem.examples.output));
158    } else {
159        let s = fs::read_to_string(args.path).unwrap();
160        let problem = PBEProblem::parse(s.as_str()).unwrap();
161        let mut cfg = Cfg::from_synthfun(problem.synthfun());
162        if let Some(s) = args.cfg {
163            let sygus_if = fs::read_to_string(s).unwrap();
164            cfg = enrich_configuration(sygus_if.as_str(), cfg);
165        } else {
166            let ctx = Context::from_examples(&problem.examples);
167            if text::parsing::detector(&ctx) {
168                let sygus_if = include_str!("../test/test.sl");
169                cfg = enrich_configuration(sygus_if, cfg);
170            } else {
171                let sygus_if = include_str!("../test/test2map.sl");
172                cfg = enrich_configuration(sygus_if, cfg);
173            }
174        }
175
176        if args.extract_constants {
177            let constants = problem.examples.extract_constants();
178            for nt in cfg.iter_mut() {
179                if nt.ty == Type::Str {
180                    for c in constants.iter() {
181                        nt.rules.push(ProdRule::Const(ConstValue::Str(c)));
182                    }
183                }
184            }
185        }
186
187        info!("CFG: {:?}", cfg);
188        let ctx = Context::from_examples(&problem.examples);
189        debg!("Examples: {:?}", ctx.output);
190        if args.showex {
191            for i in ctx.inputs() {
192                println!("{:?}", i);
193            }
194            println!("{:?}", ctx.output);
195            return Ok(());
196        }
197        cfg.config.no_deduction = args.no_deduction;
198        cfg.config.ite_limit_rate = args.ite_limit_rate;
199        if args.no_ite {
200            if args.no_ite {
201                cfg.config.cond_search = true;
202            }
203            let exec = Executor::new(ctx, cfg);
204            info!("Deduction Configuration: {:?}", exec.deducers);
205            let result = exec.solve_top_blocked();
206            let func = DefineFun { sig: problem.synthfun().sig.clone(), expr: result};
207            println!("{}", func);
208        } else {
209            let mut solutions = Solutions::new(cfg.clone(), ctx.clone());
210
211            // solutions.create_cond_search_thread();
212            let mut nthread = min(args.thread, ctx.len);
213            if nthread > 1  && args.with_all_example_thread {
214                solutions.create_all_search_thread();
215                nthread -= 1;
216            }
217            for _ in 0..nthread {
218                solutions.create_new_thread();
219            }
220
221            let result = solutions.solve_loop().await;
222            let func = DefineFun { sig: problem.synthfun().sig.clone(), expr: result};
223            // let nsols = solutions.count();
224            // let ncons = CONDITIONS.lock().as_ref().unwrap().len();
225            // eprintln!("nsols: {nsols}, ncons: {ncons}");
226            STOP_SIGNAL.store(true, std::sync::atomic::Ordering::Relaxed);
227            
228            println!("{}", func);
229
230            if !solutions.threads.is_empty() {
231                std::thread::sleep(std::time::Duration::from_millis(50));
232            }
233            exit(0);
234        }
235    }
236    Ok(())
237}
238
239/// Enhances the given configuration by integrating it with a parsed problem derived from the provided SyGuS-IF string. 
240fn enrich_configuration(sygus_if: &str, mut cfg: Cfg) -> Cfg {
241    let problem = PBEProblem::parse(sygus_if).unwrap();
242    let mut synthfun = problem.synthfun().clone();
243    synthfun.cfg.start = synthfun.cfg.get_nt_by_type(&cfg[0].ty);
244    synthfun.cfg.reset_start();
245    let mut cfg1 = Cfg::from_synthfun(&synthfun);
246    for nt in cfg1.iter_mut() {
247        nt.rules.retain(|x| !matches!(x, ProdRule::Var(_)));
248    }
249    for (nt1, nt) in cfg1.iter_mut().zip(cfg.iter()) {
250        for r in nt.rules.iter() {
251            if let ProdRule::Const(_) | ProdRule::Var(_) = r {
252                nt1.rules.push(r.clone());
253            }
254        }
255    }
256    cfg1
257}
258
synthphonia/main.rs

synthphonia/
main.rs
