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

9282 commits

This branch
This branch
All branches
Author SHA1 Message Date
Arie Gurfinkel 5a6bd5e782 hypothesis_reducer: worked around propositional literals 
propositional formulas (disjunctions) can appear as literals.  This
makes it tricky to recognize whether a formula is a unit clause when
re-building unit resolution.

Added work-around that identifies whether a formula is a literal based
on its appearance in previous unit resolution step.
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel b39c532f19 Order of methods in spacer_context.cpp 2018-06-14 16:08:48 -07:00
Nikolaj Bjorner 7931bd1dfc updates to mbqi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 0fe5e6c2a6 Fix handling of complex literals in hypothesis_reducer 
In Z3, an arbitrary, even propositional, formula can be a literal.

This requires careful handling of restructuring of unit resolution.
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel d1a7c0ceb0 Remove a print 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 05c8067392 Changed pob queue management strategy in spacer_context 2018-06-14 16:08:48 -07:00
Arie Gurfinkel a696a40a3a Refactoring 2018-06-14 16:08:48 -07:00
Arie Gurfinkel ec8f99fee7 Rename expand_node --> expand_pob 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 3f9b5bce99 Remove debug function 2018-06-14 16:08:48 -07:00
Arie Gurfinkel ac3bbed311 Remove dead code in spacer_manager 
- removed bg_assertions. Incompatible with mbp in spacer
  - removed unique number. Unused
  - removed mk_and() and switched to ast_util:mk_and() instead
       spacer_manager::mk_and() uses bool_rewriter to simplify the
       conjunction
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 33466c75a6 mss loop in prop_solver 
max sat assignment (mss) to replace core-based maxsmt()
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel d379b14942 Cleanup spacer_iuc_solver 2018-06-14 16:08:48 -07:00
Arie Gurfinkel fd13eb9e0e Final cleanup of hypothesis_reducer 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 9d4784baf6 Fix dealloc order in hypotheses_reducer::reset() 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 689414d055 Fix debug printing in iuc_solver 2018-06-14 16:08:48 -07:00
Nikolaj Bjorner ff0f257102 remove iff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Nikolaj Bjorner ecf15ab07d add model_evaluator_util features to model_evalautor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 8d312f9d1f Cleanup of hypothesis_reducer 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 2db38fedd6 Cleanup of theory_axiom_reducer proof trasfomation 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 07ad67ebad Move proof dot printing into iuc_proof 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 45500ff7d3 Cleanup iuc_proof 2018-06-14 16:08:48 -07:00
Arie Gurfinkel abe67705d3 Cleanup iuc_proof 2018-06-14 16:08:48 -07:00
Arie Gurfinkel ebf6b18821 maxsat standalone mode 2018-06-14 16:08:48 -07:00
Arie Gurfinkel 49821e7c91 Revised solver_pool 2018-06-14 16:08:48 -07:00
Arie Gurfinkel c893740e13 Fix compilation 2018-06-14 16:08:48 -07:00
Nikolaj Bjorner b649cd93cb change pool solver to enable external control of pool allocation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
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