more Ostrich compatibility

pruemmer · Dec 12, 2020 · f3c0c48 · f3c0c48
1 parent 39e279c
commit f3c0c48
Show file tree

Hide file tree

Showing 4 changed files with 67 additions and 66 deletions.
diff --git a/lib/model.js b/lib/model.js
@@ -32,6 +32,9 @@ function parsePrimitive(value) {
             contents = contents.replace(/\\x([a-fA-F0-9]{2})/g, (a, b) => {
                 return String.fromCharCode(parseInt(b, 16));
             });
+            contents = contents.replace(/\\u\{([a-fA-F0-9]+)\}/g, (a, b) => {
+                return String.fromCharCode(parseInt(b, 16));
+            });
             contents = contents.replace(/\\b/g, "\b");
             contents = contents.replace(/\\e/g, "\x1B");
             contents = contents.replace(/\\n/g, "\n");

diff --git a/lib/smt.js b/lib/smt.js
@@ -97,7 +97,7 @@ exports.SMTSolver = class SMTSolver {
             this._commandLogs[i].write(output, "utf8");
         }
 // Enable to see the SMT-LIB commands
-//        console.error(output);
+	fs.appendFileSync("smt-log.smt2", output);
         this.process.stdin.write(output);
     }
 

diff --git a/lib/smt2/ostrich/prelude.smt2 b/lib/smt2/ostrich/prelude.smt2
@@ -23,4 +23,4 @@
 (define-sort Properties () (Array String MaybeVal))
 (declare-fun GetProperties (Int) Properties)
 
-(declare-fun EmptyObject () Properties) ; not supported: ((as const Properties) Nothing))
+(define-fun EmptyObject () Properties ((as const Properties) Nothing))
diff --git a/package-lock.json b/package-lock.json