mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 10:51:50 +00:00
Code Activity
8919 commits 23 branches 48 tags 156 MiB
Commit graph

8919 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner d7f51f2443 try flags to fix gcc build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-06 18:20:23 -07:00
Nikolaj Bjorner 99bdb46158 int64_t 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-06 17:48:30 -07:00
Nikolaj Bjorner 8ab428b660 try new gcd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-06 17:42:44 -07:00
Nikolaj Bjorner add8d26807 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-01 08:07:14 -07:00
Nikolaj Bjorner fee4f91e2d add set operations to python request by Francois 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-01 08:07:06 -07:00
Nikolaj Bjorner e2eb883c71 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-30 16:48:17 -07:00
Nikolaj Bjorner b9637924c4 fix #1662 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-30 16:47:17 -07:00
Nikolaj Bjorner 0d668e1428 fix #1661 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-30 03:18:22 -07:00
Nikolaj Bjorner 0aa3245c37 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-29 20:55:46 -07:00
Nikolaj Bjorner db3f439e88 fix memory leak from Arie 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-29 20:55:30 -07:00
Nikolaj Bjorner 6dc9c3a587 fix ml build breakd #1659, #1660 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-29 07:37:27 -07:00
Nikolaj Bjorner da0239d200 fix #1655 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-25 21:21:27 -07:00
Nikolaj Bjorner 727ba13566 fix #1653 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-25 12:55:04 -07:00
Nikolaj Bjorner a06926915d remove stale file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-25 10:47:54 -07:00
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