mirror of
https://github.com/Z3Prover/z3
synced 2025-08-25 04:26:00 +00:00
10145366b2
Add an alternative to unit-subsume-simplify It is called solver-subsumption It does a little more than unit-subsume-simplify and also uses a different decomposition algorithm for clauses. It removes redundant constraints and simplifies clauses in a single pass. A possible use of this tactic is in isolation where the maximal number of conflicts (smt.conflicts_max, sat.conflicts_max) are bounded. For simpler formulas full solver calls may be still feasible.
22 lines
393 B
CMake
22 lines
393 B
CMake
z3_add_component(portfolio
|
|
SOURCES
|
|
default_tactic.cpp
|
|
smt_strategic_solver.cpp
|
|
solver2lookahead.cpp
|
|
solver_subsumption_tactic.cpp
|
|
COMPONENT_DEPENDENCIES
|
|
aig_tactic
|
|
fp
|
|
fpa_tactics
|
|
qe
|
|
sat_solver
|
|
sls_tactic
|
|
smtlogic_tactics
|
|
subpaving_tactic
|
|
ufbv_tactic
|
|
fd_solver
|
|
TACTIC_HEADERS
|
|
default_tactic.h
|
|
solver_subsumption_tactic.h
|
|
|
|
)
|