summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-05-28 10:35:17 -0500
committerGitHub <noreply@github.com>2018-05-28 10:35:17 -0500
commit74c1ad7e4a8e93316b7555ac8a1b88ee777335e2 (patch)
tree3f9c1b691a87a8cbbc73cc5bf46d23638d016856 /src/options
parenta08914e449c3df26322551a968b4edee12a615f9 (diff)
Builtin evaluation functions for sygus (#1991)
Diffstat (limited to 'src/options')
-rw-r--r--src/options/datatypes_options.toml9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 8d6f0baf3..b74244fe1 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -175,3 +175,12 @@ header = "options/datatypes_options.h"
default = "-1"
read_only = true
help = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)"
+
+[[option]]
+ name = "sygusEvalBuiltin"
+ category = "regular"
+ long = "sygus-eval-builtin"
+ type = "bool"
+ default = "true"
+ read_only = true
+ help = "use builtin kind for evaluation functions in sygus"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback