Nikolaj Bjorner
b37a5b1679
clean up python build files
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 10:27:12 -07:00
Nikolaj Bjorner
434ff31629
Merge pull request #1646 from NikolajBjorner/master
...
Remove depedencies on interp
2018-05-25 10:25:31 -07:00
Nikolaj Bjorner
d66f2af45e
Merge branch 'master' of https://github.com/z3prover/z3
2018-05-25 08:56:40 -07:00
Nikolaj Bjorner
753b9dd734
fix #1650 fix #1648
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 08:56:13 -07:00
Nikolaj Bjorner
af2fecd724
Merge pull request #1651 from Z3Prover/revert-1650-add-soname-to-libz3.so
...
Revert "Fix missing SONAME in libz3.so, which breaks loading from Java"
2018-05-25 08:43:56 -07:00
Nikolaj Bjorner
2b73b7c7f3
Revert "Fix missing SONAME in libz3.so, which breaks loading from Java"
2018-05-25 08:43:35 -07:00
Nikolaj Bjorner
19fb3e98dc
Merge pull request #1650 from PhilippWendler/add-soname-to-libz3.so
...
Fix missing SONAME in libz3.so, which breaks loading from Java
2018-05-25 07:44:32 -07:00
Nikolaj Bjorner
7145a9ac41
fix #1647
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 07:38:30 -07:00
Nikolaj Bjorner
8eeaa27cf3
remove interp from documentation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 07:33:43 -07:00
Philipp Wendler
3e0506a71b
Set the SONAME field of libz3.so to libz3.so.
...
This fixes a problem when loading libz3java from Java,
where the dependency on libz3 is not detected as fulfilled
if the latter does not have SONAME set.
2018-05-25 15:01:07 +02:00
Nikolaj Bjorner
6b700f1f5f
remove interpolation from test_capi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 20:32:04 -07:00
Nikolaj Bjorner
9f3da32a77
remove interpolation from test_capi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 16:28:23 -07:00
Nikolaj Bjorner
a9ca01d8d3
deprecating interp
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 13:12:07 -07:00
Nikolaj Bjorner
da32997f93
fix #1638
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 10:15:36 -07:00
Nikolaj Bjorner
6ecae2b986
fix #1645
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 09:21:20 -07:00
Nikolaj Bjorner
4f5775c531
remove interpolation and duality dependencies
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 08:33:48 -07:00
Nikolaj Bjorner
d088a1b9f6
updated release notes for merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 18:25:14 -07:00
Nikolaj Bjorner
2e4fb8d356
work around VS2012 compiler bug
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 16:33:27 -07:00
Nikolaj Bjorner
278fd03f19
GLU -> GNU fix #1643
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 13:31:55 -07:00
Nikolaj Bjorner
a9b1966ff2
Merge branch 'master' of https://github.com/z3prover/z3
2018-05-23 10:30:22 -07:00
Nikolaj Bjorner
f9bdfe2978
fix x86 warning
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 10:30:14 -07:00
Nikolaj Bjorner
b1e83dfc58
Merge pull request #1642 from waywardmonkeys/cxx-docs-missing-word
...
Fix missing word in C++ API docs.
2018-05-23 10:01:29 -07:00
Nikolaj Bjorner
148ccc93f0
Merge pull request #1641 from waywardmonkeys/remove-proof-mode-from-ocaml-docs
...
Update OCaml docs for changes made elsewhere.
2018-05-23 10:01:11 -07:00
Nikolaj Bjorner
77aef356cf
Merge pull request #1640 from waywardmonkeys/z3-true-false-bool
...
Z3_TRUE/Z3_FALSE should be true/false, not 1/0.
2018-05-23 10:00:48 -07:00
Bruce Mitchener
6db90a9333
Fix missing word in C++ API docs.
2018-05-23 23:58:08 +07:00
Bruce Mitchener
a3facc82fb
Update OCaml docs for changes made elsewhere.
...
This removes references to the PROOF_MODE that have been removed
elsewhere.
2018-05-23 23:55:17 +07:00
Bruce Mitchener
510cb5ee6e
Z3_TRUE/Z3_FALSE should be true/false, not 1/0.
...
Now that Z3_bool is a C bool, the associated constants should
be as well.
2018-05-23 23:51:36 +07:00
Nikolaj Bjorner
f5775f265a
fix python build script dependencies
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 09:21:33 -07:00
Nikolaj Bjorner
0708ecb543
dealing with compilers that don't take typename in non-template classes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 09:11:33 -07:00
Nikolaj Bjorner
2800049dd4
stale files
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 08:49:49 -07:00
Nikolaj Bjorner
75eba45926
Merge pull request #1606 from NikolajBjorner/opt
...
This integrates several features and improvements to the SAT and finite domain solver.
- The SAT solver by default handle cardinality and PB constraints using a custom plugin that operates directly on cardinality and PB constraints.
- 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.
- 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 technques 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.
- 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.
2018-05-23 08:47:08 -07:00
Nikolaj Bjorner
c963f6f2df
merge with master
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 08:02:16 -07:00
Nikolaj Bjorner
b5100b5b6a
Merge branch 'master' of https://github.com/z3prover/z3
2018-05-22 20:02:16 -07:00
Nikolaj Bjorner
363d7aad2a
fix bug reported in #1637
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-22 20:02:08 -07:00
Nikolaj Bjorner
50c93d1ad4
merge with 4.7.1
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-22 17:10:36 -07:00
Nikolaj Bjorner
87ae679db6
delay dereferencing justification
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-22 17:03:35 -07:00
Nikolaj Bjorner
f2aae7cffa
release notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-22 16:59:11 -07:00
Nikolaj Bjorner
3b1b82bef0
bumping version number by 1 for release tagging
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-22 10:19:38 -07:00
Nikolaj Bjorner
c390b72e42
Merge pull request #1635 from danielschemmel/cmake-cpp11
...
Use CMake's own mechanism for selecting language version
2018-05-21 08:46:01 -07:00
Daniel Schemmel
7467368266
Use CMake's own mechanism for selecting language version if CMake version is new enough
2018-05-21 07:35:43 +02:00
Nikolaj Bjorner
6938c76950
Merge pull request #1630 from danielschemmel/warnings
...
Fix GCC Warnings
2018-05-20 10:24:05 -07:00
Daniel Schemmel
78087483ca
Add missing include
...
The code should not have compiled previously, as smt::context was only forward declared at this point.
2018-05-20 15:34:01 +02:00
Daniel Schemmel
9c5a0ee810
Remove unnecessary (and confusing) parantheses around variable name in its declaration.
...
Also fixes GCC warning [-Wparentheses].
2018-05-20 15:34:01 +02:00
Nikolaj Bjorner
470e49afc1
Merge pull request #1631 from JoranHonig/master
...
Parallel python example
2018-05-19 11:08:23 -07:00
Joran Honig
e32dfad81e
Add comments
2018-05-19 11:16:20 +02:00
Joran Honig
7d51353b8b
Implement parallel python example
2018-05-19 11:13:53 +02:00
Daniel Schemmel
f02d031d11
As of GCC8, the throw by value, catch by reference idiom is enforced via -Wcatch-value
2018-05-19 04:39:36 +02:00
Daniel Schemmel
5134c16833
NULL-initialize pointers to help GCC static analyzer Fixes: variable may be used uninitialized
2018-05-19 03:45:05 +02:00
Daniel Schemmel
1cc4a4ccc5
remove unused constructor that would construct lar_constraint in an partly initialized state. Fixes: variable may be used uninitialized
2018-05-19 02:56:46 +02:00
Nikolaj Bjorner
ad973d5c6d
Merge branch 'master' of https://github.com/z3prover/z3
2018-05-18 14:31:16 -07:00