Refactor mkoptions (cvc5#1631)

This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation.

The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick.

This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.

Makefile.am

@@ -127,7 +127,7 @@ EXTRA_DIST = \
 	doc/find_public_interface.sh \
 	doc/cvc4.1_template.in \
 	doc/cvc4.5.in \
-	doc/libcvc4.3_template.in \
+	doc/libcvc4.3.in \
 	doc/SmtEngine.3cvc_template.in \
 	doc/options.3cvc_template.in \
 	doc/libcvc4parser.3.in \
@@ -167,7 +167,6 @@ DISTCLEANFILES = \
 	doc/pcvc4.1 \
 	doc/cvc4.5 \
 	doc/libcvc4.3 \
-	doc/libcvc4.3_template \
 	doc/libcvc4compat.3 \
 	doc/libcvc4parser.3 \
 	doc/SmtEngine.3cvc \

configure.ac

@@ -1547,7 +1547,7 @@ CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
 
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])

contrib/new-theory

@@ -179,8 +179,8 @@ if ! mv -f src/Makefile.am.new-theory src/Makefile.am; then
   exit 1
 fi
 
-echo "Adding ${dir}_options to src/options/Makefile.am..."
-if grep -q '^	${dir}_options' src/options/Makefile.am &>/dev/null; then
+echo "Adding ${dir}_options.toml to src/options/Makefile.am..."
+if grep -q '^	${dir}_options.toml' src/options/Makefile.am &>/dev/null; then
   echo "NOTE: src/options/Makefile.am already seems to link to $dir option files"
 else
   awk -v name="$dir" -f contrib/new-theory.awk src/options/Makefile.am > src/options/Makefile.am.new-theory

contrib/new-theory.awk

@@ -1,17 +1,7 @@
 #!/bin/awk -v name=theory_new -f
 #
 
-# The do nothing rule
-!/^OPTIONS_SRC_FILES = \\|^OPTIONS_TEMPS = \\|^OPTIONS_OPTIONS_FILES = \\|^OPTIONS_SEDS = \\|^OPTIONS_HEADS = \\|^OPTIONS_CPPS = \\/ {print$0}
-# Add the name to the correct locations.
-/^OPTIONS_SRC_FILES = \\/{print $0; printf "\t%s_options \\\n", name;}
-/^OPTIONS_TEMPS = \\/{print $0; printf "\t%s_options.tmp \\\n", name;}
-/^OPTIONS_OPTIONS_FILES = \\/{print $0; printf "\t%s_options.options \\\n", name;}
-/^OPTIONS_SEDS = \\/{print $0; printf "\t%s_options.sed \\\n", name;}
-/^OPTIONS_HEADS = \\/{print $0; printf "\t%s_options.h \\\n", name;}
-/^OPTIONS_CPPS = \\/{print $0; printf "\t%s_options.cpp \\\n", name;}
-# Add the rule for name_options.
-END{printf "%s_options:;\n", name}
-# Add the rules for name_options.tmp
-END{printf ".PHONY: %s_options.tmp\n", name}
-END{printf "%s_options.tmp:\n\techo \"$@\" \"$(@:.tmp=)\"\n\t$(AM_V_GEN)(cp \"@srcdir@/$(@:.tmp=)\" \"$@\" || true)\n", name}
+# Keep non-matching lines unchanged
+!/^OPTIONS_CONFIG_FILES = \\/ {print$0}
+# Add *_options.toml to OPTIONS_CONFIG_FILES
+/^OPTIONS_CONFIG_FILES = \\/{print $0; printf "\t%s_options.toml \\\n", name;}

contrib/optionsskel/DIR_options.toml

@@ -0,0 +1,8 @@
+#
+# Option specification file for CVC4
+# See src/options/README for a description of this file format
+#
+
+id     = "$id"
+name   = "$camel"
+header = "options/$dir_options.h"

contrib/run-script-smtcomp2018

@@ -26,12 +26,12 @@ function finishwith {
 case "$logic" in
 
 QF_LRA)
-  trywith 200 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
+  trywith 200 --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
   finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp
   ;;
 QF_LIA)
   # same as QF_LRA but add --pb-rewrites
-  finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
   ;;
 QF_NIA)
   trywith 300 --nl-ext --nl-ext-tplanes --decision=internal

contrib/run-script-smtcomp2018-unsat-cores

@@ -17,7 +17,7 @@ QF_LRA)
   finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp
   ;;
 QF_LIA)
-  finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
   ;;
 QF_NIA)
   finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat

doc/SmtEngine.3cvc_template.in

@@ -24,9 +24,9 @@ use the following option keys.
 .RS
 .TP 10
 .I "COMMON OPTIONS"
-${common_manpage_smt_documentation}
+${man_common_smt}$
 
-${remaining_manpage_smt_documentation}
+${man_others_smt}$
 .PD
 .RE
 

doc/cvc4.1_template.in

@@ -48,9 +48,9 @@ is connected to a terminal, interactive mode is assumed.
 
 .IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option."
 
-${common_manpage_documentation}
+${man_common}$
 
-${remaining_manpage_documentation}
+${man_others}$
 
 .IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option."
 

doc/options.3cvc_template.in

@@ -12,9 +12,9 @@ options \- the options infrastructure
 .RS
 .TP 10
 .I "COMMON OPTIONS"
-${common_manpage_internals_documentation}
+${man_common_internals}$
 
-${remaining_manpage_internals_documentation}
+${man_others_internals}$
 .PD
 .RE