diff --git a/Cargo.lock b/Cargo.lock index 3603d8c..6a1a29f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,6 +2,12 @@ # It is not intended for manual editing. version = 3 +[[package]] +name = "adler" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe" + [[package]] name = "adler32" version = "1.2.0" @@ -277,12 +283,36 @@ dependencies = [ "pkg-config", ] +[[package]] +name = "filetime" +version = "0.2.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "975ccf83d8d9d0d84682850a38c8169027be83368805971cc4f238c2b245bc98" +dependencies = [ + "cfg-if 1.0.0", + "libc", + "redox_syscall", + "winapi", +] + [[package]] name = "fixedbitset" version = "0.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "37ab347416e802de484e4d03c7316c48f1ecb56574dfd4a46a80f173ce1de04d" +[[package]] +name = "flate2" +version = "1.0.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e6988e897c1c9c485f43b47a529cef42fde0547f9d8d41a7062518f1d8fc53f" +dependencies = [ + "cfg-if 1.0.0", + "crc32fast", + "libc", + "miniz_oxide 0.4.4", +] + [[package]] name = "float-ord" version = "0.2.0" @@ -482,9 +512,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.82" +version = "0.2.111" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "89203f3fba0a3795506acaad8ebce3c80c0af93f994d5a1d7a0b1eeb23271929" +checksum = "8e167738f1866a7ec625567bae89ca0d44477232a4f7c52b1c7f2adc2c98804f" [[package]] name = "log" @@ -510,6 +540,16 @@ dependencies = [ "adler32", ] +[[package]] +name = "miniz_oxide" +version = "0.4.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a92518e98c078586bc6c934028adcca4c92a53d6a958196de835170a01d84e4b" +dependencies = [ + "adler", + "autocfg", +] + [[package]] name = "multiset" version = "0.0.5" @@ -738,7 +778,7 @@ dependencies = [ "bitflags", "crc32fast", "deflate 0.8.6", - "miniz_oxide", + "miniz_oxide 0.3.7", ] [[package]] @@ -892,9 +932,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.2.8" +version = "0.2.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "742739e41cd49414de871ea5e549afb7e2a3ac77b589bcbebe8c82fab37147fc" +checksum = "8383f39639269cde97d255a32bdb68c047337295414940c68bdd30c2e13203ff" dependencies = [ "bitflags", ] @@ -909,6 +949,15 @@ dependencies = [ "redox_syscall", ] +[[package]] +name = "remove_dir_all" +version = "0.5.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3acd125665422973a33ac9d3dd2df85edad0f4ae9b00dafb1a05e43a9f5ef8e7" +dependencies = [ + "winapi", +] + [[package]] name = "rustc_version" version = "0.2.3" @@ -1004,6 +1053,43 @@ dependencies = [ "pkg-config", ] +[[package]] +name = "signal-hook" +version = "0.3.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c35dfd12afb7828318348b8c408383cf5071a086c1d4ab1c0f9840ec92dbb922" +dependencies = [ + "libc", + "signal-hook-registry", +] + +[[package]] +name = "signal-hook-registry" +version = "1.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e51e73328dc4ac0c7ccbda3a494dfa03df1de2f46018127f60c693f2648455b0" +dependencies = [ + "libc", +] + +[[package]] +name = "smt2model" +version = "0.1.0" +dependencies = [ + "anyhow", + "flate2", + "libc", + "once_cell", + "petgraph", + "rand 0.8.3", + "signal-hook", + "smt2parser 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)", + "structopt", + "tar", + "tempfile", + "thiserror", +] + [[package]] name = "smt2parser" version = "0.6.1" @@ -1020,13 +1106,31 @@ dependencies = [ "thiserror", ] +[[package]] +name = "smt2parser" +version = "0.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "af4984e7d5d09ac0ac8b64ed7fa6033492699cb11c5ae99be0cd9d02c797c4e8" +dependencies = [ + "fst", + "itertools", + "num", + "permutation_iterator", + "pomelo", + "rand 0.8.3", + "serde", + "structopt", + "strum", + "thiserror", +] + [[package]] name = "smt2patch" version = "0.1.1" dependencies = [ "anyhow", "rand 0.8.3", - "smt2parser", + "smt2parser 0.6.1", "structopt", "thiserror", ] @@ -1036,7 +1140,7 @@ name = "smt2proxy" version = "0.2.4" dependencies = [ "rand 0.8.3", - "smt2parser", + "smt2parser 0.6.1", "structopt", "strum", ] @@ -1112,6 +1216,31 @@ dependencies = [ "unicode-xid", ] +[[package]] +name = "tar" +version = "0.4.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d6f5515d3add52e0bbdcad7b83c388bb36ba7b754dda3b5f5bc2d38640cdba5c" +dependencies = [ + "filetime", + "libc", + "xattr", +] + +[[package]] +name = "tempfile" +version = "3.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dac1c663cfc93810f88aed9b8941d48cabf856a1b111c29a40439018d870eb22" +dependencies = [ + "cfg-if 1.0.0", + "libc", + "rand 0.8.3", + "redox_syscall", + "remove_dir_all", + "winapi", +] + [[package]] name = "textwrap" version = "0.11.0" @@ -1308,6 +1437,15 @@ dependencies = [ "winapi", ] +[[package]] +name = "xattr" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "244c3741f4240ef46274860397c7c74e50eb23624996930e484c16679633a54c" +dependencies = [ + "libc", +] + [[package]] name = "z3tracer" version = "0.11.2" @@ -1317,7 +1455,7 @@ dependencies = [ "once_cell", "petgraph", "plotters", - "smt2parser", + "smt2parser 0.6.1", "structopt", "thiserror", ] diff --git a/Cargo.toml b/Cargo.toml index 5e71314..ab06750 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,6 +4,7 @@ members = [ "smt2proxy", "z3tracer", "smt2patch", + "smt2model", ] [profile.release] diff --git a/README.md b/README.md index 079b9cb..8cc1dd2 100644 --- a/README.md +++ b/README.md @@ -22,6 +22,9 @@ as Z3 and CVC4. * [smt2patch](smt2patch) is an experimental library and tool to modify SMT files. +* [smt2model](smt2model) is an experimental tool to transform SMT2 files into suitable + formats for "language modeling" with machine learning. + The code in this repository is still under active development. ## Contributing diff --git a/smt2model/Cargo.toml b/smt2model/Cargo.toml new file mode 100644 index 0000000..04c6ef4 --- /dev/null +++ b/smt2model/Cargo.toml @@ -0,0 +1,25 @@ +[package] +name = "smt2model" +version = "0.1.0" +repository = "https://github.com/facebookincubator/smt2utils" +authors = ["Mathieu Baudet "] +license = "MIT OR Apache-2.0" +readme = "README.md" +keywords = ["smt2", "ml"] +categories = ["solver", "research"] +edition = "2018" + +[dependencies] +anyhow = "1.0.38" +thiserror = "1.0.25" +once_cell = "1.7.2" +structopt = "0.3.12" +flate2 = "1.0.2" +tar = "0.4.33" +tempfile = "3.2.0" +libc = "0.2.93" +rand = { version = "0.8.3", features = ["small_rng"] } +signal-hook = "0.3.8" +petgraph = "0.5.1" + +smt2parser = { version = "0.6.1", path = "../smt2parser" } diff --git a/smt2model/src/graph.rs b/smt2model/src/graph.rs new file mode 100644 index 0000000..32cf3ee --- /dev/null +++ b/smt2model/src/graph.rs @@ -0,0 +1,971 @@ +// Copyright (c) Facebook, Inc. and its affiliates +// SPDX-License-Identifier: MIT OR Apache-2.0 + +use smt2parser::{ + concrete::{Constant, Symbol}, + visitors, Binary, Decimal, Error, Hexadecimal, Numeral, Position, +}; +use std::collections::{BTreeSet, HashMap}; +use structopt::StructOpt; + +#[derive(Debug, Default, StructOpt, Clone)] +pub struct GraphBuilderConfig { + /// Whether to add space around word tokens. + #[structopt(long)] + add_spaces: bool, + /// Whether to keep the original symbol names in text outputs. + #[structopt(long)] + keep_symbols: bool, + /// Whether to tag local symbol node with their names in graph outputs. + #[structopt(long)] + export_local_names: bool, + /// Whether to normalize datatype declarations. + #[structopt(long)] + normalize_datatype_dec: bool, + /// Whether to reuse generated symbol names (x0, x1, ..) when possible. + #[structopt(long)] + reuse_symbol_indices: bool, +} + +/// State of the graph writer. +#[derive(Debug, Default)] +pub struct GraphBuilder { + config: GraphBuilderConfig, + nodes: Vec, + commands: Vec, + bound_symbols: HashMap>, + // Used to generate fresh names for local symbols. + next_symbol_index: usize, + available_symbol_indices: BTreeSet, + globals: HashMap, + constants: HashMap, + keywords: HashMap, + identifiers: HashMap, NodeRef>, +} + +// This corresponds to syntactic tokens. +#[derive(Debug)] +pub enum Node { + Constant(Constant), + // Local symbols are considered anonymous in graph outputs unless --export-local-names + // is passed. + LocalSymbol(String, usize), + GlobalSymbol(String), + Keyword(String), + Sequence(SeqKind, Vec), +} + +#[derive(Debug, Clone, Copy)] +pub enum SeqKind { + // Anonymous sequences + Script, + AttributeValue, + ConstructorDecSymbol, + ConstructorDec, + DatatypeDec, + DatatypeDecParams, + DatatypeDecConstr, + FunctionDec, + FunctionDecParams, + SExpr, + Sort, + Application, + VarBinding, + VarBindings, + Pattern, + Case, + Cases, + // Primitive + Not, + // Reserved keywords + Underscore, + Exclam, + As, + Let, + Exists, + Forall, + Match, + Par, + Assert, + CheckSat, + CheckSatAssuming, + CheckSatAssumingLiterals, + DeclareConst, + DeclareDatatype, + DeclareDatatypes, + DeclareDatatypesArity, + DeclareDatatypesSorts, + DeclareDatatypesTypes, + DeclareFun, + DeclareFunParams, + DeclareSort, + DefineFun, + DefineFunRec, + DefineFunsRec, + DefineFunsRecSig, + DefineFunsRecSigs, + DefineFunsRecTerms, + DefineSort, + DefineSortParams, + Echo, + Exit, + GetAssertions, + GetAssignment, + GetInfo, + GetModel, + GetOption, + GetProof, + GetUnsatAssumptions, + GetUnsatCore, + GetValue, + GetValueTerms, + Pop, + Push, + Reset, + ResetAssertions, + SetInfo, + SetLogic, + SetOption, +} + +#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Hash, Copy)] +pub struct NodeRef(usize); + +impl GraphBuilder { + pub fn new(config: GraphBuilderConfig) -> Self { + GraphBuilder { + config, + ..Self::default() + } + } + + pub fn write_smt_ast( + &self, + f: &mut W, + node: NodeRef, + ) -> std::io::Result<()> { + use Node::*; + match &self.nodes[node.0] { + Constant(c) => { + write!(f, "{}", c)?; + } + LocalSymbol(name, _) if self.config.keep_symbols => { + write!(f, "{}", Symbol(name.to_string()))?; + } + LocalSymbol(_, n) => { + write!(f, "x{}", n)?; + } + GlobalSymbol(name) => { + write!(f, "{}", Symbol(name.to_string()))?; + } + Keyword(name) => { + write!(f, ":{}", name)?; + } + Sequence(kind, nodes) if self.config.add_spaces => { + write!(f, "( ")?; + if let Some(name) = kind.reserved_name() { + write!(f, "{} ", name)?; + } + for node in nodes { + self.write_smt_ast(f, *node)?; + write!(f, " ")?; + } + write!(f, ")")?; + } + Sequence(kind, nodes) => { + write!(f, "(")?; + let mut nodes = nodes.iter(); + match kind.reserved_name() { + Some(name) => { + write!(f, "{}", name)?; + } + None => { + if let Some(node) = nodes.next() { + self.write_smt_ast(f, *node)?; + } + } + } + for node in nodes { + write!(f, " ")?; + self.write_smt_ast(f, *node)?; + } + write!(f, ")")?; + } + } + Ok(()) + } + + pub fn to_graph(&self) -> petgraph::graph::Graph { + let mut pg_nodes = Vec::new(); + let mut graph = petgraph::graph::Graph::new(); + let mut edge_count = 0; + for node in &self.nodes { + use Node::*; + let label = match node { + Constant(c) => c.to_string(), + LocalSymbol(name, _) if self.config.keep_symbols => { + format!("{}", Symbol(name.to_string())) + } + LocalSymbol(_, n) => format!("x{}", n), + GlobalSymbol(name) => format!("{}", Symbol(name.to_string())), + Keyword(name) => format!(":{}", name), + Sequence(kind, _) => format!("{:?}", kind), + }; + let n = graph.add_node(label); + if let Sequence(_, nodes) = node { + edge_count += nodes.len(); + for (i, node) in nodes.iter().enumerate() { + graph.add_edge(n, pg_nodes[node.0], i); + } + } + pg_nodes.push(n); + } + let n = graph.add_node("SCRIPT".to_string()); + for (i, command) in self.commands.iter().enumerate() { + edge_count += 1; + graph.add_edge(n, pg_nodes[command.0], i); + } + eprintln!( + "Done exporting graph with {} nodes and {} edges", + self.nodes.len() + 1, + edge_count + ); + graph + } +} + +type AttributeValue = visitors::AttributeValue; +type ConstructorDec = visitors::ConstructorDec; +type DatatypeDec = visitors::DatatypeDec; +type FunctionDec = visitors::FunctionDec; + +impl SeqKind { + fn reserved_name(self) -> Option<&'static str> { + use SeqKind::*; + match self { + Underscore => Some("_"), + Exclam => Some("!"), + As => Some("as"), + Let => Some("let"), + Exists => Some("exists"), + Forall => Some("forall"), + Match => Some("match"), + Par => Some("par"), + Assert => Some("assert"), + CheckSat => Some("check-sat"), + CheckSatAssuming => Some("check-sat-assuming"), + DeclareConst => Some("declare-const"), + DeclareDatatype => Some("declare-datatype"), + DeclareDatatypes => Some("declare-datatypes"), + DeclareFun => Some("declare-fun"), + DeclareSort => Some("declare-sort"), + DefineFun => Some("define-fun"), + DefineFunRec => Some("define-fun-rec"), + DefineFunsRec => Some("define-funs-rec"), + DefineSort => Some("define-sort"), + Echo => Some("echo"), + Exit => Some("exit"), + GetAssertions => Some("get-assertions"), + GetAssignment => Some("get-assignment"), + GetInfo => Some("get-info"), + GetModel => Some("get-model"), + GetOption => Some("get-option"), + GetProof => Some("get-proof"), + GetUnsatAssumptions => Some("get-unsat-assumptions"), + GetUnsatCore => Some("get-unsat-core"), + GetValue => Some("get-value"), + Pop => Some("pop"), + Push => Some("push"), + Reset => Some("reset"), + ResetAssertions => Some("reset-assertions"), + SetInfo => Some("set-info"), + SetLogic => Some("set-logic"), + SetOption => Some("set-option"), + _ => None, + } + } +} + +impl GraphBuilder { + fn make_node(&mut self, node: Node) -> NodeRef { + let i = self.nodes.len(); + self.nodes.push(node); + NodeRef(i) + } + + fn make_sequence(&mut self, kind: SeqKind, children: Vec) -> NodeRef { + self.make_node(Node::Sequence(kind, children)) + } + + fn make_constant(&mut self, value: Constant) -> NodeRef { + if let Some(n) = self.constants.get(&value) { + return *n; + } + let n = self.make_node(Node::Constant(value.clone())); + self.constants.insert(value, n); + n + } + + fn make_keyword(&mut self, value: String) -> NodeRef { + if let Some(n) = self.keywords.get(&value) { + return *n; + } + let n = self.make_node(Node::Keyword(value.clone())); + self.keywords.insert(value, n); + n + } + + fn make_local_symbol(&mut self, name: String) -> NodeRef { + if self.config.reuse_symbol_indices { + if let Some(k) = self.available_symbol_indices.iter().next() { + // Reuse symbol index of previously unbinded symbol. + let k = *k; + self.available_symbol_indices.remove(&k); + return self.make_node(Node::LocalSymbol(name, k)); + } + } + let node = Node::LocalSymbol(name, self.next_symbol_index); + self.next_symbol_index += 1; + self.make_node(node) + } + + fn make_global_symbol(&mut self, value: String) -> NodeRef { + if let Some(n) = self.globals.get(&value) { + return *n; + } + let n = self.make_node(Node::GlobalSymbol(value.clone())); + self.globals.insert(value, n); + n + } + + fn make_attribute_value(&mut self, value: AttributeValue) -> Option { + use visitors::AttributeValue::*; + match value { + None => Option::None, + Constant(c) => Some(c), + Symbol(s) => Some(s), + SExpr(exprs) => Some(self.make_sequence(SeqKind::AttributeValue, exprs)), + } + } + + fn make_constructor_dec(&mut self, value: ConstructorDec) -> NodeRef { + let mut children = vec![value.symbol]; + for (symbol, sort) in value.selectors { + children.push(self.make_sequence(SeqKind::ConstructorDecSymbol, vec![symbol, sort])) + } + self.make_sequence(SeqKind::ConstructorDecSymbol, children) + } + + fn make_datatype_dec(&mut self, value: DatatypeDec) -> NodeRef { + let constructors = value + .constructors + .into_iter() + .map(|c| self.make_constructor_dec(c)) + .collect(); + if value.parameters.is_empty() && !self.config.normalize_datatype_dec { + self.make_sequence(SeqKind::DatatypeDec, constructors) + } else { + let children = vec![ + self.make_sequence(SeqKind::DatatypeDecParams, value.parameters), + self.make_sequence(SeqKind::DatatypeDecConstr, constructors), + ]; + self.make_sequence(SeqKind::Par, children) + } + } + + fn make_function_dec(&mut self, value: FunctionDec) -> Vec { + let parameters = value + .parameters + .into_iter() + .map(|(symbol, sort)| { + self.make_sequence(SeqKind::FunctionDecParams, vec![symbol, sort]) + }) + .collect(); + vec![ + value.name, + self.make_sequence(SeqKind::FunctionDec, parameters), + value.result, + ] + } + + fn symbol_name(&self, s: NodeRef) -> Option<&str> { + match &self.nodes[s.0] { + Node::LocalSymbol(s, _) | Node::GlobalSymbol(s) => Some(s), + _ => None, + } + } + + fn make_identifier(&mut self, value: visitors::Identifier) -> NodeRef { + match &value { + visitors::Identifier::Simple { symbol } => *symbol, + visitors::Identifier::Indexed { symbol, indices } => { + if let Some(c) = self.identifiers.get(&value) { + return *c; + } + let mut children = vec![*symbol]; + for i in indices { + let m = match i { + visitors::Index::Numeral(n) => { + self.make_constant(Constant::Numeral(n.clone())) + } + visitors::Index::Symbol(s) => *s, + }; + children.push(m); + } + let n = self.make_sequence(SeqKind::Underscore, children); + self.identifiers.insert(value, n); + n + } + } + } +} + +impl visitors::ConstantVisitor for GraphBuilder { + type T = NodeRef; + type E = Error; + + fn visit_numeral_constant(&mut self, value: Numeral) -> Result { + Ok(self.make_constant(Constant::Numeral(value))) + } + fn visit_decimal_constant(&mut self, value: Decimal) -> Result { + Ok(self.make_constant(Constant::Decimal(value))) + } + fn visit_hexadecimal_constant(&mut self, value: Hexadecimal) -> Result { + Ok(self.make_constant(Constant::Hexadecimal(value))) + } + fn visit_binary_constant(&mut self, value: Binary) -> Result { + Ok(self.make_constant(Constant::Binary(value))) + } + fn visit_string_constant(&mut self, value: String) -> Result { + Ok(self.make_constant(Constant::String(value))) + } +} + +impl visitors::SymbolVisitor for GraphBuilder { + type T = NodeRef; + type E = Error; + + fn visit_bound_symbol(&mut self, value: String) -> Result { + let s = self + .bound_symbols + .get(&value) + .map(|v| *v.last().unwrap()) + .unwrap_or_else(|| self.make_global_symbol(value)); + Ok(s) + } + + fn visit_fresh_symbol( + &mut self, + value: String, + _: visitors::SymbolKind, + ) -> Result { + Ok(self.make_local_symbol(value)) + } + + fn bind_symbol(&mut self, symbol: &NodeRef) { + let name = self.symbol_name(*symbol).unwrap().to_string(); + self.bound_symbols.entry(name).or_default().push(*symbol); + } + + fn unbind_symbol(&mut self, symbol: &NodeRef) { + use std::collections::hash_map; + + let name = self.symbol_name(*symbol).unwrap().to_string(); + match self.bound_symbols.entry(name) { + hash_map::Entry::Occupied(mut e) => { + let node = e.get_mut().pop().unwrap(); + if self.config.reuse_symbol_indices { + if let Node::LocalSymbol(_, k) = &self.nodes[node.0] { + // Make symbol index available for the next call to make_local_symbol. + self.available_symbol_indices.insert(*k); + } + } + if e.get().is_empty() { + e.remove_entry(); + } + } + _ => panic!("invalid entry"), + } + } +} + +impl visitors::KeywordVisitor for GraphBuilder { + type T = NodeRef; + type E = Error; + + fn visit_keyword(&mut self, value: String) -> Result { + Ok(self.make_keyword(value)) + } +} + +impl visitors::SExprVisitor for GraphBuilder { + type T = NodeRef; + type E = Error; + + fn visit_constant_s_expr(&mut self, value: NodeRef) -> Result { + Ok(value) + } + + fn visit_symbol_s_expr(&mut self, value: NodeRef) -> Result { + Ok(value) + } + + fn visit_keyword_s_expr(&mut self, value: NodeRef) -> Result { + Ok(value) + } + + fn visit_application_s_expr(&mut self, values: Vec) -> Result { + Ok(self.make_sequence(SeqKind::SExpr, values)) + } +} + +impl visitors::SortVisitor for GraphBuilder { + type T = NodeRef; + type E = Error; + + fn visit_simple_sort( + &mut self, + identifier: visitors::Identifier, + ) -> Result { + Ok(self.make_identifier(identifier)) + } + + fn visit_parameterized_sort( + &mut self, + identifier: visitors::Identifier, + parameters: Vec, + ) -> Result { + let mut children = vec![self.make_identifier(identifier)]; + children.extend(parameters); + Ok(self.make_sequence(SeqKind::Sort, children)) + } +} + +impl visitors::QualIdentifierVisitor, NodeRef> for GraphBuilder { + type T = NodeRef; + type E = Error; + + fn visit_simple_identifier( + &mut self, + identifier: visitors::Identifier, + ) -> Result { + Ok(self.make_identifier(identifier)) + } + + fn visit_sorted_identifier( + &mut self, + identifier: visitors::Identifier, + sort: NodeRef, + ) -> Result { + let children = vec![self.make_identifier(identifier), sort]; + Ok(self.make_sequence(SeqKind::As, children)) + } +} + +impl visitors::TermVisitor for GraphBuilder { + type T = NodeRef; + type E = Error; + + fn visit_constant(&mut self, constant: NodeRef) -> Result { + Ok(constant) + } + + fn visit_qual_identifier(&mut self, qual_identifier: NodeRef) -> Result { + Ok(qual_identifier) + } + + fn visit_application( + &mut self, + qual_identifier: NodeRef, + arguments: Vec, + ) -> Result { + let mut children = vec![qual_identifier]; + children.extend(arguments); + Ok(self.make_sequence(SeqKind::Application, children)) + } + + fn visit_let( + &mut self, + var_bindings: Vec<(NodeRef, Self::T)>, + term: Self::T, + ) -> Result { + let var_bindings = var_bindings + .into_iter() + .map(|(x, t)| self.make_sequence(SeqKind::VarBinding, vec![x, t])) + .collect(); + let children = vec![self.make_sequence(SeqKind::VarBindings, var_bindings), term]; + Ok(self.make_sequence(SeqKind::Let, children)) + } + + fn visit_forall( + &mut self, + vars: Vec<(NodeRef, NodeRef)>, + term: Self::T, + ) -> Result { + let var_bindings = vars + .into_iter() + .map(|(x, t)| self.make_sequence(SeqKind::VarBinding, vec![x, t])) + .collect(); + let children = vec![self.make_sequence(SeqKind::VarBindings, var_bindings), term]; + Ok(self.make_sequence(SeqKind::Forall, children)) + } + + fn visit_exists( + &mut self, + vars: Vec<(NodeRef, NodeRef)>, + term: Self::T, + ) -> Result { + let var_bindings = vars + .into_iter() + .map(|(x, t)| self.make_sequence(SeqKind::VarBinding, vec![x, t])) + .collect(); + let children = vec![self.make_sequence(SeqKind::VarBindings, var_bindings), term]; + Ok(self.make_sequence(SeqKind::Exists, children)) + } + + fn visit_match( + &mut self, + term: Self::T, + cases: Vec<(Vec, Self::T)>, + ) -> Result { + let cases = cases + .into_iter() + .map(|(xs, t)| { + let xs = self.make_sequence(SeqKind::Pattern, xs); + self.make_sequence(SeqKind::Case, vec![xs, t]) + }) + .collect(); + let children = vec![term, self.make_sequence(SeqKind::Cases, cases)]; + Ok(self.make_sequence(SeqKind::Match, children)) + } + + fn visit_attributes( + &mut self, + term: Self::T, + attributes: Vec<(NodeRef, AttributeValue)>, + ) -> Result { + let mut children = vec![term]; + for (keyword, value) in attributes { + children.push(keyword); + if let Some(value) = self.make_attribute_value(value) { + children.push(value); + } + } + Ok(self.make_sequence(SeqKind::Exclam, children)) + } +} + +impl visitors::CommandVisitor + for GraphBuilder +{ + type T = NodeRef; + type E = Error; + + fn visit_assert(&mut self, term: NodeRef) -> Result { + let children = vec![term]; + let n = self.make_sequence(SeqKind::Assert, children); + self.commands.push(n); + Ok(n) + } + + fn visit_check_sat(&mut self) -> Result { + let children = Vec::new(); + let n = self.make_sequence(SeqKind::CheckSat, children); + self.commands.push(n); + Ok(n) + } + + fn visit_check_sat_assuming( + &mut self, + literals: Vec<(NodeRef, bool)>, + ) -> Result { + let literals = literals + .into_iter() + .map(|(n, x)| { + if x { + n + } else { + let children = vec![n]; + self.make_sequence(SeqKind::Not, children) + } + }) + .collect(); + let children = vec![self.make_sequence(SeqKind::CheckSatAssumingLiterals, literals)]; + let n = self.make_sequence(SeqKind::CheckSatAssuming, children); + self.commands.push(n); + Ok(n) + } + + fn visit_declare_const(&mut self, symbol: NodeRef, sort: NodeRef) -> Result { + let children = vec![symbol, sort]; + let n = self.make_sequence(SeqKind::DeclareConst, children); + self.commands.push(n); + Ok(n) + } + + fn visit_declare_datatype( + &mut self, + symbol: NodeRef, + datatype: DatatypeDec, + ) -> Result { + let children = vec![symbol, self.make_datatype_dec(datatype)]; + let n = self.make_sequence(SeqKind::DeclareDatatype, children); + self.commands.push(n); + Ok(n) + } + + fn visit_declare_datatypes( + &mut self, + datatypes: Vec<(NodeRef, Numeral, DatatypeDec)>, + ) -> Result { + let sorts = datatypes + .iter() + .map(|(sym, num, _)| { + let n = self.make_constant(Constant::Numeral(num.clone())); + self.make_sequence(SeqKind::DeclareDatatypesArity, vec![*sym, n]) + }) + .collect(); + let types = datatypes + .iter() + .map(|(_, _, ty)| self.make_datatype_dec(ty.clone())) + .collect(); + let children = vec![ + self.make_sequence(SeqKind::DeclareDatatypesSorts, sorts), + self.make_sequence(SeqKind::DeclareDatatypesTypes, types), + ]; + let n = self.make_sequence(SeqKind::DeclareDatatypes, children); + self.commands.push(n); + Ok(n) + } + + fn visit_declare_fun( + &mut self, + symbol: NodeRef, + parameters: Vec, + sort: NodeRef, + ) -> Result { + let children = vec![ + symbol, + self.make_sequence(SeqKind::DeclareFunParams, parameters), + sort, + ]; + let n = self.make_sequence(SeqKind::DeclareFun, children); + self.commands.push(n); + Ok(n) + } + + fn visit_declare_sort(&mut self, symbol: NodeRef, arity: Numeral) -> Result { + let children = vec![symbol, self.make_constant(Constant::Numeral(arity))]; + let n = self.make_sequence(SeqKind::DeclareSort, children); + self.commands.push(n); + Ok(n) + } + + fn visit_define_fun(&mut self, sig: FunctionDec, term: NodeRef) -> Result { + let mut children = self.make_function_dec(sig); + children.push(term); + let n = self.make_sequence(SeqKind::DefineFun, children); + self.commands.push(n); + Ok(n) + } + + fn visit_define_fun_rec( + &mut self, + sig: FunctionDec, + term: NodeRef, + ) -> Result { + let mut children = self.make_function_dec(sig); + children.push(term); + let n = self.make_sequence(SeqKind::DefineFunRec, children); + self.commands.push(n); + Ok(n) + } + + fn visit_define_funs_rec( + &mut self, + funs: Vec<(FunctionDec, NodeRef)>, + ) -> Result { + let sigs = funs + .iter() + .map(|(sig, _)| { + let sig = self.make_function_dec(sig.clone()); + self.make_sequence(SeqKind::DefineFunsRecSig, sig) + }) + .collect(); + let terms = funs.iter().map(|(_, t)| *t).collect(); + let children = vec![ + self.make_sequence(SeqKind::DefineFunsRecSigs, sigs), + self.make_sequence(SeqKind::DefineFunsRecTerms, terms), + ]; + let n = self.make_sequence(SeqKind::DefineFunsRec, children); + self.commands.push(n); + Ok(n) + } + + fn visit_define_sort( + &mut self, + symbol: NodeRef, + parameters: Vec, + sort: NodeRef, + ) -> Result { + let children = vec![ + symbol, + self.make_sequence(SeqKind::DefineSortParams, parameters), + sort, + ]; + let n = self.make_sequence(SeqKind::DefineSort, children); + self.commands.push(n); + Ok(n) + } + + fn visit_echo(&mut self, message: String) -> Result { + let children = vec![self.make_constant(Constant::String(message))]; + let n = self.make_sequence(SeqKind::Echo, children); + self.commands.push(n); + Ok(n) + } + + fn visit_exit(&mut self) -> Result { + let n = self.make_sequence(SeqKind::Exit, Vec::new()); + self.commands.push(n); + Ok(n) + } + + fn visit_get_assertions(&mut self) -> Result { + let n = self.make_sequence(SeqKind::GetAssertions, Vec::new()); + self.commands.push(n); + Ok(n) + } + + fn visit_get_assignment(&mut self) -> Result { + let n = self.make_sequence(SeqKind::GetAssignment, Vec::new()); + self.commands.push(n); + Ok(n) + } + + fn visit_get_info(&mut self, flag: NodeRef) -> Result { + let children = vec![flag]; + let n = self.make_sequence(SeqKind::GetInfo, children); + self.commands.push(n); + Ok(n) + } + + fn visit_get_model(&mut self) -> Result { + let n = self.make_sequence(SeqKind::GetModel, Vec::new()); + self.commands.push(n); + Ok(n) + } + + fn visit_get_option(&mut self, keyword: NodeRef) -> Result { + let children = vec![keyword]; + let n = self.make_sequence(SeqKind::GetOption, children); + self.commands.push(n); + Ok(n) + } + + fn visit_get_proof(&mut self) -> Result { + let n = self.make_sequence(SeqKind::GetProof, Vec::new()); + self.commands.push(n); + Ok(n) + } + + fn visit_get_unsat_assumptions(&mut self) -> Result { + let n = self.make_sequence(SeqKind::GetUnsatAssumptions, Vec::new()); + self.commands.push(n); + Ok(n) + } + + fn visit_get_unsat_core(&mut self) -> Result { + let n = self.make_sequence(SeqKind::GetUnsatCore, Vec::new()); + self.commands.push(n); + Ok(n) + } + + fn visit_get_value(&mut self, terms: Vec) -> Result { + let children = vec![self.make_sequence(SeqKind::GetValueTerms, terms)]; + let n = self.make_sequence(SeqKind::GetValue, children); + self.commands.push(n); + Ok(n) + } + + fn visit_pop(&mut self, level: Numeral) -> Result { + let children = vec![self.make_constant(Constant::Numeral(level))]; + let n = self.make_sequence(SeqKind::Pop, children); + self.commands.push(n); + Ok(n) + } + + fn visit_push(&mut self, level: Numeral) -> Result { + let children = vec![self.make_constant(Constant::Numeral(level))]; + let n = self.make_sequence(SeqKind::Push, children); + self.commands.push(n); + Ok(n) + } + + fn visit_reset(&mut self) -> Result { + let n = self.make_sequence(SeqKind::Reset, Vec::new()); + self.commands.push(n); + Ok(n) + } + + fn visit_reset_assertions(&mut self) -> Result { + let n = self.make_sequence(SeqKind::ResetAssertions, Vec::new()); + self.commands.push(n); + Ok(n) + } + + fn visit_set_info( + &mut self, + keyword: NodeRef, + value: AttributeValue, + ) -> Result { + let mut children = vec![keyword]; + if let Some(value) = self.make_attribute_value(value) { + children.push(value); + } + let n = self.make_sequence(SeqKind::SetInfo, children); + self.commands.push(n); + Ok(n) + } + + fn visit_set_logic(&mut self, symbol: NodeRef) -> Result { + let children = vec![symbol]; + let n = self.make_sequence(SeqKind::SetLogic, children); + self.commands.push(n); + Ok(n) + } + + fn visit_set_option( + &mut self, + keyword: NodeRef, + value: AttributeValue, + ) -> Result { + let mut children = vec![keyword]; + if let Some(value) = self.make_attribute_value(value) { + children.push(value); + } + let n = self.make_sequence(SeqKind::SetOption, children); + self.commands.push(n); + Ok(n) + } +} + +impl visitors::Smt2Visitor for GraphBuilder { + type Error = Error; + type Constant = NodeRef; + type QualIdentifier = NodeRef; + type Keyword = NodeRef; + type Sort = NodeRef; + type SExpr = NodeRef; + type Symbol = NodeRef; + type Term = NodeRef; + type Command = NodeRef; + + fn syntax_error(&mut self, pos: Position, s: String) -> Self::Error { + Error::SyntaxError(pos, s) + } + + fn parsing_error(&mut self, pos: Position, s: String) -> Self::Error { + Error::ParsingError(pos, s) + } +} diff --git a/smt2model/src/lib.rs b/smt2model/src/lib.rs new file mode 100644 index 0000000..9c9513a --- /dev/null +++ b/smt2model/src/lib.rs @@ -0,0 +1,8 @@ +// Copyright (c) Facebook, Inc. and its affiliates +// SPDX-License-Identifier: MIT OR Apache-2.0 + +/// Rewrite and skip part of SMT inputs. +pub mod rewriter; + +/// Index SMT inputs as a graph of terms. +pub mod graph; diff --git a/smt2model/src/main.rs b/smt2model/src/main.rs new file mode 100644 index 0000000..6e12800 --- /dev/null +++ b/smt2model/src/main.rs @@ -0,0 +1,339 @@ +// Copyright (c) Facebook, Inc. and its affiliates +// SPDX-License-Identifier: MIT OR Apache-2.0 + +use anyhow::Result; +use smt2model::{ + graph::{GraphBuilder, GraphBuilderConfig}, + rewriter::{Error, Rewriter, RewriterConfig}, +}; +use smt2parser::{concrete::SyntaxBuilder, renaming::TesterModernizer, CommandStream}; +use std::{ + io::Write, + path::{Path, PathBuf}, + sync::{ + atomic::{AtomicBool, Ordering}, + Arc, + }, +}; +use structopt::{clap::arg_enum, StructOpt}; + +arg_enum! { +#[derive(Debug, StructOpt, Clone, Copy)] +enum OutputFormat { + Smt, + Dot, +} +} + +/// Compute simple features for SMT2 files (including Z3 execution time). +#[derive(Debug, StructOpt)] +struct Options { + /// Output Format. + #[structopt(long, possible_values = &OutputFormat::variants(), case_insensitive = true, default_value = "smt")] + format: OutputFormat, + #[structopt(flatten)] + rewriter_config: RewriterConfig, + #[structopt(flatten)] + graph_builder_config: GraphBuilderConfig, + /// Output directory. + #[structopt(long)] + output_dir: Option, + /// Whether to concatenate all outputs into a single file. + #[structopt(long)] + output_file: Option, + /// Whether to skip input files that seem to have been processed already. + #[structopt(long)] + incremental: bool, + /// Discard input files whose bucket number is higher or equal than `sampling_offset + sampling_increment`. + #[structopt(long, default_value = "1")] + sampling_increment: u64, + /// Discard input files whose bucket number is lower than `sampling_offset`. + #[structopt(long, default_value = "0")] + sampling_offset: u64, + /// Set the number of buckets 0..=(N-1) used for sampling base paths. See --sampling-increment and --sampling-offset + #[structopt(long, default_value = "1")] + sampling_total: u64, + /// Whether to reschedule a slurm job in case of interruptions. + #[structopt(long)] + slurm: bool, + /// Path to the smt2 files. + #[structopt(parse(from_os_str))] + inputs: Vec, +} + +fn append_os_str(mut os_str: std::ffi::OsString, ext: &std::ffi::OsStr) -> std::ffi::OsString { + os_str.push(ext); + os_str +} + +fn append_suffix(path: PathBuf, suffix: &str) -> PathBuf { + append_os_str(path.into_os_string(), suffix.as_ref()).into() +} + +fn parse_suffix<'a>(s: &'a str, suffix: &str) -> Option<&'a str> { + if s.ends_with(suffix) { + Some(&s[0..s.len() - suffix.len()]) + } else { + None + } +} + +fn parse_tar_gz_base_path(path: &Path) -> Option<&str> { + let s = path.to_str().unwrap_or(""); + parse_suffix(s, ".tar.gz").or_else(|| parse_suffix(s, ".tgz")) +} + +fn parse_smt_base_path(path: &Path) -> Option<&str> { + let s = path.to_str().unwrap_or(""); + parse_suffix(s, ".smt").or_else(|| parse_suffix(s, ".smt2")) +} + +fn get_output_path(format: OutputFormat, output_dir: &Path, entry: &Path) -> PathBuf { + let entry = if entry.is_relative() { + PathBuf::from(&output_dir).join(entry) + } else { + entry.to_path_buf() + }; + let s = match format { + OutputFormat::Smt => ".out.smt2", + OutputFormat::Dot => ".out.dot", + }; + append_suffix(entry, s) +} + +fn handle_input( + rewriter_config: RewriterConfig, + graph_builder_config: GraphBuilderConfig, + format: OutputFormat, + append: bool, + output_path: &Path, + input_path: &Path, +) -> Result<()> { + if append { + eprintln!( + "Writing {} with data from {}", + output_path.to_str().unwrap_or(""), + input_path.to_str().unwrap_or("") + ); + } else { + eprintln!("Writing {}", output_path.to_str().unwrap_or("")); + } + let file = std::io::BufReader::new(std::fs::File::open(&input_path)?); + let mut builder = GraphBuilder::new(graph_builder_config); + let mut stream = CommandStream::new( + file, + Rewriter::new(rewriter_config, TesterModernizer::new(SyntaxBuilder)), + input_path.to_str().map(String::from), + ); + std::fs::create_dir_all(output_path.parent().unwrap_or_else(|| Path::new(".")))?; + let mut output = std::fs::OpenOptions::new() + .create(true) + .write(true) + .append(append) + .open(output_path)?; + let mut need_space = false; + for result in &mut stream { + match result { + Ok(command) => { + // Visit the syntax again for name-binding-aware rewriting. + let command = command.accept(&mut builder)?; + // Print the command. + if let OutputFormat::Smt = format { + if need_space { + write!(output, " ")?; + } + builder.write_smt_ast(&mut output, command)?; + if append { + need_space = true; + } else { + writeln!(output)?; + } + } + } + Err(Error::SkipCommand) => {} + Err(error) => { + eprintln!("{}", error); + break; + } + } + } + if let OutputFormat::Dot = format { + use petgraph::{dot::*, visit::NodeRef}; + + let graph = builder.to_graph(); + // let dot = petgraph::dot::Dot::new(&graph); + let dot = Dot::with_attr_getters( + &graph, + &[Config::NodeNoLabel, Config::EdgeNoLabel], + &|_, er| format!("label = \"{}\"", er.weight()), + &|_, nr| { + let w = nr.weight(); + // '"' '\\' '\n' + format!("label = \"{}\"", w) + }, + ); + writeln!(output, "{:?}", dot)?; + } + if append { + writeln!(output)?; + } + Ok(()) +} + +fn is_selected(options: &Options, path: &Path) -> bool { + use rand::{Rng, SeedableRng}; + use std::hash::{Hash, Hasher}; + + let mut hasher = std::collections::hash_map::DefaultHasher::new(); + path.hash(&mut hasher); + let seed = hasher.finish(); + let mut rng = rand::rngs::SmallRng::seed_from_u64(seed); + let s = rng.gen_range(0..options.sampling_total); + s >= options.sampling_offset && s < options.sampling_offset + options.sampling_increment +} + +fn process_input( + options: &Options, + sigterm: &AtomicBool, + sigusr: &AtomicBool, + output_dir: &Path, + input_path: &Path, + mut pre_process: F, + post_process: G, +) -> Result<()> +where + F: FnMut(&Path) -> Result>, + G: Fn(&Path) -> std::io::Result<()>, +{ + if sigterm.swap(false, Ordering::Relaxed) { + eprintln!("Ignoring SIGTERM"); + } + if sigusr.swap(false, Ordering::Relaxed) { + eprintln!("Handling SIGUSR1"); + // TODO: to be future-proof, we must test that this is not a child process. + if let Ok("0") = std::env::var("SLURM_PROCID").as_deref() { + if let Ok(id) = std::env::var("SLURM_JOB_ID") { + let status = std::process::Command::new("scontrol") + .args(&["requeue", &id]) + .status()?; + eprintln!("scontrol finished with: {}", status); + } + } + anyhow::bail!("Interrupted by SIGUSR1"); + } + if !is_selected(options, input_path) { + // Entry is not selected. + return Ok(()); + } + if parse_smt_base_path(input_path).is_none() { + eprintln!( + "Skipping non-SMT entry {}", + input_path.to_str().unwrap_or("") + ); + return Ok(()); + } + let output_path = match &options.output_file { + Some(path) => { + if options.sampling_total > 1 { + append_suffix(path.clone(), &format!(".{}", options.sampling_offset)) + } else { + path.clone() + } + } + None => get_output_path(options.format, output_dir, input_path), + }; + + if options.incremental && output_path.exists() { + eprintln!( + "Skipping processed entry {}", + input_path.to_str().unwrap_or("") + ); + return Ok(()); + } + + let input = match pre_process(input_path)? { + None => return Ok(()), + Some(i) => i, + }; + match handle_input( + options.rewriter_config.clone(), + options.graph_builder_config.clone(), + options.format, + options.output_file.is_some(), + &output_path, + &input, + ) { + Ok(()) => (), + Err(e) => { + eprintln!( + "Error while sampling {}: {} (skipping entry)", + input.to_str().unwrap_or(""), + e + ); + } + }; + post_process(&input)?; + Ok(()) +} + +fn main() -> Result<()> { + let options = Options::from_args(); + if options.incremental && options.output_file.is_some() { + panic!("--incremental and --output-file cannot be used at the same time."); + } + let sigterm = Arc::new(AtomicBool::new(false)); + let siguser = Arc::new(AtomicBool::new(false)); + if options.slurm { + signal_hook::flag::register(signal_hook::consts::SIGTERM, Arc::clone(&sigterm))?; + signal_hook::flag::register(signal_hook::consts::SIGUSR1, Arc::clone(&siguser))?; + } + let output_dir = options + .output_dir + .clone() + .unwrap_or_else(|| PathBuf::from(".")); + std::fs::create_dir_all(&output_dir)?; + for input in &options.inputs { + if parse_tar_gz_base_path(&input).is_some() { + // Tar-gz archive. + let tmp_dir = tempfile::tempdir()?; + let tgz_input = std::fs::File::open(&input)?; + let tar_input = flate2::read::GzDecoder::new(tgz_input); + let mut archive = tar::Archive::new(tar_input); + for entry in archive.entries()? { + let mut entry = entry?; + let input_path = entry.path()?.to_path_buf(); + process_input( + &options, + &sigterm, + &siguser, + &output_dir, + &input_path, + |input_path| { + // Make input file ready. + let input = tmp_dir.path().join(input_path); + if !entry.unpack_in(tmp_dir.path())? { + // Entries outside `tmp_dir` are skipped. + eprintln!("Skipping incorrect path {}", input.to_str().unwrap_or("")); + Ok(None) + } else { + Ok(Some(input)) + } + }, + |input| std::fs::remove_file(&input), + )?; + } + } else { + // Plain SMT2 file. + process_input( + &options, + &sigterm, + &siguser, + &output_dir, + &input, + |path| Ok(Some(path.to_path_buf())), + |_| Ok(()), + )?; + } + } + Ok(()) +} diff --git a/smt2model/src/rewriter.rs b/smt2model/src/rewriter.rs new file mode 100644 index 0000000..2aaece7 --- /dev/null +++ b/smt2model/src/rewriter.rs @@ -0,0 +1,92 @@ +// Copyright (c) Facebook, Inc. and its affiliates +// SPDX-License-Identifier: MIT OR Apache-2.0 + +use smt2parser::visitors::AttributeValue; +use structopt::StructOpt; +use thiserror::Error; + +/// Configuration for the SMT2 rewriting operations. +#[derive(Debug, Clone, StructOpt)] +pub struct RewriterConfig { + /// Whether to skip set-option commands. + #[structopt(long)] + skip_set_option: bool, + + /// Whether to override --skip-option-info for certain keywords. + #[structopt(long)] + allow_set_option_keywords: Vec, + + /// Whether to skip set-info commands. + #[structopt(long)] + skip_set_info: bool, + + /// Whether to override --skip-set-info for certain keywords. + #[structopt(long)] + allow_set_info_keywords: Vec, +} + +/// State of the SMT2 rewriter. +#[derive(Debug)] +pub struct Rewriter { + config: RewriterConfig, + visitor: V, +} + +impl Rewriter { + pub fn new(config: RewriterConfig, visitor: V) -> Self { + Self { config, visitor } + } +} + +#[derive(Error, Debug)] +pub enum Error { + #[error("Command was skipped")] + SkipCommand, + #[error("{0}")] + Error(E), +} + +impl std::convert::From for Error { + fn from(e: E) -> Self { + Self::Error(e) + } +} + +impl smt2parser::rewriter::Rewriter for Rewriter +where + V: smt2parser::visitors::Smt2Visitor, + V::Error: std::error::Error, +{ + type V = V; + type Error = Error; + + fn visitor(&mut self) -> &mut V { + &mut self.visitor + } + + fn visit_set_info( + &mut self, + keyword: V::Keyword, + value: AttributeValue, + ) -> Result { + if self.config.skip_set_info && !self.config.allow_set_info_keywords.contains(&keyword.0) { + return Err(Error::SkipCommand); + } + let value = self.visitor().visit_set_info(keyword, value)?; + self.process_command(value) + } + + fn visit_set_option( + &mut self, + keyword: V::Keyword, + value: AttributeValue, + ) -> Result { + if self.config.skip_set_option + && !self.config.allow_set_option_keywords.contains(&keyword.0) + { + return Err(Error::SkipCommand); + } + let value = self.visitor().visit_set_option(keyword, value)?; + self.process_command(value) + } +}