satellite_format/
advanced_cnf.rs

1//! Advanced-CNF JSON format.
2//!
3//! The native format for Satellite, supporting typed variables and ABI constraints.
4
5use satellite_base::types::VarType;
6use serde::{Deserialize, Serialize};
7
8/// A variable definition in Advanced-CNF.
9#[derive(Debug, Clone, Serialize, Deserialize)]
10pub struct VariableDef {
11    /// Unique variable ID.
12    pub id: u64,
13    /// Variable type.
14    #[serde(rename = "type")]
15    pub var_type: VarType,
16    /// Optional human-readable name.
17    #[serde(skip_serializing_if = "Option::is_none")]
18    pub name: Option<String>,
19}
20
21/// A clause in Advanced-CNF.
22#[derive(Debug, Clone, Serialize, Deserialize)]
23pub struct Clause {
24    /// Literals in DIMACS format (positive = true, negative = negated).
25    pub literals: Vec<i64>,
26    /// Whether this is an original or learned clause.
27    #[serde(rename = "type")]
28    pub clause_type: ClauseType,
29    /// Literal Block Distance for learned clauses.
30    #[serde(skip_serializing_if = "Option::is_none")]
31    pub lbd: Option<u32>,
32}
33
34/// Type of clause.
35#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
36#[serde(rename_all = "lowercase")]
37pub enum ClauseType {
38    Original,
39    Learned,
40}
41
42/// An ABI constraint reference.
43#[derive(Debug, Clone, Serialize, Deserialize)]
44pub struct AbiConstraint {
45    /// Function name.
46    pub name: String,
47    /// Input variable IDs.
48    pub inputs: Vec<u64>,
49    /// SHA256 hash of the compiled code.
50    pub code_hash: String,
51    /// Whether the compiled code is cached.
52    #[serde(default)]
53    pub cached: bool,
54}
55
56/// The Advanced-CNF document.
57#[derive(Debug, Clone, Serialize, Deserialize)]
58pub struct AdvancedCnf {
59    /// Variable definitions.
60    pub variables: Vec<VariableDef>,
61    /// Clauses.
62    pub clauses: Vec<Clause>,
63    /// ABI constraint references.
64    #[serde(default, skip_serializing_if = "Vec::is_empty")]
65    pub abi_constraints: Vec<AbiConstraint>,
66}
67
68impl AdvancedCnf {
69    /// Creates an empty Advanced-CNF document.
70    #[must_use]
71    pub fn new() -> Self {
72        Self {
73            variables: Vec::new(),
74            clauses: Vec::new(),
75            abi_constraints: Vec::new(),
76        }
77    }
78
79    /// Parses from JSON string.
80    pub fn from_json(json: &str) -> Result<Self, serde_json::Error> {
81        serde_json::from_str(json)
82    }
83
84    /// Serializes to JSON string.
85    pub fn to_json(&self) -> Result<String, serde_json::Error> {
86        serde_json::to_string_pretty(self)
87    }
88
89    /// Parses from JSON reader.
90    pub fn from_reader<R: std::io::Read>(reader: R) -> Result<Self, serde_json::Error> {
91        serde_json::from_reader(reader)
92    }
93
94    /// Writes to JSON writer.
95    pub fn to_writer<W: std::io::Write>(&self, writer: W) -> Result<(), serde_json::Error> {
96        serde_json::to_writer_pretty(writer, self)
97    }
98}
99
100impl Default for AdvancedCnf {
101    fn default() -> Self {
102        Self::new()
103    }
104}
satellite_format/advanced_cnf.rs

satellite_format/
advanced_cnf.rs
