Skip to content

Commit 589fb1b

Browse files
base line specbot
Signed-off-by: Nikolaj Bjorner <[email protected]>
1 parent 67d77e2 commit 589fb1b

File tree

2 files changed

+39
-0
lines changed

2 files changed

+39
-0
lines changed

genaisrc/myai.genai.mts

+26
Original file line numberDiff line numberDiff line change
@@ -210,4 +210,30 @@ export async function invokeLLMOpt(code: string) {
210210
}
211211
);
212212
return answer.text;
213+
}
214+
215+
export async function invokeLLMClassInvariant(header : string, code : string) {
216+
const answer = await runPrompt(
217+
(_) => {
218+
_.def("HEADER", header);
219+
_.def("CODE", code);
220+
_.$`You are a highly experienced compiler engineer with over 20 years of expertise,
221+
specializing in C and C++ programming. Your deep knowledge of best coding practices
222+
and software engineering principles enables you to produce robust, efficient, and
223+
maintainable code in any scenario.
224+
225+
Please create class invariant methods for the classes used in <CODE>.
226+
The signature of the class invariant methods should be 'bool well_formed()'.
227+
If the code already has class invariant methods, please do not add new ones.
228+
Create only code for the class invariant methods and optionally auxiliary helper functions.
229+
230+
In addition, for each method, provide pre and post conditions.
231+
Include the well_formed() method in the pre and post conditions if it should be included.
232+
`
233+
}, {
234+
system: [],
235+
systemSafety: false
236+
}
237+
);
238+
return answer.text;
213239
}

genaisrc/specbot.genai.mts

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
2+
script({
3+
title: "optimize functions in a file",
4+
files: "src/muz/spacer/spacer_qe_project.cpp"
5+
})
6+
7+
import { invokeLLMClassInvariant} from "./myai.genai.mts";
8+
9+
const headerFile = env.files[0];
10+
const cppFile = env.files[1];
11+
let answer = await invokeLLMClassInvariant(headerFile.content, cppFile.content);
12+
13+
await workspace.writeText(headerFile.filename + ".spec.h", answer);

0 commit comments

Comments
 (0)