mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fixes to opt-tool

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-02-13 22:24:02 -08:00
parent 719ea6a2a7
commit 6b9ce8638f
2 changed files with 23 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
genaisrc/myai.genai.mts
View file

@ -64,7 +64,7 @@ async function parseOptFunctions(inputFile: WorkspaceFile) {
import * as fs from 'fs'; import * as fs from 'fs';
export async function mergeModifiedFunction(code :string, funs : { code: string, name: string }[], new_code : string) { export async function mergeModifiedFunction(code: string, funs: { code: string, name: string }[], new_code: string) {
let name = function_name_from_code(new_code); let name = function_name_from_code(new_code);
let fun = funs.find(f => f.name === name); let fun = funs.find(f => f.name === name);
if (fun) { if (fun) {
@ -74,30 +74,32 @@ export async function mergeModifiedFunction(code :string, funs : { code: string,
return code; return code;
} }
async function canCompileCode(inputFile : WorkspaceFile, code : string) { async function canCompileCode(inputFile: WorkspaceFile, new_code: string) {
//
// move input file to a temp file // move input file to a temp file
// move code to the inputFile.filename // move code to the inputFile.filename
// invoke ninja in the build directory: ninja -b build // invoke ninja in the build directory: ninja -b build
// move the temp file back to the original file // move the temp file back to the original file
// return true iff it succeeded // return true iff it succeeded
//
let tempFile = inputFile.filename + ".tmp"; let tempFile = inputFile.filename + ".tmp";
let original_content = inputFile.content; let old_code = inputFile.content;
await workspace.writeText(tempFile, inputFile.content); await workspace.writeText(tempFile, old_code);
await workspace.writeText(inputFile.filename, code); await workspace.writeText(inputFile.filename, new_code);
let result = await host.exec(`cmd /k "C:\Program\ Files/Microsoft\ Visual\ Studio/2022/Enterprise/Common7/Tools/VsDevCmd.bat" -arch=x64 & ninja`, { cwd: "build" }); let result = await host.exec(`cmd /k "C:\Program\ Files/Microsoft\ Visual\ Studio/2022/Enterprise/Common7/Tools/VsDevCmd.bat" -arch=x64 & ninja`, { cwd: "build" });
await workspace.writeText(inputFile.filename, old_code);
// await fs.delete(tempFile); if (result.exitCode == 0) {
if (result.exitCode !== 0) { await workspace.writeText(tempFile, new_code);
await workspace.writeText(inputFile.filename, original_content); return true;
console.log(result.stderr);
return false;
} }
return true; console.log(result.stderr);
return false;
} }
export async function mergeCompileFunction(inputFile : WorkspaceFile, code : string, funs : { code: string, name: string }[], new_code_input : string) { export async function mergeCompileFunction(inputFile: WorkspaceFile, code: string, funs: { code: string, name: string }[], new_code_input: string) {
let match_new_code = new_code_input.match(/```cpp([\s\S]*?)```/); let match_new_code = new_code_input.match(/```cpp([\s\S]*?)```/);
if (!match_new_code) { if (!match_new_code) {
console.log("Invalid new code"); console.log("Invalid new code");
@ -110,8 +112,10 @@ export async function mergeCompileFunction(inputFile : WorkspaceFile, code : str
if (!fun) { if (!fun) {
console.log(`Function name '${name}' not found`); console.log(`Function name '${name}' not found`);
for (const fun of funs) console.log("Available functions: ");
for (const fun of funs)
console.log("'" + fun.name + "'"); console.log("'" + fun.name + "'");
console.log(new_code);
return code; return code;
} }
console.log("Updated function: " + name); console.log("Updated function: " + name);
@ -122,15 +126,15 @@ export async function mergeCompileFunction(inputFile : WorkspaceFile, code : str
} }
let canCompile = await canCompileCode(inputFile, modified_code); let canCompile = await canCompileCode(inputFile, modified_code);
console.log("Can compile: " + canCompile); console.log("Can compile: " + canCompile);
if (canCompile) if (canCompile)
return modified_code; return modified_code;
return code; return code;
} }
export async function mergeFunctionsFromList(inputCode: string, funs: { code: string, name: string }[], modifiedFunctionList: string[]) { export async function mergeFunctionsFromList(inputCode: string, funs: { code: string, name: string }[], modifiedFunctionList: string[]) {
let code = inputCode; let code = inputCode;
for (const new_code of modifiedFunctionList) for (const new_code of modifiedFunctionList)
code = await mergeModifiedFunction(code, funs, new_code); code = await mergeModifiedFunction(code, funs, new_code);
return code; return code;
} }
@ -140,7 +144,7 @@ export async function mergeFunctions(inputFile: WorkspaceFile) {
return mergeFunctionsFromList(inputFile.content, funs, modifiedFunctionList); return mergeFunctionsFromList(inputFile.content, funs, modifiedFunctionList);
} }
export async function invokeLLMOpt(code : string) { export async function invokeLLMOpt(code: string) {
const answer = await runPrompt( const answer = await runPrompt(
(_) => { (_) => {
_.def("CODE", code); _.def("CODE", code);

2
genaisrc/myopttool.genai.mts
View file

@ -15,4 +15,4 @@ for (const fun of funs) {
new_code = await mergeCompileFunction(inputFile, new_code, funs, answer); new_code = await mergeCompileFunction(inputFile, new_code, funs, answer);
} }
await workspace.writeText(inputFile.filename + "opt.cpp", new_code); await workspace.writeText(inputFile.filename + ".opt.cpp", new_code);