satellite_format/
canonical.rs

1use serde::{Deserialize, Serialize};
2
3/// The Canonical JSON format for Satellite (.jsonc).
4#[derive(Debug, Clone, Serialize, Deserialize)]
5pub struct CanonicalCnf {
6    pub version: String,
7    pub vars: Vec<VarDef>,
8    #[serde(default)]
9    pub imports: Vec<ImportDef>,
10    #[serde(default)]
11    pub functions: Vec<FunctionDef>,
12    pub clauses: Vec<ClauseDef>,
13    pub metadata: Metadata,
14}
15
16#[derive(Debug, Clone, Serialize, Deserialize)]
17pub struct VarDef {
18    pub name: String,
19    #[serde(rename = "type")]
20    pub var_type: String, // "bool", "batch", "vec"
21    #[serde(skip_serializing_if = "Option::is_none")]
22    pub dim1: Option<usize>,
23    #[serde(skip_serializing_if = "Option::is_none")]
24    pub dim2: Option<usize>,
25}
26
27#[derive(Debug, Clone, Serialize, Deserialize)]
28pub struct ImportDef {
29    pub path: String,
30    pub hash: String,
31    pub content: String,
32}
33
34#[derive(Debug, Clone, Serialize, Deserialize)]
35pub struct FunctionDef {
36    pub name: String,
37    pub signature: String,
38    #[serde(default)]
39    pub auto_generated: bool,
40}
41
42#[derive(Debug, Clone, Serialize, Deserialize)]
43pub struct ClauseDef {
44    pub expr: String,
45    pub id: u64,
46}
47
48#[derive(Debug, Clone, Serialize, Deserialize)]
49pub struct Metadata {
50    pub style: String,
51    pub source_hash: String,
52}
53
54impl CanonicalCnf {
55    pub fn from_reader<R: std::io::Read>(reader: R) -> serde_json::Result<Self> {
56        serde_json::from_reader(reader)
57    }
58
59    pub fn to_writer<W: std::io::Write>(&self, writer: W) -> serde_json::Result<()> {
60        serde_json::to_writer_pretty(writer, self)
61    }
62}
63
64use crate::advanced_cnf::{AdvancedCnf, VariableDef, Clause, ClauseType, AbiConstraint};
65use crate::parser::{Parser, Expr};
66use satellite_base::types::VarType;
67use std::collections::HashMap;
68
69impl TryFrom<CanonicalCnf> for AdvancedCnf {
70    type Error = String;
71
72    fn try_from(canonical: CanonicalCnf) -> Result<Self, Self::Error> {
73        let mut acnf = AdvancedCnf::new();
74        let mut name_to_id = HashMap::new();
75        let mut next_id = 1;
76
77        // 1. Process variables
78        for var in canonical.vars {
79            let id = next_id;
80            name_to_id.insert(var.name.clone(), id);
81            
82            let vtype = match var.var_type.as_str() {
83                "bool" => VarType::Bool,
84                "batch" => VarType::Batch { 
85                    dim: var.dim1.ok_or("Batch missing dim1")? 
86                },
87                "vec" => VarType::Vec {
88                    inner_dim: var.dim1.ok_or("Vec missing dim1")?,
89                    outer_dim: var.dim2.ok_or("Vec missing dim2")?,
90                },
91                _ => return Err(format!("Unknown var type: {}", var.var_type)),
92            };
93
94            acnf.variables.push(VariableDef {
95                id,
96                var_type: vtype.clone(),
97                name: Some(var.name),
98            });
99            
100            next_id += vtype.bool_count() as u64;
101        }
102
103        // 2. Process clauses (expressions)
104        for clause_def in canonical.clauses {
105            let mut parser = Parser::new(&clause_def.expr);
106            let expr = parser.parse().map_err(|e| format!("Parse error in clause {}: {}", clause_def.id, e))?;
107            
108            // Lower expression to CNF clauses or AbiConstraint
109            lower_expr(expr, &name_to_id, &mut acnf)?;
110        }
111
112        Ok(acnf)
113    }
114}
115
116fn lower_expr(expr: Expr, map: &HashMap<String, u64>, acnf: &mut AdvancedCnf) -> Result<(), String> {
117    match expr {
118        Expr::BinaryOp { op, left, right } => {
119            if op == "AND" || op == "and" || op == "&&" {
120                // Conjunction: Split
121                lower_expr(*left, map, acnf)?;
122                lower_expr(*right, map, acnf)?;
123            } else if op == "OR" || op == "or" || op == "||" {
124                // Disjunction: Create clause (simplistic CNF only support for now)
125                // We assume strict CNF structure for standard clauses: OR of Literals
126                // Handling (A AND B) OR C requires distribution which we skip for MVP
127                let mut literals = Vec::new();
128                collect_disjunction(*left, map, &mut literals)?;
129                collect_disjunction(*right, map, &mut literals)?;
130                acnf.clauses.push(Clause {
131                    literals,
132                    clause_type: ClauseType::Original,
133                    lbd: None
134                });
135            } else if op == "eq" {
136                 // Arithmetic/Constraint
137                 // Treat as ABI constraint
138                 // Collect variables used
139                 let inputs = collect_vars_deep(&Expr::BinaryOp{op: op.clone(), left: left.clone(), right: right.clone()}, map);
140                 acnf.abi_constraints.push(AbiConstraint {
141                     name: "eq".to_string(), // Or generate a specific name based on expression
142                     inputs,
143                     code_hash: "interactive_eq".to_string(), // Placeholder
144                     cached: false,
145                 });
146            } else {
147                 return Err(format!("Unsupported binary op at top level: {}", op));
148            }
149        },
150        Expr::UnaryOp { .. } | Expr::Var(_) | Expr::Lit(_) => {
151             // Single literal clause
152             let mut literals = Vec::new();
153             collect_disjunction(expr, map, &mut literals)?;
154             acnf.clauses.push(Clause {
155                literals,
156                clause_type: ClauseType::Original,
157                lbd: None
158             });
159        }
160        _ => return Err("Unsupported top level expression".to_string())
161    }
162    Ok(())
163}
164
165fn collect_disjunction(expr: Expr, map: &HashMap<String, u64>, literals: &mut Vec<i64>) -> Result<(), String> {
166    match expr {
167        Expr::BinaryOp { op, left, right } => {
168            if op == "OR" || op == "or" || op == "||" {
169                collect_disjunction(*left, map, literals)?;
170                collect_disjunction(*right, map, literals)?;
171            } else {
172                return Err("Nested non-OR in disjunction not supported in MVP".to_string()); // Correct distribution needed here for full support
173            }
174        },
175        Expr::Var(name) => {
176            if let Some(&id) = map.get(&name) {
177                // Remove % prefix if present in name? Parser handles % in parse_var, returning var name with %.
178                // Wait, parser: Token::Var includes %.
179                // Map keys include %.
180                 literals.push(id as i64);
181            } else {
182                 // Try removing %
183                 if let Some(&id) = map.get(name.trim_start_matches('%')) {
184                     literals.push(id as i64);
185                 } else {
186                     return Err(format!("Unknown variable: {}", name));
187                 }
188            }
189        },
190        Expr::UnaryOp { op, expr } => {
191            if op == "NOT" || op == "not" || op == "!" || op == "-" {
192                 if let Expr::Var(name) = *expr {
193                     let id = if let Some(&id) = map.get(&name) { id }
194                     else if let Some(&id) = map.get(name.trim_start_matches('%')) { id }
195                     else { return Err(format!("Unknown variable: {}", name)); };
196                     literals.push(-(id as i64));
197                 } else {
198                     return Err("Only direct negation of vars supported in MVP".to_string());
199                 }
200            } else {
201                return Err(format!("Unknown unary op: {}", op));
202            }
203        }
204        _ => return Err("Unsupported element in disjunction".to_string())
205    }
206    Ok(())
207}
208
209fn collect_vars_deep(expr: &Expr, map: &HashMap<String, u64>) -> Vec<u64> {
210     let mut vars = Vec::new();
211     match expr {
212         Expr::Var(name) => {
213             if let Some(&id) = map.get(name) { vars.push(id); }
214             else if let Some(&id) = map.get(name.trim_start_matches('%')) { vars.push(id); }
215         },
216         Expr::BinaryOp { left, right, .. } => {
217             vars.extend(collect_vars_deep(left, map));
218             vars.extend(collect_vars_deep(right, map));
219         },
220         Expr::UnaryOp { expr, .. } => {
221             vars.extend(collect_vars_deep(expr, map));
222         },
223         Expr::Call { args, .. } => {
224             for arg in args {
225                 vars.extend(collect_vars_deep(arg, map));
226             }
227         }
228         _ => {}
229     }
230     vars
231}
satellite_format/canonical.rs

satellite_format/
canonical.rs
