mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity
15359 commits 23 branches 48 tags 157 MiB
Commit graph

296 commits

Author SHA1 Message Date
Nikolaj Bjorner 44a0dbbc61 fix #1864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 08:06:51 -07:00
Nikolaj Bjorner b540868cd7 Merge branch 'master' of https://github.com/z3prover/z3 2018-10-04 13:43:04 -07:00
Nikolaj Bjorner a549e73b86 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-04 13:43:01 -07:00
Nikolaj Bjorner 3bc2213d54 fix #1577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 17:43:42 -07:00
Bruce Mitchener cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nikolaj Bjorner 18bec88a8a purify non-constant terms by default to enforce theory #1820 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-10 15:52:02 -07:00
Nikolaj Bjorner 85e7b18451 fix name to divisible, guard under smtlib2_compliant as sugguested in #1757 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-01 18:22:10 -07:00
Nikolaj Bjorner d74978c277 fix #1762, #1764, #1768 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-26 20:29:26 +01:00
Nikolaj Bjorner e187023304 fix #1699 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-23 21:57:10 -07:00
Nikolaj Bjorner 335d672bf1 fix #1675, regression in core processing in maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 23:23:19 -07:00
Nikolaj Bjorner 74621e0b7d first eufi example running 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -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 434ff31629
Merge pull request #1646 from NikolajBjorner/master 
Remove depedencies on interp
 2018-05-25 10:25:31 -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
Nikolaj Bjorner 6ecae2b986 fix #1645 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-24 09:21:20 -07:00
Nikolaj Bjorner 96914d8578 update model conversion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-03 11:46:26 -07:00
Nikolaj Bjorner f525f43e43 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 09:30:43 -07:00
Nikolaj Bjorner 480e1c4dab add warning message for optimization with quantifiers. Fix #1580 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-23 07:20:24 +02:00
Nikolaj Bjorner a81a8de975 remove lns 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 19:54:11 -07:00
Nikolaj Bjorner c4ff5c7ac7 remove lns code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 18:32:16 -07:00
Nikolaj Bjorner c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Nikolaj Bjorner 59b142f803 fixing local search 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-15 06:48:26 -07:00
Nikolaj Bjorner 4375f54c45 adding lns 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-13 13:31:27 -07:00
Nikolaj Bjorner e7d43ed516 fix pb rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-12 11:22:05 -07:00
Nikolaj Bjorner fadcac8f6d fix #1491 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-15 12:39:08 -08:00
Bruce Mitchener 76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Nikolaj Bjorner 4f630f2a00 fix configuration for compiling equalities, add extended binaries 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-08 09:09:53 -08:00
Nikolaj Bjorner 5e482def18 fix local search encoding bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-08 07:27:32 -08:00
Nikolaj Bjorner 615e1e0845 remove redundant tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 17:17:27 -08:00
Nikolaj Bjorner bee4716a85 lia2card simplifications, move up before elim01 (which could be deprecated) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 12:56:30 -08: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 e4f29a7b8a debugging mc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-19 21:09:52 -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 4adb24ede5 fix model bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-13 16:12:59 -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 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 2f218b0bdc remove also cores as arguments to tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-19 12:18:50 -08:00
Nikolaj Bjorner 4bbece6616 re-organize proof and model converters to be associated with goals instead of external 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-18 16:33:54 -08:00
Nikolaj Bjorner df6b1a707e remove proof_converter from tactic application, removing nlsat_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 23:32:29 -08:00
Nikolaj Bjorner 0d15b6abb7 add stubs for converting assertions, consolidate filter_model_converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 14:51:13 -08:00
Nikolaj Bjorner fd49a0c89c added facility to persist model transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 00:05:52 -05:00
Nikolaj Bjorner 3de8c193ea implementing model updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-30 16:11:51 -05:00
Nikolaj Bjorner 0589a20b46 fix #1326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 19:24:45 -07:00
Nikolaj Bjorner 651587ce01 merge with master branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-19 09:39: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 b482dbd589 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 17:02:27 -07:00
Nikolaj Bjorner 7386f2e045 #1101 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-22 14:18:53 -07:00
Nikolaj Bjorner e0a86ccc1a add lrb/chb and experiment with them 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 10:48:31 -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 cc7a176c89 update to retain original behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 19:32:03 -07:00
Nikolaj Bjorner eeb79e1c3c update to retain original behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 19:30:54 -07:00
Nikolaj Bjorner 8205b45839 initial integration of opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-27 19:13:00 -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 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 05c5b3b07b merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-09 22:45:52 +01:00
Nikolaj Bjorner 5f5819f029 fix xor handling, and defaults for cardinality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-09 22:44:41 +01: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 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 2bd29548da improve parser error message over API, streamline names of statistics for arithmetic solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-25 17:27:56 -08:00
Nikolaj Bjorner 2307a7ffa7 fix bug in handling of repeated soft constraints. #815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 10:19:57 +01:00
Nikolaj Bjorner 0ab2067b69 produce error message for cores with optimization. Issue #825 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 13:15:40 +01:00
Nikolaj Bjorner ba942af5a8 disable sat solver when proofs are turned on. Fixes issue #768 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-31 23:27:39 +01:00
Nikolaj Bjorner 23b9d3ef55 fix at-most-1 constraint compiler bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-22 18:50:16 -07:00
Nikolaj Bjorner b2db2f1eb6 allow negative weights for weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-02 10:21:58 -07:00
Nikolaj Bjorner 527c5191a6 Add C++ functions for set operations per stackoverflow post, set relevancy = 2 for quantified maxsmt per example from Aaron Gember, fix conversion of default weights based on bug report from Patrick Trentin on maxsat. Annotating soft constraints with weight=0 caused the weight to be adjusted to 1 and therefore produce wrong results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 12:24:24 -07:00
Nikolaj Bjorner 56c78753f0 updating default solver selection. Add dt2bv transformation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-24 18:16:32 -07:00
Nikolaj Bjorner 3581f6de42 remove stale SLS option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-21 18:18:42 -07:00
Nikolaj Bjorner 4f5b0667ef fix rounding mode for pseudo-boolean constraint creation, Issue #683 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-14 12:34:18 -07:00
Nikolaj Bjorner 0fdf01e410 avoid crash on box models under cancellation. Issue # SASSERT(!m_box_models.empty()); 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-29 04:53:28 -07:00
Nikolaj Bjorner 9c099d6b1b fix mb maximization logic, so far not accessible 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-20 16:39:03 -07:00
Nikolaj Bjorner c7ff05cc78 enable core minimization with qsat in case it turns out to be useful 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-12 15:58:12 -07:00
Nikolaj Bjorner ea201a776d enable qsat-opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-11 10:39:27 -07:00
Nikolaj Bjorner c725fe7698 tune lra optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-22 17:03:29 -07:00
Nikolaj Bjorner 1aa3fdab8a remove min/max, use qmax; disable cancellation during model evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-19 13:04:20 -07:00
Nikolaj Bjorner 5b31f54501 max/min 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-05 14:11:13 -07:00
Nikolaj Bjorner e29adbf304 fix issues #581: nested timeouts canceled each-other 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-30 11:18:34 -07:00
Nikolaj Bjorner 2428bf18f1 add model correction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-29 19:08:10 -07:00
Nikolaj Bjorner c75fd02c95 qsat-opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-28 21:31:16 -07:00
Nikolaj Bjorner 0094b36636 fix bounds check to fix segfault reported in issue #565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 12:25:29 -07:00
Nikolaj Bjorner 45fdb95f53 fix performance for model construction, recognize concats of values as a value for pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-23 17:23:57 -07:00
Nikolaj Bjorner 55956df8d8 remove critical sections that are now redundant due to different cancellation model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-13 12:10:14 -04:00
Nikolaj Bjorner 5db84575f6 fix regression in o7.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-08 22:27:47 -08:00
Nikolaj Bjorner 5994c5a948 fix partial model tracking over cancellation/exceptions, reported by August Shi. Fix regression test for fp-to-real, reset the pre-processor in inc_sat_solver on exceptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-07 16:42:29 -08:00
Nikolaj Bjorner 2a65503235 fix #425 and report from Patrick Trentin of same bug in preprocessing soft constraints that are simplified to true/false 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-04 22:35:02 +00:00
Nikolaj Bjorner 85d44c5d66 fix axioms for extract, add extensionality checking for shared variables, convert exceptions to unknown status per #419 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-18 11:09:41 +05:30
Nikolaj Bjorner 32b6b2da44 moving to resource managed cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 13:13:11 -08:00
Nuno Lopes b26735a887 fix build with gcc 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-22 11:24:30 +00:00
Nikolaj Bjorner 0592e76574 Enhancement for Valentin #332 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-19 10:26:01 -08:00
Nikolaj Bjorner c58e640563 extract labels for optimal model. Fix to #325 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 14:53:08 -08:00
Nikolaj Bjorner 1575dd06a7 expose labels from optimization. Move printing of objectives to after sat/unsat. Cahnge format to something that is somewhat related to how other output is created. Issue #325. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 09:42:12 -08:00
Nikolaj Bjorner 0a26bcf14c ensure unique symbols when MaxSAT problems are extracted from linear objectives such that multiple objectives can be supported. Fixes issue #308 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-13 15:12:08 -05:00