kpriv/pkgsrc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
pkgsrc/math/z3/options.mk

24 lines
523 B
Makefile
Raw Normal View History

z3: Upgrade to 4.8.3 Eliminate merged patches. Improve java support. Patch by Michal Gorny. Upstream changelog ================== z3-4.8.3 This release covers bug fixes since 4.8.1 .NET bindings for dotnet standard 1.4 on windows and 64 bit Linux systems and MacOs z3-4.8.1 New requirements: A breaking change to the API is that parsers for SMT-LIB2 formulas return a vector of formulas as opposed to a conjunction of formulas. The vector of formulas correspond to the set of "assert" instructions in the SMT-LIB input. New features A parallel mode is available for select theories, including QF_BV. By setting parallel.enable=true Z3 will spawn a number of worker threads proportional to the number of available CPU cores to apply cube and conquer solving on the goal. The SAT solver by default handle cardinality and PB constraints using a custom plugin that operates directly on cardinality and PB constraints. A "cube" interface is exposed over the solver API. Model conversion is first class over the textual API, such that subgoals created from running a solver can be passed in text files and a model for the original formula can be recreated from the result. This has also led to changes in how models are tracked over tactic subgoals. The API for extracting models from apply_result have been replaced. An optional mode handles xor constraints using a custom xor propagator. It is off by default and its value not demonstrated. The SAT solver includes new inprocessing techniques that are available during simplification. It performs asymmetric tautology elimination by default, and one can turn on more powerful inprocessing techniques (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs. Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged as lemmas (redundant) and are garbage collected if their glue level is high. Substantial overhaul of the spacer horn clause engine. Added basic features to support Lambda bindings. Added model compression to eliminate local function definitions in models when inlining them does not incur substantial overhead. The old behavior, where models are left uncompressed can be replayed by setting the top-level parameter model_compress=false. Integration of a new solver for linear integer arithmetic and mixed linear integer arithmetic by Lev Nachmanson. It incorporates several improvements to QF_LIA solving based on . using a better LP engine, which is already the foundation for QF_LRA . including cuts based on Hermite Normal Form (thanks to approaches described in "cuts from proofs" and "cutting the mix"). . extracting integer solutions from LP solutions by tightening bounds selectively. We use a generalization of Bromberger and Weidenbach that allows avoiding selected bounds tighthenings (https://easychair.org/publications/paper/qGfG). It solves significantly more problems in the QF_LIA category and may at this point also be the best solver for your problem as well. The new solver is enabled only for select SMT-LIB logics. These include QF_LIA, QF_IDL, and QF_UFLIA. Other theories (still) use the legacy solver for arithmetic. You can enable the new solver by setting the parameter smt.arith.solver=6 to give it a spin. Removed features: interpolation API duality engine for constrained Horn clauses. pdr engine for constrained Horn clauses. The engine's functionality has been folded into spacer as one of optional strategies. long deprecated API functions have been removed from z3_api.h Z3 4.7.1. official release cumulative bug fix since 4.6.0 minor version incremented as API now uses stdbool and stdint: bool and int64_t, uint64_t Official release Z3 4.6.0.
2018-12-18 07:46:39 +01:00
# $NetBSD: options.mk,v 1.4 2018/12/18 06:46:39 kamil Exp $
Package the Z3 theorem prover / SMT solver from Microsoft Research.
2015-11-24 06:45:58 +01:00
PKG_OPTIONS_VAR= PKG_OPTIONS.z3
PKG_SUPPORTED_OPTIONS= ocaml java
PKG_SUGGESTED_OPTIONS= ocaml
.include "../../mk/bsd.options.mk"
z3: Upgrade to 4.8.3 Eliminate merged patches. Improve java support. Patch by Michal Gorny. Upstream changelog ================== z3-4.8.3 This release covers bug fixes since 4.8.1 .NET bindings for dotnet standard 1.4 on windows and 64 bit Linux systems and MacOs z3-4.8.1 New requirements: A breaking change to the API is that parsers for SMT-LIB2 formulas return a vector of formulas as opposed to a conjunction of formulas. The vector of formulas correspond to the set of "assert" instructions in the SMT-LIB input. New features A parallel mode is available for select theories, including QF_BV. By setting parallel.enable=true Z3 will spawn a number of worker threads proportional to the number of available CPU cores to apply cube and conquer solving on the goal. The SAT solver by default handle cardinality and PB constraints using a custom plugin that operates directly on cardinality and PB constraints. A "cube" interface is exposed over the solver API. Model conversion is first class over the textual API, such that subgoals created from running a solver can be passed in text files and a model for the original formula can be recreated from the result. This has also led to changes in how models are tracked over tactic subgoals. The API for extracting models from apply_result have been replaced. An optional mode handles xor constraints using a custom xor propagator. It is off by default and its value not demonstrated. The SAT solver includes new inprocessing techniques that are available during simplification. It performs asymmetric tautology elimination by default, and one can turn on more powerful inprocessing techniques (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs. Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged as lemmas (redundant) and are garbage collected if their glue level is high. Substantial overhaul of the spacer horn clause engine. Added basic features to support Lambda bindings. Added model compression to eliminate local function definitions in models when inlining them does not incur substantial overhead. The old behavior, where models are left uncompressed can be replayed by setting the top-level parameter model_compress=false. Integration of a new solver for linear integer arithmetic and mixed linear integer arithmetic by Lev Nachmanson. It incorporates several improvements to QF_LIA solving based on . using a better LP engine, which is already the foundation for QF_LRA . including cuts based on Hermite Normal Form (thanks to approaches described in "cuts from proofs" and "cutting the mix"). . extracting integer solutions from LP solutions by tightening bounds selectively. We use a generalization of Bromberger and Weidenbach that allows avoiding selected bounds tighthenings (https://easychair.org/publications/paper/qGfG). It solves significantly more problems in the QF_LIA category and may at this point also be the best solver for your problem as well. The new solver is enabled only for select SMT-LIB logics. These include QF_LIA, QF_IDL, and QF_UFLIA. Other theories (still) use the legacy solver for arithmetic. You can enable the new solver by setting the parameter smt.arith.solver=6 to give it a spin. Removed features: interpolation API duality engine for constrained Horn clauses. pdr engine for constrained Horn clauses. The engine's functionality has been folded into spacer as one of optional strategies. long deprecated API functions have been removed from z3_api.h Z3 4.7.1. official release cumulative bug fix since 4.6.0 minor version incremented as API now uses stdbool and stdint: bool and int64_t, uint64_t Official release Z3 4.6.0.
2018-12-18 07:46:39 +01:00
PLIST_VARS+= ocaml java
Package the Z3 theorem prover / SMT solver from Microsoft Research.
2015-11-24 06:45:58 +01:00
.if !empty(PKG_OPTIONS:Mocaml)
CONFIGURE_ARGS+= --ml
Requires ocaml-num with ocaml 4.06
2018-03-11 07:14:45 +01:00
.include "../../math/ocaml-num/buildlink3.mk"
Package the Z3 theorem prover / SMT solver from Microsoft Research.
2015-11-24 06:45:58 +01:00
.include "../../lang/ocaml/buildlink3.mk"
Update math/z3 to version 4.5.0 From the release notes: New features: - New theories of strings and sequences. - Incremental consequence finder for finite domains. - CMake build system (thanks @delcypher). - Updated and improved OCaml API (thanks @martin-neuhaeusser). - Updated and improved Java API (thanks @cheshire). - New resource limit facilities to avoid non-deterministic timeout behaviour. - New bit-vector simplification and ackermannization tactics (thanks @MikolasJanota, @nunoplopes). - QSAT: a new solver for quantified arithmetic problems. See: Bjorner, Janota: Playing with Quantified Satisfaction, LPAR 2016. A multitude of bugs has been fixed. I am about to commit a separate package for the Python bindings. Coordinated with dholland@
2018-03-13 01:31:16 +01:00
PLIST.ocaml= yes
Package the Z3 theorem prover / SMT solver from Microsoft Research.
2015-11-24 06:45:58 +01:00
.endif
.if !empty(PKG_OPTIONS:Mjava)
# XXX untested
USE_JAVA= yes
CONFIGURE_ARGS+= --java
.include "../../mk/java-vm.mk"
z3: Upgrade to 4.8.3 Eliminate merged patches. Improve java support. Patch by Michal Gorny. Upstream changelog ================== z3-4.8.3 This release covers bug fixes since 4.8.1 .NET bindings for dotnet standard 1.4 on windows and 64 bit Linux systems and MacOs z3-4.8.1 New requirements: A breaking change to the API is that parsers for SMT-LIB2 formulas return a vector of formulas as opposed to a conjunction of formulas. The vector of formulas correspond to the set of "assert" instructions in the SMT-LIB input. New features A parallel mode is available for select theories, including QF_BV. By setting parallel.enable=true Z3 will spawn a number of worker threads proportional to the number of available CPU cores to apply cube and conquer solving on the goal. The SAT solver by default handle cardinality and PB constraints using a custom plugin that operates directly on cardinality and PB constraints. A "cube" interface is exposed over the solver API. Model conversion is first class over the textual API, such that subgoals created from running a solver can be passed in text files and a model for the original formula can be recreated from the result. This has also led to changes in how models are tracked over tactic subgoals. The API for extracting models from apply_result have been replaced. An optional mode handles xor constraints using a custom xor propagator. It is off by default and its value not demonstrated. The SAT solver includes new inprocessing techniques that are available during simplification. It performs asymmetric tautology elimination by default, and one can turn on more powerful inprocessing techniques (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs. Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged as lemmas (redundant) and are garbage collected if their glue level is high. Substantial overhaul of the spacer horn clause engine. Added basic features to support Lambda bindings. Added model compression to eliminate local function definitions in models when inlining them does not incur substantial overhead. The old behavior, where models are left uncompressed can be replayed by setting the top-level parameter model_compress=false. Integration of a new solver for linear integer arithmetic and mixed linear integer arithmetic by Lev Nachmanson. It incorporates several improvements to QF_LIA solving based on . using a better LP engine, which is already the foundation for QF_LRA . including cuts based on Hermite Normal Form (thanks to approaches described in "cuts from proofs" and "cutting the mix"). . extracting integer solutions from LP solutions by tightening bounds selectively. We use a generalization of Bromberger and Weidenbach that allows avoiding selected bounds tighthenings (https://easychair.org/publications/paper/qGfG). It solves significantly more problems in the QF_LIA category and may at this point also be the best solver for your problem as well. The new solver is enabled only for select SMT-LIB logics. These include QF_LIA, QF_IDL, and QF_UFLIA. Other theories (still) use the legacy solver for arithmetic. You can enable the new solver by setting the parameter smt.arith.solver=6 to give it a spin. Removed features: interpolation API duality engine for constrained Horn clauses. pdr engine for constrained Horn clauses. The engine's functionality has been folded into spacer as one of optional strategies. long deprecated API functions have been removed from z3_api.h Z3 4.7.1. official release cumulative bug fix since 4.6.0 minor version incremented as API now uses stdbool and stdint: bool and int64_t, uint64_t Official release Z3 4.6.0.
2018-12-18 07:46:39 +01:00
PLIST.java= yes
Package the Z3 theorem prover / SMT solver from Microsoft Research.
2015-11-24 06:45:58 +01:00
.endif
Reference in a new issue Copy permalink