mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-03 04:33:28 +00:00
Code Activity

Merge branch 'master' into generation

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-08 15:43:29 -07:00 • committed by GitHub
commit 84935b3746
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
474 changed files with 2071 additions and 761 deletions
Download patch file Download diff file Expand all files Collapse all files

4
.github/workflows/academic-citation-tracker.lock.yml generated vendored
View file

@ -33,7 +33,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
# - actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
@ -1592,7 +1592,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

4
.github/workflows/agentics-maintenance.yml vendored
View file

@ -393,7 +393,7 @@ jobs:
- name: Save activity report logs cache
if: ${{ always() }}
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
path: ./.cache/gh-aw/activity-report-logs
key: ${{ steps.activity_report_logs_cache.outputs.cache-primary-key }}
@ -520,7 +520,7 @@ jobs:
- name: Save forecast report logs cache
if: ${{ always() }}
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
path: ./.github/aw/logs
key: ${{ runner.os }}-forecast-report-logs-${{ github.repository }}-${{ github.ref_name }}-${{ github.run_id }}

4
.github/workflows/api-coherence-checker.lock.yml generated vendored
View file

@ -33,7 +33,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
@ -1590,7 +1590,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

2
.github/workflows/build-z3-cache.yml vendored
View file

@ -45,7 +45,7 @@ jobs:
- name: Restore or create cache
id: cache-z3
uses: actions/cache@v6.0.0
uses: actions/cache@v6.1.0
with:
path: |
build/z3

4
.github/workflows/code-conventions-analyzer.lock.yml generated vendored
View file

@ -32,7 +32,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
# - actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
@ -1647,7 +1647,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

4
.github/workflows/csa-analysis.lock.yml generated vendored
View file

@ -32,7 +32,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
@ -1593,7 +1593,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

4
.github/workflows/issue-backlog-processor.lock.yml generated vendored
View file

@ -33,7 +33,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
# - actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
@ -1615,7 +1615,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

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

@ -35,7 +35,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
@ -1667,7 +1667,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

8
.github/workflows/nightly.yml vendored
View file

@ -33,6 +33,8 @@ jobs:
name: "Mac Build x64"
runs-on: macos-latest
timeout-minutes: 90
env:
MACOSX_DEPLOYMENT_TARGET: "13.0"
steps:
- name: Checkout code
uses: actions/checkout@v7.0.0
@ -43,7 +45,7 @@ jobs:
python-version: '3.x'
- name: Build
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=x64
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=x64 --os=osx-13.0
- name: Validate libz3.dylib and z3 architecture (must be x86_64)
run: |
@ -69,6 +71,8 @@ jobs:
name: "Mac ARM64 Build"
runs-on: macos-latest
timeout-minutes: 90
env:
MACOSX_DEPLOYMENT_TARGET: "13.0"
steps:
- name: Checkout code
uses: actions/checkout@v7.0.0
@ -79,7 +83,7 @@ jobs:
python-version: '3.x'
- name: Build
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=arm64
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=arm64 --os=osx-13.0
- name: Validate libz3.dylib and z3 architecture (must be arm64)
run: |

4
.github/workflows/ocaml.yaml vendored
View file

@ -21,7 +21,7 @@ jobs:
# Cache ccache (shared across runs)
- name: Cache ccache
uses: actions/cache@v6.0.0
uses: actions/cache@v6.1.0
with:
path: ~/.ccache
key: ${{ runner.os }}-ccache-${{ github.sha }}
@ -30,7 +30,7 @@ jobs:
# Cache opam (compiler + packages)
- name: Cache opam
uses: actions/cache@v6.0.0
uses: actions/cache@v6.1.0
with:
path: ~/.opam
key: ${{ runner.os }}-opam-${{ matrix.ocaml-version }}-${{ github.sha }}

8
.github/workflows/release.yml vendored
View file

@ -34,6 +34,8 @@ jobs:
name: "Mac Build x64"
runs-on: macos-15
timeout-minutes: 90
env:
MACOSX_DEPLOYMENT_TARGET: "13.0"
steps:
- name: Checkout code
uses: actions/checkout@v7.0.0
@ -44,7 +46,7 @@ jobs:
python-version: '3.x'
- name: Build
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=x64
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=x64 --os=osx-13.0
- name: Validate libz3.dylib and z3 architecture (must be x86_64)
run: |
@ -76,6 +78,8 @@ jobs:
name: "Mac ARM64 Build"
runs-on: macos-15
timeout-minutes: 90
env:
MACOSX_DEPLOYMENT_TARGET: "13.0"
steps:
- name: Checkout code
uses: actions/checkout@v7.0.0
@ -86,7 +90,7 @@ jobs:
python-version: '3.x'
- name: Build
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=arm64
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=arm64 --os=osx-13.0
- name: Validate libz3.dylib and z3 architecture (must be arm64)
run: |

4
.github/workflows/smtlib-benchmark-finder.lock.yml generated vendored
View file

@ -32,7 +32,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
# - actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
@ -1594,7 +1594,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

4
.github/workflows/specbot-crash-analyzer.lock.yml generated vendored
View file

@ -32,7 +32,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
@ -1631,7 +1631,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

4
.github/workflows/tactic-to-simplifier.lock.yml generated vendored
View file

@ -32,7 +32,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
@ -1599,7 +1599,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

4
.github/workflows/workflow-suggestion-agent.lock.yml generated vendored
View file

@ -32,7 +32,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
@ -1592,7 +1592,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

4
.github/workflows/zipt-code-reviewer.lock.yml generated vendored
View file

@ -32,7 +32,7 @@
#
# Custom actions used:
# - actions/cache/restore@2c8a9bd7457de244a408f35966fab2fb45fda9c8 # v6.0.0
# - actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
# - actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
@ -1620,7 +1620,7 @@ jobs:
fi
- name: Save cache-memory to cache (default)
if: steps.check_cache_default.outputs.has_content == 'true'
uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
key: memory-none-nopolicy-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
path: /tmp/gh-aw/cache-memory

3
cmake/compiler_warnings.cmake
View file

@ -24,8 +24,9 @@ set(CLANG_ONLY_WARNINGS
"-Wsuggest-override"
"-Winconsistent-missing-override"
"-Wno-missing-field-initializers"
"-Wcast-qual"
"-Wcast-qual"
)
set(MSVC_WARNINGS "/W3")
################################################################################

2
src/api/api_algebraic.cpp
View file

@ -447,4 +447,4 @@ extern "C" {
return _am.get_i(av);
Z3_CATCH_RETURN(0);
}
};
}

2
src/api/api_arith.cpp
View file

@ -235,4 +235,4 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_array.cpp
View file

@ -358,4 +358,4 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_ast.cpp
View file

@ -1547,4 +1547,4 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_ast_map.cpp
View file

@ -161,4 +161,4 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_ast_vector.cpp
View file

@ -135,4 +135,4 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_ast_vector.h
View file

@ -21,7 +21,7 @@ Revision History:
namespace api {
class context;
};
}
struct Z3_ast_vector_ref : public api::object {
ast_ref_vector m_ast_vector;

2
src/api/api_bv.cpp
View file

@ -399,4 +399,4 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_CATCH_RETURN(0);
}
};
}

2
src/api/api_config_params.cpp
View file

@ -121,4 +121,4 @@ extern "C" {
Z3_CATCH;
}
};
}

4
src/api/api_context.cpp
View file

@ -359,7 +359,7 @@ namespace api {
return *(m_rcf_manager.get());
}
};
}
// ------------------------
@ -531,4 +531,4 @@ extern "C" {
Z3_CATCH;
}
};
}

8
src/api/api_context.h
View file

@ -45,16 +45,16 @@ Revision History:
namespace smtlib {
class parser;
};
}
namespace realclosure {
class manager;
};
}
namespace smt2 {
class parser;
void free_parser(parser*);
};
}
namespace api {
@ -267,7 +267,7 @@ namespace api {
};
};
}
inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*>(c); }
#define RESET_ERROR_CODE() { mk_c(c)->reset_error_code(); }

4
src/api/api_datalog.cpp
View file

@ -142,7 +142,7 @@ namespace api {
void collect_param_descrs(param_descrs & p) { m_context.collect_params(p); }
void updt_params(params_ref const& p) { m_context.updt_params(p); }
};
};
}
extern "C" {
@ -705,4 +705,4 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_datalog.h
View file

@ -30,7 +30,7 @@ typedef void (*reduce_assign_callback_fptr)(void*, func_decl*, unsigned, expr*co
namespace api {
class fixedpoint_context;
class context;
};
}
struct Z3_fixedpoint_ref : public api::object {

2
src/api/api_datatype.cpp
View file

@ -687,4 +687,4 @@ extern "C" {
}
};
}

2
src/api/api_finite_set.cpp
View file

@ -184,4 +184,4 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_fpa.cpp
View file

@ -1337,4 +1337,4 @@ extern "C" {
Z3_CATCH_RETURN(false);
}
};
}

2
src/api/api_goal.cpp
View file

@ -213,4 +213,4 @@ extern "C" {
Z3_CATCH_RETURN("");
}
};
}

2
src/api/api_model.cpp
View file

@ -448,4 +448,4 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_numeral.cpp
View file

@ -489,4 +489,4 @@ extern "C" {
}
#endif
};
}

2
src/api/api_opt.cpp
View file

@ -503,4 +503,4 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_params.cpp
View file

@ -212,4 +212,4 @@ extern "C" {
Z3_CATCH_RETURN("");
}
};
}

2
src/api/api_pb.cpp
View file

@ -106,4 +106,4 @@ extern "C" {
}
};
}

2
src/api/api_polynomial.cpp
View file

@ -80,4 +80,4 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_quant.cpp
View file

@ -583,5 +583,5 @@ extern "C" {
return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(p));
}
};
}

2
src/api/api_rcf.cpp
View file

@ -437,4 +437,4 @@ extern "C" {
return from_rcnumeral(rcfm(c).get_sign_condition_coefficient(to_rcnumeral(a), i, j));
Z3_CATCH_RETURN(nullptr);
}
};
}

2
src/api/api_seq.cpp
View file

@ -369,4 +369,4 @@ extern "C" {
MK_FOURARY(Z3_mk_seq_foldli, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDLI, SKIP);
};
}

2
src/api/api_solver.cpp
View file

@ -1218,4 +1218,4 @@ extern "C" {
};
}

2
src/api/api_special_relations.cpp
View file

@ -61,4 +61,4 @@ extern "C" {
}
MK_DECL(Z3_mk_transitive_closure, OP_SPECIAL_RELATION_TC);
};
}

2
src/api/api_stats.cpp
View file

@ -133,4 +133,4 @@ extern "C" {
return memory::get_allocation_size();
}
};
}

2
src/api/api_tactic.cpp
View file

@ -669,4 +669,4 @@ extern "C" {
};
}

2
src/api/api_util.h
View file

@ -46,7 +46,7 @@ namespace api {
void inc_ref();
void dec_ref();
};
};
}
inline ast * to_ast(Z3_ast a) { return reinterpret_cast<ast *>(a); }
inline Z3_ast of_ast(ast* a) { return reinterpret_cast<Z3_ast>(a); }

2
src/ast/arith_decl_plugin.h
View file

@ -24,7 +24,7 @@ class sexpr;
namespace algebraic_numbers {
class anum;
class manager;
};
}
enum arith_sort_kind {
REAL_SORT,

4
src/ast/datatype_decl_plugin.h
View file

@ -171,7 +171,7 @@ namespace datatype {
size* subst(obj_map<sort, size*>& S) override;
sort_size eval(obj_map<sort, sort_size> const& S) override { return S[m_param]; }
};
};
}
class def {
ast_manager& m;
@ -465,7 +465,7 @@ namespace datatype {
sort_ref mk_tuple_datatype(svector<std::pair<symbol, sort*>> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs);
};
};
}
typedef datatype::accessor accessor_decl;
typedef datatype::constructor constructor_decl;

4
src/ast/dl_decl_plugin.cpp
View file

@ -648,7 +648,7 @@ namespace datalog {
m_fid = m.mk_family_id(symbol("datalog_relation"));
}
return m_fid;
};
}
arith_util& dl_decl_util::arith() const {
if (!m_arith) m_arith = alloc(arith_util, m);
@ -788,4 +788,4 @@ namespace datalog {
return m.mk_app(f, num_args, args);
}
};
}

2
src/ast/dl_decl_plugin.h
View file

@ -199,5 +199,5 @@ namespace datalog {
};
};
}

4
src/ast/euf/euf_ac_plugin.h
View file

@ -319,14 +319,14 @@ namespace euf {
struct eq_pp {
ac_plugin const& p; eq const& e;
eq_pp(ac_plugin const& p, eq const& e) : p(p), e(e) {};
eq_pp(ac_plugin const& p, eq const& e) : p(p), e(e) {}
eq_pp(ac_plugin const& p, unsigned eq_id): p(p), e(p.m_active[eq_id]) {}
std::ostream& display(std::ostream& out) const { return p.display_equation(out, e); }
};
struct eq_pp_ll {
ac_plugin const& p; eq const& e;
eq_pp_ll(ac_plugin const& p, eq const& e) : p(p), e(e) {};
eq_pp_ll(ac_plugin const& p, eq const& e) : p(p), e(e) {}
eq_pp_ll(ac_plugin const& p, unsigned eq_id) : p(p), e(p.m_active[eq_id]) {}
std::ostream& display(std::ostream& out) const { return p.display_equation_ll(out, e); }
};

2
src/ast/euf/euf_etable.cpp
View file

@ -276,5 +276,5 @@ namespace euf {
return find(n) == n;
}
};
}

2
src/ast/euf/euf_etable.h
View file

@ -179,7 +179,7 @@ namespace euf {
};
};
}

2
src/ast/euf/euf_mam.h
View file

@ -81,5 +81,5 @@ namespace euf {
static void ground_subterms(expr* e, ptr_vector<app>& ground);
};
};
}

2
src/ast/euf/euf_plugin.h
View file

@ -47,7 +47,7 @@ namespace euf {
virtual void merge_eh(enode* n1, enode* n2) = 0;
virtual void diseq_eh(enode* eq) {};
virtual void diseq_eh(enode* eq) {}
virtual void propagate() = 0;

126
src/ast/euf/ho_matcher.cpp
View file

@ -43,6 +43,7 @@ Author:
--*/
#include "ast/euf/ho_matcher.h"
#include "ast/well_sorted.h"
@ -66,7 +67,15 @@ namespace euf {
void ho_matcher::search() {
IF_VERBOSE(10, display(verbose_stream()));
unsigned budget = m_max_iterations;
while (m.inc()) {
if (budget-- == 0) {
IF_VERBOSE(2, verbose_stream() << "ho_matcher: search budget exhausted\n");
while (!m_backtrack.empty())
backtrack();
break;
}
// Q, B -> Q', B'. Push work on the backtrack stack and new work items
// e, Bw -> Q', B'. Consume backtrack stack
if (!m_goals.empty())
@ -270,6 +279,11 @@ namespace euf {
if (wi.is_done())
return false;
if (wi.level > m_max_depth) {
wi.set_done();
return false;
}
reduce(wi);
auto t = wi.t;
@ -348,6 +362,7 @@ namespace euf {
if (qp->get_decl_sort(i) != qt->get_decl_sort(i))
return false;
m_goals.push(wi.level, wi.term_offset() + td, qp->get_expr(), qt->get_expr());
wi.set_done();
return true;
}
@ -373,6 +388,9 @@ namespace euf {
pats.push_back(to_app(p1));
p1 = to_app(p1)->get_arg(0);
}
// innermost select is a meta variable,
// order patterns from inner-most application to outer-most.
pats.reverse();
auto v = to_var(p1);
if (wi.is_init())
wi.set_project();
@ -421,31 +439,53 @@ namespace euf {
// H (p1) (p2) = f(t1, .., tn)
// H -> \x1 \x2 f(H1(x1, x2), .., Hn(x1, x2))
// H1(p1, p2) = t1, .., Hn(p1, p2) = tn
//
// The select chain `pats` was collected from the outermost
// select down to the flex head, i.e. in reverse order of
// application. The imitating lambda must curry the arguments in
// application order (the first-applied select binds the
// outermost lambda), so process the applications inner-to-outer.
// Without this the constructed lambda has the argument arities
// in the wrong nesting order and its sort disagrees with the
// flex head variable (producing an ill-typed binding).
ptr_vector<sort> domain, pat_domain;
ptr_vector<expr> pat_args;
svector<unsigned> pat_pos; // forward binder position (in domain) of each distinct index
expr_ref_vector args(m), pat_vars(m), bound_args(m);
vector<symbol> names;
pat_args.push_back(nullptr);
pat_vars.push_back(nullptr);
pat_pos.push_back(0); // placeholder for the flex-head slot 0
unsigned num_bound = 0;
expr_mark seen;
for (auto pat : pats) {
for (auto pi : array_select_indices(pat)) {
if (!seen.is_marked(pi)) {
pat_domain.push_back(pi->get_sort());
pat_args.push_back(pi);
pat_pos.push_back(num_bound);
seen.mark(pi);
}
++num_bound;
domain.push_back(pi->get_sort());
names.push_back(symbol(num_bound));
if (seen.is_marked(pi))
continue;
pat_domain.push_back(pi->get_sort());
pat_args.push_back(pi);
seen.mark(pi);
}
}
for (unsigned i = pat_args.size(); i-- > 1; ) {
auto pi = pat_args.get(i);
pat_vars.push_back(m.mk_var(pat_args.size() - i - 1, pi->get_sort()));
}
// pat_vars[k] references the lambda binder for the k-th distinct
// index and must carry that index' sort, so the reconstructed
// select stays aligned with the flex head's array domain
// (pat_domain). The binder at forward position p has de Bruijn
// index num_bound-1-p (the outermost binder has the highest
// index). Emitting in forward slot order keeps the select
// arguments in the same order as pat_domain even when the
// indices have heterogeneous sorts (otherwise the array plugin
// rejects the ill-ordered select).
for (unsigned k = 1; k < pat_args.size(); ++k) {
unsigned db = num_bound - 1 - pat_pos[k];
pat_vars.push_back(m.mk_var(db, pat_args.get(k)->get_sort()));
}
for (auto ti : *ta) {
sort* v_sort = m_array.mk_array_sort(pat_domain.size(), pat_domain.data(), ti->get_sort());
@ -453,7 +493,8 @@ namespace euf {
auto w = m.mk_var(m_subst.size() + wi.pat_offset() + num_bound, v_sort); // shifted by number of bound
m_subst.resize(m_subst.size() + 1);
pat_args[0] = v;
auto sel = m_array.mk_select(pat_args.size(), pat_args.data());
expr_ref sel(m);
sel = m_array.mk_select(pat_args.size(), pat_args.data());
m_goals.push(wi.level + 1, wi.term_offset(), sel, ti);
pat_vars[0] = w;
sel = m_array.mk_select(pat_vars.size(), pat_vars.data());
@ -469,6 +510,7 @@ namespace euf {
num_bound -= sz;
lam = m.mk_lambda(sz, domain.data() + num_bound, names.data() + num_bound, lam);
}
add_binding(v, wi.pat_offset(), lam);
wi.set_done();
return true;
@ -581,6 +623,7 @@ namespace euf {
}
lam = m.mk_lambda(names.size(), sorts.data(), names.data(), lam);
}
SASSERT(is_well_sorted(m, lam));
return lam;
}
@ -622,6 +665,8 @@ namespace euf {
SASSERT(var_sort);
body = m.mk_var(num_binders - i - 1, var_sort);
bind_lambdas(num_lambdas, s, body);
SASSERT(body->get_sort() == s);
SASSERT(is_well_sorted(m, body));
return body;
}
@ -636,6 +681,8 @@ namespace euf {
decl_names.push_back(symbol(i));
}
body = m.mk_lambda(sz, decl_sorts.data(), decl_names.data(), body);
SASSERT(s == body->get_sort());
SASSERT(is_well_sorted(m, body));
}
void ho_matcher::add_binding(var* v, unsigned offset, expr* t) {
@ -655,7 +702,6 @@ namespace euf {
}
auto is_ho = any_of(subterms::all(expr_ref(p, m)), [&](expr* t) {
return m_unitary.is_flex(0, t) ||
// m.is_lambda_def(t) ||
is_lambda(t);
});
if (!is_ho)
@ -674,8 +720,7 @@ namespace euf {
todo.pop_back();
continue;
}
if ((m_unitary.is_flex(0, t) && lvl > 1) || // m.is_lambda_def(t) ||
is_lambda(t)) {
if ((m_unitary.is_flex(0, t) && lvl > 1) || is_lambda(t)) {
if (!contains_pat2abs)
m_pat2abs.insert_if_not_there(p, svector<std::pair<unsigned, expr*>>()).push_back({ nb, t });
auto v = m.mk_var(nb++, t->get_sort());
@ -807,6 +852,7 @@ namespace euf {
auto& abs = m_pat2abs[fo_pat];
verbose_stream() << " m_pat2abs size: " << abs.size() << "\n";
for (auto [v, pat] : abs) verbose_stream() << " v=" << v << " pat=" << mk_pp(pat, m) << "\n";);
unsigned base_scope = m_trail.get_num_scopes();
m_trail.push_scope();
m_subst.resize(0);
m_subst.resize(s.size());
@ -824,17 +870,68 @@ namespace euf {
TRACE(ho_matching, tout << "refine " << mk_pp(p, m) << "\n" << s << "\n");
unsigned num_bound = 0, level = 0;
for (auto [v, pat] : m_pat2abs[fo_pat]) {
// If a binding's sort disagrees with the pattern variable it would
// fill, substituting it would build an ill-sorted term. This can
// arise for deeply nested multi-select patterns whose de Bruijn
// remapping does not line up, or when E-matching delivers a
// candidate binding whose sort is incompatible with the abstracted
// higher-order pattern. Discard this refinement candidate (produce
// no instance) instead of aborting the whole solve.
if (!subst_sorts_match(m, pat, s, true)) {
m_trail.pop_scope(1);
IF_VERBOSE(0, verbose_stream() << "refine_ho_match: sorts do not match for " << mk_pp(pat, m) << " and "
<< s << "\n";);
UNREACHABLE();
return;
}
}
for (auto [v, pat] : m_pat2abs[fo_pat]) {
var_subst sub(m, true);
auto pat_refined = sub(pat, s);
TRACE(ho_matching, tout << mk_pp(pat, m) << " -> " << pat_refined << "\n");
m_goals.push(level, num_bound, pat_refined, m_subst.get(v));
}
search();
m_trail.pop_scope(1);
}
bool ho_matcher::subst_sorts_match(ast_manager& m, expr* t, expr_ref_vector const& s, bool std_order) {
unsigned sz = s.size();
ptr_buffer<expr> es;
svector<unsigned> offs;
es.push_back(t);
offs.push_back(0);
while (!es.empty()) {
expr* e = es.back(); es.pop_back();
unsigned off = offs.back(); offs.pop_back();
if (is_var(e)) {
unsigned idx = to_var(e)->get_idx();
if (idx < off)
continue;
unsigned k = idx - off;
if (k >= sz)
continue;
expr* r = std_order ? s.get(sz - k - 1) : s.get(k);
if (r && r->get_sort() != e->get_sort())
return false;
}
else if (is_app(e)) {
for (expr* arg : *to_app(e)) {
es.push_back(arg);
offs.push_back(off);
}
}
else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
es.push_back(q->get_expr());
offs.push_back(off + q->get_num_decls());
}
}
return true;
}
std::ostream& ho_matcher::display(std::ostream& out) const {
m_subst.display(out << "subst\n");
m_goals.display(out << "goals\n");
@ -853,6 +950,7 @@ namespace euf {
};
void match_goals::push(unsigned level, unsigned offset, expr_ref const& pat, expr_ref const& t) {
SASSERT(pat->get_sort() == t->get_sort());
match_goal* wi = new (ho.trail().get_region()) match_goal(level, offset, pat, t);
ho.trail().push(retire_match_goal(*wi)); // reset on undo
wi->init(wi);

13
src/ast/euf/ho_matcher.h
View file

@ -315,6 +315,8 @@ namespace euf {
match_goals m_goals;
unitary_patterns m_unitary;
ptr_vector<match_goal> m_backtrack;
unsigned m_max_depth = 10; // bound on imitation/projection depth (secondary safety cap)
unsigned m_max_iterations = 10000; // per-search expansion-step budget to guarantee termination
mutable array_rewriter m_rewriter;
array_util m_array;
obj_map<app, app*> m_pat2hopat, m_hopat2pat;
@ -386,6 +388,10 @@ namespace euf {
void set_on_match(std::function<void(ho_subst&)>& on_match) { m_on_match = on_match; }
void set_max_depth(unsigned d) { m_max_depth = d; }
void set_max_iterations(unsigned n) { m_max_iterations = n; }
void operator()(expr *pat, expr *t, unsigned num_vars);
void operator()(expr* pat, expr* t, unsigned num_bound, unsigned num_vars);
@ -400,6 +406,13 @@ namespace euf {
void refine_ho_match(app* p, expr_ref_vector& s);
// Returns true iff applying the substitution s to t (with the given
// variable ordering) is sort-safe: every free variable of t that is
// bound by s maps to a value of the same sort. Used to defensively
// skip higher-order matches whose bindings would produce ill-typed
// instantiation terms (which would otherwise abort the whole solve).
static bool subst_sorts_match(ast_manager& m, expr* t, expr_ref_vector const& s, bool std_order);
bool is_free(app* p, unsigned i) const { return m_hopat2free_vars[p].contains(i); }
quantifier* hoq2q(quantifier* q) const { return m_hoq2q[q]; }

2
src/ast/for_each_expr.cpp
View file

@ -94,7 +94,7 @@ namespace has_skolem_functions_ns {
void operator()(app const * n) const { if (n->get_decl()->is_skolem() && n->get_num_args() > 0) throw found(); }
void operator()(quantifier * n) const {}
};
};
}
bool has_skolem_functions(expr * n) {
has_skolem_functions_ns::proc p;

2
src/ast/format.cpp
View file

@ -195,4 +195,4 @@ namespace format_ns {
return fm(m).mk_app(fid(m), OP_NIL);
}
};
}

2
src/ast/format.h
View file

@ -198,6 +198,6 @@ namespace format_ns {
return mk_seq4(m, begin, end, proc, static_cast<unsigned>(strlen(lp)), lp, rp);
}
};
}

8
src/ast/fpa/fpa2bv_converter.h
View file

@ -162,10 +162,10 @@ public:
void dbg_decouple(const char * prefix, expr_ref & e);
expr_ref_vector m_extra_assertions;
special_t const & get_min_max_specials() const { return m_min_max_ufs; };
const2bv_t const & get_const2bv() const { return m_const2bv; };
const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; };
uf2bvuf_t const & get_uf2bvuf() const { return m_uf2bvuf; };
special_t const & get_min_max_specials() const { return m_min_max_ufs; }
const2bv_t const & get_const2bv() const { return m_const2bv; }
const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; }
uf2bvuf_t const & get_uf2bvuf() const { return m_uf2bvuf; }
protected:
void mk_one(func_decl *f, expr_ref & sign, expr_ref & result);

2
src/ast/macros/macro_manager.cpp
View file

@ -167,7 +167,7 @@ namespace macro_manager_ns {
}
}
};
};
}
/**
\brief Mark all func_decls used in exprs as forbidden.

2
src/ast/macros/quasi_macros.cpp
View file

@ -71,7 +71,7 @@ void quasi_macros::find_occurrences(expr * e) {
default: UNREACHABLE();
}
}
};
}
bool quasi_macros::is_non_ground_uninterp(expr const * e) const {
return is_non_ground(e) && is_uninterp(e);

42
src/ast/pattern/pattern_inference.cpp
View file

@ -42,9 +42,7 @@ bool smaller_pattern::process(expr * p1, expr * p2) {
m_cache.reset();
save(p1, p2);
while (!m_todo.empty()) {
expr_pair & curr = m_todo.back();
p1 = curr.first;
p2 = curr.second;
auto [p1, p2] = m_todo.back();
m_todo.pop_back();
ast_kind k1 = p1->get_kind();
if (k1 != AST_VAR && k1 != p2->get_kind())
@ -123,12 +121,11 @@ void pattern_inference_cfg::collect::operator()(expr * n, unsigned num_bindings)
SASSERT(m_info.empty());
SASSERT(m_todo.empty());
SASSERT(m_cache.empty());
SASSERT(is_well_sorted(m, n));
m_num_bindings = num_bindings;
m_todo.push_back(entry(n, 0));
while (!m_todo.empty()) {
entry & e = m_todo.back();
n = e.m_node;
unsigned delta = e.m_delta;
auto [n, delta] = m_todo.back();
TRACE(collect, tout << "processing: " << n->get_id() << " " << delta << " kind: " << n->get_kind() << "\n";);
TRACE(collect_info, tout << mk_pp(n, m) << "\n";);
if (visit_children(n, delta)) {
@ -177,21 +174,15 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
switch (n->get_kind()) {
case AST_VAR: {
unsigned idx = to_var(n)->get_idx();
if (idx >= delta) {
idx = idx - delta;
uint_set free_vars;
if (idx < m_num_bindings)
free_vars.insert(idx);
info * i = nullptr;
if (delta == 0)
i = alloc(info, m, n, free_vars, 1);
else
i = alloc(info, m, m.mk_var(idx, to_var(n)->get_sort()), free_vars, 1);
save(n, delta, i);
}
else {
if (idx >= m_num_bindings + delta) {
save(n, delta, nullptr);
return;
}
uint_set free_vars;
if (delta <= idx)
free_vars.insert(idx - delta);
info * i = alloc(info, m, n, free_vars, 1);
save(n, delta, i);
return;
}
case AST_APP: {
@ -247,7 +238,8 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
// stating properties about these operators.
family_id fid = c->get_family_id();
decl_kind k = c->get_decl_kind();
if (!free_vars.empty() &&
if (!free_vars.empty() &&
delta == 0 &&
(fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only && (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL)))) {
TRACE(pattern_inference, tout << "potential candidate: \n" << mk_pp(new_node, m) << "\n";);
m_owner.add_candidate(new_node, free_vars, size);
@ -258,15 +250,13 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
quantifier * q = to_quantifier(n);
unsigned num_decls = q->get_num_decls();
info * body_info = nullptr;
m_cache.find(entry(q->get_expr(), delta + num_decls), body_info);
if (body_info == nullptr) {
expr *body = q->get_expr();
m_cache.find(entry(body, delta + num_decls), body_info);
if (!body_info) {
save(n, delta, nullptr);
return;
}
// The lambda/quantifier itself is a valid sub-term in a pattern.
// Propagate the free variables from the body (they already refer
// to the outer quantifier's bindings) and keep the node as-is.
expr * new_body = body_info->m_node.get();
expr *new_body = body_info->m_node.get();
quantifier_ref new_q(m);
if (new_body != q->get_expr())
new_q = m.update_quantifier(q, new_body);

9
src/ast/polymorphism_inst.cpp
View file

@ -57,9 +57,11 @@ namespace polymorphism {
m_assertions.push_back(e);
t.push(push_back_vector(m_assertions));
u.collect_type_vars(e, inst.m_tvs);
auto* init = alloc(substitution, m);
inst.m_subst = alloc(substitutions);
inst.m_subst->insert(alloc(substitution, m));
inst.m_subst->insert(init);
m_instances.insert(e, inst);
t.push(new_obj_trail(init));
t.push(new_obj_trail(inst.m_subst));
t.push(insert_map(m_instances, e));
}
@ -107,13 +109,14 @@ namespace polymorphism {
auto const& [tv, fns, substs] = m_instances[e];
for (auto* f2 : fns) {
substitution sub1(m), new_sub(m);
substitution sub1(m);
if (!u.unify(f1, f2, sub1))
continue;
if (substs->contains(&sub1))
continue;
substitutions new_substs;
for (auto* sub2 : *substs) {
substitution new_sub(m);
if (!u.unify(sub1, *sub2, new_sub))
continue;
if (substs->contains(&new_sub))
@ -128,7 +131,7 @@ namespace polymorphism {
new_substs.insert(new_sub1);
m_from_instantiation.insert(e_inst);
m.inc_ref(e_inst);
t.push(insert_ref_map(m, m_from_instantiation, e_inst));
t.push(insert_ref_map(m, m_from_instantiation, e_inst.get()));
}
}
for (auto* sub2 : new_substs) {

2
src/ast/polymorphism_inst.h
View file

@ -58,7 +58,7 @@ namespace polymorphism {
void undo() override {
i.m_in_decl_queue.mark(i.m_decl_queue.back(), false);
i.m_decl_queue.pop_back();
};
}
};
struct remove_back : public trail {

24
src/ast/polymorphism_util.cpp
View file

@ -39,11 +39,13 @@ namespace polymorphism {
}
unsigned n = s->get_num_parameters();
vector<parameter> ps;
sort_ref_vector pin(m); // keep substituted sub-sorts alive until mk_sort below
for (unsigned i = 0; i < n; ++i) {
auto &p = s->get_parameter(i);
if (p.is_ast() && is_sort(p.get_ast())) {
sort_ref s = (*this)(to_sort(p.get_ast()));
ps.push_back(parameter(s.get()));
sort_ref ss = (*this)(to_sort(p.get_ast()));
pin.push_back(ss);
ps.push_back(parameter(ss.get()));
}
else
ps.push_back(p);
@ -242,15 +244,27 @@ namespace polymorphism {
bool util::unify(substitution const& s1, substitution const& s2,
substitution& sub) {
sort* v2;
for (auto const& [k, v] : s1)
SASSERT(&s1 != &sub);
SASSERT(&s2 != &sub);
for (auto const& [k, v] : s1) {
// Guard against building a cyclic substitution (e.g. A |-> list(A)),
// which would make substitution application diverge. Such a binding
// means the two substitutions are not simultaneously unifiable.
if (occurs(k, v))
return false;
sub.insert(k, v);
}
for (auto const& [k, v] : s2) {
if (sub.find(k, v2)) {
if (!sub.unify(sub(v), v2))
return false;
}
else
sub.insert(k, sub(v));
else {
sort_ref vr = sub(v);
if (occurs(k, vr))
return false;
sub.insert(k, vr);
}
}
return true;
}

2
src/ast/quantifier_stat.cpp
View file

@ -115,5 +115,5 @@ namespace q {
return r;
}
};
}

2
src/ast/quantifier_stat.h
View file

@ -149,6 +149,6 @@ namespace q {
quantifier_stat * operator()(quantifier * q, unsigned generation);
};
};
}

4
src/ast/recfun_decl_plugin.h
View file

@ -60,7 +60,7 @@ namespace recfun {
func_decl_ref m_pred; //<! predicate used for this case
expr_ref_vector m_guards; //<! conjunction that is equivalent to this case
expr_ref m_rhs; //<! if guard is true, `f(t1...tn) = rhs` holds
def * m_def = nullptr;; //<! definition this is a part of
def * m_def = nullptr; //<! definition this is a part of
bool m_immediate = false; //<! does `rhs` contain no defined_fun/case_pred?
case_def(ast_manager& m):
@ -92,7 +92,7 @@ namespace recfun {
expr * get_guard(unsigned i) const { return m_guards[i]; }
expr * get_rhs() const { return m_rhs; }
unsigned num_guards() const { return m_guards.size(); }
bool is_immediate() const { return m_immediate; };
bool is_immediate() const { return m_immediate; }
void set_is_immediate(bool b) { m_immediate = b; }
};

2
src/ast/rewriter/array_rewriter.cpp
View file

@ -21,6 +21,7 @@ Notes:
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/well_sorted.h"
#include "ast/rewriter/var_subst.h"
#include "params/array_rewriter_params.hpp"
#include "util/util.h"
@ -818,6 +819,7 @@ expr_ref array_rewriter::expand_store(expr* s) {
result = m().mk_ite(mk_and(eqs), tmp, result);
}
result = m().mk_lambda(sorts.size(), sorts.data(), names.data(), result);
SASSERT(is_well_sorted(m(), result));
return result;
}

2
src/ast/rewriter/bv_bounds.h
View file

@ -34,7 +34,7 @@ public:
typedef rational numeral;
typedef std::pair<numeral, numeral> interval;
typedef obj_map<app, numeral> bound_map;
bv_bounds(ast_manager& m) : m_m(m), m_bv_util(m), m_okay(true) {};
bv_bounds(ast_manager& m) : m_m(m), m_bv_util(m), m_okay(true) {}
~bv_bounds();
public: // bounds addition methods
br_status rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result);

9
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2678,8 +2678,15 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
}
bool bv_rewriter::is_concat_split_target(expr * t) const {
// A bare (de Bruijn) variable is deliberately excluded as a split target:
// splitting (= x (concat ...)) into per-slice extract equalities rewrites
// an eliminable (= VAR t) equality into (= (extract .. VAR) t) fragments
// that destructive equality resolution (der) can no longer use to eliminate
// the bound variable, turning solvable quantified goals into residual
// quantifiers. Splitting is only a bit-blasting heuristic, so skipping it
// here is sound and preserves der-based variable elimination.
return
m_split_concat_eq ||
(m_split_concat_eq && !is_var(t)) ||
m_util.is_concat(t) ||
m_util.is_numeral(t) ||
m_util.is_bv_or(t);

2
src/ast/rewriter/seq_axioms.h
View file

@ -123,5 +123,5 @@ namespace seq {
};
};
}

2
src/ast/rewriter/seq_eq_solver.cpp
View file

@ -727,5 +727,5 @@ namespace seq {
};
}

2
src/ast/rewriter/seq_eq_solver.h
View file

@ -167,5 +167,5 @@ namespace seq {
};
};
}

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

@ -3263,6 +3263,39 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
return BR_DONE;
}
// (str.in_re e (re.range lo hi)) where a bound is not a concrete character.
// By SMT-LIB semantics (re.range lo hi) is the set of single characters c
// with lo <= c <= hi when lo and hi are themselves single characters, and
// the empty language otherwise; so membership is equivalent to lo, hi and
// e all being single characters with lo <= e <= hi. The derivative engine
// only unfolds ranges whose bounds are concrete characters, so without this
// reduction a range with a symbolic bound is left unsolved (and mk_re_range
// deliberately keeps such a range symbolic rather than unsoundly collapsing
// it to re.empty). Ranges with two concrete single-character bounds keep
// their existing derivative-based handling.
{
expr* rlo = nullptr, *rhi = nullptr;
if (re().is_range(b, rlo, rhi)) {
auto concrete_char = [&](expr* e) {
zstring s;
expr* ch = nullptr;
unsigned uc = 0;
return (str().is_string(e, s) && s.length() == 1) ||
(str().is_unit(e, ch) && m_util.is_const_char(ch, uc));
};
if (!concrete_char(rlo) || !concrete_char(rhi)) {
expr_ref_vector conj(m());
conj.push_back(m().mk_eq(str().mk_length(rlo), one()));
conj.push_back(m().mk_eq(str().mk_length(rhi), one()));
conj.push_back(m().mk_eq(str().mk_length(a), one()));
conj.push_back(str().mk_lex_le(rlo, a));
conj.push_back(str().mk_lex_le(a, rhi));
result = m().mk_and(conj);
return BR_REWRITE_FULL;
}
}
}
zstring s;
if (str().is_string(a, s) && re().is_ground(b)) {
// Just check membership and replace by true/false
@ -4122,39 +4155,55 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
len = min_length(hi).second;
if (len > 1)
is_empty = true;
// A bound that is provably of length 0 (e.g. the empty string "") can
// likewise never be a single character, so the range is empty. Unlike a
// symbolic bound, max_length == 0 is a provable emptiness fact, so this is
// sound (it is never true for a model-dependent bound such as a variable).
if (max_length(lo) == std::make_pair(true, rational(0)))
is_empty = true;
if (max_length(hi) == std::make_pair(true, rational(0)))
is_empty = true;
if (!is_empty) {
if (str().is_string(lo, slo) && slo.length() == 1)
clo = slo[0];
else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo))
;
else
is_empty = true;
}
if (!is_empty) {
if (str().is_string(hi, shi) && shi.length() == 1)
chi = shi[0];
else if (str().is_unit(hi, hi1) && m_util.is_const_char(hi1, chi))
;
else
is_empty = true;
}
// clo/chi are only meaningful once both bounds were extracted; an early
// is_empty (from the length checks) leaves them at their default 0, so the
// is_empty return must come before the singleton/ordering checks below.
if (!is_empty && clo > chi)
is_empty = true;
// A provable length constraint (a bound can never be a single character)
// is the only sound way to conclude emptiness for a possibly-symbolic
// bound, so decide emptiness here before attempting to read concrete
// characters.
if (is_empty) {
sort* srt = re().mk_re(lo->get_sort());
result = re().mk_empty(srt);
return BR_DONE;
}
// Try to read concrete single-character bounds. A bound that is not a
// syntactic single-character literal is *symbolic* (its value depends on
// the model), NOT empty: collapsing such a range to re.empty is unsound
// (e.g. (re.range x x) is {x} whenever x is a single character), so we
// leave the range unevaluated (BR_FAILED) and let the theory solver
// reason about it.
bool has_clo = false, has_chi = false;
if (str().is_string(lo, slo) && slo.length() == 1) {
clo = slo[0];
has_clo = true;
}
else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo))
has_clo = true;
if (str().is_string(hi, shi) && shi.length() == 1) {
chi = shi[0];
has_chi = true;
}
else if (str().is_unit(hi, hi1) && m_util.is_const_char(hi1, chi))
has_chi = true;
if (!has_clo || !has_chi)
return BR_FAILED;
// Both bounds are concrete characters: an inverted range is empty.
if (clo > chi) {
sort* srt = re().mk_re(lo->get_sort());
result = re().mk_empty(srt);
return BR_DONE;
}
// Singleton: re.range "a" "a" → str.to_re "a"
if (clo == chi) {
result = re().mk_to_re(str().mk_string(zstring(clo)));

2
src/ast/rewriter/seq_skolem.h
View file

@ -171,5 +171,5 @@ namespace seq {
};
};
}

1
src/ast/rewriter/seq_split.cpp
View file

@ -1,3 +1,4 @@
/*++
Copyright (c) 2026 Microsoft Corporation

2
src/ast/simplifiers/distribute_forall.cpp
View file

@ -101,5 +101,5 @@ void distribute_forall_simplifier::reduce() {
if (r != d.fml())
m_fmls.update(idx, dependent_expr(m, r, mp(d.pr(), pr), d.dep()));
}
};
}

13
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -116,6 +116,7 @@ eliminate:
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/polymorphism_util.h"
#include "ast/simplifiers/elim_unconstrained.h"
elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) :
@ -425,6 +426,18 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
void elim_unconstrained::reduce() {
if (!m_config.m_enabled)
return;
// has_type_vars() is a manager-wide flag that is set as soon as any type variable is
// created, including the ones used to define polymorphic signatures of builtin plugins
// (e.g. finite_set) that never occur in the asserted formulas. Only bail out when the
// formulas actually contain type-variable typed terms, which this simplifier cannot invert.
if (m.has_type_vars()) {
polymorphism::util u(m);
for (unsigned i : indices()) {
auto [f, p, d] = m_fmls[i]();
if (u.has_type_vars(f))
return;
}
}
generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
m_inverter.set_model_converter(mc.get());
m_created_compound = true;

2
src/ast/simplifiers/propagate_values.cpp
View file

@ -62,7 +62,7 @@ void propagate_values::add_sub(dependent_expr const& de) {
else if (m.is_value(y) && m_shared.is_shared(x))
m_subst.insert(x, y, dep);
}
};
}
void propagate_values::reduce() {
m_shared.reset();

6
src/ast/sls/sls_array_plugin.h
View file

@ -36,7 +36,7 @@ namespace sls {
for (unsigned i = 1; i < a.sel->num_args(); ++i)
h ^= a.sel->get_arg(i)->get_root()->hash();
return h;
};
}
};
struct select_args_eq {
bool operator()(select_args const& a, select_args const& b) const {
@ -103,13 +103,13 @@ namespace sls {
euf::enode* mk_select(euf::egraph& g, euf::enode* b, euf::enode* sel);
void resolve_conflict();
size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); };
size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); }
size_t* to_ptr(euf::enode* t) { return reinterpret_cast<size_t*>((reinterpret_cast<size_t>(t) << 4) + 1); }
size_t* to_ptr(unsigned n) { return reinterpret_cast<size_t*>((size_t)(n << 4) + 3); }
bool is_literal(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 0; }
bool is_index(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 3; }
bool is_enode(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 1; }
sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); };
sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); }
euf::enode* to_enode(size_t* p) { return reinterpret_cast<euf::enode*>(reinterpret_cast<size_t>(p) >> 4); }
unsigned to_index(size_t* p) { return static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4); }

4
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -871,8 +871,8 @@ namespace sls {
if (m_la.m_config.use_top_level_assertions)
return m_la.ctx.input_assertions().get(idx);
return m_la.ctx.atom(m_la.ctx.root_literals()[idx].var());
};
}
}
}

2
src/ast/sls/sls_bv_tracker.h
View file

@ -40,7 +40,7 @@ class sls_tracker {
mpz m_zero, m_one, m_two;
struct value_score {
value_score() : value(unsynch_mpz_manager::mk_z(0)) {};
value_score() : value(unsynch_mpz_manager::mk_z(0)) {}
value_score(value_score&&) noexcept = default;
value_score(const value_score &other) {
m = other.m;

6
src/ast/sls/sls_context.h
View file

@ -44,15 +44,15 @@ namespace sls {
virtual expr_ref get_value(expr* e) = 0;
virtual bool is_fixed(expr* e, expr_ref& value) { return false; }
virtual void initialize() = 0;
virtual void start_propagation() {};
virtual void start_propagation() {}
virtual bool propagate() = 0;
virtual void propagate_literal(sat::literal lit) = 0;
virtual void repair_literal(sat::literal lit) = 0;
virtual bool repair_down(app* e) = 0;
virtual void repair_up(app* e) = 0;
virtual bool is_sat() = 0;
virtual void on_rescale() {};
virtual void on_restart() {};
virtual void on_rescale() {}
virtual void on_restart() {}
virtual std::ostream& display(std::ostream& out) const = 0;
virtual bool set_value(expr* e, expr* v) = 0;
virtual void collect_statistics(statistics& st) const = 0;

4
src/ast/sls/sls_euf_plugin.h
View file

@ -52,8 +52,8 @@ namespace sls {
bool is_user_sort(sort* s) { return s->get_family_id() == user_sort_family_id; }
size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); };
sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); };
size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); }
sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); }
void validate_model();
void log_clause(sat::literal_vector const& lits);

94
src/ast/well_sorted.cpp
View file

@ -25,31 +25,73 @@ Revision History:
#include "util/warning.h"
#include "ast/ast_smt2_pp.h"
namespace {
struct well_sorted_proc {
ast_manager & m_manager;
bool m_error;
ast_manager & m;
bool m_error;
ptr_vector<sort> m_binding;
well_sorted_proc(ast_manager & m):m_manager(m), m_error(false) {}
void operator()(var * v) {}
well_sorted_proc(ast_manager & m):m(m), m_error(false) {}
void operator()(quantifier * n) {
expr const * e = n->get_expr();
if (!is_lambda(n) && !m_manager.is_bool(e)) {
warning_msg("quantifier's body must be a boolean.");
m_error = true;
UNREACHABLE();
void check(expr* e) {
ptr_vector<expr> todo;
expr_mark visited;
todo.push_back(e);
while (!todo.empty()) {
expr* term = todo.back();
todo.pop_back();
if (visited.is_marked(term))
continue;
visited.mark(term, true);
if (is_app(term)) {
for (expr* arg : *to_app(term))
if (!visited.is_marked(arg))
todo.push_back(arg);
check_app(to_app(term));
}
else if (is_var(term)) {
check_var(to_var(term));
}
else if (is_quantifier(term)) {
check_quantifier(to_quantifier(term));
}
}
}
void operator()(app * n) {
void check_quantifier(quantifier * n) {
if (!is_lambda(n) && !m.is_bool(n->get_expr())) {
warning_msg("quantifier's body must be a boolean.");
m_error = true;
}
unsigned sz = m_binding.size();
m_binding.append(n->get_num_decls(), n->get_decl_sorts());
for (unsigned i = 0; i < n->get_num_patterns(); i++)
check(n->get_pattern(i));
check(n->get_expr());
m_binding.shrink(sz);
}
void check_var(var* v) {
if (v->get_idx() >= m_binding.size()) {
return;
}
sort *s = m_binding[m_binding.size() - v->get_idx() - 1];
if (s != v->get_sort()) {
warning_msg("variable sort does not match binding sort.");
m_error = true;
// UNREACHABLE();
}
}
void check_app(app * n) {
unsigned num_args = n->get_num_args();
func_decl * decl = n->get_decl();
if (num_args != decl->get_arity() && !decl->is_associative() &&
!decl->is_right_associative() && !decl->is_left_associative()) {
TRACE(ws, tout << "unexpected number of arguments.\n" << mk_ismt2_pp(n, m_manager););
TRACE(ws, tout << "unexpected number of arguments.\n" << mk_ismt2_pp(n, m););
warning_msg("unexpected number of arguments.");
m_error = true;
return;
@ -59,19 +101,20 @@ struct well_sorted_proc {
sort * actual_sort = n->get_arg(i)->get_sort();
sort * expected_sort = decl->is_associative() ? decl->get_domain(0) : decl->get_domain(i);
if (expected_sort != actual_sort) {
TRACE(tc, tout << "sort mismatch on argument #" << i << ".\n" << mk_ismt2_pp(n, m_manager);
tout << "Sort mismatch for argument " << i+1 << " of " << mk_ismt2_pp(n, m_manager, false) << "\n";
tout << "Expected sort: " << mk_pp(expected_sort, m_manager) << "\n";
tout << "Actual sort: " << mk_pp(actual_sort, m_manager) << "\n";
tout << "Function sort: " << mk_pp(decl, m_manager) << ".";
TRACE(tc, tout << "sort mismatch on argument #" << i << ".\n" << mk_ismt2_pp(n, m);
tout << "Sort mismatch for argument " << i+1 << " of " << mk_ismt2_pp(n, m, false) << "\n";
tout << "Expected sort: " << mk_pp(expected_sort, m) << "\n";
tout << "Actual sort: " << mk_pp(actual_sort, m) << "\n";
tout << "Function sort: " << mk_pp(decl, m) << ".";
);
std::ostringstream strm;
strm << "Sort mismatch for argument " << i+1 << " of " << mk_ll_pp(n, m_manager, false) << "\n";
strm << "Expected sort: " << mk_pp(expected_sort, m_manager) << '\n';
strm << "Actual sort: " << mk_pp(actual_sort, m_manager) << '\n';
strm << "Function sort: " << mk_pp(decl, m_manager) << '.';
strm << "Sort mismatch for argument " << i+1 << " of " << mk_ll_pp(n, m, false) << "\n";
strm << "Expected sort: " << mk_pp(expected_sort, m) << '\n';
strm << "Actual sort: " << mk_pp(actual_sort, m) << '\n';
strm << "Function sort: " << mk_pp(decl, m) << '.';
warning_msg("%s", std::move(strm).str().c_str());
m_error = true;
// UNREACHABLE();
return;
}
}
@ -82,8 +125,11 @@ struct well_sorted_proc {
bool is_well_sorted(ast_manager const & m, expr * n) {
well_sorted_proc p(const_cast<ast_manager&>(m));
for_each_expr(p, n);
p.check(n);
if (p.m_error) {
IF_VERBOSE(0, verbose_stream() << "expression is not well sorted.\n" << mk_pp(n, const_cast<ast_manager&>(m)) << "\n";);
IF_VERBOSE(0, verbose_stream() << mk_ll_pp(n, const_cast<ast_manager &>(m)) << "\n";);
}
return !p.m_error;
}

6
src/cmd_context/extra_cmds/dbg_cmds.cpp
View file

@ -581,7 +581,7 @@ class mbp_qel_cmd : public cmd {
ptr_vector<expr> m_vars;
public:
mbp_qel_cmd() : cmd("mbp-qel"){};
mbp_qel_cmd() : cmd("mbp-qel"){}
char const *get_usage() const override { return "(exprs) (vars)"; }
char const *get_descr(cmd_context &ctx) const override {
return "Model based projection using e-graphs";
@ -639,7 +639,7 @@ class qel_cmd : public cmd {
ptr_vector<func_decl> m_vars;
public:
qel_cmd() : cmd("qel"){};
qel_cmd() : cmd("qel"){}
char const *get_usage() const override { return "(lits) (vars)"; }
char const *get_descr(cmd_context &ctx) const override {
return "QE lite over e-graphs";
@ -703,7 +703,7 @@ class qe_lite_cmd : public cmd {
ptr_vector<func_decl> m_vars;
public:
qe_lite_cmd() : cmd("qe-lite"){};
qe_lite_cmd() : cmd("qe-lite"){}
char const *get_usage() const override { return "(lits) (vars)"; }
char const *get_descr(cmd_context &ctx) const override {
return "QE lite over e-graphs";

785
src/cmd_context/tptp_frontend.cpp
View file

File diff suppressed because it is too large Load diff

2
src/math/grobner/pdd_simplifier.cpp
View file

@ -494,7 +494,7 @@ namespace dd {
hash(unsigned_vector& vars):vars(vars) {}
bool operator()(mon const& m) const {
return unsigned_ptr_hash(vars.data() + m.offset, m.sz, 1);
};
}
};
struct eq {
unsigned_vector& vars;

20
src/math/lp/lar_solver.cpp
View file

@ -63,6 +63,7 @@ namespace lp {
unsigned_vector m_row_bounds_to_replay;
u_dependency_manager m_dependencies;
svector<constraint_index> m_tmp_dependencies;
ptr_vector<u_dependency> m_tmp_witnesses;
u_dependency* m_crossed_bounds_deps = nullptr;
lpvar m_crossed_bounds_column = null_lpvar;
@ -1132,6 +1133,24 @@ namespace lp {
ex.push_back(ci);
}
// Linearize the bound witnesses of all fixed columns in the row together, so the
// mark bits walk each dependency sub-DAG shared between columns only once.
void lar_solver::explain_fixed_in_row(unsigned row, explanation& ex) {
auto& witnesses = m_imp->m_tmp_witnesses;
witnesses.reset();
for (auto const& c : get_row(row)) {
if (!column_is_fixed(c.var()))
continue;
const column& ul = m_imp->m_columns[c.var()];
witnesses.push_back(ul.lower_bound_witness());
witnesses.push_back(ul.upper_bound_witness());
}
m_imp->m_tmp_dependencies.reset();
m_imp->m_dependencies.linearize(witnesses, m_imp->m_tmp_dependencies);
for (auto ci : m_imp->m_tmp_dependencies)
ex.push_back(ci);
}
void lar_solver::remove_fixed_vars_from_base() {
// this will allow to disable and restore the tracking of the touched rows
flet<indexed_uint_set*> f(get_core_solver().m_r_solver.m_touched_rows, nullptr);
@ -3006,4 +3025,3 @@ namespace lp {
}
} // namespace lp

1
src/math/lp/lar_solver.h
View file

@ -521,6 +521,7 @@ public:
}
void explain_fixed_column(unsigned j, explanation& ex);
void explain_fixed_in_row(unsigned row, explanation& ex);
u_dependency* join_deps(u_dependency* a, u_dependency *b) { return dep_manager().mk_join(a, b); }
const constraint_set & constraints() const;
void push();

16
src/math/lp/lp_bound_propagator.h
View file

@ -248,22 +248,16 @@ public:
void explain_fixed_in_row(unsigned row, explanation& ex) {
TRACE(eq, tout << lp().get_row(row) << std::endl);
for (const auto& c : lp().get_row(row))
if (lp().column_is_fixed(c.var()))
lp().explain_fixed_column(c.var(), ex);
lp().explain_fixed_in_row(row, ex);
}
unsigned explain_fixed_in_row_and_get_base(unsigned row, explanation& ex) {
unsigned base = UINT_MAX;
TRACE(eq, tout << lp().get_row(row) << std::endl);
for (const auto& c : lp().get_row(row)) {
if (lp().column_is_fixed(c.var())) {
lp().explain_fixed_column(c.var(), ex);
}
else if (lp().is_base(c.var())) {
lp().explain_fixed_in_row(row, ex);
unsigned base = UINT_MAX;
for (const auto& c : lp().get_row(row))
if (!lp().column_is_fixed(c.var()) && lp().is_base(c.var()))
base = c.var();
}
}
return base;
}

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

@ -267,7 +267,7 @@ namespace lp {
unsigned j, const T &m, X &theta, bool &unlimited) {
SASSERT(m > 0 && this->m_column_types[j] == column_type::upper_bound);
limit_inf_on_bound_m_pos(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited);
};
}
void get_bound_on_variable_and_update_leaving_precisely(
unsigned j, vector<unsigned> &leavings, T m, X &t,

6
src/math/lp/nla_types.h
View file

@ -43,9 +43,9 @@ namespace nla {
ineq(lpvar v, lp::lconstraint_kind cmp, rational const& r): m_cmp(cmp), m_term(v), m_rs(r) {}
bool operator==(const ineq& a) const = delete;
bool operator!=(const ineq& a) const = delete;
const lp::lar_term& term() const { return m_term; };
lp::lconstraint_kind cmp() const { return m_cmp; };
const rational& rs() const { return m_rs; };
const lp::lar_term& term() const { return m_term; }
lp::lconstraint_kind cmp() const { return m_cmp; }
const rational& rs() const { return m_rs; }
};
class lemma {

2
src/math/polynomial/algebraic_numbers.cpp
View file

@ -3511,4 +3511,4 @@ namespace algebraic_numbers {
void manager::collect_statistics(statistics & st) const {
m_imp->collect_statistics(st);
}
};
}

2
src/math/polynomial/algebraic_numbers.h
View file

@ -410,7 +410,7 @@ namespace algebraic_numbers {
anum& operator=(basic_cell* cell) { SASSERT(is_null()); m_cell = TAG(void*, cell, BASIC); return *this; }
anum& operator=(algebraic_cell* cell) { SASSERT(is_null()); m_cell = TAG(void*, cell, ROOT); return *this; }
};
};
}
typedef algebraic_numbers::manager anum_manager;
typedef algebraic_numbers::manager::numeral anum;

Some files were not shown because too many files have changed in this diff Show more