Use propt::lcnf when cnf_handled_well is true

[tautschnig]

We can avoid Tseitin variables when using lcnf directly instead of using set_to_{true,false}. Pending performance evaluation.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 29.13907% with 107 lines in your changes missing coverage. Please review.

Project coverage is 77.90%. Comparing base (bf58af8) to head (2a0c726).

Files	Patch %	Lines
src/cprover/bv_pointers_wide.cpp	0.00%	24 Missing ⚠️
src/solvers/flattening/bv_utils.cpp	36.36%	21 Missing ⚠️
src/solvers/refinement/refine_arithmetic.cpp	14.28%	12 Missing ⚠️
src/solvers/flattening/boolbv_index.cpp	61.53%	10 Missing ⚠️
src/solvers/flattening/boolbv_byte_extract.cpp	43.75%	9 Missing ⚠️
src/solvers/flattening/bv_pointers.cpp	43.75%	9 Missing ⚠️
src/solvers/flattening/boolbv_cond.cpp	0.00%	6 Missing ⚠️
src/solvers/flattening/boolbv_extractbit.cpp	0.00%	6 Missing ⚠️
src/solvers/prop/prop_conv_solver.cpp	0.00%	4 Missing ⚠️
src/solvers/flattening/boolbv_bv_rel.cpp	0.00%	3 Missing ⚠️
... and 1 more

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7402      +/-   ##
===========================================
- Coverage    78.02%   77.90%   -0.12%     
===========================================
  Files         1726     1726              
  Lines       189432   189733     +301     
  Branches     18465    18488      +23     
===========================================
+ Hits        147807   147816       +9     
- Misses       41625    41917     +292     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[martin-cs]

Looks good and I can see that this could save quite a bit in some cases. I wonder if there is a way we can change the API to avoid the all of the branching on cnf_handled_well? It seems like prop.l_set_to_true(prop.limplies(...)) is in many of the changes. Although it's not orthogonal, would prop.l_set_implies_true be worth having?