Nikolaj Bjorner
82d9e4a4fc
update goal2sat interface to use explicit initialization
2022-11-28 15:04:12 +07:00
Nikolaj Bjorner
500626e814
add sat-smt-preprocess module
...
self-contained pre-processing initialization
2022-11-28 12:13:00 +07:00
Nikolaj Bjorner
85f9c7eefa
replace restore_size_trail by more generic restore_vector
...
other updates:
- change signature of advance_qhead to simplify call sites
- have model reconstruction replay work on a tail of dependent_expr state, while adding formulas to the tail.
2022-11-28 11:45:56 +07:00
Nikolaj Bjorner
6454014119
enable incrementality for model reconstruction
2022-11-25 15:28:38 +07:00
Nikolaj Bjorner
4e9f21c2a1
add rewriter and seq simplifiers
2022-11-25 15:16:14 +07:00
Nikolaj Bjorner
a152f9cfd6
port bit-blaster to simplifiers
...
inc_sat_solver uses bit-blaster, card2bv and max_bv_sharing.
By turning these into simplifiers it will be possible to remove
dependencies on tactics and goals in inc_sat_simplifier and instead use a modular and general incremental pre-processing infrastructure.
2022-11-25 13:37:16 +07:00
Nikolaj Bjorner
f0570fbc0e
remove tactic exception dependency
2022-11-25 11:48:44 +07:00
Nikolaj Bjorner
e95b0bd2cd
remove include of tactical
2022-11-25 11:47:38 +07:00
Nikolaj Bjorner
8184e7fe0a
keep track of qhead
2022-11-25 11:42:16 +07:00
Nikolaj Bjorner
5af6e1a046
make max_bv_sharing a simplifier
2022-11-25 11:38:41 +07:00
Nikolaj Bjorner
db74e23de1
make card2bv a simplifier
2022-11-25 11:07:31 +07:00
Nikolaj Bjorner
cb789f6ca8
add arithmetical macros
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-24 23:44:35 +07:00
Nikolaj Bjorner
eb812e47be
cleanup
2022-11-24 22:46:35 +07:00
Nikolaj Bjorner
a64c7c5d19
add incremental version of value propagate
2022-11-24 21:52:55 +07:00
Nikolaj Bjorner
decb3d3907
stashed header file
2022-11-24 19:51:26 +07:00
Nikolaj Bjorner
3479129582
remove unused structs
2022-11-24 19:47:26 +07:00
Nikolaj Bjorner
caf204ab95
hoist macro-replacer as shared utility, update eliminate-predicates and model reconstruction
2022-11-24 19:45:51 +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
f87e187b62
#6429
2022-11-23 17:52:14 +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
cd0d52acec
using C++11 features to simplify for-loops
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
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
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
