Nikolaj Bjorner
7df4e04a2c
add der description
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-06 05:46:52 -08:00
Nikolaj Bjorner
90ba225ae3
add more doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-06 05:39:05 -08:00
Nikolaj Bjorner
5a5758baaa
add documentation to initial selection of tactics
2022-12-05 20:05:06 -08:00
Nikolaj Bjorner
f1a65d9642
add documentation notes
2022-12-05 20:05:06 -08:00
Nuno Lopes
a2f5a5b50b
remove memory alloc from statistics_report
2022-12-05 14:29:14 +00:00
Nuno Lopes
eb8c53c164
simplify factory of dependent_expr_state_tactic
...
And as a side-effect, remove heap allocations for factories
2022-12-05 14:07:57 +00:00
Nikolaj Bjorner
de916f50d6
add demodulator tactic based on demodulator-simplifier
...
- some handling for commutative operators
- fix bug in demodulator_index where fwd and bwd are swapped
2022-12-05 03:20:46 -08:00
Nikolaj Bjorner
87095950cb
fix #6477
2022-12-04 13:02:45 -08:00
Nikolaj Bjorner
ead2a46a88
build
2022-12-04 10:38:24 -08:00
Nikolaj Bjorner
b76ed6a47f
proper fix to #6476
2022-12-04 10:19:39 -08:00
Nikolaj Bjorner
9b58135876
try to fix linux builds
2022-12-04 09:55:31 -08:00
Nikolaj Bjorner
0f7bebcbed
try big M for linux build
2022-12-04 09:49:32 -08:00
Nikolaj Bjorner
1974c224ab
add demodulator simplifier
...
refactor demodulator-rewriter a bit to separate reusable features.
2022-12-04 09:39:28 -08:00
Nikolaj Bjorner
9acbfa3923
move it into substitution to handle dependencies
2022-12-04 06:23:32 -08:00
Nikolaj Bjorner
3d7bd40a87
a round of cleanup
2022-12-04 06:07:45 -08:00
Nikolaj Bjorner
d218083145
The demodulator doesn't produce proofs so remove code path that depends it does.
2022-12-04 04:48:48 -08:00
Nikolaj Bjorner
7fe6787748
ufbv-rewriter is really a demodulator rewriter and does not reference ufbv
...
so moving first the rewriter into place of other rewriters
2022-12-04 04:44:02 -08:00
Nikolaj Bjorner
e455897178
fix #6476
2022-12-04 04:36:06 -08:00
Nikolaj Bjorner
79e6d4e32d
tune and debug elim-unconstrained (v2 - for simplifiers infrastructure)
2022-12-04 03:53:31 -08:00
Nikolaj Bjorner
59fa8964ca
minor code cleanup
2022-12-04 03:53:31 -08:00
Nikolaj Bjorner
3ebbb8472a
fix perf bugs in new value propagation
2022-12-04 03:53:30 -08:00
Nikolaj Bjorner
758c3b2c3b
fix filtering for recursive functions
2022-12-04 03:53:30 -08:00
Nikolaj Bjorner
cf7bba6288
use ast_manager as an attribute
2022-12-04 03:53:30 -08:00
Nikolaj Bjorner
5073959ae0
add macro attribute
2022-12-04 03:53:29 -08:00
yizhou7
54a8d65617
move flushes in display_statistics ( #6472 )
2022-12-02 13:56:53 -08:00
Nikolaj Bjorner
a96b7d243a
remove incorrect check for quantifier
2022-12-01 00:04:08 -08:00
Nikolaj Bjorner
e5984dd397
add cnf/nnf simplifier
2022-11-30 23:04:38 -08:00
Nikolaj Bjorner
e3e2c21632
Create cnf_nnf.h
2022-11-30 22:53:14 -08:00
Nikolaj Bjorner
847aec1d30
update dependencies
2022-11-30 22:48:10 -08:00
Nikolaj Bjorner
529f116be0
disable new code until pre-condition gets fixed
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-30 22:29:59 -08:00
Nikolaj Bjorner
147fb0d9c1
fix tptp5 build
2022-11-30 21:41:44 -08:00
Nikolaj Bjorner
30c9cda61e
increment generation for literals created during E-matching
2022-12-01 10:04:33 +09:00
Nikolaj Bjorner
f24ecde35c
wip - fixes to simplifiers
2022-12-01 09:31:52 +09:00
Nikolaj Bjorner
cfc8e19baf
add more simplifiers, fix model reconstruction order for elim_unconstrained
...
- enable sat.smt in smt_tactic that
is invoked by default on first goals
add flatten-clauses
add push-ite
have tptp5 front-end pretty print SMT2 formulas a little nicer.
2022-12-01 02:35:43 +09:00
Nikolaj Bjorner
edb0fc394b
rewrite some simplifiers
2022-11-30 23:15:32 +09:00
Nikolaj Bjorner
23c53c6820
fix build
2022-11-30 19:36:13 +09:00
Nikolaj Bjorner
c1ff3d3192
wip - adding quasi macro detection
2022-11-30 13:46:00 +07:00
Nikolaj Bjorner
7b9dfb8e1e
update dependencies for python build
2022-11-30 13:43:40 +07:00
Nikolaj Bjorner
b084821a0c
wip - dependent expr simpliifer
...
- simplify iterator over current indices
- add more simplifiers used by asserted_formulas
- improve diagnostics printing
2022-11-30 13:41:40 +07:00
Nikolaj Bjorner
bec3acd146
consolidate freeze functionality into dependent_expr_state
...
rename size() to qtail() and introduce shortcuts
ensure tactic goals are not updated if they are in inconsistent state (because indices could be invalidated)
2022-11-30 08:35:29 +07:00
Nikolaj Bjorner
73a652cf4b
some fixes to backtracking restore points in new solver
2022-11-29 16:42:42 +07:00
Nikolaj Bjorner
dd1ca8f6bd
move qhead to attribute on the state instead of the simplifier,
...
- add sat.smt option to enable the new incremental core (it is not ready for mainstream consumption as cloning and other features are not implemented and it hasn't been tested in any detail yet).
- move "name" into attribute on simplifier so it can be reused for diagnostics by the seq-simplifier.
2022-11-29 16:36:02 +07:00
Nikolaj Bjorner
ac023935a3
introduce sat-smt-solver
...
in an iteration of inc-sat-solver introduce sat-smt-solver to allow incremental pre-processing.
The aim is to allow incrementally handling formulas while at the same time retaining the main benefits of global in/pre-processing that change models. Previous incremental solving capabilities have been limited to use pre-processing that does not require model conversion.
2022-11-28 15:06:31 +07:00
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
