mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

Merge branch 'Z3Prover:master' into master

Browse source
This commit is contained in:
davedets 2026-06-09 15:45:16 -07:00 • committed by GitHub
commit 9c5653a65a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
27 changed files with 542 additions and 155 deletions
Download patch file Download diff file Expand all files Collapse all files

17
.github/skills/memory-safety/scripts/memory_safety.py vendored
View file

@ -18,7 +18,7 @@ import time
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parent.parent.parent / "shared"))
from z3db import Z3DB, setup_logging
from z3db import Z3DB, require_repo_root, setup_logging
logger = logging.getLogger("z3agent")
@ -52,19 +52,6 @@ def check_dependencies():
sys.exit(1)
def find_repo_root() -> Path:
d = Path.cwd()
for _ in range(10):
if (d / "CMakeLists.txt").exists() and (d / "src").is_dir():
return d
parent = d.parent
if parent == d:
break
d = parent
logger.error("could not locate Z3 repository root")
sys.exit(1)
def build_is_configured(build_dir: Path, sanitizer: str) -> bool:
"""Check whether the build directory already has a matching cmake config."""
cache = build_dir / "CMakeCache.txt"
@ -220,7 +207,7 @@ def main():
setup_logging(args.debug)
check_dependencies()
repo_root = find_repo_root()
repo_root = require_repo_root()
sanitizers = ["asan", "ubsan"] if args.sanitizer == "both" else [args.sanitizer]
all_findings = []

18
.github/skills/shared/z3db.py vendored
View file

@ -3,7 +3,7 @@
z3db: shared library and CLI for Z3 skill scripts.
Library usage:
from z3db import Z3DB, find_z3, run_z3
from z3db import Z3DB, find_z3, find_repo_root, require_repo_root, run_z3
CLI usage:
python z3db.py init
@ -131,7 +131,7 @@ class Z3DB:
"""Write to stderr and to the interaction_log table."""
getattr(logger, level, logger.info)(message)
self.conn.execute(
"INSERT INTO interaction_log (run_id, level, message) " "VALUES (?, ?, ?)",
"INSERT INTO interaction_log (run_id, level, message) VALUES (?, ?, ?)",
(run_id, level, message),
)
self.conn.commit()
@ -182,7 +182,7 @@ def find_z3(hint: str = None) -> str:
if hint:
candidates.append(hint)
repo_root = _find_repo_root()
repo_root = find_repo_root()
if repo_root:
for build_dir in ["build", "build/release", "build/debug"]:
candidates.append(str(repo_root / build_dir / "z3"))
@ -201,7 +201,8 @@ def find_z3(hint: str = None) -> str:
sys.exit(1)
def _find_repo_root() -> Optional[Path]:
def find_repo_root() -> Optional[Path]:
"""Best-effort search for the Z3 repository root from the current directory."""
d = Path.cwd()
for _ in range(10):
if (d / "CMakeLists.txt").exists() and (d / "src").is_dir():
@ -213,6 +214,15 @@ def _find_repo_root() -> Optional[Path]:
return None
def require_repo_root() -> Path:
"""Return the Z3 repository root or exit the process if it is not found."""
repo_root = find_repo_root()
if repo_root is None:
logger.error("could not locate Z3 repository root")
sys.exit(1)
return repo_root
def run_z3(
formula: str,
z3_bin: str = None,

4
.github/skills/static-analysis/scripts/static_analysis.py vendored
View file

@ -176,9 +176,7 @@ def print_findings(findings: list):
return
for f in findings:
label = f["category"]
if f["type"]:
label = f["type"]
label = f["type"] or f["category"]
print(f"[{label}] {f['file']}:{f['line']}: {f['description']}")
print()

94
.github/workflows/fstar-master-build.yml vendored
View file

@ -28,7 +28,7 @@ on:
fstar_otherflags:
description: "Extra FStar OTHERFLAGS"
required: false
default: "--split_queries --log_failing_queries --ext higher_order_smt --proof_recovery"
default: "--split_queries on_failure --log_failing_queries --ext higher_order_smt --proof_recovery"
discussion_category:
description: Discussion category name
required: false
@ -86,6 +86,8 @@ jobs:
/tmp/gh-aw/agent/z3-bin/z3 --version
- name: Build FStar
id: build_fstar
continue-on-error: true
run: |
set -euo pipefail
rm -rf /tmp/gh-aw/agent/FStar
@ -105,19 +107,97 @@ jobs:
test -x /tmp/gh-aw/agent/FStar/out/bin/fstar.exe || { echo "Error: FStar binary not found or not executable at /tmp/gh-aw/agent/FStar/out/bin/fstar.exe"; exit 1; }
/tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt
- name: Collect generated SMT2 files
id: collect_smt2
if: always()
run: |
set -euo pipefail
rm -rf /tmp/gh-aw/agent/smt2-artifact
mkdir -p /tmp/gh-aw/agent/smt2-artifact
SMT2_PREVIEW=/tmp/gh-aw/agent/smt2-preview.md
SMT2_HEAD_LINES=1000
> "$SMT2_PREVIEW"
if [ -d /tmp/gh-aw/agent/FStar ]; then
mapfile -t SMT2_FILES < <(find /tmp/gh-aw/agent/FStar -type f -name '*.smt2' | sort)
else
SMT2_FILES=()
fi
if [ "${#SMT2_FILES[@]}" -eq 0 ]; then
echo "has_files=false" >> "$GITHUB_OUTPUT"
exit 0
fi
for file in "${SMT2_FILES[@]}"; do
rel="${file#/tmp/gh-aw/agent/FStar/}"
target="/tmp/gh-aw/agent/smt2-artifact/${rel}"
mkdir -p "$(dirname "$target")"
cp "$file" "$target"
{
printf '#### `%s`\n\n' "$rel"
printf '```smt2\n'
head -n "$SMT2_HEAD_LINES" "$file"
printf '\n```\n\n'
} >> "$SMT2_PREVIEW"
done
echo "has_files=true" >> "$GITHUB_OUTPUT"
- name: Upload generated SMT2 artifact
id: upload_smt2
if: always() && steps.collect_smt2.outputs.has_files == 'true'
uses: actions/upload-artifact@v4
with:
name: fstar-generated-smt2-${{ github.run_id }}
path: /tmp/gh-aw/agent/smt2-artifact
if-no-files-found: error
retention-days: 7
- name: Create discussion summary
if: always()
uses: actions/github-script@v9
env:
RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }}
SMT2_ARTIFACT_ID: ${{ steps.upload_smt2.outputs.artifact-id }}
with:
script: |
const fs = require('fs');
const z3VersionText = fs.readFileSync('/tmp/gh-aw/agent/z3-version.txt', 'utf8').trim();
const fstarVersionFile = fs.readFileSync('/tmp/gh-aw/agent/fstar-version.txt', 'utf8').trim();
const readIfExists = (path) => fs.existsSync(path) ? fs.readFileSync(path, 'utf8').trim() : null;
const z3VersionText = readIfExists('/tmp/gh-aw/agent/z3-version.txt') ?? 'unknown';
const fstarVersionFile = readIfExists('/tmp/gh-aw/agent/fstar-version.txt') ?? '';
const fstarVersionText = fstarVersionFile ? fstarVersionFile.split('\n')[0] : 'unknown';
const fstarCommitLine = fs.readFileSync('/tmp/gh-aw/agent/fstar-commit.txt', 'utf8').trim();
const fstarCommit = fstarCommitLine.replace(/^FStar commit:\s*/, '');
const fstarCommitLine = readIfExists('/tmp/gh-aw/agent/fstar-commit.txt') ?? '';
const fstarCommit = fstarCommitLine ? fstarCommitLine.replace(/^FStar commit:\s*/, '') : 'unknown';
const fstarBuildOutcome = process.env.FSTAR_BUILD_OUTCOME || 'unknown';
const fstarBuildSucceeded = fstarBuildOutcome === 'success';
const fstarStatus = fstarBuildSucceeded
? '✅ FStar build completed'
: `⚠️ FStar build ${fstarBuildOutcome} (pipeline continued)`;
const smt2ArtifactId = (process.env.SMT2_ARTIFACT_ID || '').trim();
const smt2ArtifactUrl = smt2ArtifactId ? `${process.env.RUN_URL}/artifacts/${smt2ArtifactId}` : '';
const smt2PreviewFile = '/tmp/gh-aw/agent/smt2-preview.md';
const maxPreviewChars = 55000; // Keep below GitHub's 65536-character discussion body limit, leaving room for non-preview sections.
let smt2Preview = readIfExists(smt2PreviewFile) ?? '';
const smt2PreviewChars = Array.from(smt2Preview);
if (smt2PreviewChars.length > maxPreviewChars) {
smt2Preview = `${smt2PreviewChars.slice(0, maxPreviewChars).join('')}\n\n... (truncated due to discussion size limits)`;
}
const smt2Section = smt2ArtifactId
? [
`### Generated SMT2 files`,
`- Artifact: ${smt2ArtifactUrl}`,
``,
`First 1000 lines per generated \`.smt2\` file:`,
``,
smt2Preview || '_No preview content available._'
].join('\n')
: [
`### Generated SMT2 files`,
`- No generated \`.smt2\` files were found.`
].join('\n');
const date = new Date().toISOString().slice(0, 10);
const owner = context.repo.owner;
@ -146,7 +226,7 @@ jobs:
const body = [
`### Build status`,
`- ✅ Z3 build completed`,
`- ✅ FStar build completed`,
`- ${fstarStatus}`,
``,
`### Inputs used`,
`- z3_ref: \`${process.env.Z3_REF}\``,
@ -161,6 +241,8 @@ jobs:
`- FStar: \`${fstarVersionText}\``,
`- FStar commit: \`${fstarCommit}\``,
``,
smt2Section,
``,
`### Run`,
`- Workflow run: ${process.env.RUN_URL}`
].join('\n');

68
.github/workflows/memory-safety-report.lock.yml generated vendored
View file

@ -1,4 +1,4 @@
# gh-aw-metadata: {"schema_version":"v4","frontmatter_hash":"3ed9f3a1cb53ff5095a4ff6a8169b75a50977baeddb965694ad30555729d56e4","body_hash":"3fece373efec3e8c9950482fd433a5bb06b3eb702a2e638af34815f937642fbe","compiler_version":"v0.77.5","strict":true,"agent_id":"copilot"}
# gh-aw-metadata: {"schema_version":"v4","frontmatter_hash":"01e10498ee43530594fb5994a345b01b5718ffabe2872be157994f5489d81dad","body_hash":"f43683a4995003e2678ccce2706b639eb627b48daeafc7f9dded40d4508ef26c","compiler_version":"v0.77.5","strict":true,"agent_id":"copilot"}
# gh-aw-manifest: {"version":1,"secrets":["COPILOT_GITHUB_TOKEN","GH_AW_GITHUB_MCP_SERVER_TOKEN","GH_AW_GITHUB_TOKEN","GITHUB_TOKEN"],"actions":[{"repo":"actions/cache/restore","sha":"27d5ce7f107fe9357f9df03efb73ab90386fccae","version":"v5.0.5"},{"repo":"actions/cache/save","sha":"27d5ce7f107fe9357f9df03efb73ab90386fccae","version":"v5.0.5"},{"repo":"actions/checkout","sha":"de0fac2e4500dabe0009e67214ff5f5447ce83dd","version":"v6.0.2"},{"repo":"actions/download-artifact","sha":"3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c","version":"v8.0.1"},{"repo":"actions/github-script","sha":"3a2844b7e9c422d3c10d287c895573f7108da1b3","version":"v9.0.0"},{"repo":"actions/github-script","sha":"v9","version":"v9"},{"repo":"actions/setup-node","sha":"48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e","version":"v6.4.0"},{"repo":"actions/upload-artifact","sha":"043fb46d1a93c77aae656e7c1c64a875d1fc6a0a","version":"v7.0.1"},{"repo":"github/gh-aw-actions/setup","sha":"v0.77.5","version":"v0.77.5"}],"resolution_failures":[{"repo":"actions/github-script","ref":"v9","error_type":"dynamic_resolution_failed"}],"containers":[{"image":"ghcr.io/github/gh-aw-firewall/agent:0.25.58"},{"image":"ghcr.io/github/gh-aw-firewall/api-proxy:0.25.58"},{"image":"ghcr.io/github/gh-aw-firewall/squid:0.25.58"},{"image":"ghcr.io/github/gh-aw-mcpg:v0.3.22"},{"image":"ghcr.io/github/github-mcp-server:v1.1.0"},{"image":"node:lts-alpine","digest":"sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f","pinned_image":"node:lts-alpine@sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f"}]}
# ___ _ _
# / _ \ | | (_)
@ -22,7 +22,7 @@
#
# For more information: https://github.github.com/gh-aw/introduction/overview/
#
# Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and post findings as a GitHub Discussion.
# Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and file findings as a GitHub issue.
#
# Frontmatter env variables:
# - GH_TOKEN: (main workflow)
@ -210,21 +210,21 @@ jobs:
run: |
bash "${RUNNER_TEMP}/gh-aw/actions/create_prompt_first.sh"
{
cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF'
cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF'
<system>
GH_AW_PROMPT_413c70864e673ac4_EOF
GH_AW_PROMPT_0d048d29da1eafa3_EOF
cat "${RUNNER_TEMP}/gh-aw/prompts/xpia.md"
cat "${RUNNER_TEMP}/gh-aw/prompts/temp_folder_prompt.md"
cat "${RUNNER_TEMP}/gh-aw/prompts/markdown.md"
cat "${RUNNER_TEMP}/gh-aw/prompts/cache_memory_prompt.md"
cat "${RUNNER_TEMP}/gh-aw/prompts/safe_outputs_prompt.md"
cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF'
cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF'
<safe-output-tools>
Tools: create_discussion, missing_tool, missing_data, noop
Tools: create_issue, missing_tool, missing_data, noop
</safe-output-tools>
GH_AW_PROMPT_413c70864e673ac4_EOF
GH_AW_PROMPT_0d048d29da1eafa3_EOF
cat "${RUNNER_TEMP}/gh-aw/prompts/mcp_cli_tools_prompt.md"
cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF'
cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF'
<github-context>
The following GitHub context information is available for this workflow:
{{#if github.actor}}
@ -253,12 +253,12 @@ jobs:
{{/if}}
</github-context>
GH_AW_PROMPT_413c70864e673ac4_EOF
GH_AW_PROMPT_0d048d29da1eafa3_EOF
cat "${RUNNER_TEMP}/gh-aw/prompts/github_mcp_tools_with_safeoutputs_prompt.md"
cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF'
cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF'
</system>
{{#runtime-import .github/workflows/memory-safety-report.md}}
GH_AW_PROMPT_413c70864e673ac4_EOF
GH_AW_PROMPT_0d048d29da1eafa3_EOF
} > "$GH_AW_PROMPT"
- name: Interpolate variables and render templates
uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
@ -356,7 +356,6 @@ jobs:
permissions:
actions: read
contents: read
discussions: read
issues: read
pull-requests: read
concurrency:
@ -503,40 +502,49 @@ jobs:
mkdir -p "${RUNNER_TEMP}/gh-aw/safeoutputs"
mkdir -p /tmp/gh-aw/safeoutputs
mkdir -p /tmp/gh-aw/mcp-logs/safeoutputs
cat > "${RUNNER_TEMP}/gh-aw/safeoutputs/config.json" << 'GH_AW_SAFE_OUTPUTS_CONFIG_a51ec95cdbf8205c_EOF'
{"create_discussion":{"category":"agentic workflows","close_older_discussions":true,"expires":168,"fallback_to_issue":true,"max":1,"title_prefix":"[Memory Safety] "},"create_report_incomplete_issue":{},"max_bot_mentions":1,"mentions":{"enabled":false},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"false"},"report_incomplete":{}}
GH_AW_SAFE_OUTPUTS_CONFIG_a51ec95cdbf8205c_EOF
cat > "${RUNNER_TEMP}/gh-aw/safeoutputs/config.json" << 'GH_AW_SAFE_OUTPUTS_CONFIG_c9563548363f5229_EOF'
{"create_issue":{"labels":["bug","memory-safety","automated-analysis"],"max":1,"title_prefix":"[Memory Safety] "},"create_report_incomplete_issue":{},"max_bot_mentions":1,"mentions":{"enabled":false},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"false"},"report_incomplete":{}}
GH_AW_SAFE_OUTPUTS_CONFIG_c9563548363f5229_EOF
- name: Generate Safe Outputs Tools
env:
GH_AW_TOOLS_META_JSON: |
{
"description_suffixes": {
"create_discussion": " CONSTRAINTS: Maximum 1 discussion(s) can be created. Title will be prefixed with \"[Memory Safety] \". Discussions will be created in category \"agentic workflows\"."
"create_issue": " CONSTRAINTS: Maximum 1 issue(s) can be created. Title will be prefixed with \"[Memory Safety] \". Labels [\"bug\" \"memory-safety\" \"automated-analysis\"] will be automatically added."
},
"repo_params": {},
"dynamic_tools": []
}
GH_AW_VALIDATION_JSON: |
{
"create_discussion": {
"create_issue": {
"defaultMax": 1,
"fields": {
"body": {
"required": true,
"type": "string",
"sanitize": true,
"maxLength": 65000,
"minLength": 64
"maxLength": 65000
},
"category": {
"type": "string",
"sanitize": true,
"maxLength": 128
"fields": {
"type": "array"
},
"labels": {
"type": "array",
"itemType": "string",
"itemSanitize": true,
"itemMaxLength": 128
},
"parent": {
"issueOrPRNumber": true
},
"repo": {
"type": "string",
"maxLength": 256
},
"temporary_id": {
"type": "string"
},
"title": {
"required": true,
"type": "string",
@ -704,7 +712,7 @@ jobs:
mkdir -p /home/runner/.copilot
GH_AW_NODE=$(which node 2>/dev/null || command -v node 2>/dev/null || echo node)
cat << GH_AW_MCP_CONFIG_d1c0e6d43d005b0a_EOF | "$GH_AW_NODE" "${RUNNER_TEMP}/gh-aw/actions/start_mcp_gateway.cjs"
cat << GH_AW_MCP_CONFIG_5e59fdbe6d1c695e_EOF | "$GH_AW_NODE" "${RUNNER_TEMP}/gh-aw/actions/start_mcp_gateway.cjs"
{
"mcpServers": {
"github": {
@ -745,7 +753,7 @@ jobs:
"payloadDir": "${MCP_GATEWAY_PAYLOAD_DIR}"
}
}
GH_AW_MCP_CONFIG_d1c0e6d43d005b0a_EOF
GH_AW_MCP_CONFIG_5e59fdbe6d1c695e_EOF
- name: Mount MCP servers as CLIs
id: mount-mcp-clis
continue-on-error: true
@ -1015,7 +1023,6 @@ jobs:
runs-on: ubuntu-slim
permissions:
contents: read
discussions: write
issues: write
concurrency:
group: "gh-aw-conclusion-memory-safety-report"
@ -1143,8 +1150,6 @@ jobs:
GH_AW_AGENTIC_ENGINE_TIMEOUT: ${{ needs.agent.outputs.agentic_engine_timeout }}
GH_AW_MODEL_NOT_SUPPORTED_ERROR: ${{ needs.agent.outputs.model_not_supported_error }}
GH_AW_ENGINE_API_HOSTS: "api.enterprise.githubcopilot.com,api.githubcopilot.com,api.business.githubcopilot.com,api.individual.githubcopilot.com"
GH_AW_CREATE_DISCUSSION_ERRORS: ${{ needs.safe_outputs.outputs.create_discussion_errors }}
GH_AW_CREATE_DISCUSSION_ERROR_COUNT: ${{ needs.safe_outputs.outputs.create_discussion_error_count }}
GH_AW_LOCKDOWN_CHECK_FAILED: ${{ needs.activation.outputs.lockdown_check_failed }}
GH_AW_STALE_LOCK_FILE_FAILED: ${{ needs.activation.outputs.stale_lock_file_failed }}
GH_AW_GROUP_REPORTS: "false"
@ -1258,7 +1263,7 @@ jobs:
uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
env:
WORKFLOW_NAME: "Memory Safety Analysis Report Generator"
WORKFLOW_DESCRIPTION: "Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and post findings as a GitHub Discussion."
WORKFLOW_DESCRIPTION: "Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and file findings as a GitHub issue."
HAS_PATCH: ${{ needs.agent.outputs.has_patch }}
with:
script: |
@ -1421,7 +1426,6 @@ jobs:
runs-on: ubuntu-slim
permissions:
contents: read
discussions: write
issues: write
timeout-minutes: 15
env:
@ -1440,6 +1444,8 @@ jobs:
code_push_failure_errors: ${{ steps.process_safe_outputs.outputs.code_push_failure_errors }}
create_discussion_error_count: ${{ steps.process_safe_outputs.outputs.create_discussion_error_count }}
create_discussion_errors: ${{ steps.process_safe_outputs.outputs.create_discussion_errors }}
created_issue_number: ${{ steps.process_safe_outputs.outputs.created_issue_number }}
created_issue_url: ${{ steps.process_safe_outputs.outputs.created_issue_url }}
process_safe_outputs_processed_count: ${{ steps.process_safe_outputs.outputs.processed_count }}
process_safe_outputs_temporary_id_map: ${{ steps.process_safe_outputs.outputs.temporary_id_map }}
steps:
@ -1489,7 +1495,7 @@ jobs:
GH_AW_ALLOWED_DOMAINS: "api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,api.snapcraft.io,archive.ubuntu.com,azure.archive.ubuntu.com,crl.geotrust.com,crl.globalsign.com,crl.identrust.com,crl.sectigo.com,crl.thawte.com,crl.usertrust.com,crl.verisign.com,crl3.digicert.com,crl4.digicert.com,crls.ssl.com,github.com,host.docker.internal,json-schema.org,json.schemastore.org,keyserver.ubuntu.com,ocsp.digicert.com,ocsp.geotrust.com,ocsp.globalsign.com,ocsp.identrust.com,ocsp.sectigo.com,ocsp.ssl.com,ocsp.thawte.com,ocsp.usertrust.com,ocsp.verisign.com,packagecloud.io,packages.cloud.google.com,packages.microsoft.com,ppa.launchpad.net,raw.githubusercontent.com,registry.npmjs.org,s.symcb.com,s.symcd.com,security.ubuntu.com,telemetry.enterprise.githubcopilot.com,ts-crl.ws.symantec.com,ts-ocsp.ws.symantec.com,www.googleapis.com"
GITHUB_SERVER_URL: ${{ github.server_url }}
GITHUB_API_URL: ${{ github.api_url }}
GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_discussion\":{\"category\":\"agentic workflows\",\"close_older_discussions\":true,\"expires\":168,\"fallback_to_issue\":true,\"max\":1,\"title_prefix\":\"[Memory Safety] \"},\"create_report_incomplete_issue\":{},\"mentions\":{\"enabled\":false},\"missing_data\":{},\"missing_tool\":{},\"noop\":{\"max\":1,\"report-as-issue\":\"false\"},\"report_incomplete\":{}}"
GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_issue\":{\"labels\":[\"bug\",\"memory-safety\",\"automated-analysis\"],\"max\":1,\"title_prefix\":\"[Memory Safety] \"},\"create_report_incomplete_issue\":{},\"mentions\":{\"enabled\":false},\"missing_data\":{},\"missing_tool\":{},\"noop\":{\"max\":1,\"report-as-issue\":\"false\"},\"report_incomplete\":{}}"
with:
github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
script: |

20
.github/workflows/memory-safety-report.md vendored
View file

@ -1,7 +1,7 @@
---
description: >
Analyze ASan/UBSan sanitizer logs from the memory-safety workflow
and post findings as a GitHub Discussion.
and file findings as a GitHub issue.
on:
workflow_run:
@ -16,7 +16,6 @@ timeout-minutes: 30
permissions:
actions: read
contents: read
discussions: read
issues: read
pull-requests: read
@ -35,11 +34,10 @@ safe-outputs:
mentions: false
allowed-github-references: []
max-bot-mentions: 1
create-discussion:
create-issue:
title-prefix: "[Memory Safety] "
category: "Agentic Workflows"
close-older-discussions: true
expires: 7d
labels: [bug, memory-safety, automated-analysis]
max: 1
missing-tool:
create-issue: true
noop:
@ -111,9 +109,9 @@ Check cache memory for previous run results:
- List of previously known issues
- Identify new findings (regressions) vs. resolved findings (improvements)
### 4. Generate the Discussion Report
### 4. Generate the Issue Report
Create a GitHub Discussion. Use `###` or lower for section headers, never `##` or `#`. Wrap verbose sections in `<details>` tags to keep the report scannable.
Create a GitHub issue using `create-issue`. Use `##` or lower for section headers and wrap verbose sections in `<details>` tags to keep the report scannable.
```markdown
**Date**: YYYY-MM-DD
@ -190,7 +188,7 @@ Create a GitHub Discussion. Use `###` or lower for section headers, never `##` o
</details>
```
If zero findings across all tools, create a discussion noting a clean run with the commit and workflow run link.
If zero findings across all tools, call `noop` and include a clean-run summary (commit and workflow run link) in the no-op message.
### 5. Update Cache Memory
@ -203,7 +201,7 @@ Store the current run's results in cache memory for future comparison:
- If the triggering workflow failed entirely, report that analysis could not complete and include any partial results.
- If no artifacts are available, report that and suggest running the workflow manually.
- If the helper scripts fail, report the error in the discussion body and stop.
- If the helper scripts fail, report the error in the issue body and stop.
## Guidelines
@ -217,6 +215,6 @@ Store the current run's results in cache memory for future comparison:
- DO NOT create pull requests or modify source files.
- DO NOT attempt to fix the findings automatically.
- DO close older Memory Safety discussions automatically (configured via `close-older-discussions: true`).
- DO create issues only when there are actionable findings; use `noop` for clean runs.
- DO always report the commit SHA so findings can be correlated with specific code versions.
- DO use cache memory to track trends over multiple runs.

BIN
gmon.out Normal file
View file

Binary file not shown.

3
scripts/mk_util.py
View file

@ -1919,6 +1919,9 @@ class JavaDLLComponent(Component):
if IS_WINDOWS: # On Windows, CL creates a .lib file to link against.
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
os.path.join('api', 'java', 'Native'))
elif IS_OSX:
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT) -Wl,-rpath,@loader_path $(SLINK_EXTRA_FLAGS)\n' %
os.path.join('api', 'java', 'Native'))
else:
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT) $(SLINK_EXTRA_FLAGS)\n' %
os.path.join('api', 'java', 'Native'))

39
scripts/tests/test_jni_arch_flags.py
View file

@ -208,6 +208,45 @@ class TestJNIArchitectureFlagsInMakefile(unittest.TestCase):
"(the import library)",
)
# ------------------------------------------------------------------
# Tests for macOS rpath, so libz3java.dylib can find libz3.dylib
# ------------------------------------------------------------------
def test_macos_uses_loader_path_rpath(self):
"""
On macOS, the JNI link command must include -Wl,-rpath,@loader_path
so that libz3java.dylib can find libz3.dylib in the same directory
at runtime. Without this, Java fails with UnsatisfiedLinkError.
"""
comp = self._make_java_dll_component()
text = self._generate_makefile(
comp, is_windows=False, is_osx=True, is_arch_arm64=True
)
link_lines = self._find_jni_link_lines(text)
self.assertTrue(link_lines, "Expected at least one JNI link line")
for line in link_lines:
self.assertIn(
'-Wl,-rpath,@loader_path', line,
"macOS JNI link command must set rpath to @loader_path "
"so libz3java.dylib finds libz3.dylib at runtime",
)
def test_linux_does_not_use_loader_path(self):
"""
On Linux, @loader_path is a macOS concept and must not appear.
"""
comp = self._make_java_dll_component()
text = self._generate_makefile(
comp, is_windows=False, is_osx=False, is_arch_arm64=False
)
link_lines = self._find_jni_link_lines(text)
self.assertTrue(link_lines, "Expected at least one JNI link line")
for line in link_lines:
self.assertNotIn(
'@loader_path', line,
"@loader_path is macOS-specific and must not appear on Linux",
)
# ------------------------------------------------------------------
# Consistency check: SLINK_EXTRA_FLAGS in mk_config for cross-compile
# ------------------------------------------------------------------

11
scripts/update_api.py
View file

@ -631,7 +631,16 @@ def mk_java(java_src, java_dir, package_name):
java_native.write(' try {\n')
java_native.write(' System.loadLibrary("z3java");\n')
java_native.write(' } catch (UnsatisfiedLinkError ex) {\n')
java_native.write(' System.loadLibrary("libz3java");\n')
java_native.write(' try {\n')
java_native.write(' System.loadLibrary("libz3java");\n')
java_native.write(' } catch (UnsatisfiedLinkError ex2) {\n')
java_native.write(' throw new UnsatisfiedLinkError(\n')
java_native.write(' "Failed to load z3java native library. "\n')
java_native.write(' + "Tried z3java: " + ex.getMessage() + "; "\n')
java_native.write(' + "Tried libz3java: " + ex2.getMessage() + ". "\n')
java_native.write(' + "Make sure both the JNI library and libz3 are in java.library.path "\n')
java_native.write(' + "or set DYLD_LIBRARY_PATH (macOS) / LD_LIBRARY_PATH (Linux).");\n')
java_native.write(' }\n')
java_native.write(' }\n')
java_native.write(' }\n')
java_native.write(' }\n')

13
src/api/java/CMakeLists.txt
View file

@ -48,17 +48,18 @@ target_include_directories(z3java PRIVATE
"${PROJECT_BINARY_DIR}/src/api"
${JNI_INCLUDE_DIRS}
)
# Add header padding for macOS to allow install_name_tool to modify the dylib
# On macOS, set rpath so libz3java.dylib can find libz3.dylib in the same directory,
# and add header padding to allow install_name_tool to modify the dylib.
if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
set_target_properties(z3java PROPERTIES
MACOSX_RPATH TRUE
INSTALL_RPATH "@loader_path"
BUILD_RPATH "@loader_path"
)
target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names")
endif()
# FIXME: Should this library have SONAME and VERSION set?
# On macOS, add headerpad for install_name_tool compatibility
if(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names")
endif()
# This prevents CMake from automatically defining ``z3java_EXPORTS``
set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")

1
src/ast/rewriter/CMakeLists.txt
View file

@ -39,6 +39,7 @@ z3_add_component(rewriter
rewriter.cpp
seq_axioms.cpp
seq_eq_solver.cpp
seq_subset.cpp
seq_rewriter.cpp
seq_skolem.cpp
th_rewriter.cpp

105
src/ast/rewriter/seq_rewriter.cpp
View file

@ -4491,10 +4491,60 @@ br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
r* ++ r -> r ++ r*
*/
br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
auto accepts_empty_word = [&](expr* r) {
auto info = re().get_info(r);
return info.interpreted && info.nullable == l_true && info.min_length == 0;
};
auto starts_with_full_seq = [&](expr* r) {
expr* r1 = nullptr, *r2 = nullptr;
return re().is_full_seq(r) || (re().is_concat(r, r1, r2) && re().is_full_seq(r1));
};
auto ends_with_full_seq = [&](expr* r) {
expr* r1 = nullptr, *r2 = nullptr;
while (re().is_concat(r, r1, r2))
r = r2;
return re().is_full_seq(r);
};
auto all_inter_arms_end_with_full_seq = [&](expr* r) {
ptr_buffer<expr> todo;
todo.push_back(r);
while (!todo.empty()) {
expr* r1 = nullptr, *r2 = nullptr;
expr* t = todo.back();
todo.pop_back();
if (re().is_intersection(t, r1, r2)) {
todo.push_back(r1);
todo.push_back(r2);
}
else if (!ends_with_full_seq(t)) {
return false;
}
}
return true;
};
if (re().is_full_seq(a) && re().is_full_seq(b)) {
result = a;
return BR_DONE;
}
if (re().is_full_seq(a) && accepts_empty_word(b)) {
result = a;
return BR_DONE;
}
if (re().is_full_seq(b) && accepts_empty_word(a)) {
result = b;
return BR_DONE;
}
expr* u1 = nullptr, *u2 = nullptr;
if (re().is_full_seq(a) && re().is_union(b, u1, u2) &&
(starts_with_full_seq(u1) || starts_with_full_seq(u2))) {
result = mk_regex_union_normalize(mk_regex_concat(a, u1), mk_regex_concat(a, u2));
return BR_REWRITE2;
}
if (re().is_intersection(a, u1, u2) && re().is_full_seq(b) &&
all_inter_arms_end_with_full_seq(a)) {
result = a;
return BR_DONE;
}
if (re().is_empty(a)) {
result = a;
return BR_DONE;
@ -4525,7 +4575,8 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
result = re().mk_to_re(str().mk_concat(a_str, b_str));
return BR_REWRITE2;
}
expr* a1 = nullptr, *b1 = nullptr;
expr* a1 = nullptr;
expr* b1 = nullptr;
if (re().is_to_re(a, a1) && re().is_to_re(b, b1)) {
result = re().mk_to_re(str().mk_concat(a1, b1));
return BR_DONE;
@ -4534,6 +4585,11 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
result = a;
return BR_DONE;
}
expr* b2 = nullptr, *b3 = nullptr;
if (re().is_star(a, a1) && re().is_concat(b, b1, b2) && re().is_star(b1, b3) && a1 == b3) {
result = b;
return BR_DONE;
}
if (re().is_star(a, a1) && a1 == b) {
result = re().mk_concat(b, a);
return BR_DONE;
@ -4587,51 +4643,7 @@ bool seq_rewriter::are_complements(expr* r1, expr* r2) const {
* basic subset checker.
*/
bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
// return false;
expr* ra1 = nullptr, *ra2 = nullptr, *ra3 = nullptr;
expr* rb1 = nullptr, *rb2 = nullptr, *rb3 = nullptr;
unsigned la, ua, lb, ub;
if (re().is_complement(r1, ra1) &&
re().is_complement(r2, rb1)) {
return is_subset(rb1, ra1);
}
auto is_concat = [&](expr* r, expr*& a, expr*& b, expr*& c) {
return re().is_concat(r, a, b) && re().is_concat(b, b, c);
};
while (true) {
if (r1 == r2)
return true;
if (re().is_full_seq(r2))
return true;
if (re().is_dot_plus(r2) && re().get_info(r1).nullable == l_false)
return true;
if (is_concat(r1, ra1, ra2, ra3) &&
is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) {
r1 = ra3;
r2 = rb3;
continue;
}
if (re().is_concat(r1, ra1, ra2) &&
re().is_concat(r2, rb1, rb2) && re().is_full_seq(rb1)) {
r1 = ra2;
continue;
}
// r1=ra3{la,ua}ra2, r2=rb3{lb,ub}rb2, ra3=rb3, lb<=la, ua<=ub
if (re().is_concat(r1, ra1, ra2) && re().is_loop(ra1, ra3, la, ua) &&
re().is_concat(r2, rb1, rb2) && re().is_loop(rb1, rb3, lb, ub) &&
ra3 == rb3 && lb <= la && ua <= ub) {
r1 = ra2;
r2 = rb2;
continue;
}
// ra1=ra3{la,ua}, r2=rb3{lb,ub}, ra3=rb3, lb<=la, ua<=ub
if (re().is_loop(r1, ra3, la, ua) &&
re().is_loop(r2, rb3, lb, ub) &&
ra3 == rb3 && lb <= la && ua <= ub) {
return true;
}
return false;
}
return m_subset.is_subset(r1, r2);
}
br_status seq_rewriter::mk_re_union0(expr* a, expr* b, expr_ref& result) {
@ -6163,4 +6175,3 @@ bool seq_rewriter::get_bounds(expr* e, unsigned& low, unsigned& high) {
}
return low <= high;
}

5
src/ast/rewriter/seq_rewriter.h
View file

@ -23,6 +23,7 @@ Notes:
#include "ast/arith_decl_plugin.h"
#include "ast/rewriter/rewriter_types.h"
#include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/seq_subset.h"
#include "util/params.h"
#include "util/lbool.h"
#include "util/sign.h"
@ -128,6 +129,7 @@ class seq_rewriter {
};
seq_util m_util;
seq_subset m_subset;
arith_util m_autil;
bool_rewriter m_br;
// re2automaton m_re2aut;
@ -340,7 +342,7 @@ class seq_rewriter {
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m), m_br(m, p), // m_re2aut(m),
m_util(m), m_subset(m_util.re), m_autil(m), m_br(m, p), // m_re2aut(m),
m_op_cache(m), m_es(m),
m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
}
@ -424,4 +426,3 @@ public:
*/
lbool some_string_in_re(expr* r, zstring& s);
};

146
src/ast/rewriter/seq_subset.cpp Normal file
View file

@ -0,0 +1,146 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_subset.cpp
Abstract:
Heuristic regular-expression subset checks used by seq_rewriter.
Author:
Nikolaj Bjorner (nbjorner) 2026-6-8
--*/
#include "ast/rewriter/seq_subset.h"
bool seq_subset::is_subset_rec(expr* a, expr* b, unsigned depth) const {
while (true) {
if (a == b)
return true;
if (m_re.is_empty(a))
return true;
if (m_re.is_full_seq(b))
return true;
if (m_re.is_epsilon(a) && m_re.get_info(b).nullable == l_true)
return true;
if (depth >= m_max_depth)
return false;
expr* a1 = nullptr, * a2 = nullptr, * b1 = nullptr, * b2 = nullptr;
unsigned la, ua, lb, ub;
// a ⊆ .+ iff a is non-nullable
if (m_re.is_dot_plus(b) && m_re.get_info(a).nullable == l_false)
return true;
// a ⊆ a*
if (m_re.is_star(b, b1) && is_subset_rec(a, b1, depth))
return true;
// e ⊆ a*
if (m_re.is_epsilon(a) && m_re.is_star(b, b1))
return true;
// R ⊆ R*
if (m_re.is_star(b, b1) && is_subset_rec(a, b1, depth + 1))
return true;
// R1* ⊆ R2* if R1 ⊆ R2
if (m_re.is_star(a, a1) && m_re.is_star(b, b1) && is_subset_rec(a1, b1, depth + 1))
return true;
// R1+ ⊆ R2+ if R1 ⊆ R2
if (m_re.is_plus(a, a1) && m_re.is_plus(b, b1) && is_subset_rec(a1, b1, depth))
return true;
// R ⊆ R+
if (m_re.is_plus(b, b1) && is_subset_rec(a, b1, depth))
return true;
// R+ ⊆ R*
if (m_re.is_plus(a, a1) && m_re.is_star(b, b1) && is_subset_rec(a1, b1, depth + 1))
return true;
// range containment
if (m_re.is_range(a, la, ua) && m_re.is_range(b, lb, ub) && lb <= la && ua <= ub)
return true;
// to_re(s) ⊆ range
if (m_re.is_to_re(a, a1) && m_re.is_range(b, lb, ub) && is_app(a1)) {
func_decl* f = to_app(a1)->get_decl();
if (f->get_decl_kind() == OP_STRING_CONST && f->get_num_parameters() == 1) {
zstring const& s = f->get_parameter(0).get_zstring();
if (s.length() == 1 && lb <= s[0] && s[0] <= ub)
return true;
}
}
// a ⊆ b1 ∪ b2 if a ⊆ b1 or a ⊆ b2
if (m_re.is_union(b, b1, b2) && (is_subset_rec(a, b1, depth + 1) || is_subset_rec(a, b2, depth + 1)))
return true;
// a1 ∪ a2 ⊆ b if a1 ⊆ b and a2 ⊆ b
if (m_re.is_union(a, a1, a2) && is_subset_rec(a1, b, depth + 1) && is_subset_rec(a2, b, depth + 1))
return true;
// a1 ∩ a2 ⊆ b if a1 ⊆ b or a2 ⊆ b
if (m_re.is_intersection(a, a1, a2) && (is_subset_rec(a1, b, depth + 1) || is_subset_rec(a2, b, depth + 1)))
return true;
// a ⊆ b1 ∩ b2 if a ⊆ b1 and a ⊆ b2
if (m_re.is_intersection(b, b1, b2) && is_subset_rec(a, b1, depth + 1) && is_subset_rec(a, b2, depth + 1))
return true;
// R{la,ua} ⊆ R'{lb,ub} if R ⊆ R', lb<=la, ua<=ub
if (m_re.is_loop(a, a1, la, ua) &&
m_re.is_loop(b, b1, lb, ub) &&
lb <= la && ua <= ub && is_subset_rec(a1, b1, depth + 1)) {
return true;
}
// a1 \ a2 ⊆ b if a1 ⊆ b
if (m_re.is_diff(a, a1, a2) && is_subset_rec(a1, b, depth + 1))
return true;
// R ⊆ Σ*·R' if R ⊆ R'
if (m_re.is_concat(b, b1, b2) && m_re.is_full_seq(b1) && is_subset_rec(a, b2, depth))
return true;
// R ⊆ R'·Σ* if R ⊆ R'
if (m_re.is_concat(b, b1, b2) && m_re.is_full_seq(b2) && is_subset_rec(a, b1, depth))
return true;
// star absorption: R·R* ⊆ R*, R*·R ⊆ R*
bool const is_concat_star = m_re.is_concat(a, a1, a2) && m_re.is_star(b, b1);
if (is_concat_star &&
is_subset_rec(a1, b1, depth + 1) && is_subset_rec(a2, b, depth + 1))
return true;
if (is_concat_star &&
is_subset_rec(a2, b1, depth + 1) && is_subset_rec(a1, b, depth + 1))
return true;
// concat monotonicity:
// tail-recursive on second arguments (without increasing depth bound).
if (m_re.is_concat(a, a1, a2) && m_re.is_concat(b, b1, b2) && is_subset_rec(a1, b1, depth + 1)) {
a = a2;
b = b2;
continue;
}
// complement: ~a ⊆ ~b if b ⊆ a
if (m_re.is_complement(a, a1) && m_re.is_complement(b, b1))
return is_subset_rec(b1, a1, depth + 1);
return false;
}
}
bool seq_subset::is_subset(expr* a, expr* b) const {
return is_subset_rec(a, b, 0);
}

30
src/ast/rewriter/seq_subset.h Normal file
View file

@ -0,0 +1,30 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_subset.h
Abstract:
Heuristic regular-expression subset checks used by seq_rewriter.
Author:
Nikolaj Bjorner (nbjorner) 2026-6-8
--*/
#pragma once
#include "ast/seq_decl_plugin.h"
class seq_subset {
seq_util::rex& m_re;
static constexpr unsigned m_max_depth = 3;
bool is_subset_rec(expr* a, expr* b, unsigned depth) const;
public:
explicit seq_subset(seq_util::rex& re) : m_re(re) {}
bool is_subset(expr* a, expr* b) const;
};

37
src/ast/seq_decl_plugin.cpp
View file

@ -1653,9 +1653,9 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
if (e->get_family_id() == u.get_family_id()) {
switch (e->get_decl()->get_decl_kind()) {
case OP_RE_EMPTY_SET:
return info(true, l_false, UINT_MAX);
return info(true, l_false, UINT_MAX, false);
case OP_RE_FULL_SEQ_SET:
return info(true, l_true, 0);
return info(true, l_true, 0, true);
case OP_RE_STAR:
i1 = get_info_rec(e->get_arg(0));
return i1.star();
@ -1667,7 +1667,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
case OP_RE_OF_PRED:
//TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat
//TBD: check if the range is unsat
return info(true, l_false, 1);
return info(true, l_false, 1, false);
case OP_RE_CONCAT:
i1 = get_info_rec(e->get_arg(0));
i2 = get_info_rec(e->get_arg(1));
@ -1684,7 +1684,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
min_length = u.str.min_length(e->get_arg(0));
is_value = m.is_value(e->get_arg(0));
nullable = (is_value && min_length == 0 ? l_true : (min_length > 0 ? l_false : l_undef));
return info(is_value, nullable, min_length);
return info(is_value, nullable, min_length, true);
case OP_RE_REVERSE:
return get_info_rec(e->get_arg(0));
case OP_RE_PLUS:
@ -1720,7 +1720,8 @@ std::ostream& seq_util::rex::info::display(std::ostream& out) const {
if (is_known()) {
out << "info("
<< "nullable=" << (nullable == l_true ? "T" : (nullable == l_false ? "F" : "U")) << ", "
<< "min_length=" << min_length << ")";
<< "min_length=" << min_length << ", "
<< "classical=" << (classical ? "T" : "F") << ")";
}
else if (is_valid())
out << "UNKNOWN";
@ -1740,13 +1741,13 @@ std::string seq_util::rex::info::str() const {
seq_util::rex::info seq_util::rex::info::star() const {
//if is_known() is false then all mentioned properties will remain false
return seq_util::rex::info(interpreted, l_true, 0);
return seq_util::rex::info(interpreted, l_true, 0, classical);
}
seq_util::rex::info seq_util::rex::info::plus() const {
if (is_known()) {
//plus never occurs in a normalized regex
return info(interpreted, nullable, min_length);
return info(interpreted, nullable, min_length, classical);
}
else
return *this;
@ -1755,14 +1756,14 @@ seq_util::rex::info seq_util::rex::info::plus() const {
seq_util::rex::info seq_util::rex::info::opt() const {
// if is_known() is false then all mentioned properties will remain false
// optional construct never occurs in a normalized regex
return seq_util::rex::info(interpreted, l_true, 0);
return seq_util::rex::info(interpreted, l_true, 0, classical);
}
seq_util::rex::info seq_util::rex::info::complement() const {
if (is_known()) {
lbool compl_nullable = (nullable == l_true ? l_false : (nullable == l_false ? l_true : l_undef));
unsigned compl_min_length = (compl_nullable == l_false ? 1 : 0);
return info(interpreted, compl_nullable, compl_min_length);
return info(interpreted, compl_nullable, compl_min_length, false);
}
else
return *this;
@ -1776,7 +1777,8 @@ seq_util::rex::info seq_util::rex::info::concat(seq_util::rex::info const& rhs,
m = UINT_MAX;
return info(interpreted && rhs.interpreted,
((nullable == l_false || rhs.nullable == l_false) ? l_false : ((nullable == l_true && rhs.nullable == l_true) ? l_true : l_undef)),
m);
m,
classical && rhs.classical);
}
else
return rhs;
@ -1790,7 +1792,8 @@ seq_util::rex::info seq_util::rex::info::disj(seq_util::rex::info const& rhs) co
//works correctly if one of the arguments is unknown
return info(interpreted && rhs.interpreted,
((nullable == l_true || rhs.nullable == l_true) ? l_true : ((nullable == l_false && rhs.nullable == l_false) ? l_false : l_undef)),
std::min(min_length, rhs.min_length));
std::min(min_length, rhs.min_length),
classical && rhs.classical);
}
else
return rhs;
@ -1801,7 +1804,8 @@ seq_util::rex::info seq_util::rex::info::conj(seq_util::rex::info const& rhs) co
if (rhs.is_known()) {
return info(interpreted && rhs.interpreted,
((nullable == l_true && rhs.nullable == l_true) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)),
std::max(min_length, rhs.min_length));
std::max(min_length, rhs.min_length),
false);
}
else
return rhs;
@ -1815,7 +1819,8 @@ seq_util::rex::info seq_util::rex::info::diff(seq_util::rex::info const& rhs) co
if (rhs.is_known()) {
return info(interpreted & rhs.interpreted,
((nullable == l_true && rhs.nullable == l_false) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)),
std::max(min_length, rhs.min_length));
std::max(min_length, rhs.min_length),
false);
}
else
return rhs;
@ -1832,7 +1837,8 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co
// TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted
return info(false,
((nullable == l_true && i.nullable == l_true) ? l_true : ((nullable == l_false && i.nullable == l_false) ? l_false : l_undef)),
std::min(min_length, i.min_length));
std::min(min_length, i.min_length),
classical && i.classical);
}
else
return i;
@ -1848,7 +1854,7 @@ seq_util::rex::info seq_util::rex::info::loop(unsigned lower, unsigned upper) co
if (m > 0 && (m < min_length || m < lower))
m = UINT_MAX;
lbool loop_nullable = (nullable == l_true || lower == 0 ? l_true : nullable);
return info(interpreted, loop_nullable, m);
return info(interpreted, loop_nullable, m, classical);
}
else
return *this;
@ -1863,6 +1869,7 @@ seq_util::rex::info& seq_util::rex::info::operator=(info const& other) {
interpreted = other.interpreted;
nullable = other.nullable;
min_length = other.min_length;
classical = other.classical;
return *this;
}

8
src/ast/seq_decl_plugin.h
View file

@ -443,6 +443,8 @@ public:
lbool nullable { l_undef };
/* Lower bound on the length of all accepted words. */
unsigned min_length { 0 };
/* Classical regular expression: does not use complement, intersection, diff, or the empty language (fail). */
bool classical { true };
/*
Default constructor of invalid info.
@ -459,11 +461,13 @@ public:
*/
info(bool is_interpreted,
lbool is_nullable,
unsigned min_l) :
unsigned min_l,
bool is_classical) :
known(l_true),
interpreted(is_interpreted),
nullable(is_nullable),
min_length(min_l) {}
min_length(min_l),
classical(is_classical) {}
/*
Appends a string representation of the info into the stream.

2
src/ast/sls/sls_seq_plugin.cpp
View file

@ -912,7 +912,7 @@ namespace sls {
m_string_updates.reset();
u[i][j] = d[i - 1][j];
}
if (d[i][j - 1] < u[i][j] && b.can_add(i - 1)) {
if (d[i][j - 1] < u[i][j] && b.can_add(j - 1)) {
m_string_updates.reset();
u[i][j] = d[i][j - 1];
}

2
src/math/lp/dioph_eq.cpp
View file

@ -709,8 +709,8 @@ namespace lp {
while (column.size() > 1) {
auto& c = column.back();
SASSERT(c.var() != last_row_index);
m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j);
m_changed_rows.insert(c.var());
m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j);
}
}

8
src/math/lp/lp_core_solver_base_def.h
View file

@ -277,13 +277,11 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
m_A.m_rows[c.var()][c.offset()].offset() = pivot_col_cell_index;
}
while (column.size() > 1) {
auto & c = column.back();
auto& c = column.back();
SASSERT(c.var() != piv_row_index);
if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) {
return false;
}
if (m_touched_rows!= nullptr)
if (m_touched_rows != nullptr)
m_touched_rows->insert(c.var());
m_A.pivot_row_to_row_given_cell(piv_row_index, c, j);
}
if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs)

4
src/math/lp/static_matrix.cpp
View file

@ -51,8 +51,8 @@ namespace lp {
template void static_matrix<mpq, numeric_pair<mpq> >::set(unsigned int, unsigned int, mpq const&);
template bool static_matrix<mpq, mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
template bool static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
template void static_matrix<mpq, mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
template void static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
template void static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell_with_sign(unsigned int, column_cell&, unsigned int, int);
template void static_matrix<mpq, mpq>::pivot_row_to_row_given_cell_with_sign(unsigned int, row_cell<empty_struct>&, unsigned int, int);
template void static_matrix<mpq, numeric_pair<mpq> >::add_rows(mpq const&, unsigned int, unsigned int);

2
src/math/lp/static_matrix.h
View file

@ -293,7 +293,7 @@ public:
// pivot row i to row ii
bool pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j);
void pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j);
void pivot_row_to_row_given_cell_with_sign(unsigned piv_row_index, column_cell& c, unsigned j, int j_sign);
void transpose_rows(unsigned i, unsigned ii) {
auto t = m_rows[i];

4
src/math/lp/static_matrix_def.h
View file

@ -48,7 +48,7 @@ namespace lp {
}
template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_given_cell(unsigned i,
template <typename T, typename X> void static_matrix<T, X>::pivot_row_to_row_given_cell(unsigned i,
column_cell & c, unsigned pivot_col) {
unsigned ii = c.var();
SASSERT(i < row_count() && ii < column_count() && i != ii);
@ -82,7 +82,7 @@ namespace lp {
if (is_zero(rowii[k].coeff()))
remove_element(rowii, rowii[k]);
}
return !rowii.empty();
SASSERT(!rowii.empty());
}

7
src/muz/spacer/spacer_qe_project.cpp
View file

@ -1148,6 +1148,7 @@ class arith_project_util {
expr_ref_vector const &lits) {
app_ref_vector new_vars(m);
expr_ref_vector result(lits);
model::scoped_model_completion _smc(mdl, true);
for (unsigned i = 0; i < vars.size(); ++i) {
app *v = vars.get(i);
m_var = alloc(contains_app, m, v);
@ -1183,6 +1184,12 @@ class arith_project_util {
expr_map &map) {
app_ref_vector new_vars(m);
// Variables to be projected may not be assigned in the model
// (e.g. grounded auxiliary variables that are don't-cares). Enable
// model completion so their evaluation yields concrete numerals,
// matching the behavior of the native MBP arith projector.
model::scoped_model_completion _smc(mdl, true);
// factor out mod terms by introducing new variables
TRACE(qe, tout << "before factoring out mod terms:" << "\n";
tout << mk_pp(fml, m) << "\n"; tout << "mdl:\n";

25
src/smt/theory_fpa.cpp
View file

@ -494,6 +494,31 @@ namespace smt {
else if (is_app(n) && to_app(n)->get_family_id() == get_family_id()) {
// These are the conversion functions fp.to_* */
SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n));
// The conversion equality and side conditions for fp.to_* terms are
// emitted in internalize_term(), which runs exactly once. Those are
// asserted as theory axioms at the current decision level and are
// undone on DPLL backtracking, while internalize_term() is not run
// again for the already-internalized term (e.g. when the term lives
// at the user push base level and its clause is not reinitialized).
// The side conditions include the axioms linking FP uninterpreted
// functions to their bit-vector counterparts; losing them leaves the
// BV counterpart unconstrained and causes an incremental-mode
// soundness bug. relevant_eh re-fires on relevancy re-propagation
// after a backtrack, so re-emit them here to keep them in force.
switch ((fpa_op_kind)to_app(n)->get_decl_kind()) {
case OP_FPA_TO_FP:
case OP_FPA_TO_UBV:
case OP_FPA_TO_SBV:
case OP_FPA_TO_REAL:
case OP_FPA_TO_IEEE_BV: {
expr_ref conv = convert(n);
assert_cnstr(m.mk_eq(n, conv));
assert_cnstr(mk_side_conditions());
break;
}
default: /* ignore */;
}
}
else {
/* Theory variables can be merged when (= bv-term (bvwrap fp-term)),

24
src/test/sls_seq_plugin.cpp
View file

@ -351,4 +351,28 @@ void tst_sls_seq_plugin() {
app_ref eq(m.mk_eq(l, r), m);
verbose_stream() << eq << "\n";
ts.repair_down_str_eq_edit_distance_incremental(eq);
test_seq::string_instance lhs, rhs;
lhs.s = zstring("a");
lhs.is_value.push_back(false);
lhs.prev_is_var.push_back(false);
lhs.next_is_var.push_back(false);
rhs.s = zstring("ab");
rhs.is_value.push_back(true);
rhs.prev_is_var.push_back(false);
rhs.next_is_var.push_back(false);
rhs.is_value.push_back(false);
rhs.prev_is_var.push_back(false);
rhs.next_is_var.push_back(false);
ENSURE(ts.edit_distance_with_updates(lhs, rhs) == 0);
ENSURE(ts.m_string_updates.size() == 2);
ENSURE(ts.m_string_updates[0].side == test_seq::side_t::right);
ENSURE(ts.m_string_updates[0].op == test_seq::op_t::add);
ENSURE(ts.m_string_updates[0].i == 0);
ENSURE(ts.m_string_updates[0].j == 1);
ENSURE(ts.m_string_updates[1].side == test_seq::side_t::right);
ENSURE(ts.m_string_updates[1].op == test_seq::op_t::del);
ENSURE(ts.m_string_updates[1].i == 1);
ENSURE(ts.m_string_updates[1].j == 0);
}