mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 14:13:23 +00:00
mild refactoring
This commit is contained in:
parent
0e881e7abb
commit
eb97fcc273
3 changed files with 40 additions and 18 deletions
36
genaisrc/genaiscript.d.ts
generated
vendored
36
genaisrc/genaiscript.d.ts
generated
vendored
|
@ -1,6 +1,6 @@
|
||||||
/**
|
/**
|
||||||
* GenAIScript Ambient Type Definition File
|
* GenAIScript Ambient Type Definition File
|
||||||
* @version 1.114.2
|
* @version 1.115.0
|
||||||
*/
|
*/
|
||||||
type OptionsOrString<TOptions extends string> = (string & {}) | TOptions
|
type OptionsOrString<TOptions extends string> = (string & {}) | TOptions
|
||||||
|
|
||||||
|
@ -108,6 +108,7 @@ type SystemPromptId = OptionsOrString<
|
||||||
| "system.annotations"
|
| "system.annotations"
|
||||||
| "system.assistant"
|
| "system.assistant"
|
||||||
| "system.changelog"
|
| "system.changelog"
|
||||||
|
| "system.cooperation"
|
||||||
| "system.diagrams"
|
| "system.diagrams"
|
||||||
| "system.diff"
|
| "system.diff"
|
||||||
| "system.english"
|
| "system.english"
|
||||||
|
@ -1936,6 +1937,10 @@ interface ParsePDFOptions {
|
||||||
* Disable caching with cache: false
|
* Disable caching with cache: false
|
||||||
*/
|
*/
|
||||||
cache?: boolean
|
cache?: boolean
|
||||||
|
/**
|
||||||
|
* Force system fonts use
|
||||||
|
*/
|
||||||
|
useSystemFonts?: boolean
|
||||||
}
|
}
|
||||||
|
|
||||||
interface HTMLToTextOptions {
|
interface HTMLToTextOptions {
|
||||||
|
@ -3319,7 +3324,23 @@ interface HighlightOptions {
|
||||||
maxLength?: number
|
maxLength?: number
|
||||||
}
|
}
|
||||||
|
|
||||||
interface VectorSearchOptions extends EmbeddingsModelOptions {
|
interface WorkspaceFileIndex {
|
||||||
|
list: () => Promise<WorkspaceFile[]>
|
||||||
|
upsert: (file: ElementOrArray<WorkspaceFile>) => Promise<void>
|
||||||
|
query: (
|
||||||
|
query: string,
|
||||||
|
options?: { topK?: number; minScore?: number }
|
||||||
|
) => Promise<WorkspaceFileWithScore[]>
|
||||||
|
}
|
||||||
|
|
||||||
|
interface VectorIndexOptions extends EmbeddingsModelOptions {
|
||||||
|
version?: number
|
||||||
|
deleteIfExists?: boolean
|
||||||
|
chunkSize?: number
|
||||||
|
chunkOverlap?: number
|
||||||
|
}
|
||||||
|
|
||||||
|
interface VectorSearchOptions extends VectorIndexOptions {
|
||||||
/**
|
/**
|
||||||
* Maximum number of embeddings to use
|
* Maximum number of embeddings to use
|
||||||
*/
|
*/
|
||||||
|
@ -3328,11 +3349,6 @@ interface VectorSearchOptions extends EmbeddingsModelOptions {
|
||||||
* Minimum similarity score
|
* Minimum similarity score
|
||||||
*/
|
*/
|
||||||
minScore?: number
|
minScore?: number
|
||||||
|
|
||||||
/**
|
|
||||||
* Cache identifier for the embeddings
|
|
||||||
*/
|
|
||||||
cache?: string
|
|
||||||
}
|
}
|
||||||
|
|
||||||
interface FuzzSearchOptions {
|
interface FuzzSearchOptions {
|
||||||
|
@ -3407,6 +3423,12 @@ interface Retrieval {
|
||||||
options?: VectorSearchOptions
|
options?: VectorSearchOptions
|
||||||
): Promise<WorkspaceFile[]>
|
): Promise<WorkspaceFile[]>
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Loads or creates a file index using a vector index
|
||||||
|
* @param options
|
||||||
|
*/
|
||||||
|
index(id: string, options?: VectorIndexOptions): Promise<WorkspaceFileIndex>
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Performs a fuzzy search over the files
|
* Performs a fuzzy search over the files
|
||||||
* @param query keywords to search
|
* @param query keywords to search
|
||||||
|
|
|
@ -25,18 +25,18 @@ Notes:
|
||||||
static void display_anums(std::ostream & out, scoped_anum_vector const & rs) {
|
static void display_anums(std::ostream & out, scoped_anum_vector const & rs) {
|
||||||
out << "numbers in decimal:\n";
|
out << "numbers in decimal:\n";
|
||||||
algebraic_numbers::manager & m = rs.m();
|
algebraic_numbers::manager & m = rs.m();
|
||||||
for (unsigned i = 0; i < rs.size(); i++) {
|
for (const auto& r : rs) {
|
||||||
m.display_decimal(out, rs[i], 10);
|
m.display_decimal(out, r, 10);
|
||||||
out << "\n";
|
out << "\n";
|
||||||
}
|
}
|
||||||
out << "numbers as root objects\n";
|
out << "numbers as root objects\n";
|
||||||
for (unsigned i = 0; i < rs.size(); i++) {
|
for (const auto& r : rs) {
|
||||||
m.display_root(out, rs[i]);
|
m.display_root(out, r);
|
||||||
out << "\n";
|
out << "\n";
|
||||||
}
|
}
|
||||||
out << "numbers as intervals\n";
|
out << "numbers as intervals\n";
|
||||||
for (unsigned i = 0; i < rs.size(); i++) {
|
for (const auto& r : rs) {
|
||||||
m.display_interval(out, rs[i]);
|
m.display_interval(out, r);
|
||||||
out << "\n";
|
out << "\n";
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -158,8 +158,8 @@ struct gomory_test {
|
||||||
TRACE("gomory_cut_detail", tout << "pol.size() > 1" << std::endl;);
|
TRACE("gomory_cut_detail", tout << "pol.size() > 1" << std::endl;);
|
||||||
lcm_den = lcm(lcm_den, denominator(k));
|
lcm_den = lcm(lcm_den, denominator(k));
|
||||||
TRACE("gomory_cut_detail", tout << "k: " << k << " lcm_den: " << lcm_den << "\n";
|
TRACE("gomory_cut_detail", tout << "k: " << k << " lcm_den: " << lcm_den << "\n";
|
||||||
for (unsigned i = 0; i < pol.size(); i++) {
|
for (const auto& p : pol) {
|
||||||
tout << pol[i].first << " " << pol[i].second << "\n";
|
tout << p.first << " " << p.second << "\n";
|
||||||
}
|
}
|
||||||
tout << "k: " << k << "\n";);
|
tout << "k: " << k << "\n";);
|
||||||
lp_assert(lcm_den.is_pos());
|
lp_assert(lcm_den.is_pos());
|
||||||
|
@ -172,8 +172,8 @@ struct gomory_test {
|
||||||
k *= lcm_den;
|
k *= lcm_den;
|
||||||
}
|
}
|
||||||
TRACE("gomory_cut_detail", tout << "after *lcm\n";
|
TRACE("gomory_cut_detail", tout << "after *lcm\n";
|
||||||
for (unsigned i = 0; i < pol.size(); i++) {
|
for (const auto& p : pol) {
|
||||||
tout << pol[i].first << " * v" << pol[i].second << "\n";
|
tout << p.first << " * v" << p.second << "\n";
|
||||||
}
|
}
|
||||||
tout << "k: " << k << "\n";);
|
tout << "k: " << k << "\n";);
|
||||||
|
|
||||||
|
@ -210,7 +210,7 @@ struct gomory_test {
|
||||||
bool some_int_columns = false;
|
bool some_int_columns = false;
|
||||||
mpq f_0 = fractional_part(get_value(inf_col));
|
mpq f_0 = fractional_part(get_value(inf_col));
|
||||||
mpq one_min_f_0 = 1 - f_0;
|
mpq one_min_f_0 = 1 - f_0;
|
||||||
for ( auto pp : row) {
|
for (const auto& pp : row) {
|
||||||
a = pp.first;
|
a = pp.first;
|
||||||
x_j = pp.second;
|
x_j = pp.second;
|
||||||
if (x_j == inf_col)
|
if (x_j == inf_col)
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue