mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity
8960 commits 23 branches 48 tags 157 MiB
Commit graph

8960 commits

This branch
This branch
All branches
Author SHA1 Message Date
Arie Gurfinkel be77b1de39 Improve interface of term_graph 2018-06-14 16:08:47 -07:00
Arie Gurfinkel 6407ec8725 spacer_term_graph: an egraph of terms 
Used to determine and factor out equalities
 2018-06-14 16:08:47 -07:00
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 6818eb3340 Improve factor 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 e94b97376c fix memory leak in relation_manager, use for loops 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 10:16:03 -07:00
Nikolaj Bjorner 187f1a8cbd Merge branch 'master' of https://github.com/z3prover/z3 2018-06-08 10:30:28 -07:00
Nikolaj Bjorner 63a1b2e714 fix #1665 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-08 10:30:20 -07:00
Nikolaj Bjorner 5ffd06c608
Merge pull request #1673 from NikolajBjorner/master 
gcd/#1667
 2018-06-08 09:29:27 -07:00
Nikolaj Bjorner 0520d1a1f6 remove trial with mfsr flag 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-08 07:38:30 -07:00
Nikolaj Bjorner 24adae4166 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-07 22:03:16 -07:00
Nikolaj Bjorner 4547f2c001 enable non-expression bodies of quantifiers to fix #1667 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-07 22:03:03 -07:00
Nikolaj Bjorner 29c2672407 fix bugs exposed by Nuno's PB example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-07 21:43:37 -07:00
Nuno Lopes 9e916edcb0 z3.py: add overflow checks to PB API 2018-06-07 15:40:04 +01:00
Nikolaj Bjorner 88ead235f0 gcc mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-06 19:30:56 -07:00
Nikolaj Bjorner bb53060313 int64_t 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-06 19:26:40 -07:00
Nikolaj Bjorner 8565de2c5b deal with shift exponent error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-06 19:17:37 -07:00
Nikolaj Bjorner ad67424987 deal with shift exponent error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-06 18:23:04 -07:00
Nikolaj Bjorner d7f51f2443 try flags to fix gcc build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-06 18:20:23 -07:00
Nikolaj Bjorner 99bdb46158 int64_t 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-06 17:48:30 -07:00
Nikolaj Bjorner 8ab428b660 try new gcd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-06 17:42:44 -07:00
Nikolaj Bjorner add8d26807 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-01 08:07:14 -07:00
Nikolaj Bjorner fee4f91e2d add set operations to python request by Francois 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-01 08:07:06 -07:00
Nikolaj Bjorner e2eb883c71 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-30 16:48:17 -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 0d668e1428 fix #1661 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-30 03:18:22 -07:00
Nikolaj Bjorner 0aa3245c37 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-29 20:55:46 -07:00