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
Nikolaj Bjorner
196788a091
bug fix for equality solving
2022-11-13 12:09:56 -08:00
Nikolaj Bjorner
ce76e3138d
streamlining expr-inverter code
2022-11-13 11:48:32 -08:00
Nikolaj Bjorner
3d570aaa0a
add missing process_eq
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-12 18:43:57 -08:00
Nikolaj Bjorner
0b83732b82
missing override specifier
2022-11-12 18:35:41 -08:00
Nikolaj Bjorner
343603f643
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-12 18:34:04 -08:00
Nikolaj Bjorner
e33e66212c
propagate values should not flatten and/or
...
also, elim_uncstr should only be disabled on recursive functions
2022-11-12 18:03:47 -08:00
Nikolaj Bjorner
f4e17ecc65
add logging and diagnostics
2022-11-12 18:03:47 -08:00
Nikolaj Bjorner
9d09064ad0
add comments to elim_unconstrained and remove unused function
2022-11-12 18:01:38 -08:00
Nikolaj Bjorner
efbe0a6554
wip - updated version of elim_uncstr_tactic
...
- remove reduce_invertible. It is subsumed by reduce_uncstr(2)
- introduce a simplifier for reduce_unconstrained. It uses reference counting to deal with inefficiency bug of legacy reduce_uncstr. It decomposes theory plugins into expr_inverter.
reduce_invertible is a tactic used in most built-in scenarios. It is useful for removing subterms that can be eliminated using "cheap" quantifier elimination. Specifically variables that occur only once can be removed in many cases by computing an expression that represents the effect computing a value for the eliminated occurrence.
The theory plugins for variable elimination are very partial and should be augmented by extensions, esp. for the case of bit-vectors where the invertibility conditions are thoroughly documented by Niemetz and Preiner.
2022-11-12 17:56:45 -08:00
