3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00

genai testing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-02-12 19:55:39 -08:00
parent 4e51af1167
commit 5c18ce8cea
2 changed files with 50 additions and 24 deletions

View file

@ -1,33 +1,21 @@
script({ script({
title: "Invoke LLM code update", title: "Invoke LLM code update",
files: "src/muz/spacer/spacer_qe_project.cpp"
}) })
async function runCodePrompt(role, message, code) { async function invokeLLMUpdate(code) {
const answer = await runPrompt( const answer = await runPrompt(
(_) => { (_) => {
_.def("ROLE", role); _.def("CODE", code);
_.def("REQUEST", message); _.$`
_.def("CODE", code); You are a highly experienced compiler engineer with over 20 years of expertise,
_.$`Your role is <ROLE>.
The request is given by <REQUEST>
original code:
<CODE>.`
}
)
console.log(answer.text);
return answer.text;
}
async function invokeLLMUpdate(code, inputFile) {
let role = `You are a highly experienced compiler engineer with over 20 years of expertise,
specializing in C and C++ programming. Your deep knowledge of best coding practices specializing in C and C++ programming. Your deep knowledge of best coding practices
and software engineering principles enables you to produce robust, efficient, and and software engineering principles enables you to produce robust, efficient, and
maintainable code in any scenario.`; maintainable code in any scenario.
let userMessage = `Please modify the original code to ensure that it enforces the following: Please modify the original code in <CODE> to ensure that it enforces the following:
- do not use pointer arithmetic. - do not use pointer arithmetic.
- do not introduce uses of std::vector. - do not introduce uses of std::vector.
- do not remove comments from the code. - do not remove comments from the code.
@ -80,17 +68,21 @@ async function invokeLLMUpdate(code, inputFile) {
for (auto arg : *a) { for (auto arg : *a) {
... ...
} }
`; `
}, {
return runCodePrompt(role, userMessage, code); system: [],
systemSafety: false
}
)
console.log(answer.text);
return answer.text;
} }
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, inputFile); const answer = await invokeLLMUpdate(file.content);
// Extract the code from the answer by removing ```cpp and ```: // Extract the code from the answer by removing ```cpp and ```:
let code = answer.replace(/```cpp/g, "").replace(/```/g, ""); let code = answer.replace(/```cpp/g, "").replace(/```/g, "");
const outputFile = inputFile.filename + ".patch"; const outputFile = inputFile.filename + ".patch";
await workspace.writeText(outputFile, code); await workspace.writeText(outputFile, code);

34
genaisrc/myopt.genai.mts Normal file
View file

@ -0,0 +1,34 @@
script({
title: "Invoke LLM code optimization",
files: "code_slices/muz/spacer/orig_spacer_antiunify.cpp_anti_unifier.cpp"
})
async function invokeLLMUpdate(code) {
const answer = await runPrompt(
(_) => {
_.def("CODE", code);
_.$`
You are a highly experienced compiler engineer with over 20 years of expertise,
specializing in C and C++ programming. Your deep knowledge of best coding practices
and software engineering principles enables you to produce robust, efficient, and
maintainable code in any scenario.
Please modify the original code in <CODE> to ensure that it uses best practices for optimal code execution.' `
}, {
system: [],
systemSafety: false
}
)
console.log(answer.text);
return answer.text;
}
const inputFile = env.files[0];
const file = await workspace.readText(inputFile);
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 + ".patch";
await workspace.writeText(outputFile, code);