mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
adding mergeopt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
01ba749a5d
commit
9fad15e2ca
BIN
genaisrc/genaiscript.d.ts
generated
vendored
BIN
genaisrc/genaiscript.d.ts
generated
vendored
Binary file not shown.
57
genaisrc/mergeopt.genai.mts
Normal file
57
genaisrc/mergeopt.genai.mts
Normal file
|
@ -0,0 +1,57 @@
|
||||||
|
script({
|
||||||
|
title: "Merge optimizations function changes for a C++ file"
|
||||||
|
})
|
||||||
|
|
||||||
|
// given a source file <src>
|
||||||
|
// list files in code_slice directory based on that name with extension opt
|
||||||
|
// replace functions in src by the corresponding ones in the opt files.
|
||||||
|
// Save into <dst>
|
||||||
|
|
||||||
|
|
||||||
|
import * as fs from 'fs';
|
||||||
|
|
||||||
|
|
||||||
|
function get_functions(captures : QueryCapture[], code : string) {
|
||||||
|
return captures.map(({ name, node }) => ({
|
||||||
|
code : node.text,
|
||||||
|
start : node.startIndex,
|
||||||
|
end : node.endIndex,
|
||||||
|
name : node.text.split('(')[0].trim()
|
||||||
|
}))
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
const inputFile = env.files[0];
|
||||||
|
|
||||||
|
const { captures: functions } = await parsers.code(
|
||||||
|
inputFile,
|
||||||
|
`(function_definition) @function`
|
||||||
|
);
|
||||||
|
|
||||||
|
|
||||||
|
let funs = get_functions(functions, inputFile.content);
|
||||||
|
|
||||||
|
const modifiedFunctions = "slice_" + path.basename(inputFile.filename) + "*.opt";
|
||||||
|
|
||||||
|
let inputCode = inputFile.content;
|
||||||
|
console.log(modifiedFunctions);
|
||||||
|
const directory_path = path.join("code_slices", modifiedFunctions);
|
||||||
|
const files = await workspace.findFiles(directory_path);
|
||||||
|
for (const file of files) {
|
||||||
|
console.log(file.filename);
|
||||||
|
const code = file.content.match(/```cpp([\s\S]*?)```/);
|
||||||
|
if (!code) {
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
const modifiedFunction = code[1];
|
||||||
|
const name = modifiedFunction.split('(')[0].trim();
|
||||||
|
console.log(name);
|
||||||
|
const fun = funs.find(f => f.name === name);
|
||||||
|
if (fun) {
|
||||||
|
console.log("Updated function: " + name);
|
||||||
|
inputCode = inputCode.replace(fun.code, modifiedFunction);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
console.log(inputCode);
|
||||||
|
await workspace.writeText(inputFile.filename + ".opt.cpp", inputCode);
|
|
@ -28,7 +28,5 @@ async function invokeLLMUpdate(code) {
|
||||||
const inputFile = env.files[0];
|
const inputFile = env.files[0];
|
||||||
const file = await workspace.readText(inputFile);
|
const file = await workspace.readText(inputFile);
|
||||||
const answer = await invokeLLMUpdate(file.content);
|
const answer = await invokeLLMUpdate(file.content);
|
||||||
// Extract the code from the answer by removing ```cpp and ```:
|
|
||||||
let code = answer.replace(/```cpp/g, "").replace(/```/g, "");
|
|
||||||
const outputFile = inputFile.filename + ".opt";
|
const outputFile = inputFile.filename + ".opt";
|
||||||
await workspace.writeText(outputFile, code);
|
await workspace.writeText(outputFile, answer);
|
||||||
|
|
|
@ -25,11 +25,10 @@ for (const fun of funs) {
|
||||||
let name = fun.code.split('(')[0].trim();
|
let name = fun.code.split('(')[0].trim();
|
||||||
name = name
|
name = name
|
||||||
.replace(/::/g, '_')
|
.replace(/::/g, '_')
|
||||||
.replace(/ /g, '_');
|
.replace(/ /g, '_')
|
||||||
let outputFile = path.basename(inputFile.filename)
|
.replace(/\*/g, '');
|
||||||
.replace(/\.cpp$/, `.${name}.cpp`)
|
console.log(name);
|
||||||
.replace(/\.h$/, `.${name}.h`);
|
let outputFile = "slice_" + path.basename(inputFile.filename) + name + ".cpp";
|
||||||
outputFile = "slice_" + outputFile;
|
|
||||||
outputFile = path.join("code_slices", outputFile);
|
outputFile = path.join("code_slices", outputFile);
|
||||||
|
|
||||||
await workspace.writeText(outputFile, `//Extracted ${name} in ${inputFile.filename}\n${fun.code}\n\n`);
|
await workspace.writeText(outputFile, `//Extracted ${name} in ${inputFile.filename}\n${fun.code}\n\n`);
|
||||||
|
|
Loading…
Reference in a new issue