mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity
17299 commits 23 branches 48 tags 156 MiB
Commit graph

17299 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 5fe2ff84e9 change functionality to not track ite terms for congruence closure 2022-11-24 19:45:16 +07:00
Nikolaj Bjorner 15dc7b78a0 Move merge_tf handling to euf_internalize 
literals true/false are not necessarily created when the merge flag is set.
Also disable merge_tf for if-then-else expressions
Perhaps even not insert children of if expressions into congruence table?
 2022-11-24 15:09:13 +07:00
Nikolaj Bjorner eceeb295fc fix #6457 2022-11-24 14:41:50 +07:00
Nikolaj Bjorner 4ac5e51e3a #6429 2022-11-23 18:35:17 +07:00
Nikolaj Bjorner f87e187b62 #6429 2022-11-23 17:52:14 +07:00
Nikolaj Bjorner 0a671f2f44 fix #6464 2022-11-23 17:21:51 +07:00
Nikolaj Bjorner 0a28bacd0f remove debug out 2022-11-23 16:42:36 +07:00
Nikolaj Bjorner 9a2693bb72 tune euf-completion 2022-11-23 16:39:20 +07:00
Nikolaj Bjorner 22353c2d6c new core perf - add merge_tf and enable_cgc distinction 
perf fix for propagation behavior for equalities in the new core.
The old behavior was not to allow congruence closure on equalities.
The new behavior is to just not allow merging tf with equalities unless they appear somewhere in a foreign context (not under a Boolean operator)

The change re-surfaces merge_tf and enable_cgc distinction from the old core.
They can both be turned on or off.

merge_enabled renamed to cgc_enabled

The change is highly likely to introduce regressions in the new core.

Change propagation of literals from congruence:
- track antecedent enode. There are four ways to propagate
literals from the egraph.
- the literal is an equality and the two arguments are congruent
- the antecedent is merged with node n and the antecedent has a Boolean variable assignment.
- the antecedent is true or false, they are merged.
- the merge_tf flag is toggled to true but the node n has not been merged with true/false
 2022-11-23 11:37:24 +07:00
Nikolaj Bjorner 11b712fee0 switch to new configuration convention in solver object 2022-11-23 11:37:23 +07:00
Nikolaj Bjorner 6188c536ef add logging of propagations to smt core 
log theory propagations with annotation "smt".
It allows tracking theory propagations (when used in conflicts) in the clause logs similar to the new core.
 2022-11-23 11:37:23 +07:00
Nikolaj Bjorner 5374142e3e continue updates for adding proof-log to smt core 2022-11-23 11:37:23 +07:00
Nikolaj Bjorner c7781f346d move parameter sat.smt.proof to solver.proof.log 
this update breaks use cases that set sat.smt.proof to True.
As it is such a new feature and the change affects possibly at most the tutorial it is made without compatibility layers.
 2022-11-23 11:37:23 +07:00
Nikolaj Bjorner cd0d52acec using C++11 features to simplify for-loops 2022-11-23 11:37:23 +07:00
Nikolaj Bjorner 5c5673bc09 make sure parser context within solver object has its parameters updated 
this is to enable use cases like:

```
from z3 import *

s = Solver()
OnClause(s, print)
s.set("solver.proof.check", False)
s.from_file("../satproof.smt2")
```

instead of setting global parameters before the proof replay is initialized.
 2022-11-23 11:37:23 +07:00
Nuno Lopes 477b90228e fix #6460: crash in mk_to_ieee_bv_i 2022-11-20 19:19:12 +00:00
Nuno Lopes 0445d6f264 FPA->BV fix unused vars 2022-11-20 19:03:32 +00:00
Nikolaj Bjorner b9f34286a7 generalize macro head detection and elaboration 2022-11-20 11:36:45 +07:00
Nikolaj Bjorner fcaa85d7a8 #6456 - elaborate on error message 2022-11-20 11:27:39 +07:00
Nikolaj Bjorner 86f3702403 prevent re-declaration of enumeration sort names 
preventing redeclaration of all ADT cases is not part of this update.
 2022-11-19 19:46:34 +07:00
Nikolaj Bjorner c3c45f495a add some comments to elim_predicates 2022-11-19 19:45:25 +07:00
Nikolaj Bjorner 251d49d133 remove outdated comment 2022-11-19 18:55:30 +07:00
Nikolaj Bjorner 3f10933225 remove VERBOSE 0 2022-11-19 18:55:01 +07:00
Nikolaj Bjorner 771157696b new simplifier/tactic 
eliminate_predicates finds macros and eliminates predicates from formulas as pre-processing.
 2022-11-19 18:51:20 +07:00
Nikolaj Bjorner d735faae4e add isolated hide/add model converter functions 2022-11-19 18:50:37 +07:00
Nikolaj Bjorner a81a5ec68c add virtual function requirement to dependent_expr_state 2022-11-19 18:46:31 +07:00
Nikolaj Bjorner dcc995f0e5 code simplification 2022-11-19 18:45:54 +07:00
Nikolaj Bjorner 41b40c3a51 remove dead code 2022-11-19 18:45:07 +07:00
Nikolaj Bjorner c2e9016d04 display model-add parameters in correct order 2022-11-19 18:44:52 +07:00
Nikolaj Bjorner ba68652c72 add destructive equality resolution to existentials 2022-11-19 18:43:46 +07:00
Nikolaj Bjorner 7da91f4313 allow printing declarations with reverse variable order 2022-11-19 18:43:21 +07:00
Nikolaj Bjorner 59b7845c7d reset visited (fast mark) to not clash with occurs 2022-11-17 17:36:21 +09:00
Nikolaj Bjorner 6662afdd26 perf improvements to solve-eqs and euf-completion 2022-11-16 22:15:02 -08:00
Nikolaj Bjorner 2c7799939e wip - tuning and fixes to euf-completion 2022-11-16 03:47:38 -08:00
Nikolaj Bjorner 98fc8c99db add shortcut to equality mk utility 2022-11-16 03:47:01 -08:00
Nikolaj Bjorner 55ab7778f4 fix perf bug in new solve_eqs. 2022-11-16 03:46:17 -08:00
Nikolaj Bjorner d70dbdad50 wip euf-completion - debugging 2022-11-15 20:17:39 -08:00
Nikolaj Bjorner 255414f4a9 fix regression crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-15 11:20:12 -08:00
Nikolaj Bjorner 9845c33236 add shortcuts in rewriter, eliminate redundancies in dependent_expr tactic 2022-11-15 09:13:13 -08:00
Nikolaj Bjorner bfae8b2162 set flat_and_or to false in bv rewriter 2022-11-15 05:47:28 -08:00
Nikolaj Bjorner 041b5f9ef0 rename away solve_eqs2 to solve_eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-14 20:01:37 -08:00
Nikolaj Bjorner 48c0f8694f euf-completion bug fix, streamline name to solve_eqs 2022-11-14 20:01:00 -08:00
Nikolaj Bjorner 3eeb59db34 fix #6451 missing occurrence marking when there is an unsafe equality already 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-14 19:23:27 -08:00
Nikolaj Bjorner 95e07ffe8e disable unsound context equality solving 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-14 19:14:51 -08:00
Nikolaj Bjorner 6297c001ee remove legacy solve_eqs_tactic entirely 
also, bug fixes to elim_unconstrained (elim_uncnstr2) which is to replace legacy tactic for eliminating unconstrained constants.
 2022-11-14 18:57:16 -08:00
Nikolaj Bjorner 3f2bbe5589 harness del_object #6452 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-14 08:54:08 -08:00
Nikolaj Bjorner 3d2bf13577 streamline statistics, fix bug in updating goals 2022-11-13 20:30:00 -08:00
Nikolaj Bjorner ce6cfeaa68 fix bug in euf-completion relating to missed normalization 2022-11-13 18:01:17 -08:00
Nikolaj Bjorner 3fa81d6527 bug fixes to elim-uncnstr2 tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-13 13:25:19 -08:00
Nikolaj Bjorner 38cde14e08 wip missing updates 2022-11-13 12:10:43 -08:00