Constant mikino_api::SCRIPT_DEMO

pub const SCRIPT_DEMO: &str = "//! A simple demo hsmt script.\n//!\n//! An hsmt script is a Rust-flavored syntax for (a subset of) [SMT-LIB 2][smtlib]. Such scripts\n//! allow to perform *satisfiability checks* on formulas; this is done with three basic commands.\n//! \n//! All commands can be written function-style `command(args)` or block-style `command { args }`.\n//! Some commands also allow `command!(args)` and `command! { args }` such as `check_sat!()`,\n//! `get_model!()`, `println!(...)`... and all commands that produce an output or exit the script\n//! (including `panic!(\"message\")`).\n//! \n//! The script below showcases all commands available. Note that hsmt scripts, unlike SMT-LIB 2\n//! scripts, can branch using if-then-else(-otherwise). Conditions in branchings can only be\n//! check-sat results. Also unlike SMT-LIB 2, hsmt scripts let you bind (name) check-sat results\n//! in a (meta-)variable usable in branchings.\n//!\n//! [smtlib]: https://smtlib.cs.uiowa.edu/language.shtml\n//! (SMT-LIB\'s official website)\n\n\n/// First, *declaring variables* (*constants* in SMT-LIB 2) is necessary to later write formulas\n/// that use these variables.\nvars {\n\t/// Current counter value.\n\tcnt: int,\n\t/// Next counter value.\n\tnext_cnt: int,\n\t/// True if resetting.\n\treset: bool,\n\t/// True if counting.\n\tcounting: bool,\n}\n\n/// Next, we write formulas and *assert* them. This tells the solver *\"I want this formula to be\n/// true\"*.\nassert {\n\t// This `=` is **NOT** an assignment. It is a **constraint** comparing the value of `next_cnt`\n\t// to the value of the right-hand side. It does **NOT** \"set\" `next_cnt`\'s value. In a context\n\t// where `next_cnt`\'s value is `7` and `reset` is true for instance, then this formula becomes\n\t// `7 = 0`, which is `false`.\n\t//       v\n\tnext_cnt = if reset {\n\t\t0 // resetting\n\t} else if counting {\n\t\tcnt + 1 // incrementing\n\t} else {\n\t\tcnt // stuttering\n\t}\n}\n\n/// `assert { ... }` actually accepts a comma-separated list (with optional trailing comma) of\n/// formulas, making it convenient to assert more than one formula.\nassert {\n\t// `cnt` is positive\n\tcnt \u{2265} 0,\n\t// `next_cnt` is not positive\n\t\u{ac}(next_cnt \u{2265} 0),\n}\n\n\n/// So far, we have asserted what `next_cnt` is based on `cnt`, `reset` and `counting`. We have\n/// also asserted that `cnt` is positive or zero, and that `next_cnt` is strictly negative. We now\n/// *check sat* to ask the solver *\"can all of these formulas be true for valuation of the\n/// variables?\".\ncheck_sat!()\n// outputs `unsat`\n\n\n/// Solver says it\'s not possible: we just proved that with this definition of `next_cnt`, it is\n/// not possible to get a strictly negative value assuming `cnt` is itself positive.\n/// \n/// Interestingly, hsmt scripts provides *branching* (if-then-else) on check sat results, so we\n/// can communicate this result explicitly.\nif check_sat!() {\n\t// sat case\n\techo!(\"`next_cnt` can be *strictly* negative \u{1f63f}\")\n\t// produce a model\n\tget_model!()\n} else {\n\t// unsat case\n\techo!(\"`next_cnt` can only be **positive or zero** \u{1f638}\")\n} otherwise {\n\t// this *optional* `otherwise` branch triggers when the check sat returns `unknown` or\n\t// `timeout`. Here, we decide to *panic* with a message, which ends the script with an error.\n\tpanic!(\"solver was not able to decide satisfiability of this easy check \u{1f640}\")\n}\n\n/// Hsmt scripts even let you (meta-)bind check sat results to meta-variables using `let ... =\n/// ...;`.\nlet is_sat = check_sat!();\n\n/// Meta-variables can then be used in branching.\nif is_sat {\n\t// Can use `println!` instead of `echo!`.\n\tprintln!(\"sat \u{1f63f}\")\n\tget_model!()\n} else {\n\tprintln!(\"unsat \u{1f638}\")\n}\n// No `otherwise` branch, will panic if the check sat was inconclusive.\n\n\necho!(\"**reset**ting solver\")\nreset!()\n\n// This just echoes a newline.\necho!()\necho!(\"nothing declared or asserted at this point\")\n\n/// Nothing there, should be sat.\nif check_sat!() {\n\techo!(\"*of course* it\'s **sat**\")\n} else {\n\tpanic!(\"no way this is **unsat**\")\n} otherwise {\n\techo!(\"epic fail, this check was so easy\")\n\t/// We can exit with a unix-style signed integer exit code.\n\texit!(2)\n}\n\n\n/// Let\'s declare/assert almost the same things as previously.\nvars {\n\tcnt next_cnt: int,\n\treset counting: bool,\n}\n\nassert {\n\tnext_cnt =\n\t\tif reset {\n\t\t\t0\n\t\t} else if counting {\n\t\t\tcnt + 1\n\t\t} else {\n\t\t\tcnt\n\t\t}\n\t,\n\t// `cnt` is **strictly** positive\n\tcnt > 0,\n\t// `next_cnt` is not **strictly** positive\n\t\u{ac}(next_cnt > 0),\n}\n\n/// What do you think?\nlet not_strictly_positive = check_sat!();\n\n/// Let\'s take a look.\nif not_strictly_positive {\n\techo!(\"yeah, `next_cnt` can actually be not **strictly** positive if `reset`:\")\n\tget_model!()\n} else {\n\tpanic!(\"unreachable\")\n}\n\n\n/// Let\'s get some values.\neval! {\n\tcnt,\n\tcnt + 2,\n\tcnt \u{2265} 0,\n\tif \u{ac}reset {\n\t\t11\n\t} else {\n\t\t7 * (cnt + next_cnt)\n\t},\n}\n\n/// You can also use `get_values` or `get_value` for that.\nget_values! {\n\tcnt * (next_cnt + 7),\n}\n\n/// Let\'s force `reset` to be false.\necho!(\"if we forbid `reset`ting, `next_cnt` should always be strictly positive\")\nassert {\n\t\u{ac}reset\n}\n\n/// This time `next_cnt` can only be strictly positive.\nif check_sat!() {\n\tpanic!(\"unreachable\")\n} else {\n\techo!(\"indeed it is\")\n}\n\n\necho!()\necho!(\"all done here\")\n\n/// We can omit the `exit!` code, which is the same as `exit!(0)`.\nexit!()\n";

String representation of a simple demo script.