diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 0bf2aef61..d31edc45f 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -49,7 +49,8 @@ jobs: timeoutInMinutes: 90 pool: vmImage: "ubuntu-latest" - container: "quay.io/pypa/manylinux2014_x86_64:latest" + container: "quay.io/pypa/manylinux_2_34_x86_64:latest" + condition: eq(1,1) steps: - script: "/opt/python/cp38-cp38/bin/python -m venv $PWD/env" - script: 'echo "##vso[task.prependpath]$PWD/env/bin"' @@ -66,7 +67,6 @@ jobs: pool: vmImage: "ubuntu-latest" container: "quay.io/pypa/manylinux2014_x86_64:latest" - condition: eq(0,1) steps: - script: curl -L -o /tmp/arm-toolchain.tar.xz 'https://developer.arm.com/-/media/Files/downloads/gnu/11.2-2022.02/binrel/gcc-arm-11.2-2022.02-x86_64-aarch64-none-linux-gnu.tar.xz?rev=33c6e30e5ac64e6dba8f0431f2c35f1b&hash=9918A05BF47621B632C7A5C8D2BB438FB80A4480' - script: mkdir -p /tmp/arm-toolchain/ diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c7ce4801a..ec889da61 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -120,6 +120,9 @@ namespace smt { if (!m_setup.already_configured()) { m_fparams.updt_params(p); } + for (auto th : m_theory_set) + if (th) + th->updt_params(); } unsigned context::relevancy_lvl() const { diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 20c7380eb..8e23a6644 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -417,6 +417,8 @@ namespace smt { smt_params const& get_fparams() const; + virtual void updt_params() {} + enode * get_enode(theory_var v) const { SASSERT(v < static_cast(m_var2enode.size())); return m_var2enode[v]; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 2c58400ba..9af1c492f 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -870,15 +870,10 @@ public: get_zero(true); get_zero(false); + lp().updt_params(ctx().get_params()); lp().settings().set_resource_limit(m_resource_limit); lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode(); - - // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts - unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio; - lp().set_cut_strategy(branch_cut_ratio); - - lp().settings().set_run_gcd_test(ctx().get_fparams().m_arith_gcd_test); lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); m_lia = alloc(lp::int_solver, *m_solver.get()); } @@ -4199,6 +4194,13 @@ public: m_bound_predicate = nullptr; } + void updt_params() { + if (m_solver) + m_solver->updt_params(ctx().get_params()); + if (m_nla) + m_nla->updt_params(ctx().get_params()); + } + void validate_model(proto_model& mdl) { @@ -4359,6 +4361,10 @@ void theory_lra::setup() { m_imp->setup(); } +void theory_lra::updt_params() { + m_imp->updt_params(); +} + void theory_lra::validate_model(proto_model& mdl) { m_imp->validate_model(mdl); } diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index 1624bab0a..64d200506 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -94,6 +94,8 @@ namespace smt { bool get_lower(enode* n, rational& r, bool& is_strict); bool get_upper(enode* n, rational& r, bool& is_strict); void solve_for(vector& s) override; + + void updt_params() override; void display(std::ostream & out) const override;