3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Commit graph

10745 commits

Author SHA1 Message Date
Kate 7d43a4bca5 Fix Makefile generation for the OCaml api 2019-04-10 15:18:03 +01:00
Nikolaj Bjorner 9c9cd5ebf7 add tc and trc functionals for binary relations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-10 04:12:46 +02:00
Nikolaj Bjorner 182039eb44 add tc and trc functionals for binary relations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-10 04:12:45 +02:00
Nikolaj Bjorner ae982c5225 add tc and trc functionals for binary relations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-10 04:12:45 +02:00
Nikolaj Bjorner d3305aac16
Merge pull request #2224 from maxzinkus/patch-1
Require verbosity=1 to log parallel tactic progress
2019-04-10 02:26:29 +02:00
Max Zinkus 45595af665
Require verbosity=1 to log parallel tactic progress 2019-04-09 12:35:04 -04:00
Nikolaj Bjorner 6cc82f0401 enable theory_lra on non-linear reals if configured to use
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-07 07:23:32 -07:00
Nikolaj Bjorner 9e62a7834d Merge branch 'master' of https://github.com/z3prover/z3 2019-04-05 03:06:58 -07:00
Nikolaj Bjorner f1a2e875b5 fixing #2217
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-05 03:06:41 -07:00
Nikolaj Bjorner 56ac3f86a5 fix justification for implied equalities in special relations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-03 17:08:10 -07:00
Nikolaj Bjorner dfd327f287 add tuple and disjoint sum shorthands
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-02 18:36:35 -07:00
Nikolaj Bjorner 6360798a53 local
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-02 17:40:38 -07:00
Nikolaj Bjorner ff6d703c05 add tracing, fix #2214, remove unused variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-02 12:20:55 -07:00
Nikolaj Bjorner 5fdf5b67a4 remove not
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-01 12:17:49 -07:00
Nikolaj Bjorner 7e7cdf3635 update dependencies in legacy build system
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-01 12:13:50 -07:00
Nikolaj Bjorner a9c20c96ee Merge branch 'master' of https://github.com/z3prover/z3 2019-04-01 12:10:17 -07:00
Nikolaj Bjorner b18864d4cc
Merge pull request #2204 from Z3Prover/sr
Special relations
2019-04-01 12:01:55 -07:00
Nikolaj Bjorner 4fb867a49c na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-01 11:57:07 -07:00
Nikolaj Bjorner 3afe081f62 fixup compiled patterns
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-29 11:42:40 -07:00
Nikolaj Bjorner ebc4b93d52 update documentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-29 08:41:31 -07:00
Nikolaj Bjorner 1c694fd42f sr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 16:11:16 -07:00
Nikolaj Bjorner 7a6823aef1 add special relations tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 10:07:50 -07:00
Nikolaj Bjorner ec6cf7950e Merge branch 'sr' of https://github.com/z3prover/z3 into sr 2019-03-28 09:21:37 -07:00
Nikolaj Bjorner bce1ee6d39 new files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 09:21:34 -07:00
Nikolaj Bjorner e4eca577f6 fix po model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:22 -07:00
Nikolaj Bjorner 175008a6c6 adding po evaluator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:22 -07:00
Nikolaj Bjorner f55e4ccc41 support indexed relations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:22 -07:00
Nikolaj Bjorner 81b1338af6 display methods
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:22 -07:00
Nikolaj Bjorner 87bc4cf693 virtual -> override
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:22 -07:00
Nikolaj Bjorner 57609e57f5 include path
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:22 -07:00
Nikolaj Bjorner b46cedf647 include path
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 8d5507008e adding cmd_context
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 5536834019 add API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner e3a2168a20 e_id3
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 6a9cbe1461 l -> eq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 892be69d51 nits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 168b0bcc44 tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 1e751422e1 remove unused code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner f8b8d5b870 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 10ba731697 tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner c714abbff2 use override
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 5baef8bcf3 use for pattern
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 876aa01167 add sr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 4e38e90e2b fix po model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:03:04 -07:00
Nikolaj Bjorner c69e911a79 adding po evaluator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-27 16:59:13 -07:00
Nikolaj Bjorner deb48bffe1 possible fix for #2182
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-27 10:35:27 -07:00
Christoph M. Wintersteiger ce8263cf27
Merge branch 'master' of https://github.com/Z3Prover/z3 2019-03-27 17:34:40 +00:00
Christoph M. Wintersteiger d1d49ef3a9
Fix BV-conversion of fp.roundToIntegral. Fixes #2191. 2019-03-27 17:13:00 +00:00
Nikolaj Bjorner 51a26ceb9e more segfault sources #2205, examining bit2bool internalization for #2282
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-27 09:50:13 -07:00
Nikolaj Bjorner 5478955199 disable cancelation during propagation at base level
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-26 16:19:50 -07:00