1use std::collections::HashMap;
2use std::rc::Rc;
3use std::sync::{Arc, RwLock};
4
5use serde_json::Value;
6use serde_json::Value as JsonValue;
7
8use crate::ast::Declaration;
9use crate::ast::{Atom, Domain, Expression, Literal, Name, Range, SymbolTable};
10use crate::context::Context;
11use crate::error::{Error, Result};
12use crate::metadata::Metadata;
13use crate::Model;
14use crate::{bug, error, throw_error};
15
16macro_rules! parser_trace {
17 ($($arg:tt)+) => {
18 log::trace!(target:"jsonparser",$($arg)+)
19 };
20}
21
22macro_rules! parser_debug {
23 ($($arg:tt)+) => {
24 log::debug!(target:"jsonparser",$($arg)+)
25 };
26}
27
28pub fn model_from_json(str: &str, context: Arc<RwLock<Context<'static>>>) -> Result<Model> {
29 let mut m = Model::new(context);
30 let v: JsonValue = serde_json::from_str(str)?;
31 let statements = v["mStatements"]
32 .as_array()
33 .ok_or(error!("mStatements is not an array"))?;
34
35 for statement in statements {
36 let entry = statement
37 .as_object()
38 .ok_or(error!("mStatements contains a non-object"))?
39 .iter()
40 .next()
41 .ok_or(error!("mStatements contains an empty object"))?;
42
43 match entry.0.as_str() {
44 "Declaration" => {
45 let decl = entry
46 .1
47 .as_object()
48 .ok_or(error!("Declaration is not an object".to_owned()))?;
49
50 let mut valid_decl: bool = false;
57 let submodel = m.as_submodel_mut();
58 for (kind, value) in decl {
59 match kind.as_str() {
60 "FindOrGiven" => {
61 parse_variable(value, &mut submodel.symbols_mut())?;
62 valid_decl = true;
63 break;
64 }
65 "Letting" => {
66 parse_letting(value, &mut submodel.symbols_mut())?;
67 valid_decl = true;
68 break;
69 }
70 _ => continue,
71 }
72 }
73
74 if !valid_decl {
75 throw_error!("Declaration is not a valid kind")?;
76 }
77 }
78 "SuchThat" => {
79 let constraints_arr = match entry.1.as_array() {
80 Some(x) => x,
81 None => bug!("SuchThat is not a vector"),
82 };
83
84 let constraints: Vec<Expression> =
85 constraints_arr.iter().flat_map(parse_expression).collect();
86 m.as_submodel_mut().add_constraints(constraints);
87 }
89 otherwise => bug!("Unhandled Statement {:#?}", otherwise),
90 }
91 }
92
93 Ok(m)
94}
95
96fn parse_variable(v: &JsonValue, symtab: &mut SymbolTable) -> Result<()> {
97 let arr = v.as_array().ok_or(error!("FindOrGiven is not an array"))?;
98 let name = arr[1]
99 .as_object()
100 .ok_or(error!("FindOrGiven[1] is not an object"))?["Name"]
101 .as_str()
102 .ok_or(error!("FindOrGiven[1].Name is not a string"))?;
103
104 let name = Name::UserName(name.to_owned());
105 let domain = arr[2]
106 .as_object()
107 .ok_or(error!("FindOrGiven[2] is not an object"))?
108 .iter()
109 .next()
110 .ok_or(error!("FindOrGiven[2] is an empty object"))?;
111 let domain = match domain.0.as_str() {
112 "DomainInt" => Ok(parse_int_domain(domain.1)?),
113 "DomainBool" => Ok(Domain::BoolDomain),
114 "DomainReference" => Ok(Domain::DomainReference(Name::UserName(
115 domain
116 .1
117 .as_array()
118 .ok_or(error!("DomainReference is not an array"))?[0]
119 .as_object()
120 .ok_or(error!("DomainReference[0] is not an object"))?["Name"]
121 .as_str()
122 .ok_or(error!("DomainReference[0].Name is not a string"))?
123 .into(),
124 ))),
125 _ => throw_error!(
126 "FindOrGiven[2] is an unknown object" ),
128 }?;
129
130 symtab
131 .insert(Rc::new(Declaration::new_var(name.clone(), domain)))
132 .ok_or(Error::Parse(format!(
133 "Could not add {name} to symbol table as it already exists"
134 )))
135}
136
137fn parse_letting(v: &JsonValue, symtab: &mut SymbolTable) -> Result<()> {
138 let arr = v.as_array().ok_or(error!("Letting is not an array"))?;
139 let name = arr[0]
140 .as_object()
141 .ok_or(error!("Letting[0] is not an object"))?["Name"]
142 .as_str()
143 .ok_or(error!("Letting[0].Name is not a string"))?;
144 let name = Name::UserName(name.to_owned());
145
146 if let Some(value) = parse_expression(&arr[1]) {
148 symtab
149 .insert(Rc::new(Declaration::new_value_letting(name.clone(), value)))
150 .ok_or(Error::Parse(format!(
151 "Could not add {name} to symbol table as it already exists"
152 )))
153 } else {
154 let domain = &arr[1]
156 .as_object()
157 .ok_or(error!("Letting[1] is not an object".to_owned()))?["Domain"]
158 .as_object()
159 .ok_or(error!("Letting[1].Domain is not an object"))?
160 .iter()
161 .next()
162 .ok_or(error!("Letting[1].Domain is an empty object"))?;
163
164 let domain = match domain.0.as_str() {
165 "DomainInt" => Ok(parse_int_domain(domain.1)?),
166 "DomainBool" => Ok(Domain::BoolDomain),
167 _ => throw_error!("Letting[1] is an unknown object".to_owned()),
168 }?;
169
170 symtab
171 .insert(Rc::new(Declaration::new_domain_letting(
172 name.clone(),
173 domain,
174 )))
175 .ok_or(Error::Parse(format!(
176 "Could not add {name} to symbol table as it already exists"
177 )))
178 }
179}
180
181fn parse_int_domain(v: &JsonValue) -> Result<Domain> {
182 let mut ranges = Vec::new();
183 let arr = v
184 .as_array()
185 .ok_or(error!("DomainInt is not an array".to_owned()))?[1]
186 .as_array()
187 .ok_or(error!("DomainInt[1] is not an array".to_owned()))?;
188 for range in arr {
189 let range = range
190 .as_object()
191 .ok_or(error!("DomainInt[1] contains a non-object"))?
192 .iter()
193 .next()
194 .ok_or(error!("DomainInt[1] contains an empty object"))?;
195 match range.0.as_str() {
196 "RangeBounded" => {
197 let arr = range
198 .1
199 .as_array()
200 .ok_or(error!("RangeBounded is not an array".to_owned()))?;
201 let mut nums = Vec::new();
202 for item in arr.iter() {
203 let num = parse_domain_value_int(item)
204 .ok_or(error!("Could not parse int domain constant"))?;
205 nums.push(num);
206 }
207 ranges.push(Range::Bounded(nums[0], nums[1]));
208 }
209 "RangeSingle" => {
210 let num = parse_domain_value_int(range.1)
211 .ok_or(error!("Could not parse int domain constant"))?;
212 ranges.push(Range::Single(num));
213 }
214 _ => return throw_error!("DomainInt[1] contains an unknown object"),
215 }
216 }
217 Ok(Domain::IntDomain(ranges))
218}
219
220fn parse_domain_value_int(obj: &JsonValue) -> Option<i32> {
231 parser_trace!("trying to parse domain value: {}", obj);
232
233 fn try_parse_positive_int(obj: &JsonValue) -> Option<i32> {
234 parser_trace!(".. trying as a positive domain value: {}", obj);
235 let leaf_node = obj.pointer("/Constant/ConstantInt/1")?;
238
239 match leaf_node.as_i64()?.try_into() {
240 Ok(x) => {
241 parser_trace!(".. success!");
242 Some(x)
243 }
244 Err(_) => {
245 println!(
246 "Could not convert integer constant to i32: {:#?}",
247 leaf_node
248 );
249 None
250 }
251 }
252 }
253
254 fn try_parse_negative_int(obj: &JsonValue) -> Option<i32> {
255 parser_trace!(".. trying as a negative domain value: {}", obj);
262 let inner_constant_node = obj.pointer("/Op/MkOpNegate")?;
263 let inner_num = try_parse_positive_int(inner_constant_node)?;
264
265 parser_trace!(".. success!");
266 Some(-inner_num)
267 }
268
269 try_parse_positive_int(obj).or_else(|| try_parse_negative_int(obj))
270}
271
272type BinOp = Box<dyn Fn(Metadata, Box<Expression>, Box<Expression>) -> Expression>;
274type UnaryOp = Box<dyn Fn(Metadata, Box<Expression>) -> Expression>;
275type VecOp = Box<dyn Fn(Metadata, Vec<Expression>) -> Expression>;
276
277fn parse_expression(obj: &JsonValue) -> Option<Expression> {
278 let binary_operators: HashMap<&str, BinOp> = [
279 (
280 "MkOpEq",
281 Box::new(Expression::Eq) as Box<dyn Fn(_, _, _) -> _>,
282 ),
283 (
284 "MkOpNeq",
285 Box::new(Expression::Neq) as Box<dyn Fn(_, _, _) -> _>,
286 ),
287 (
288 "MkOpGeq",
289 Box::new(Expression::Geq) as Box<dyn Fn(_, _, _) -> _>,
290 ),
291 (
292 "MkOpLeq",
293 Box::new(Expression::Leq) as Box<dyn Fn(_, _, _) -> _>,
294 ),
295 (
296 "MkOpGt",
297 Box::new(Expression::Gt) as Box<dyn Fn(_, _, _) -> _>,
298 ),
299 (
300 "MkOpLt",
301 Box::new(Expression::Lt) as Box<dyn Fn(_, _, _) -> _>,
302 ),
303 (
304 "MkOpGt",
305 Box::new(Expression::Gt) as Box<dyn Fn(_, _, _) -> _>,
306 ),
307 (
308 "MkOpLt",
309 Box::new(Expression::Lt) as Box<dyn Fn(_, _, _) -> _>,
310 ),
311 (
312 "MkOpDiv",
313 Box::new(Expression::UnsafeDiv) as Box<dyn Fn(_, _, _) -> _>,
314 ),
315 (
316 "MkOpMod",
317 Box::new(Expression::UnsafeMod) as Box<dyn Fn(_, _, _) -> _>,
318 ),
319 (
320 "MkOpMinus",
321 Box::new(Expression::Minus) as Box<dyn Fn(_, _, _) -> _>,
322 ),
323 (
324 "MkOpImply",
325 Box::new(Expression::Imply) as Box<dyn Fn(_, _, _) -> _>,
326 ),
327 (
328 "MkOpPow",
329 Box::new(Expression::UnsafePow) as Box<dyn Fn(_, _, _) -> _>,
330 ),
331 ]
332 .into_iter()
333 .collect();
334
335 let unary_operators: HashMap<&str, UnaryOp> = [
336 (
337 "MkOpNot",
338 Box::new(Expression::Not) as Box<dyn Fn(_, _) -> _>,
339 ),
340 (
341 "MkOpNegate",
342 Box::new(Expression::Neg) as Box<dyn Fn(_, _) -> _>,
343 ),
344 (
345 "MkOpTwoBars",
346 Box::new(Expression::Abs) as Box<dyn Fn(_, _) -> _>,
347 ),
348 ]
349 .into_iter()
350 .collect();
351
352 let vec_operators: HashMap<&str, VecOp> = [
353 (
354 "MkOpSum",
355 Box::new(Expression::Sum) as Box<dyn Fn(_, _) -> _>,
356 ),
357 (
358 "MkOpProduct",
359 Box::new(Expression::Product) as Box<dyn Fn(_, _) -> _>,
360 ),
361 (
362 "MkOpAnd",
363 Box::new(Expression::And) as Box<dyn Fn(_, _) -> _>,
364 ),
365 ("MkOpOr", Box::new(Expression::Or) as Box<dyn Fn(_, _) -> _>),
366 (
367 "MkOpMin",
368 Box::new(Expression::Min) as Box<dyn Fn(_, _) -> _>,
369 ),
370 (
371 "MkOpMax",
372 Box::new(Expression::Max) as Box<dyn Fn(_, _) -> _>,
373 ),
374 (
375 "MkOpAllDiff",
376 Box::new(Expression::AllDiff) as Box<dyn Fn(_, _) -> _>,
377 ),
378 ]
379 .into_iter()
380 .collect();
381
382 let mut binary_operator_names = binary_operators.iter().map(|x| x.0);
383 let mut unary_operator_names = unary_operators.iter().map(|x| x.0);
384 let mut vec_operator_names = vec_operators.iter().map(|x| x.0);
385
386 match obj {
387 Value::Object(op) if op.contains_key("Op") => match &op["Op"] {
388 Value::Object(bin_op) if binary_operator_names.any(|key| bin_op.contains_key(*key)) => {
389 parse_bin_op(bin_op, binary_operators)
390 }
391 Value::Object(un_op) if unary_operator_names.any(|key| un_op.contains_key(*key)) => {
392 parse_unary_op(un_op, unary_operators)
393 }
394 Value::Object(vec_op) if vec_operator_names.any(|key| vec_op.contains_key(*key)) => {
395 parse_vec_op(vec_op, vec_operators)
396 }
397 otherwise => bug!("Unhandled Op {:#?}", otherwise),
398 },
399 Value::Object(refe) if refe.contains_key("Reference") => {
400 let name = refe["Reference"].as_array()?[0].as_object()?["Name"].as_str()?;
401 Some(Expression::Atomic(
402 Metadata::new(),
403 Atom::Reference(Name::UserName(name.to_string())),
404 ))
405 }
406 Value::Object(constant) if constant.contains_key("Constant") => parse_constant(constant),
407 Value::Object(constant) if constant.contains_key("ConstantInt") => parse_constant(constant),
408 Value::Object(constant) if constant.contains_key("ConstantBool") => {
409 parse_constant(constant)
410 }
411 _ => None,
412 }
413}
414
415fn parse_bin_op(
416 bin_op: &serde_json::Map<String, Value>,
417 binary_operators: HashMap<&str, BinOp>,
418) -> Option<Expression> {
419 let (key, value) = bin_op.into_iter().next()?;
422
423 let constructor = binary_operators.get(key.as_str())?;
424
425 match &value {
426 Value::Array(bin_op_args) if bin_op_args.len() == 2 => {
427 let arg1 = parse_expression(&bin_op_args[0])?;
428 let arg2 = parse_expression(&bin_op_args[1])?;
429 Some(constructor(Metadata::new(), Box::new(arg1), Box::new(arg2)))
430 }
431 otherwise => bug!("Unhandled parse_bin_op {:#?}", otherwise),
432 }
433}
434
435fn parse_unary_op(
436 un_op: &serde_json::Map<String, Value>,
437 unary_operators: HashMap<&str, UnaryOp>,
438) -> Option<Expression> {
439 let (key, value) = un_op.into_iter().next()?;
440 let constructor = unary_operators.get(key.as_str())?;
441
442 let arg = parse_expression(value)?;
443 Some(constructor(Metadata::new(), Box::new(arg)))
444}
445
446fn parse_vec_op(
447 vec_op: &serde_json::Map<String, Value>,
448 vec_operators: HashMap<&str, VecOp>,
449) -> Option<Expression> {
450 let (key, value) = vec_op.into_iter().next()?;
451 let constructor = vec_operators.get(key.as_str())?;
452
453 parser_debug!("Trying to parse vec_op: {key} ...");
454
455 let mut args_parsed: Option<Vec<Option<Expression>>> = None;
456 if let Some(abs_lit_matrix) = value.pointer("/AbstractLiteral/AbsLitMatrix/1") {
457 parser_trace!("... containing a matrix of literals");
458 args_parsed = abs_lit_matrix.as_array().map(|x| {
459 x.iter()
460 .map(parse_expression)
461 .collect::<Vec<Option<Expression>>>()
462 });
463 }
464 else if let Some(const_abs_lit_matrix) =
466 value.pointer("/Constant/ConstantAbstract/AbsLitMatrix/1")
467 {
468 parser_trace!("... containing a matrix of constants");
469 args_parsed = const_abs_lit_matrix.as_array().map(|x| {
470 x.iter()
471 .map(parse_expression)
472 .collect::<Vec<Option<Expression>>>()
473 });
474 }
475
476 let args_parsed = args_parsed?;
477
478 let number_of_args = args_parsed.len();
479 parser_debug!("... with {number_of_args} args {args_parsed:#?}");
480
481 let valid_args: Vec<Expression> = args_parsed.into_iter().flatten().collect();
482 if number_of_args != valid_args.len() {
483 None
484 } else {
485 parser_debug!("... success!");
486 Some(constructor(Metadata::new(), valid_args))
487 }
488}
489
490fn parse_constant(constant: &serde_json::Map<String, Value>) -> Option<Expression> {
491 match &constant.get("Constant") {
492 Some(Value::Object(int)) if int.contains_key("ConstantInt") => {
493 let int_32: i32 = match int["ConstantInt"].as_array()?[1].as_i64()?.try_into() {
494 Ok(x) => x,
495 Err(_) => {
496 println!(
497 "Could not convert integer constant to i32: {:#?}",
498 int["ConstantInt"]
499 );
500 return None;
501 }
502 };
503
504 Some(Expression::Atomic(
505 Metadata::new(),
506 Atom::Literal(Literal::Int(int_32)),
507 ))
508 }
509
510 Some(Value::Object(b)) if b.contains_key("ConstantBool") => {
511 let b: bool = b["ConstantBool"].as_bool()?;
512 Some(Expression::Atomic(
513 Metadata::new(),
514 Atom::Literal(Literal::Bool(b)),
515 ))
516 }
517
518 None => {
521 let int_expr = constant["ConstantInt"]
522 .as_array()
523 .and_then(|x| x[1].as_i64())
524 .and_then(|x| x.try_into().ok())
525 .map(|x| Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(x))));
526
527 if let e @ Some(_) = int_expr {
528 return e;
529 }
530
531 let bool_expr = constant["ConstantBool"]
532 .as_bool()
533 .map(|x| Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(x))));
534
535 if let e @ Some(_) = bool_expr {
536 return e;
537 }
538
539 bug!("Unhandled parse_constant {:#?}", constant);
540 }
541 otherwise => bug!("Unhandled parse_constant {:#?}", otherwise),
542 }
543}