add prd (#7649)

* add prd

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* missing text

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #7647

* fix #7647 - with respect to scope level

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

genaisrc/prd.genai.mts

@@ -0,0 +1,37 @@
+script({
+    title: "Pull Request Descriptor",
+    description: "Generate a description for the current pull request",
+    systemSafety: true,
+    parameters: {
+        base: "",
+    },
+})
+const { dbg, vars } = env
+const base = vars.base || (await git.defaultBranch())
+const changes = await git.diff({
+    base,
+    llmify: true,
+})
+if (!changes) cancel("No changes found in the pull request")
+dbg(`changes: %s`, changes)
+const gitDiff = def("GIT_DIFF", changes, {
+    language: "diff",
+    maxTokens: 14000,
+    detectPromptInjection: "available",
+})
+$`## Task
+
+You are an expert code reviewer with great English technical writing skills.
+
+Your task is to generate a high level summary of the changes in ${gitDiff} for a pull request in a way that a software engineer will understand.
+This description will be used as the pull request description.
+
+## Instructions
+
+- do NOT explain that GIT_DIFF displays changes in the codebase
+- try to extract the intent of the changes, don't focus on the details
+- use bullet points to list the changes
+- use gitmojis to make the description more engaging
+- focus on the most important changes
+- do not try to fix issues, only describe the changes
+- ignore comments about imports (like added, remove, changed, etc.)`

genaisrc/tsconfig.json

@@ -11,14 +11,11 @@
         "allowJs": true,
         "skipLibCheck": true,
         "noEmit": true,
-        "allowImportingTsExtensions": true,
-        "verbatimModuleSyntax": true,
-        "resolveJsonModule": true,
-        "erasableSyntaxOnly": true
+        "allowImportingTsExtensions": true
     },
     "include": [
-        "**/*.mjs",
-        "**/*.mts",
+        "*.mjs",
+        "*.mts",
         "./genaiscript.d.ts"
     ]
 }

src/cmd_context/simplifier_cmds.cpp

@@ -156,8 +156,13 @@ public:
         auto simplifier_factory = sexpr2simplifier(ctx, m_simplifier);
         ctx.init_manager();
         auto* s = ctx.get_solver();
-        if (s)
-            ctx.set_solver(mk_simplifier_solver(s, &simplifier_factory));        
+        if (!s)
+            return;
+        if (s->get_num_assertions() > 0) 
+            throw cmd_exception("set-simplifier cannot be invoked if there are already assertions");
+        if (s->get_scope_level() > 0)
+            throw cmd_exception("set-simplifier cannot be invoked above base scope level");
+        ctx.set_solver(mk_simplifier_solver(s, &simplifier_factory));        
     }
 };