transform.rs 25 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722
  1. //! A module for operations that transform a [`StatementTree`].
  2. //! Every transformation must maintain the [disjunction invariant].
  3. //!
  4. //! [disjunction invariant]: StatementTree::check_disjunction_invariant
  5. use super::codegen::CodeGen;
  6. use super::pedersen::{
  7. convert_commitment, convert_randomness, recognize_pedersen_assignment, unique_random_scalars,
  8. LinScalar, PedersenAssignment,
  9. };
  10. use super::sigma::combiners::*;
  11. use super::syntax::{collect_cind_points, taggedvardict_to_vardict};
  12. use super::{TaggedIdent, TaggedScalar, TaggedVarDict};
  13. use quote::{format_ident, quote};
  14. use std::collections::{HashMap, HashSet};
  15. use syn::visit_mut::{self, VisitMut};
  16. use syn::{parse_quote, Error, Expr, Ident, Result};
  17. /// Simplify a [`StatementTree`] by pruning leaves that are the constant
  18. /// `true`, and simplifying `And`, `Or`, and `Thresh` combiners that
  19. /// have fewer than two children.
  20. pub fn prune_statement_tree(st: &mut StatementTree) {
  21. match st {
  22. // If the StatementTree is just a Leaf, just keep it unmodified,
  23. // even if it is leaf_true.
  24. StatementTree::Leaf(_) => {}
  25. // For the And combiner, recursively simplify each child, and then
  26. // prune the child if it is leaf_true. If we end up with 1
  27. // child replace ourselves with that child. If we end up with 0
  28. // children, replace ourselves with leaf_true.
  29. StatementTree::And(v) => {
  30. let mut i: usize = 0;
  31. // Note that v.len _can change_ during this loop
  32. while i < v.len() {
  33. prune_statement_tree(&mut v[i]);
  34. if v[i].is_leaf_true() {
  35. // Remove this child, and _do not_ increment i
  36. v.remove(i);
  37. } else {
  38. i += 1;
  39. }
  40. }
  41. if v.is_empty() {
  42. *st = StatementTree::leaf_true();
  43. } else if v.len() == 1 {
  44. let child = v.remove(0);
  45. *st = child;
  46. }
  47. }
  48. // For the Or combiner, recursively simplify each child, and if
  49. // it ends up leaf_true, replace ourselves with leaf_true.
  50. // If we end up with 1 child, we must have started wth 1 child.
  51. // Replace ourselves with that child anyway.
  52. StatementTree::Or(v) => {
  53. let mut i: usize = 0;
  54. // Note that v.len _can change_ during this loop
  55. while i < v.len() {
  56. prune_statement_tree(&mut v[i]);
  57. if v[i].is_leaf_true() {
  58. *st = StatementTree::leaf_true();
  59. return;
  60. } else {
  61. i += 1;
  62. }
  63. }
  64. if v.len() == 1 {
  65. let child = v.remove(0);
  66. *st = child;
  67. }
  68. }
  69. // For the Thresh combiner, recursively simplify each child, and
  70. // if it ends up leaf_true, prune it, and subtract 1 from the
  71. // thresh. If the thresh hits 0, replace ourselves with
  72. // leaf_true. If we end up with 1 child and thresh is 1,
  73. // replace ourselves with that child.
  74. StatementTree::Thresh(thresh, v) => {
  75. let mut i: usize = 0;
  76. // Note that v.len _can change_ during this loop
  77. while i < v.len() {
  78. prune_statement_tree(&mut v[i]);
  79. if v[i].is_leaf_true() {
  80. // Remove this child, and _do not_ increment i
  81. v.remove(i);
  82. // But decrement thresh
  83. *thresh -= 1;
  84. if *thresh == 0 {
  85. *st = StatementTree::leaf_true();
  86. return;
  87. }
  88. } else {
  89. i += 1;
  90. }
  91. }
  92. if v.len() == 1 {
  93. // If thresh == 0, we would have exited above
  94. assert!(*thresh == 1);
  95. let child = v.remove(0);
  96. *st = child;
  97. }
  98. }
  99. }
  100. }
  101. /// Add parentheses around an [`Expr`] (which represents an [arithmetic
  102. /// expression]) if needed.
  103. ///
  104. /// The parentheses are needed if the [`Expr`] would parse as multiple
  105. /// tokens. For example, `a+b` turns into `(a+b)`, but `c`
  106. /// remains `c` and `(a+b)` remains `(a+b)`.
  107. ///
  108. /// [arithmetic expression]: super::sigma::types::expr_type
  109. pub fn paren_if_needed(expr: Expr) -> Expr {
  110. match expr {
  111. Expr::Unary(_) | Expr::Binary(_) => parse_quote! { (#expr) },
  112. _ => expr,
  113. }
  114. }
  115. /// Transform the [`StatementTree`] so that it satisfies the
  116. /// [disjunction invariant].
  117. ///
  118. /// [disjunction invariant]: StatementTree::check_disjunction_invariant
  119. #[allow(non_snake_case)] // so that Points can be capital letters
  120. pub fn enforce_disjunction_invariant(
  121. codegen: &mut CodeGen,
  122. st: &mut StatementTree,
  123. vars: &mut TaggedVarDict,
  124. ) -> Result<()> {
  125. // Make the VarDict version of the variable dictionary
  126. let mut vardict = taggedvardict_to_vardict(vars);
  127. // A HashSet of the unique random Scalars in the macro input
  128. let mut randoms = unique_random_scalars(vars, st);
  129. // A list of the computationally independent (non-vector) Points in
  130. // the macro input. If we need to do any transformations, there
  131. // must be at least two of them in order to create Pedersen
  132. // commitments.
  133. let cind_points = collect_cind_points(vars);
  134. // Extra statements to be added to the root disjunction branch
  135. let mut root_extra_statements: Vec<StatementTree> = Vec::new();
  136. // The generated variable name for the rng
  137. let rng_var = codegen.gen_ident(&format_ident!("rng"));
  138. // Find any statements that look like Pedersen commitments in the
  139. // root disjunction branch of the StatementTree, and make a HashMap
  140. // mapping the committed private variable to the parsed commitment.
  141. let mut root_pedersens: HashMap<Ident, PedersenAssignment> = HashMap::new();
  142. st.for_each_disjunction_branch_leaf(&mut |leaf| {
  143. // See if we recognize this leaf expression as a
  144. // PedersenAssignment, and if so, map its variable to the
  145. // PedersenAssignment.
  146. if let StatementTree::Leaf(leafexpr) = leaf {
  147. if let Some(ped_assign) =
  148. recognize_pedersen_assignment(vars, &randoms, &vardict, leafexpr)
  149. {
  150. root_pedersens.insert(ped_assign.var(), ped_assign);
  151. }
  152. }
  153. Ok(())
  154. })?;
  155. // Count how many disjunction branches contain each private Scalar
  156. let mut branch_count: HashMap<Ident, usize> = HashMap::new();
  157. st.for_each_disjunction_branch(&mut |branch, _path| {
  158. branch
  159. .disjunction_branch_priv_scalars(&vardict)
  160. .drain()
  161. .for_each(|id| {
  162. if let Some(n) = branch_count.get(&id) {
  163. branch_count.insert(id, n + 1);
  164. } else {
  165. branch_count.insert(id, 1);
  166. }
  167. });
  168. Ok(())
  169. })?;
  170. // Make a HashSet of any of those private Scalars whose count is
  171. // strictly larger than 1. (Those private Scalars are the ones
  172. // that are in violation of the disjunction invariant.)
  173. let mut invariant_violators: HashSet<Ident> = branch_count
  174. .drain()
  175. .filter_map(|(id, n)| if n > 1 { Some(id) } else { None })
  176. .collect();
  177. // If there are no invariant violators, we're done.
  178. if invariant_violators.is_empty() {
  179. return Ok(());
  180. }
  181. // Otherwise, ensure there are at least two computationally
  182. // independent points, since we'll need to construct Pedersen
  183. // commitments.
  184. if cind_points.len() < 2 {
  185. return Err(Error::new(
  186. proc_macro2::Span::call_site(),
  187. "At least two cind Points must be declared to support Pedersen commitments",
  188. ));
  189. }
  190. let cind_A = &cind_points[0];
  191. let cind_B = &cind_points[1];
  192. // For each invariant violator, find (or create) a Pedersen
  193. // commitment in the root disjunction branch for it.
  194. let invariant_violator_pedersens: HashMap<Ident, PedersenAssignment> = invariant_violators
  195. .drain()
  196. .map(|id| {
  197. // Check if the private Scalar is a vector variable or
  198. // not
  199. let is_vec = if let Some(TaggedIdent::Scalar(TaggedScalar { is_vec, .. })) =
  200. vars.get(&id.to_string())
  201. {
  202. *is_vec
  203. } else {
  204. false
  205. };
  206. // See if we already have a PedersenAssignment in the
  207. // root disjunction branch for this private Scalar
  208. let ped_assign = if let Some(ped_assign) = root_pedersens.get(&id) {
  209. ped_assign.clone()
  210. } else {
  211. // Create new variables for the Pedersen commitment and its
  212. // random Scalar.
  213. let commitment_var = codegen.gen_point(
  214. vars,
  215. &format_ident!("disj_{}_genC", id),
  216. is_vec, // is_vec
  217. true, // send_to_verifier
  218. );
  219. let rand_var = codegen.gen_scalar(
  220. vars,
  221. &format_ident!("disj_{}_genr", id),
  222. true, // is_rand
  223. is_vec, // is_vec
  224. );
  225. // Update vardict and randoms with the new vars
  226. vardict = taggedvardict_to_vardict(vars);
  227. randoms.insert(rand_var.to_string());
  228. let ped_assign_expr: Expr = parse_quote! {
  229. #commitment_var = #id * #cind_A + #rand_var * #cind_B
  230. };
  231. let ped_assign =
  232. recognize_pedersen_assignment(vars, &randoms, &vardict, &ped_assign_expr)
  233. .unwrap();
  234. if is_vec {
  235. codegen.prove_append(quote! {
  236. let #rand_var: Vec<Scalar> = #id
  237. .map(|_| Scalar::random(#rng_var))
  238. .collect();
  239. let #commitment_var = (0..#id.len())
  240. .map(|i| {
  241. #id[i] * #cind_A + #rand_var[i] * #cind_B
  242. })
  243. .collect();
  244. });
  245. } else {
  246. codegen.prove_append(quote! {
  247. let #rand_var = Scalar::random(#rng_var);
  248. let #ped_assign_expr;
  249. });
  250. }
  251. root_extra_statements.push(StatementTree::Leaf(ped_assign_expr));
  252. ped_assign
  253. };
  254. // At this point, we have a Pedersen commitment for some linear
  255. // function of id (given by
  256. // ped_assign.pedersen.var_term.coeff), using some linear
  257. // function of rand_var (given by
  258. // ped_assign.pedersen.rand_term.coeff) as the randomness. But
  259. // what we need is a Pedersen commitment for id itself.
  260. // So we output runtime code for both the prover and the
  261. // verifier that converts the commitment, and code for just
  262. // the prover that converts the randomness.
  263. // Make new runtime variables to hold the converted
  264. // commitment and randomness
  265. let commitment_var = codegen.gen_point(
  266. vars,
  267. &format_ident!("disj_{}_C", id),
  268. is_vec, // is_vec
  269. false, // send_to_verifier
  270. );
  271. let rand_var = codegen.gen_ident(&format_ident!("disj_{}_r", id));
  272. // Update vardict and randoms with the new vars
  273. vardict = taggedvardict_to_vardict(vars);
  274. randoms.insert(rand_var.to_string());
  275. // The identity LinScalar for this id
  276. let id_linscalar = LinScalar {
  277. coeff: 1i128,
  278. pub_scalar_expr: None,
  279. id: id.clone(),
  280. is_vec,
  281. };
  282. codegen.prove_verify_append(
  283. convert_commitment(&commitment_var, &ped_assign, &id_linscalar, &vardict).unwrap(),
  284. );
  285. codegen.prove_append(
  286. convert_randomness(&rand_var, &ped_assign, &id_linscalar, &vardict).unwrap(),
  287. );
  288. (id, ped_assign)
  289. })
  290. .collect();
  291. // Do another pass over each disjunction branch (other than the
  292. // root). In each non-root branch, if there are any instances of an
  293. // invariant violator, then change all instances of that violating
  294. // identifier to a fresh identifier, and insert a Pedersen
  295. // commitment (to the same commitment variable that exists in the
  296. // root disjunction branch) to bind the new identifier to the
  297. // original.
  298. let mut disjunction_branch_num = 0usize;
  299. st.for_each_disjunction_branch(&mut |branch, path| {
  300. // Skip the root disjunction branch, which is represented by an
  301. // empty path
  302. if path.is_empty() {
  303. return Ok(());
  304. }
  305. disjunction_branch_num += 1;
  306. // Keep track of the ids in invariant_violator_pedersens
  307. // that we encounter and rename in this disjunction branch
  308. let mut ids_renamed: HashSet<Ident> = HashSet::new();
  309. // Extra statements to be added to this disjunction branch
  310. let mut branch_extra_statements: Vec<StatementTree> = Vec::new();
  311. struct Renamer<'a> {
  312. codegen: &'a CodeGen,
  313. disjunction_branch_num: usize,
  314. invariant_violators: &'a HashMap<Ident, PedersenAssignment>,
  315. ids_renamed: &'a mut HashSet<Ident>,
  316. }
  317. impl<'a> VisitMut for Renamer<'a> {
  318. fn visit_expr_mut(&mut self, node: &mut Expr) {
  319. if let Expr::Path(expath) = node {
  320. if let Some(id) = expath.path.get_ident() {
  321. if self.invariant_violators.contains_key(id) {
  322. let replacement_ident = self.codegen.gen_ident(&format_ident!(
  323. "disj{}_{}",
  324. self.disjunction_branch_num,
  325. id
  326. ));
  327. self.ids_renamed.insert(id.clone());
  328. *node = parse_quote! { #replacement_ident };
  329. return;
  330. }
  331. }
  332. }
  333. // Unless we bailed out above, continue with the default
  334. // traversal
  335. visit_mut::visit_expr_mut(self, node);
  336. }
  337. }
  338. let mut renamer = Renamer {
  339. codegen,
  340. disjunction_branch_num,
  341. invariant_violators: &invariant_violator_pedersens,
  342. ids_renamed: &mut ids_renamed,
  343. };
  344. branch.for_each_disjunction_branch_leaf(&mut |leaf| {
  345. let StatementTree::Leaf(ref mut leafexpr) = leaf else {
  346. panic!(
  347. "Should not happen: leaf {:?} is not a StatementTree::Leaf",
  348. leaf
  349. );
  350. };
  351. renamer.visit_expr_mut(leafexpr);
  352. Ok(())
  353. })?;
  354. // For each id we renamed, insert a Pedersen commitment to the
  355. // new name (using the _same_ commitment value we computed in
  356. // the root Pedersen commitment) into this disjunction branch.
  357. // This binds the new name to the old name.
  358. for id in ids_renamed {
  359. // Is it a vector variable?
  360. let is_vec = if let Some(TaggedIdent::Scalar(TaggedScalar { is_vec, .. })) =
  361. vars.get(&id.to_string())
  362. {
  363. *is_vec
  364. } else {
  365. false
  366. };
  367. // Variables for the renamed private Scalar and the randomness
  368. let id_var = codegen.gen_scalar(
  369. vars,
  370. &format_ident!("disj{}_{}", disjunction_branch_num, id,),
  371. false, // is_rand
  372. is_vec, // is_vec
  373. );
  374. let rand_var = codegen.gen_scalar(
  375. vars,
  376. &format_ident!("disj{}_{}_r", disjunction_branch_num, id,),
  377. true, // is_rand
  378. is_vec, // is_vec
  379. );
  380. let root_commitment_var = codegen.gen_ident(&format_ident!("disj_{}_C", id));
  381. let root_rand_var = codegen.gen_ident(&format_ident!("disj_{}_r", id));
  382. if is_vec {
  383. codegen.prove_append(quote! {
  384. let #id_var = #id.clone();
  385. let #rand_var = #root_rand_var.clone();
  386. });
  387. } else {
  388. codegen.prove_append(quote! {
  389. let #id_var = #id;
  390. let #rand_var = #root_rand_var;
  391. });
  392. }
  393. // The generators for the Pedersen commitment for this id
  394. let ped_assign = invariant_violator_pedersens.get(&id).unwrap();
  395. let var_generator = &ped_assign.pedersen.var_term.id;
  396. let rand_generator = &ped_assign.pedersen.rand_term.id;
  397. branch_extra_statements.push(StatementTree::Leaf(parse_quote! {
  398. #root_commitment_var = #id_var * #var_generator + #rand_var * #rand_generator
  399. }));
  400. }
  401. // Now add the branch_extra_statements to the top node of this
  402. // disjunction branch. If it's already an And node, just add
  403. // them to the vector. Otherwise, make a new And node
  404. // containing the old node and the branch_extra_statements.
  405. if let StatementTree::And(ref mut stvec) = branch {
  406. stvec.append(&mut branch_extra_statements);
  407. } else {
  408. let old_branch = std::mem::replace(branch, StatementTree::leaf_true());
  409. branch_extra_statements.push(old_branch);
  410. *branch = StatementTree::And(branch_extra_statements);
  411. }
  412. Ok(())
  413. })?;
  414. // Add the root_extra_statements to the root of the StatementTree.
  415. // If it's already an And node, just add them to the vector.
  416. // Otherwise, make a new And node containing the old root and the
  417. // root_extra_statements
  418. if let StatementTree::And(ref mut stvec) = st {
  419. stvec.append(&mut root_extra_statements);
  420. } else {
  421. let old_st = std::mem::replace(st, StatementTree::leaf_true());
  422. root_extra_statements.push(old_st);
  423. *st = StatementTree::And(root_extra_statements);
  424. }
  425. // Sanity check
  426. st.check_disjunction_invariant(&vardict)
  427. }
  428. #[cfg(test)]
  429. mod tests {
  430. use super::super::syntax::taggedvardict_from_strs;
  431. use super::*;
  432. fn prune_tester(e: Expr, pruned_e: Expr) {
  433. let mut st = StatementTree::parse(&e).unwrap();
  434. prune_statement_tree(&mut st);
  435. assert_eq!(st, StatementTree::parse(&pruned_e).unwrap());
  436. }
  437. #[test]
  438. fn prune_statement_tree_test() {
  439. prune_tester(
  440. parse_quote! {
  441. AND (
  442. true,
  443. e = f,
  444. )
  445. },
  446. parse_quote! {
  447. e = f
  448. },
  449. );
  450. prune_tester(
  451. parse_quote! {
  452. AND (
  453. e = f,
  454. true,
  455. )
  456. },
  457. parse_quote! {
  458. e = f
  459. },
  460. );
  461. prune_tester(
  462. parse_quote! {
  463. AND (
  464. e = f,
  465. true,
  466. b = c,
  467. )
  468. },
  469. parse_quote! {
  470. AND (
  471. e = f,
  472. b = c,
  473. )
  474. },
  475. );
  476. prune_tester(
  477. parse_quote! {
  478. OR (
  479. true,
  480. e = f,
  481. )
  482. },
  483. parse_quote! {
  484. true
  485. },
  486. );
  487. prune_tester(
  488. parse_quote! {
  489. AND (
  490. a = b,
  491. true,
  492. OR (
  493. c = d,
  494. true,
  495. e = f
  496. )
  497. )
  498. },
  499. parse_quote! {
  500. a = b
  501. },
  502. );
  503. prune_tester(
  504. parse_quote! {
  505. THRESH (3,
  506. a = b,
  507. true,
  508. THRESH (1,
  509. c = d,
  510. true,
  511. e = f
  512. )
  513. )
  514. },
  515. parse_quote! {
  516. a = b
  517. },
  518. );
  519. prune_tester(
  520. parse_quote! {
  521. THRESH (3,
  522. a = b,
  523. true,
  524. THRESH (2,
  525. c = d,
  526. true,
  527. e = f
  528. )
  529. )
  530. },
  531. parse_quote! {
  532. THRESH (2,
  533. a = b,
  534. THRESH (1,
  535. c = d,
  536. e = f
  537. )
  538. )
  539. },
  540. );
  541. }
  542. fn enforce_disjunction_invariant_tester(vars: (&[&str], &[&str]), e: Expr, expect: Expr) {
  543. let mut codegen = CodeGen::new_empty();
  544. let mut st = StatementTree::parse(&e).unwrap();
  545. let mut vars = taggedvardict_from_strs(vars);
  546. enforce_disjunction_invariant(&mut codegen, &mut st, &mut vars).unwrap();
  547. assert_eq!(st, StatementTree::parse(&expect).unwrap());
  548. }
  549. #[test]
  550. fn enforce_disjunction_invariant_test() {
  551. let vars = (
  552. [
  553. "x", "y", "z", "pub a", "pub b", "pub c", "rand r", "rand s", "rand t",
  554. ]
  555. .as_slice(),
  556. ["C", "D", "cind A", "cind B"].as_slice(),
  557. );
  558. enforce_disjunction_invariant_tester(
  559. vars,
  560. parse_quote! {
  561. C = x*A
  562. },
  563. parse_quote! {
  564. C = x*A
  565. },
  566. );
  567. enforce_disjunction_invariant_tester(
  568. vars,
  569. parse_quote! {
  570. AND (
  571. C = x*A + r*B,
  572. OR (
  573. y=1,
  574. z=2,
  575. )
  576. )
  577. },
  578. parse_quote! {
  579. AND (
  580. C = x*A + r*B,
  581. OR (
  582. y=1,
  583. z=2,
  584. )
  585. )
  586. },
  587. );
  588. enforce_disjunction_invariant_tester(
  589. vars,
  590. parse_quote! {
  591. AND (
  592. C = x*A + r*B,
  593. OR (
  594. x=1,
  595. x=2,
  596. )
  597. )
  598. },
  599. parse_quote! {
  600. AND (
  601. C = x*A + r*B,
  602. OR (
  603. AND (
  604. gen__disj_x_C = gen__disj1_x * A + gen__disj1_x_r * B,
  605. gen__disj1_x=1,
  606. ),
  607. AND (
  608. gen__disj_x_C = gen__disj2_x * A + gen__disj2_x_r * B,
  609. gen__disj2_x=2,
  610. ),
  611. )
  612. )
  613. },
  614. );
  615. enforce_disjunction_invariant_tester(
  616. vars,
  617. parse_quote! {
  618. AND (
  619. C = x*A,
  620. OR (
  621. x=1,
  622. x=2,
  623. )
  624. )
  625. },
  626. parse_quote! {
  627. AND (
  628. C = x*A,
  629. OR (
  630. AND (
  631. gen__disj_x_C = gen__disj1_x * A + gen__disj1_x_r * B,
  632. gen__disj1_x=1,
  633. ),
  634. AND (
  635. gen__disj_x_C = gen__disj2_x * A + gen__disj2_x_r * B,
  636. gen__disj2_x=2,
  637. ),
  638. ),
  639. gen__disj_x_genC = x*A + gen__disj_x_genr*B,
  640. )
  641. },
  642. );
  643. enforce_disjunction_invariant_tester(
  644. vars,
  645. parse_quote! {
  646. OR (
  647. x=1,
  648. x=2,
  649. )
  650. },
  651. parse_quote! {
  652. AND (
  653. gen__disj_x_genC = x*A + gen__disj_x_genr*B,
  654. OR (
  655. AND (
  656. gen__disj_x_C = gen__disj1_x * A + gen__disj1_x_r * B,
  657. gen__disj1_x=1,
  658. ),
  659. AND (
  660. gen__disj_x_C = gen__disj2_x * A + gen__disj2_x_r * B,
  661. gen__disj2_x=2,
  662. ),
  663. ),
  664. )
  665. },
  666. );
  667. }
  668. }