Model parsing from JSON

Cargo.toml

@@ -6,3 +6,7 @@ edition = "2021"
 [workspace]
 members = ["solvers/kissat", "solvers/minion", "solvers/chuffed"]
 exclude = []
+
+[dependencies]
+serde = { version = "1.0.190", features = ["derive"] }
+serde_json = "1.0.108"

examples/abc.essence

@@ -0,0 +1,5 @@
+find a,b,c : int(1..3)
+such that a + b + c = 4
+such that a >= b
+
+$ conjure pretty --output-format=astjson examples/abc.essence > examples/abc.json

examples/abc.json

@@ -0,0 +1,62 @@
+{"mInfo":
+ {"finds": [], "givens": [], "enumGivens": [], "enumLettings": [], "lettings": [], "unnameds": [],
+ "strategyQ": {"Auto": {"Interactive": []}}, "strategyA": {"Auto": {"Interactive": []}}, "trailCompact": [],
+ "nameGenState": [], "nbExtraGivens": 0, "representations": [], "representationsTree": [], "originalDomains": [],
+ "trailGeneralised": [], "trailVerbose": [], "trailRewrites": []},
+ "mLanguage": {"language": {"Name": "Essence"}, "version": [1, 3]},
+ "mStatements":
+ [{"Declaration":
+ {"FindOrGiven":
+ ["Find", {"Name": "a"},
+ {"DomainInt":
+ [{"TagInt": []},
+ [{"RangeBounded":
+ [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}},
+ {"Constant": {"ConstantInt": [{"TagInt": []}, 3]}}]}]]}]}},
+ {"Declaration":
+ {"FindOrGiven":
+ ["Find", {"Name": "b"},
+ {"DomainInt":
+ [{"TagInt": []},
+ [{"RangeBounded":
+ [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}},
+ {"Constant": {"ConstantInt": [{"TagInt": []}, 3]}}]}]]}]}},
+ {"Declaration":
+ {"FindOrGiven":
+ ["Find", {"Name": "c"},
+ {"DomainInt":
+ [{"TagInt": []},
+ [{"RangeBounded":
+ [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}},
+ {"Constant": {"ConstantInt": [{"TagInt": []}, 3]}}]}]]}]}},
+ {"SuchThat":
+ [{"Op":
+ {"MkOpEq":
+ [{"Op":
+ {"MkOpSum":
+ {"AbstractLiteral":
+ {"AbsLitMatrix":
+ [{"DomainInt":
+ [{"TagInt": []},
+ [{"RangeBounded":
+ [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}},
+ {"Constant": {"ConstantInt": [{"TagInt": []}, 2]}}]}]]},
+ [{"Op":
+ {"MkOpSum":
+ {"AbstractLiteral":
+ {"AbsLitMatrix":
+ [{"DomainInt":
+ [{"TagInt": []},
+ [{"RangeBounded":
+ [{"Constant":
+ {"ConstantInt":
+ [{"TagInt": []}, 1]}},
+ {"Constant":
+ {"ConstantInt":
+ [{"TagInt": []}, 2]}}]}]]},
+ [{"Reference": [{"Name": "a"}, null]},
+ {"Reference": [{"Name": "b"}, null]}]]}}}},
+ {"Reference": [{"Name": "c"}, null]}]]}}}},
+ {"Constant": {"ConstantInt": [{"TagInt": []}, 4]}}]}}]},
+ {"SuchThat":
+ [{"Op": {"MkOpGeq": [{"Reference": [{"Name": "a"}, null]}, {"Reference": [{"Name": "b"}, null]}]}}]}]}

src/common/ast/ast.rs → src/ast/ast.rs

@@ -7,6 +7,13 @@ pub struct Model {
 }
 
 impl Model {
+ pub fn new() -> Self {
+ Model {
+ variables: HashMap::new(),
+ constraints: Vec::new(),
+ }
+ }
+
  // Function to update a DecisionVariable based on its Name
  pub fn update_domain(&mut self, name: &Name, new_domain: Domain) {
  if let Some(decision_var) = self.variables.get_mut(name) {

src/error.rs

@@ -0,0 +1,30 @@
+use serde_json::Error as JsonError;
+use std::fmt::Display;
+
+pub enum Error {
+ Json(JsonError),
+ ParseError(String),
+ Generic(String),
+}
+
+impl From<JsonError> for Error {
+ fn from(e: JsonError) -> Self {
+ Error::Json(e)
+ }
+}
+
+impl From<&str> for Error {
+ fn from(e: &str) -> Self {
+ Error::Generic(e.to_owned())
+ }
+}
+
+impl Display for Error {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+ match &self {
+ Error::Json(e) => write!(f, "serde_json error: {}", e),
+ Error::ParseError(e) => write!(f, "Parse error: {}", e),
+ Error::Generic(e) => write!(f, "Error: {}", e),
+ }
+ }
+}

src/lib.rs

@@ -1,2 +1,6 @@
-mod common;
-pub use common::ast;
+pub mod ast;
+pub mod error;
+pub mod parse;
+
+pub use ast::Model;
+pub use error::Error;

src/main.rs

@@ -1,52 +1,59 @@
-use std::collections::HashMap;
+use std::{collections::HashMap, fs::File, io::Read};
 
-mod common;
-use common::ast::*;
+mod ast;
+mod parse;
+use {ast::Model, parse::*};
 
 fn main() {
+ let mut abc = File::open("examples/abc.json").unwrap();
+ let mut abc_str = String::new();
+ abc.read_to_string(&mut abc_str).unwrap();
+
+ let m = Model::from_json(&abc_str);
+
  // find a,b,c : int(1..3)
  // such that a + b + c = 4
  // such that a >= b
 
- let a = Name::UserName(String::from("a"));
- let b = Name::UserName(String::from("b"));
- let c = Name::UserName(String::from("c"));
+ // let a = Name::UserName(String::from("a"));
+ // let b = Name::UserName(String::from("b"));
+ // let c = Name::UserName(String::from("c"));
 
- let mut variables = HashMap::new();
- variables.insert(
- a.clone(),
- DecisionVariable {
- domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]),
- },
- );
- variables.insert(
- b.clone(),
- DecisionVariable {
- domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]),
- },
- );
- variables.insert(
- c.clone(),
- DecisionVariable {
- domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]),
- },
- );
+ // let mut variables = HashMap::new();
+ // variables.insert(
+ //  a.clone(),
+ //  DecisionVariable {
+ //  domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]),
+ //  },
+ // );
+ // variables.insert(
+ //  b.clone(),
+ //  DecisionVariable {
+ //  domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]),
+ //  },
+ // );
+ // variables.insert(
+ //  c.clone(),
+ //  DecisionVariable {
+ //  domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]),
+ //  },
+ // );
 
- let mut m = Model {
- variables,
- constraints: vec![
- Expression::Eq(
- Box::new(Expression::Sum(vec![
- Expression::Reference(a.clone()),
- Expression::Reference(b.clone()),
- Expression::Reference(c.clone()),
- ])),
- Box::new(Expression::ConstantInt(4)),
- ),
- Expression::Geq(
- Box::new(Expression::Reference(a.clone())),
- Box::new(Expression::Reference(b.clone())),
- ),
- ],
- };
+ // let mut m = Model {
+ //  variables,
+ //  constraints: vec![
+ //  Expression::Eq(
+ //  Box::new(Expression::Sum(vec![
+ //  Expression::Reference(a.clone()),
+ //  Expression::Reference(b.clone()),
+ //  Expression::Reference(c.clone()),
+ //  ])),
+ //  Box::new(Expression::ConstantInt(4)),
+ //  ),
+ //  Expression::Geq(
+ //  Box::new(Expression::Reference(a.clone())),
+ //  Box::new(Expression::Reference(b.clone())),
+ //  ),
+ //  ],
+ // };
 }

src/parse/json.rs

@@ -0,0 +1,28 @@
+use crate::ast::Model;
+use crate::error::Error;
+use serde_json::Value as JsonValue;
+
+pub fn parse_json(str: &String) -> Result<Model, Error> {
+ let v: JsonValue = serde_json::from_str(str)?;
+ let constraints: &Vec<JsonValue> = match &v["mStatements"] {
+ JsonValue::Array(a) => Ok(a),
+ _ => Err(Error::ParseError("mStatements is not an array".to_owned())),
+ }?;
+
+ let mut m = Model::new();
+ for c in constraints {
+ let obj = match c {
+ JsonValue::Object(obj) => Ok(obj),
+ _ => Err("Invalid JSON"),
+ }?;
+ println!("{:?}", c);
+ }
+
+ Ok(m)
+}
+
+impl Model {
+ pub fn from_json(str: &String) -> Result<Model, Error> {
+ parse_json(str)
+ }
+}

src/parse/mod.rs

@@ -0,0 +1,3 @@
+pub mod json;
+
+pub use json::parse_json;

tests/model_tests.rs

@@ -1,7 +1,7 @@
 // Tests for various functionalities of the Model
 
-use std::collections::HashMap;
 use conjure_oxide::ast::*;
+use std::collections::HashMap;
 
 #[test]
 fn modify_domain() {
@@ -11,25 +11,16 @@ fn modify_domain() {
  let d2 = Domain::IntDomain(vec![Range::Bounded(1, 2)]);
 
  let mut variables = HashMap::new();
- variables.insert(
- a.clone(),
- DecisionVariable {
- domain: d1.clone(),
- },
- );
+ variables.insert(a.clone(), DecisionVariable { domain: d1.clone() });
 
  let mut m = Model {
  variables,
  constraints: Vec::new(),
  };
 
- assert!(
- (*m.variables.get(&a).unwrap()).domain == d1
- );
+ assert!((*m.variables.get(&a).unwrap()).domain == d1);
 
  m.update_domain(&a, d2.clone());
 
- assert!(
- (*m.variables.get(&a).unwrap()).domain == d2
- );
+ assert!((*m.variables.get(&a).unwrap()).domain == d2);
 }

tests/rewrite_tests.rs

@@ -90,4 +90,4 @@ fn simplify_expression(expr: Expression) -> Expression {
  ),
  _ => expr,
  }
-}
+}