mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
15908 commits 49 branches 53 tags 182 MiB
Commit graph

998 commits

Author SHA1 Message Date
Arie Gurfinkel
3a01fd791b Replace rule API 2018-09-04 21:49:59 -04:00
Arie Gurfinkel
0035d9b8cb Background external invariants 
Background external invariants are constraints that are assumed to be
true of the system. This commit introduces a mode in which
background invariants are used only duing inductive generalization
and lemma pushing, but not during predecessor computation.

It is believed that this will be more efficient used of background
external invariants since they will not be able to disturb how
predecessors are generalized and computed.

Based on a patch by Jorge Navas
 2018-09-04 21:49:59 -04:00
Arie Gurfinkel
533e9c5837 Expand equality literals when eq_prop is disabled 
When equality propagation is disabled for arithmetic,
equality atoms are expanded into inequality for potentially
better generalization with interpolation
 2018-09-04 21:49:59 -04:00
Nikolaj Bjorner
84c7df75d6 record statistics setting in config_params so that fp engine can access them, fix serialization bug when check-assumptions returns unsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-06 16:21:27 -07:00
Nikolaj Bjorner
d47e06732c bmc improvements, move fd_solver to self-contained directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:02:15 -07:00
Nikolaj Bjorner
e041ebbe80 bmc improvements, move fd_solver to self-contained directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:00:49 -07:00
Arie Gurfinkel
5d1149adb2 Transformation to eliminate term-ite expressions from DL rules 2018-07-02 17:09:56 -04:00
Arie Gurfinkel
6d75c31468 First draft of elim_term_ite xform. Not working. 2018-07-02 17:09:56 -04:00
Arie Gurfinkel
7acea2791d -tr:spacer.expand-add --> -tr:spacer_progress 2018-07-02 17:09:56 -04:00
Nuno Lopes
cef17c22a1 remove some allocs from exceptions 2018-07-02 17:08:02 +01:00
Nikolaj Bjorner
c4d893dfad fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 06:10:09 -07:00
Nikolaj Bjorner
3ad7d59f22 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-29 21:25:21 -07:00
Nikolaj Bjorner
797e576195 unreferenced variable in release mode, spaces 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 21:25:08 -07:00
Arie Gurfinkel
9b578083f5 Avoid non-linear arithmetic in qgen 2018-06-28 16:50:43 -04:00
Arie Gurfinkel
5e87d7c4a3 Formatting: move q3 parameters closer together 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
bd63458778 Shuffle assumptions on every call 
Order of assumptions appears to make a huge difference on what lemmas
are discovered. Shuffling the assumptions ensures that the solver
is never stuck with any bad order.
 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
6422fa3739 Fix arithmetic equality solver in qgen 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
41a05e9d58 Add methods to print pob 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
a63e4b48ca Fix order of arguments when normalizing a conjunction 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
a8c9e3a837 Bug fix in qgen 2018-06-28 15:38:50 -04:00
Arie Gurfinkel
e8e27f0daf Don't simplify bounds when normalizing a lemma 2018-06-28 15:38:50 -04:00
Arie Gurfinkel
0e5434ce0c Debug prints 2018-06-27 22:49:36 -04:00
Arie Gurfinkel
7c924c49f6 Do not evaluate quantified formulas in a model 2018-06-27 22:49:36 -04:00
Arie Gurfinkel
704c19920d Only 10 levels of weakness 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
4339722e98 Fix segfaults in qgen 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
49e9480928 Fix lemma_as_cti option 
Use negation of a lemma as a proof obligation. This speeds up discovering
bad lemmas that do not contain some reachable states.
 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
d7234dc039 Inactive debug code 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
2b4d92821a Avoid crashing on cancel 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
f6dcc6fc72 API to find pob in pob_manager 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
5bc57238a6 Track whether pob is in pob_queue 
pob_queue is a priority queue. Changing a pob while it is in the queue might change
the priority. This is a source of subtle bugs. The flag is ment to help defend
against this issues in the future.

As a side-effect, a pob that is already in the queue will be silently not added
to it, and a new version of a pob might be created if a version being looked
for is already in the queue.
 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
c00c6b4285 Pobs are always managed 
Removed options to allow unmanaged pobs.
Other minor cleanups.
 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
1910b4c87c Rename pobs into pob_manager 2018-06-27 22:49:35 -04:00
Arie Gurfinkel
d9100437ce Weakness of the lemma independent of the pob 
Lemma inherits its weakness score from the pob. However,
pob's weakness might be reset or changed for some other reason.

To avoid affecting the lemma, the weakness is copied on
construction.
 2018-06-27 22:49:35 -04:00
Nikolaj Bjorner
eabe91cdef Merge branch 'master' of https://github.com/z3prover/z3 2018-06-27 17:05:52 -07:00
Nikolaj Bjorner
7844476a7d fixes to term-graph, add proof-checker routines for PR_BIND, remove orphaned file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 17:04:47 -07:00
Nikolaj Bjorner
06c9a9f3e1 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 08:51:22 -07:00
Nikolaj Bjorner
5762be2a0f fix 1703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 08:49:52 -07:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:23:04 -07:00
Arie Gurfinkel
3af3c82f67 Normalize lit0 in theory clause 2018-06-25 09:21:30 -04:00
Arie Gurfinkel
f330b96a35 Gracefully failing in assign-bounds to farkas 2018-06-24 21:03:09 -04:00
Arie Gurfinkel
e906930922 Debug code 2018-06-24 20:43:04 -04:00
Arie Gurfinkel
8e57ab5d97 Computing missing coeff for assign-bounds lemma 2018-06-24 20:43:04 -04:00
Arie Gurfinkel
1764bb8785 Cleaning up unsat_core_learner 2018-06-24 20:43:04 -04:00
Arie Gurfinkel
7b2ca769ef Cleanup 2018-06-24 20:43:04 -04:00
Arie Gurfinkel
58dc5451e1 iuc code cleanup 2018-06-24 20:43:04 -04:00
Arie Gurfinkel
9c9d0d0840 convert assign-bounds axioms to farkas lemmas 2018-06-24 20:43:04 -04:00
Arie Gurfinkel
ac23002dce Fix bugs in iuc generation 2018-06-24 20:43:04 -04:00
Arie Gurfinkel
4ed6783aff Formatting only. No change to code 2018-06-24 20:43:04 -04:00
Arie Gurfinkel
fcfa6baeca Refactor mk_th_lemma 2018-06-24 20:43:04 -04:00
Nikolaj Bjorner
915983821b add rewrite to each branch of mbp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-24 17:06:49 -07:00