mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-18 22:54:21 +00:00
Code Activity
8958 commits 45 branches 57 tags 176 MiB
Commit graph

80 commits

Author SHA1 Message Date
Arie Gurfinkel
088bd3ed8e Fix compiler warning 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
25fad153d1 added option fixedpoint.spacer.iuc.debug_proof to debug proof which is used for generation of iuc 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
c3a66217e1 improved options for IUC computation 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
370667722d New option fixedpoint.spacer.print_farkas_stats 
Prints the number of Farkas lemmas in each proof
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
880fc77655 Further rewrite equalities 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
5a37518e58 Improve statistics from spacer 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
00a99f01b4 improved options for IUC computation 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
fba995294d refactored options regarding farkas lemma handling 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
56fcb8e6fd added option fixedpoint.spacer.print_farkas_stats to print number of Farkas lemmas in each proof 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
4148ee128c fixed bug, which added too many edges between super-source and source in the case where the source was used by multiple inferences 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
9b050e8d30 Fix benign warning 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
e7815c703c Fix a typo 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
321cad70d6 improve comments for scoped_weakness 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
890bc0f7c9 fix scoped_weakness 
forgot to save current state of params before resetting them
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
68518b0e32 propagate weakness from pob down to all related checks 
If a pob was discharged with a weak solver, propagate the level of
weakness to inductive generalization and to lemma propagation.
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
b8b3703511 improved implementation of is_qblocked() 
Disabled by default. Has no effect if ran with the default set of
options where qlemmas=true  and instantiate=true
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
371ba4fbc0 added parameters that seem to work well with quantifiers and arith 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
27d8fa4a34 hard-code quantifier weight to 15 
With default settings, the eager threshold is 10 and lazy is 20.  15
puts us in the middle ensuring that lemmas are instantiated when UNSAT
and otherwise delayed.
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
135a4a765f Adding grounding of the current lemma 
In addition to adding the necessary instance of a quantified lemma,
add its grounding over the global set of skolems.
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
e8befc072c cleaned up lemma instantiation code 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
6917aa3eb9 debug print 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
1d478bd8d3 using sk_lt_proc order instead of ast_lt_proc when creating a lemma 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
6cf68bee80 app ordering that puts special skolem constants first 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
9f0eb367b1 ground lemmas during propagation when qlemmas are disabled 
When asserting quantified lemmas are disabled, ground a lemma
explicitly during propagate to make sure that it is ground using our
local set of skolem constants.
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel
5da0753269 (spacer) add instances even when a q-lemma already exists 
It is possible that a new instance of a quantified lemma is discovered
even though a quantified lemma it already known. In this case, the
instance should be added to a corresponding context, even though the
lemma is not new.
 2018-06-14 16:08:47 -07:00
Nikolaj Bjorner
fa93bc419d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 10:53:36 -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
Nikolaj Bjorner
fa0c75e76e rename to core2 to avoid overloaded virtual 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 15:13:13 -08:00
Nikolaj Bjorner
9d37257059
Merge pull request #1465 from waywardmonkeys/fix-typos 
thanks
 2018-02-05 18:31:09 -08:00
Bruce Mitchener
ae8027e594 Fix typos. 2018-02-01 19:39:43 +07:00
Bruce Mitchener
177414c0ee Use const refs to reduce copying. 
These are things that have been found by `clang-tidy`.
 2018-01-30 21:43:56 +07:00
Nikolaj Bjorner
a74d18a695 prepare for variable scoping and autarkies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-13 20:11:16 -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
454e12fc49 update to vector format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-10 15:28:16 -08:00
Nikolaj Bjorner
75b8d10f48 add backtrack level to cuber interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 21:44:21 -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
9e20bfe7f9 fix virtual method override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 17:23:35 -07:00
Nikolaj Bjorner
e4b595d490 add solver pool abstraction for Spacer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:10:20 -07:00
Nikolaj Bjorner
371f0b193c move min_cut, fix #1321 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 02:59:04 -07:00
Nikolaj Bjorner
48d144a6dd missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 12:51:47 -07:00
Nikolaj Bjorner
db65cc007a move more proof utils 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 10:27:48 -07:00
Nikolaj Bjorner
fc822af707 move proof utils under ast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 09:59:55 -07:00