From 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 2 Sep 2011 20:41:08 +0000 Subject: Merge from my post-smtcomp branch. Includes: Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated. --- config/cvc4.m4 | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'config/cvc4.m4') diff --git a/config/cvc4.m4 b/config/cvc4.m4 index c58d976b5..4adc88c61 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -22,8 +22,9 @@ do # regexp `\?' not supported on Mac OS X ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'` ac_cvc4_build_profile_set=yes + as_me=configure AC_MSG_NOTICE([CVC4: building profile $ac_option_build]) - for x in optimized statistics replay assertions tracing muzzle coverage profiling; do + for x in optimized statistics replay assertions tracing dumping muzzle coverage profiling; do if expr "$ac_option" : '.*-no'$x'$' >/dev/null || expr "$ac_option" : '.*-no'$x'-' >/dev/null; then eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-$x\""' fi -- cgit v1.2.3