using System using System.Text using System.IO using Nemerle.Logging using Nemerle.Utility using Nemerle.Collections using Fx7.Parser.SExpr set namespace Fx7 /* TODO: */ public partial class Parser class SmtDumper static margin = 120 static tab = 1 class Sort mutable parent : Sort public mutable name : string public this (n : string = null) name = n parent = this public Root : Sort get if (parent.parent : object == parent) parent else parent = parent.Root parent public Unify (line : int, other : Sort, desc : string) : void if (Root : object == other.Root) {} else def n1 = Root.name def n2 = other.Root.name if (n1 != n2 && n1 != null && n2 != null) throw FatalError ($ "line $line: expected $n1 got $n2 [in $(desc)]") else if (n1 != null) other.Root.parent = Root else Root.parent = other.Root public CanUnify (other : Sort) : bool if (Root : object == other.Root) true else def n1 = Root.name def n2 = other.Root.name n1 == n2 || n1 == null || n2 == null [Nemerle.OverrideObjectEquals] \ public Equals (other : Sort) : bool Root : object == other.Root || Root.name == other.Root.name && Root.name != null public override GetHashCode () : int Root.name.GetHashCode () public override ToString () : string if (Root.name == null) "Int" //"UNKNOWN" else Root.name [Record] \ class FunDesc public name : string public arg_types : list [Sort] public ret_type : Sort public is_varargs : bool public dont_print : bool functions : Hashtable [string, FunDesc] = Hashtable () casts : Hashtable [Sort * Sort, FunDesc] = Hashtable () name_meaning : Hashtable [string, string] = Hashtable () name_translation : Hashtable [string, string] = Hashtable () parser : Parser mangling_exceptions : Hashtable [string, object] = [ "!=" ].FoldLeft (Hashtable (), fun (s, a) { a.Add (s, null); a }) public this (parser : Parser) this.parser = parser Fail['a] (msg : string) : 'a throw FatalError (msg) [Record (Include = [line])] \ [ExtensionPattern (name !! args = Term (name, args, []))] \ variant Smt | Var name : string | Term name : string args : list [Smt] annot : list [string * string] | Quant forall : bool vars : list [string * Sort] form : Smt annot : list [string * string] public line : int mutable length : int [Nemerle.OverrideObjectEquals] \ public Equals (other : Smt) : bool match ((this, other)) | (Var (n), Var (n')) => n == n' | (Term (name, args, annot), Term (name', args', annot')) => name == name' && args.Equals (args') && annot.Equals (annot') | (Quant (forall, vars, form, annot), Quant (forall', vars', form', annot')) => forall == forall' && vars.Equals (vars') && form.Equals (form') && annot.Equals (annot') | _ => false public Simplify () : Smt def t (name, args) Term (line, name, args, []) match (this) | Var => this | Quant (forall, vars, form, annot) => Quant (line, forall, vars, form.Simplify (), annot) | Term (name, args, annot) => match (Term (line, name, args.Map (_.Simplify ()), annot)) | "or" !! args \ | "and" !! args => def args = args.FoldLeft ([], (arg, acc) => match (arg : Smt) { | name' !! args when name == name' => List.RevAppend (args, acc) | "true" !! [] when name == "and" => acc | arg => arg :: acc }) match (args) | [a] => a | [] => assert (name == "and"); t ("true", []) | lst => t (name, lst.Rev ()) | "implies" !! ["implies" !! [a, b], b'] when b.Equals (b') => t ("or", [b, a]).Simplify () | "implies" !! [a, "implies" !! [b, c]] => t ("implies", [t ("and", [a, b]).Simplify (), c]) | "iff" !! [f, "true" !! []] \ | "iff" !! ["true" !! [], f] \ | "implies" !! ["true" !! [], f] => f | x => x // estimated length, for pretty printing public Length : int get when (length == 0) length = match (this) | Var (name) => name.Length + 1 | Term (name, [], []) => name.Length | Term (name, args, []) => name.Length + 2 + args.Map (_.Length).FoldLeft (0, (x, y) => x + y + 1) | Quant | Term => 10000 length Print (sb : StringBuilder) : void def finish (annot) foreach ((n, v) in annot) def v = v.Replace ("{", "\\{").Replace ("}", "\\}") _ = sb.Append ($ " :$n {$v}") _ = sb.Append (")") match (this) | Var (name) => _ = sb.Append ("?").Append (name) | Term (name, [], []) => _ = sb.Append (name) | Term (name, args, annot) => _ = sb.Append ("(").Append (name) foreach (a in args) _ = sb.Append (" ") a.Print (sb) finish (annot) | Quant (forall, vars, form, annot) => _ = sb.Append ("(").Append (if (forall) "forall" else "exists") foreach ((n, t) in vars) _ = sb.Append ($" (?$n $t)") _ = sb.Append (" ") form.Print (sb) finish (annot) PrintWithIndent (ind : int, sb : StringBuilder) : void def ind = if (ind > margin / 2) margin / 2 else ind def finish (annot) foreach ((n, v) in annot) def v = v.Replace ("{", "\\{").Replace ("}", "\\}") _ = sb.Append (' ', ind + tab).Append ($ ":$n {$v}\n") // replace last '\n' with ')' assert (sb [sb.Length - 1] == '\n') sb [sb.Length - 1] = ')' _ = sb.Append ('\n') match (this) | Var \ | Term (_, [], []) \ | _ when Length + ind < margin => _ = sb.Append (' ', ind) Print (sb) _ = sb.Append ('\n') | Term (name, args, annot) => _ = sb.Append (' ', ind).Append ('(').Append (name).Append ('\n') args.Iter (_.PrintWithIndent (ind + tab, sb)) finish (annot) | Quant (forall, vars, form, annot) => _ = sb.Append (' ', ind).Append ('(').Append (if (forall) "forall" else "exists") foreach ((n, t) in vars) _ = sb.Append ($" (?$n $t)") _ = sb.Append ('\n') form.PrintWithIndent (ind + tab, sb) finish (annot) public ToString (indent : int) : string def sb = StringBuilder () PrintWithIndent (indent, sb) sb.ToString () public override ToString () : string def sb = StringBuilder () Print (sb) sb.ToString () Pred : Sort = Sort ("BOOL") Int : Sort = Sort ("Int") Object : Sort = Int //Sort ("Object") Infer (vars : Map [string, Sort], t : SExpr, expected : Sort) : Smt def const (n) Smt.Term (t.line, n, [], []) def cast (act, res, msg, exp = expected) if (exp.CanUnify (act)) exp.Unify (t.line, act, msg) res else if (exp.Equals (Pred) && act.Equals (Object)) Smt.Term (t.line, "=", [const ("Smt.true"), res], []) else if (exp.Equals (Object) && act.Equals (Pred)) log (WARN, $ "line $(t.line) converting object to BOOL") Smt.Term (t.line, "ite", [res, const ("Smt.true"), const ("Smt.false")], []) else // "" is passed for casting result of select which is OK //when (msg != "") // log (TEMP, $ "line $(t.line): casting $msg from $(act) to $(exp)") if (casts.Contains ((act, exp))) Smt.Term (t.line, casts [(act,exp)].name, [res], []) else Fail ($"line $(t.line): casting $msg from $(act) to $(exp): cannot find such a cast") def parse_pats (vars, pats) def to_string (p) Infer (vars, p, Sort ()).ToString () match (pats : SExpr) | "PATS" ::: parms => parms.Map (fun (_ : SExpr) { | "MPAT" ::: args | x with args = [x] => ("pat", args.Map (to_string).ToString (" ")) }) | "NOPATS" ::: parms => parms.Map (p => ("nopat", to_string (p))) | _ => Fail ($"line $(t.line): wrong pats: $pats") def is_select (_) | Smt.Term ("select", _, _) \ | Smt.Term ("select2", _, _) => true | _ => false def application (name, args) if (name == "=") def t1 = Sort () def t2 = Sort () expected.Unify (t.line, Pred, "result of =") match (args) | [a1, a2] => def a1 = Infer (vars, a1, t1) def a2 = Infer (vars, a2, t2) if (t1.Equals (Pred) && a2 is Term ("Smt.true", [], [])) a1 else if (t2.Equals (Pred) && a1 is Term ("Smt.true", [], [])) a2 else if (t1.Equals (Pred) || t2.Equals (Pred)) Smt.Term (t.line, "iff", [cast (t1, a1, "=/iff arg", Pred), cast (t2, a2, "=/iff arg", Pred)], []) else if (t1.CanUnify (t2)) t1.Unify (t.line, t2, "ble") Smt.Term (t.line, "=", [a1, a2], []) else if (is_select (a1)) Smt.Term (t.line, "=", [a2, cast (t1, a1, "", t2)], []) else if (is_select (a2)) Smt.Term (t.line, "=", [a1, cast (t2, a2, "", t1)], []) else Smt.Term (t.line, "=", [a1, cast (t2, a2, "= paramater", t1)], []) | _ => Fail ("wrong number of params to =") else unless (functions.Contains (name)) functions [name] = FunDesc (name, args.Map (_ => Sort ()), Sort (), false, false) def fn = functions [name] def res = if (fn.is_varargs) Smt.Term (t.line, name, List.Map (args, a => Infer (vars, a, fn.arg_types.Head)), []) else when (fn.arg_types.Length != args.Length) Fail ($ "line $(t.line): $(fn.name) requires " "$(fn.arg_types.Length) args, got $(args.Length)") Smt.Term (t.line, name, List.Map2 (fn.arg_types, args, (t, a) => Infer (vars, a, t)), []) def res = if (name == "and" || name == "or") Smt.Term (t.line, name, List.Flatten (res.args.Map (_ => { | Smt.Term (name', args, []) when name == name' => args | t => [t] })), []) else res def msg = if (name == "select" || name == "select2") "" else $"result of $name" cast (fn.ret_type, res, msg) match (t) | Name (n) => if (vars.Contains (n)) cast (vars.Get (n), Smt.Var (t.line, n), $"forall variable $n") else when (!functions.Contains (n) && n.ForAll (is_digit)) functions [n] = FunDesc (n, [], Int, false, true) application (n, []) | name ::: _ when \ parser.kill_list.Contains (name) && \ parser.kill_list [name].Exists (_.Equals (t)) => Infer (vars, Name (t.line, "true"), expected) // single- and no- argument distinct doesn't make much sense | "distinct" ::: [] \ | "distinct" ::: [_] => Infer (vars, Name (t.line, "true"), expected) | "multiply" ::: ([Name (arg), _] as args) when arg.ForAll (char.IsDigit) \ | "multiply" ::: ([_, Name (arg)] as args) when arg.ForAll (char.IsDigit) => Infer (vars, l ("*", args), expected) | "ORDER" ::: _ => Fail ("ORDER unsupported") | "LBL" ::: [_, arg] \ | "LBLPOS" ::: [_, arg] \ | "LBLNEG" ::: [_, arg] => Infer (vars, arg, expected) | "!=" ::: [a, b] => Infer (vars, l ("not", l ("=", a, b)), expected) | "-" ::: [a] => Infer (vars, l ("~", a), expected) | "explies" ::: [a, b] => Infer (vars, l ("implies", b, a), expected) | "forall" ::: [qvars, pats, form] with forall = true \ | "forall" ::: [qvars, form] with (forall = true, pats = null) \ | "exists" ::: [qvars, pats, form] with forall = false \ | "exists" ::: [qvars, form] with (forall = false, pats = null) => expected.Unify (t.line, Pred, "quantified formula return type") def qvars = match (qvars) | Cons (lst) => def seen = Hashtable () lst.FoldLeft ([], fun (e, acc) { match (e) { | Name (v) => if (seen.Contains (v)) acc else { seen [v] = v; (v, Sort ()) :: acc } | x => Fail ($ "line $(x.line): evil thing in quant var list") } }).Rev () | x => Fail ($ "line $(x.line): evil thing in quant var list") def vars = qvars.FoldLeft (vars, fun ((v, t), acc) { acc.Replace (v, t) }) def pats = if (pats == null) [] else parse_pats (vars, pats) Smt.Quant (t.line, forall, qvars, Infer (vars, form, Pred), pats) | name ::: args => application (name, args) | Cons (Cons :: _) | Cons ([]) => Fail ($ "junk in input $t, line $(t.line)") // no Unicode, please static is_digit (_ : char) : bool | '0' | '1' | '2' | '3' | '4' | '5' \ | '6' | '7' | '8' | '9' => true | _ => false NormalizeName (orig : string) : string def orig = if (orig.StartsWith ("|") && orig.EndsWith ("|")) orig.Substring (1, orig.Length - 2) else orig mutable res if (name_translation.TryGetValue (orig, out res)) res else def is_op (_) | '=' | '<' | '>' | '&' | '@' | '#' | '+' | '-' \ | '*' | '/' | '%' | '|' | '~' => true | _ => false def is_alpha (c : char) def c = c :> int (c >= 'A' :> int && c <= 'Z' :> int) || (c >= 'a' :> int && c <= 'z' :> int) def n = orig def n = if (n == "") Fail ("empty name!") else if (parser.renamings.Contains (n)) parser.renamings [n] else if (n.ForAll (is_op) || n.ForAll (is_digit) || mangling_exceptions.Contains (n)) n else def sb = StringBuilder (n.Length) def n = if (is_alpha (n [0])) n else if (n.Exists (is_alpha)) def loop (i) if (is_alpha (n [i])) n.Substring (i) else loop (i + 1) loop (0) + "_" else "a." + n foreach (c in n) if (is_alpha (c) || is_digit (c) || c == '.' || c == '\'' || c == '_') _ = sb.Append (c) else _ = sb.Append ('_') sb.ToString () if (name_meaning.Contains (n)) res = n for (mutable k = 1; name_meaning.Contains (res); k++) res = n + "." + k.ToString () //log (INFO, $ "the names: '$orig' and '$(name_meaning[n])' both mangle to '$n', switching to '$res'") else res = n name_meaning [res] = orig name_translation [orig] = res res NormalizeNames (sexpr : SExpr) : SExpr | Name (orig) => if (orig.Length >= 2 && orig.StartsWith ("-") && orig.Substring (1).ForAll (is_digit)) l ("~", Name (sexpr.line, orig.Substring (1))) else Name (sexpr.line, NormalizeName (orig)) | Cons (children) => Cons (sexpr.line, children.Map (NormalizeNames)) public AddFun (args : list [SExpr], var_args = false, is_cast = false) : void def predef = [ "and", "or", "xor", "not", "implies", "iff", "true", "false", "distinct", "<", ">", "<=", ">=", "+", "-", "*", "~" /* , "select", "store", "select2", "store2", "subtypes" */ ] def args = args.Map (n => { | Name (n) => n | _ => Fail ("wrong FUN") }) def name = args.Head def args = args.Tail.Map (Sort) def (args, ret) = args.DivideLast () def fd = FunDesc (name, args, ret, var_args, is_cast || var_args || predef.Contains (name)) functions [name] = fd when (is_cast) casts [(args.Head, ret)] = fd public Run (axioms : list [SExpr], formula : SExpr) : void def f (a) Infer (Map (), NormalizeNames (a), Pred) def name = if (parser.filename == null) "simplify_benchmark" else parser.filename def name = name.Replace (".sx","") def name = if (Driver.SmtStartNo == 0) name else def name = string.Format ("{0}.{1:000}", name, Driver.SmtStartNo) Driver.SmtStartNo++ name def the_name = System.IO.Path.GetFileName (name) def filename = name + ".smt" System.Console.WriteLine ($"Dumping to: $filename") def axioms = axioms.Map (f) def formula = f (formula) def file = FileStream (filename, FileMode.Create, FileAccess.Write) def writer = StreamWriter (file, Encoding.ASCII) writer.Write ( $ @"(benchmark $(NormalizeName (the_name)) :source { $(Driver.SmtComment) This benchmark was translated by Michal Moskal. } :logic AUFLIA :status unknown :difficulty { 5 } :category { industrial } ; ------------------------------------------------------------------------ ; Extra functions/predicates ; ------------------------------------------------------------------------ ") functions.Iter ((_, f) => unless (f.dont_print) { when (f.arg_types.Exists (_.Equals (Pred))) Fail ($ "function $(f.name) has BOOL type"); if (f.ret_type.Equals (Pred)) writer.Write ($ ":extrapreds (( $(f.name) $(f.arg_types.ToString (\" \")) ))\n") else writer.Write ($ ":extrafuns (( $(f.name) $(f.arg_types.ToString (\" \")) $(f.ret_type) ))\n") }) def axioms = List.Flatten (axioms.Map (_ => { | Smt.Term ("and", children, []) => children | t => [t] })) writer.Write ( @" ; ------------------------------------------------------------------------ ; Assumptions ; ------------------------------------------------------------------------ ") foreach (a in axioms) if (a.Length < margin - 12) writer.Write ($ ":assumption $a\n") else writer.Write ($ ":assumption\n$(a.ToString(2))") writer.Write ( @" ; ------------------------------------------------------------------------ ; Formula ; ------------------------------------------------------------------------ ") // uncomment to get simplified (in boolean sense) formulas, easier for reading // def formula = formula.Simplify () writer.Write ($ ":formula\n$(formula.ToString(2))\n)\n") writer.Close ()