mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Code Activity
9345 commits 23 branches 48 tags 156 MiB
Commit graph

9345 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner c429455f10 visit parameters during occurs count 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 08:52:25 -07:00
Nikolaj Bjorner 18121e5241
Merge pull request #1707 from agurfinkel/deep_space 
Deep space
 2018-06-28 05:38:25 -07:00
Nuno Lopes 5de6628a5d remove spurious copies and inc_refs around ref_vector 2018-06-28 10:31:38 +01:00
Arie Gurfinkel 4abab8aaf5 Fix bug in qe_term_graph 
In merge, parents of A instead of parents of B were traversed.
Among other things, it created stale marks that caused an
infinite loop in to_lits()
 2018-06-27 22:54:55 -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 bc6604441b Helpers in model_core 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 176c0a97f7 Gracefully handle absence of a proof 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 91ef84b8c9 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-27 11:25:04 -07:00
Nikolaj Bjorner 20fc573d5b add laxer check for oeq_quant_intro 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 11:24:56 -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
Nuno Lopes 6c64e138b0 ufbv_rewriter_tactic: remove unneeded imp class 2018-06-26 18:05:14 +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 ea4218a192 add upper-case files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:52:38 -07:00
Nikolaj Bjorner 1c1357af7d remove lower case files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:52:02 -07:00
Nikolaj Bjorner a8e864a3e6 add missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:36:36 -07: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 bf4edef761 fix mbi arithmetic solver for lower bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 06:37:47 -07:00
Nikolaj Bjorner 6804329661
Merge pull request #1701 from agurfinkel/deep_space 
Normalize lit0 in theory clause
 2018-06-25 07:35:34 -07:00
Arie Gurfinkel 3af3c82f67 Normalize lit0 in theory clause 2018-06-25 09:21:30 -04:00
Nikolaj Bjorner a5f4980c92
Merge pull request #1700 from agurfinkel/deep_space 
Deep space
 2018-06-24 19:13:34 -07: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
Nikolaj Bjorner c32bfb5ecd fix crash during cancelation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-24 15:29:40 -07:00
Nikolaj Bjorner 61c25fdc8e Merge branch 'master' of https://github.com/z3prover/z3 2018-06-23 21:57:19 -07:00
Nikolaj Bjorner e187023304 fix #1699 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-23 21:57:10 -07:00
Nikolaj Bjorner 3d27232b2a
Merge pull request #1697 from rainoftime/master 
Refine default_tactic for better support of pure SAT instances
 2018-06-22 09:31:19 -07:00
rainoftime fc8b1d9a7d Refine default_tactic: if the constraint is an SAT instance and proof is not enabled, then use the qffd tactic 2018-06-22 16:46:47 +08:00