Bruce Mitchener
cdfc19a885
Use nullptr.
2018-10-02 09:11:19 +07:00
Nuno Lopes
5de6628a5d
remove spurious copies and inc_refs around ref_vector
2018-06-28 10:31:38 +01:00
Nuno Lopes
2b31024dab
add obj_ref::operator=(obj_ref &&) + a few explicit uses
2018-06-26 17:00:56 +01:00
Nikolaj Bjorner
520ce9a5ee
integrate lambda expressions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-26 07:23:04 -07:00
Nikolaj Bjorner
7714d05c1a
fill out qe_solve_plugin functionality
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:52 -07:00
Arie Gurfinkel
aa77a918cd
Optimizing qe_lite
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
0452bc3d43
qe_lite: simplify definitions before deciding on elimination order
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
b120923dd5
qe_lite: bug fix in der::der_sort_vars()
...
The case of
VAR 1 = (+ (:var 2) 10)
VAR 2 = (+ 0 foo)
was not properly handled whenever VAR2 has only one reference.
In that case, VAR2 is not marked as done when VAR1 is processed,
causing VAR2 to be duplicated in elimination order
2018-06-14 16:08:50 -07:00
Nikolaj Bjorner
ff0f257102
remove iff
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:48 -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
c513f3ca09
merge with master
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-25 14:57:01 -07:00
Nikolaj Bjorner
8e09a78c26
fix #1510 by reintroducing automatic declaration of recognizers
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-02 23:02:20 +09: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
Bruce Mitchener
50f3e9c3c0
Fix typos.
2018-02-09 16:35:26 +07:00
Bruce Mitchener
73b3da37d8
Typo fixes.
2018-01-02 22:48:06 +07: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
07031798ec
fix occurs function used in qe_lite #1241
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-16 01:43:35 -08:00
Nikolaj Bjorner
5d17e28667
support for smtlib2.6 datatype parsing
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-09-04 21:12:43 -07:00
Nikolaj Bjorner
a3dba5b2f9
hide new datatype plugin
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-09-03 20:01:59 -07:00
Nikolaj Bjorner
063b6e9ea5
Merge branch 'master' of https://github.com/Z3Prover/z3
2017-07-31 13:24:57 -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
Arie Gurfinkel
331eec8a05
option to control array_der in qe_lite
2017-07-31 14:19:16 -04:00
Arie Gurfinkel
ef62621f50
make qe_lite prefer simpler definitions
2017-06-20 21:51:08 -04:00
Arie Gurfinkel
9f73359a86
improve comments
2017-06-20 21:50:35 -04:00
Arie Gurfinkel
ac6ca4d334
factored out is_variable_proc to a header file
2017-06-20 21:34:49 -04:00
Nikolaj Bjorner
894c60bdf9
fix bug in qe-lite reported in #1086 : bookkeeping of unconstrained variables only works for quantifier-free formulas
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-19 18:22:30 -05:00
Christoph M. Wintersteiger
27a1758857
Added rewriter.ignore_patterns_on_ground_qbody option to disable simplification of quantifiers that have their universals appear only in patterns, but otherwise have a ground body.
2017-04-07 21:19:20 +01:00
Nikolaj Bjorner
5b497b6249
reduce set of mainly verbose warnings raised by -Wmaybe-uninitialized and unused variable warnings from release mode builds
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-22 20:25:47 -07:00
Nikolaj Bjorner
72ec6dc8e1
remove debug code
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-21 16:58:48 -07:00
Nikolaj Bjorner
5e737641b7
remove qe-lite pass in quant_tatics
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-21 16:57:30 -07:00
Nikolaj Bjorner
1a5449c3d4
enable new NRA solver for nra benchmarks
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-20 12:35:29 -07:00
Nikolaj Bjorner
c4472ce717
include more qsat features
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 12:29:23 -07:00
Nikolaj Bjorner
a7e2fb31e3
updates to resource exceptions, update master possibly handle pull request issue
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 11:36:49 -08:00
Nikolaj Bjorner
2a051719d8
cleanup deprecated critical sections, fix cancellation for par_or_else tactic
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 09:43:00 -08:00
Nikolaj Bjorner
32b6b2da44
moving to resource managed cancellation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 13:13:11 -08:00
Nikolaj Bjorner
4be3926daa
use signed character type declarations for cross platform compilation. Fixes issue #210
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-09-05 16:30:58 -07:00
Nikolaj Bjorner
bf5419d44a
move functionality from qe_util to ast_util
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-06-23 14:33:45 +02:00
Nikolaj Bjorner
a594597906
improve equality solving in qe-lite
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-02-12 10:54:00 -08:00
Nikolaj Bjorner
137339a2e1
split muz_qe into two directories
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-08-28 12:08:47 -07:00
