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

Minor improvements to difficulty manager (#9510)

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

base

Update copyright headers for release 1.0 (#8539)

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

context

Change datastructure of CDList to std::vector (#2149)

2022-11-22 17:31:32 +00:00

main

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

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

node

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

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

options

Branch on option string names using hash map and switch-case (#9335)

2022-12-11 15:40:01 +00:00

parser

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

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

preprocessing

Minor simplification to solver engine interface (#9138)

2022-09-26 16:59:31 +00:00

printer

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

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

proof

Update copyright headers for release 1.0 (#8539)

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

prop

minisat: Move preregistration handling of new sat variables to theory level. (#9514)

2023-02-23 00:04:26 +00:00

theory

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

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

util

unit: Fix integer_black unit tests. (#9083)

2022-08-25 17:34:11 +00:00

CMakeLists.txt

Update copyright headers for release 1.0 (#8539)

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

test_api.h

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

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

test_context.h

Update copyright headers for release 1.0 (#8539)

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

test_env.h

Eliminate SolverEngineScope and OptionsScope (#8984)

2022-07-22 16:45:47 +00:00

test_node.h

NM: Initialize NodeManager on construction. (#9154)

2022-09-21 20:23:25 +00:00

test_smt.h

Add theory interface for marking unsoundness (#9238)

2022-11-08 19:26:27 +00:00

test.h

Update copyright headers for release 1.0 (#8539)

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