Andrew Reynolds 00e19fdbe2 Minor improvements to difficulty manager (#9510) ...

We now track difficulty on lemmas themselves, which can potentially used as a heuristic for measuring the usefulness of lemmas.

This also makes it so that all literals in lemmas are used for incrementing difficulty.

2023-03-08 21:36:44 +00:00

..

api_kind_black.cpp

Move public headers into top-level include directory. (#9555)

2023-03-07 23:39:29 +00:00

api_sort_kind_black.cpp

Move public headers into top-level include directory. (#9555)

2023-03-07 23:39:29 +00:00

CMakeLists.txt

Add infrastructure and API for abstract sorts (#9263)

2023-01-17 19:37:10 +00:00

datatype_api_black.cpp

Add missing tests for some corners of the API (#8688)

2022-05-02 21:08:58 +00:00

grammar_black.cpp

Add missing tests for some corners of the API (#8688)

2022-05-02 21:08:58 +00:00

op_black.cpp

Add rel.project operator to sets (#8929)

2022-07-06 21:02:23 +00:00

op_white.cpp

api: Refactor sort and term (like) objects to not depend on Solver. (#9020)

2022-08-03 10:15:50 -05:00

parametric_datatype_black.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

result_black.cpp

Add some missing API tests (#8669)

2022-04-29 00:47:10 +00:00

solver_black.cpp

Minor improvements to difficulty manager (#9510)

2023-03-08 21:36:44 +00:00

solver_white.cpp

api: Refactor sort and term (like) objects to not depend on Solver. (#9020)

2022-08-03 10:15:50 -05:00

sort_black.cpp

Add infrastructure and API for abstract sorts (#9263)

2023-01-17 19:37:10 +00:00

synth_result_black.cpp

Allow SyGuS solver to answer infeasible (#9196)

2022-10-13 15:56:55 +00:00

term_black.cpp

ff: connect sub-theories to main solver & test (#9218)

2022-12-16 16:36:41 +00:00

term_white.cpp

api: Refactor sort and term (like) objects to not depend on Solver. (#9020)

2022-08-03 10:15:50 -05:00

types_black.cpp

Move public headers into top-level include directory. (#9555)

2023-03-07 23:39:29 +00:00