Implementation of the new justification heuristic (#6465)

This adds the new implementation of the justification heuristic. It does not enable this strategy yet.

A followup PR will activate this strategy within DecisionEngine.

1 files changed, 38 insertions, 0 deletions

diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml
index b6f5a5c1b..4f3f91ba5 100644
--- a/src/options/decision_options.toml
+++ b/src/options/decision_options.toml
@@ -68,3 +68,41 @@ name   = "Decision Heuristics"
   name = "sum"
 [[option.mode.USR1]]
   name = "usr1"
+
+[[option]]
+  name       = "jhSkolemMode"
+  category   = "expert"
+  long       = "jh-skolem=MODE"
+  type       = "JutificationSkolemMode"
+  default    = "FIRST"
+  help       = "policy for when to satisfy skolem definitions in justification heuristic"
+  help_mode  = "Policy for when to satisfy skolem definitions in justification heuristic"
+[[option.mode.FIRST]]
+  name = "first"
+  help = "satisfy pending relevant skolem definitions before input assertions"
+[[option.mode.LAST]]
+  name = "last"
+  help = "satisfy pending relevant skolem definitions after input assertions"
+
+[[option]]
+  name       = "jhRlvOrder"
+  category   = "expert"
+  long       = "jh-rlv-order"
+  type       = "bool"
+  default    = "false"
+  help       = "maintain activity-based ordering for decision justification heuristic"
+
+[[option]]
+  name       = "jhSkolemRlvMode"
+  category   = "expert"
+  long       = "jh-skolem-rlv=MODE"
+  type       = "JutificationSkolemRlvMode"
+  default    = "ASSERT"
+  help       = "policy for when to consider skolem definitions relevant in justification heuristic"
+  help_mode  = "Policy for when to consider skolem definitions relevant in justification heuristic"
+[[option.mode.ASSERT]]
+  name = "assert"
+  help = "skolems are relevant when they occur in an asserted literal"
+[[option.mode.ALWAYS]]
+  name = "always"
+  help = "skolems are always relevant"