mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
8940 commits 23 branches 48 tags 157 MiB
Commit graph

547 commits

Author SHA1 Message Date
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 a9ca01d8d3 deprecating interp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-24 13:12:07 -07:00
Nikolaj Bjorner 4f5775c531 remove interpolation and duality dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-24 08:33:48 -07:00
Nikolaj Bjorner 50c93d1ad4 merge with 4.7.1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-22 17:10:36 -07:00
corrodedHash d097d90731 Fixed Segfault when failing to load datalog file 2018-05-08 19:26:14 +02:00
Nikolaj Bjorner fa93bc419d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 10:53:36 -07:00
Nikolaj Bjorner f525f43e43 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 09:30:43 -07:00
Nikolaj Bjorner b5f067bec5 fix #1592 #1587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-25 11:18:24 +02:00
Nikolaj Bjorner 97cee7d0a4 fix #1576, hopefully 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-18 07:30:26 -07:00
Nikolaj Bjorner 098bce0f46 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-14 08:44:20 -07:00
Nikolaj Bjorner d939c05e72 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-14 08:27:40 -07:00
Bruce Mitchener 2fa304d8de Remove int64, uint64 typedefs in favor of int64_t / uint64_t. 2018-03-31 14:45:04 +07:00
Nikolaj Bjorner c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Bruce Mitchener 878a6ca14f Fix typos. 2018-03-09 14:30:43 +07:00
Nikolaj Bjorner 246941f2d3 fix #1522 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-07 14:26:38 -08:00
Nikolaj Bjorner 718e5a9b6c add unit extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-06 01:08:17 -08: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
Nikolaj Bjorner 9279cbfbac don't reinit assumptions when the solver is unsat. fixes #1502 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-24 16:30:08 +09:00
Nikolaj Bjorner a4c58ec4c2 fix #1496 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-22 08:05:28 +09:00
Nikolaj Bjorner 7b6f51941c fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-21 22:18:47 +09:00
Nikolaj Bjorner 54b00f357b fix rule inlining, add WithParams to pass parameters directly to python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-21 21:57:54 +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
Bruce Mitchener 54b3cd0071 Reserve vector space when possible. 
This fixes all current instances of the
`performance-inefficient-vector-operation`
warning in clang-tidy.
 2018-02-06 11:21:17 +07:00
Nikolaj Bjorner 9d37257059
Merge pull request #1465 from waywardmonkeys/fix-typos 
thanks
 2018-02-05 18:31:09 -08:00
Nikolaj Bjorner 3e810d6c54 remove static from format (not thread safe), remove std::move #1466 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-05 16:46:49 -08:00
Nikolaj Bjorner 2853558bc2
Merge pull request #1466 from waywardmonkeys/reduce-copying 
Use const refs to reduce copying.
 2018-02-05 16:37:44 -08:00
Bruce Mitchener ae8027e594 Fix typos. 2018-02-01 19:39:43 +07:00
Bruce Mitchener 6d6b614924 Use char version of rfind. 
There is only a single character involved, so use the char version.

This was found via `clang-tidy`.
 2018-01-30 21:45:12 +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 e4f29a7b8a debugging mc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-19 21:09:52 -08:00
Nikolaj Bjorner 5159291d57 add missing interpreted tail during bottom-up simplification #1452 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-12 19:29:42 -08:00
Bruce Mitchener 73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +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 33e8113c9e adding instrumentation to debug #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-20 16:51:17 -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 dc0b2a8acf remove extension model converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 17:25:35 -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