mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
7892 commits 23 branches 48 tags 157 MiB
Commit graph

505 commits

Author SHA1 Message Date
TheRealNebus 37852807b0 Revert "WMax conflict budget bug fix" 
This reverts commit ab8d3cdc44.
 2018-04-26 22:39:45 +01:00
TheRealNebus ab8d3cdc44 WMax conflict budget bug fix 2018-04-24 17:59:21 +01:00
TheRealNebus e5aa79ba6a disjoint cores 2018-02-19 13:29:15 +00:00
TheRealNebus 3a7efb91ae implemented CLD 2018-02-16 19:48:29 +00:00
TheRealNebus 3bbc09c1d2 MSS based MaxSMT solver 2018-02-16 14:44:22 +00:00
Nikolaj Bjorner e1100af52c ensure that final model is logged by the time it is produced fix #1463 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-12 12:04:24 -08:00
Bruce Mitchener 76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener 7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Nikolaj Bjorner 1ee7871bbf to fix #1476 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-06 18:48:03 -08:00
Nikolaj Bjorner 73e9d351dc adding initial model to updated #1463 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-30 03:21:58 -08:00
Nikolaj Bjorner e4198c38e2 add solution_prefix per #1463, have parto with single objective behave similar to multipe-objectives #1439 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-28 11:45:39 -08:00
Nikolaj Bjorner 57406d6cc4 more updates for #1439 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-17 18:11:14 -08:00
Nikolaj Bjorner b5335bc34b change behavior of single-objective pareto to use Pareto GIA algorithm (so not a good idea with MaxSAT solving, but then uniform behavior #1439 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-13 20:08:23 -08:00
Nikolaj Bjorner d86e8f02d7 fix get-objectives error #1419 message (get-objectives) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-27 10:09:22 -08:00
Nikolaj Bjorner a83af22841 include special functionality in parsers for solvers and opt for additional file formats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-03 20:00:45 +01:00
Nikolaj Bjorner 5ee30a3cd9 include special functionality in parsers for solvers and opt for additional file formats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-03 20:00:24 +01:00
Nikolaj Bjorner 8357210d3c fix lack of warning/error for unbounded objectives in context of quantifiers #1382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 01:07:41 -08:00
Nikolaj Bjorner e4b595d490 add solver pool abstraction for Spacer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:10:20 -07:00
Nikolaj Bjorner e7aa6455bc fix #1326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 19:25:25 -07:00
Nikolaj Bjorner 0589a20b46 fix #1326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 19:24:45 -07:00
Christoph M. Wintersteiger db398eca7a Tabs, formatting. 2017-09-17 17:50:05 +01:00
Nikolaj Bjorner 77008dc411 Merge pull request #1226 from NikolajBjorner/master 
removing dependencies on simplifier, support SMTLIB2 parametric algebraic datatypes.
This is a breaking change. It introduces two substantial changes:
1. The legacy simplifier is removed. It was obsoleted with the introduction of the rewriter facilities, but many dependencies made it a major change to remove the legacy simplifier. All uses of the legacy simplifier have now been replaced by corresponding calls to the rewriter. It means that some normalization may behave differently. At this point, Z3 passes regressions and passes performance tests without regressing.
2. Algebraic datatypes in the form of SMT-LIB2.6 are now supported. These generalize the datatypes supported so far as parametric datatype constructors may be applied to different arguments within a recursive definition.
 2017-09-11 00:40:51 +03:00
Nikolaj Bjorner 1d6f53c310 fix #1248, fix #1249 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-07 05:32:07 -07:00
Nikolaj Bjorner 2897b98ed2 remove simplify dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-26 00:37:22 -07:00
Nikolaj Bjorner 2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Nikolaj Bjorner b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Nikolaj Bjorner 08524a2d90 cleanup for warning message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 11:47:17 -07:00
Nikolaj Bjorner 9d1852343c add separate get-objectives command #1107 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-23 16:34:38 -07:00
Nikolaj Bjorner 7386f2e045 #1101 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-22 14:18:53 -07:00
Dan Liew 4b517b96df [CMake] Move CMake files into their intended location so the 
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
 2017-06-12 11:59:00 +01:00
Nikolaj Bjorner d5f646929e print success #1068 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 09:16:36 -07:00
Nikolaj Bjorner f3a0b7e0cd change command-line experience for pareto fronts. It now requires multiple check-sat calls to loop over the fronts. This allows querying each model in turn. #1008 2017-05-23 20:05:10 -07:00
Nikolaj Bjorner 911b24784a merge LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 10:46:11 -07:00
Nikolaj Bjorner ed0b2be618 fix bug in tracking levels of variables: levels are not cleared, only truth assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 14:10:07 -07:00
Nikolaj Bjorner a048d74bae adding interval designator to output of non-optimal objectives, fix python doc test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-26 14:05:33 -07:00
Nikolaj Bjorner e4b9080165 include timeout/rlimit parameters in optmize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:04:13 +08:00
Nikolaj Bjorner c99205fa7e return box model based on index. Issue #955 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-31 08:12:53 -07:00
Nikolaj Bjorner ec47706226 fix constant offset and handling of ite in difference logic optimizer code-path. Issue #946 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 02:23:50 -07:00
Nikolaj Bjorner c56c7fd649 add handlers for dense difference logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 01:31:00 -07:00
Nikolaj Bjorner a0237ed2a6 fix crash reported in #946 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-16 18:56:43 -07:00
Nikolaj Bjorner 829519b837 fix bug for bit-vector optimization. Issue #928 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-08 10:19:35 +01:00
Nikolaj Bjorner 41e6fafc58 fix bug for bit-vector optimization. Issue #919 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-08 10:07:31 +01:00
Nikolaj Bjorner e02160c674 expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-24 11:07:40 -08:00
Nikolaj Bjorner bd0bd6052a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-02-02 10:19:21 -08:00
Nikolaj Bjorner 9ca52a3361 fix bug in lexicographic handling in maxres: previous assumptions were not committed in corner cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-02 10:19:11 -08:00
Nikolaj Bjorner 9cfd412cd0 enable pb theory always as pb terms can be introduced during transformations. Issue #884 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-01 15:28:29 -08:00
Nikolaj Bjorner 0aa912371b Another fix for #847. Reset wmax theory solver state between lex calls, otherwise it uses stale constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 14:19:24 -08:00
Nikolaj Bjorner 7df803c131 Fix unsound handling of upper bounds in wmax, thanks to Patrick Trentin for report and careful repros #847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 11:52:48 -08:00
Nikolaj Bjorner bc6b3007de remove unused features related to weighted check-sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-13 20:53:22 -08:00
Nikolaj Bjorner aaf6e67ec8 add restart.max parameter to control cancellation based on restart count 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-25 17:43:47 -08:00