summaryrefslogtreecommitdiff
path: root/src/decision/decision_mode.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/decision/decision_mode.h')
-rw-r--r--src/decision/decision_mode.h9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/decision/decision_mode.h b/src/decision/decision_mode.h
index 335e6279e..20743cba1 100644
--- a/src/decision/decision_mode.h
+++ b/src/decision/decision_mode.h
@@ -46,6 +46,15 @@ enum DecisionMode {
};/* enum DecisionMode */
+
+/** Enumeration of combining functions for computing internal weights */
+enum DecisionWeightInternal {
+ DECISION_WEIGHT_INTERNAL_OFF,
+ DECISION_WEIGHT_INTERNAL_MAX,
+ DECISION_WEIGHT_INTERNAL_SUM,
+ DECISION_WEIGHT_INTERNAL_USR1
+};/* enum DecisionInternalWeight */
+
}/* CVC4::decision namespace */
std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) CVC4_PUBLIC;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback