mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 06:15:37 +00:00
Code Activity
9006 commits 23 branches 48 tags 157 MiB
Commit graph

9006 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner ffdefa4f65 add todo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 3bc3b00fdd Post merge compile fixes 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 649bab2f58 Rename itp_solver into iuc_solver 
IUC stands for Interpolanted UNSAT Core
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 5d3b515a50 Cleanup option names and default values 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 39bdecf9c2 Minor code cleanup 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 83adb6742e Remove whitespace 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 7c727ee922 Fix compiler warnings 2018-06-14 16:08:48 -07:00
Bernhard Gleiss 4b6921dffb removed unnecessary assignment 2018-06-14 16:08:48 -07:00
Bernhard Gleiss 295d16bfae Rewrite hyp-reducer 
This is a new version that conceptually addresses the bugs in
all previous version. However, it had a hard-to-debug memory
corruption. The bug appeared only in optimized compilation under
Linux with GCC.

This code is suspect and should be reviewed and further tested
 2018-06-14 16:08:48 -07:00
Bernhard Gleiss 85c58e344c Add option to use old_hyp_reducer 2018-06-14 16:08:48 -07:00
Arie Gurfinkel f0f75d5254 Wire in arith-axiom-reducer 2018-06-14 16:08:48 -07:00
Bernhard Gleiss 0f25e9e831 Moved farkas stats printing to before and after the hyp-reduction 2018-06-14 16:08:48 -07:00
Bernhard Gleiss de31b07008 arith-theory-axiom reducer to handle arithmetic axioms 2018-06-14 16:08:48 -07:00
Arie Gurfinkel df2eb771ef Fix in spacer_itp_solver: use pr.get() instead of get_proof() 2018-06-14 16:08:48 -07:00
Arie Gurfinkel ab3a6702af Fix several bugs in hyp_reducer 
- compute_marks didn't find all units
  - call to m.mk_unit_resolution expects that there is at least one unit
  - hyp-reduced proof wasn't used
  - bug in early termination
  - any hypothesis was  replaced with the old derivation of the literal
  - handle the case of a single literal premise under hypothesis that is
    replaced by an empty clause under hypothesis
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 56114a5f6d Refactor iuc_proof as a separate class 
This also adds DOT printing support to interpolating proofs
(color for different parts)

iuc_proof is a proof used for IUC computation
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 10106e8e12 Minor fixes to ast_pp_dot 2018-06-14 16:08:48 -07:00
Bernhard Gleiss 247c570e6b Debug sanity check in spacer_context 
Triggered by bugs in hypothesis remover

only sanitycheck lemmas in debug-mode
 2018-06-14 16:08:48 -07:00
Matteo Marescotti a4e67b8bb6 Wire JSON printing into Spacer 2018-06-14 16:08:48 -07:00
Matteo Marescotti 3248f57434 Add support for printing spacer pobs in JSON 2018-06-14 16:08:48 -07:00
Matteo Marescotti 28ef9ab9d1 User option to enable starting spacer from a given level 2018-06-14 16:08:48 -07:00
Matteo Marescotti ff7c949be8 Fix: call collect_statistics() in virtual_solver 2018-06-14 16:08:48 -07:00
Matteo 65885f7eba add_constraint API 2018-06-14 16:08:48 -07:00
Matteo 3c7165780c Extend spacer with callback events 
Callback events allow the client of spacer to
get events during exection. The events include
new lemmas and unfolding.
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel b51251f394 Move tout under TRACE 2018-06-14 16:08:48 -07:00
Arie Gurfinkel fd7bcc7afc Format 2018-06-14 16:08:48 -07:00
Yakir Vizel 5df7a08d1c A simple version for finding the stride between different indices in a POB 
This current version is very limited.
It assumes a pre-defined structure (namely, an ADDER).
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 04a778f2fd Option to enable cube normalization in quic generalizer 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 852e181fed New quic3 lemma generalizer 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 9cdb63ae4a Handle conversion of quantified lemma to quantifier free 
When a cube is updated, a lemma might loose all of its quantified
variables. In this case, it is effectively quantifier free
and might be a version of an already existing lemma.

For that reason, we convert it to quantifier free lemma when
this happens.
 2018-06-14 16:08:48 -07:00
Yakir Vizel 23a8e59493 Initial commit of QGen 
Controlled by fixedpoint.spacer.use_quanti_generalizer

measure cumulative time, number of invocations, and number of failed
SMT calls

Relaxing equality in a pattern: if a variable equals a numeral, relax with GE

pob::get_skolems() returns all skolems that might appear in the pob.
New skolems must be added above the largest index in that map,
even if they are not used in the pob itself.

pattern generalization should be done before the pattern is skolemized and
added into the new cube.
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel a1efb88318 Semantic matcher 
Extends matcher with rewrites based on semantics of arithmetic operations

Like matcher, but uses arithmetic and logic rewrites to try to
get a semantic match.
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel 7dee36358d Allow bool_ind_generalizer to skip non-array literals 
Currently a hack to skip generalizing some literals.
Used together with quic generalizer to remove all array terms if possible
before quic generalization
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel 46fb0d928a Fix in spacer_term_graph 2018-06-14 16:08:47 -07:00
Yakir Vizel 068b77d43a Normalizing LE and GE with constants 2018-06-14 16:08:47 -07:00
Arie Gurfinkel 0c1ef7155a Option to rewrite expression in term_graph 
Rewrite expressions to minimize uses of constants 0 and 1
Currently disabled due to interaction with quic
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel ecf9c629b0 Fix binding handling for quantifier free lemmas 2018-06-14 16:08:47 -07:00
Arie Gurfinkel a8318b8822 Fix lemma::has_binding() 2018-06-14 16:08:47 -07:00
Arie Gurfinkel ec179da0fa API to get num of free variables in a pob 2018-06-14 16:08:47 -07:00
Arie Gurfinkel 05e876d684 Fix n-arry applications in spacer_term_graph 2018-06-14 16:08:47 -07:00
Arie Gurfinkel 7b82ec1bee Attempt bug fix 2018-06-14 16:08:47 -07:00
Arie Gurfinkel 981e521b18 Cleanup lemma definition 
exposes a potential bug. See comments in code.
 2018-06-14 16:08:47 -07:00
Yakir Vizel f51c07adf6 Moving skolems to lemma 2018-06-14 16:08:47 -07:00
Arie Gurfinkel ea73acef45 Implements mk_num_pat 
Abstracts interpreted numeric constants with variables in a ground expression
 2018-06-14 16:08:47 -07:00
Arie Gurfinkel 9bc11b2122 Wire term graph into eq_generalizer 2018-06-14 16:08:47 -07:00
Arie Gurfinkel 09d54c10a6 Wire term graph into spacer normalizer 2018-06-14 16:08:47 -07:00
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