diff options
| author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
|---|---|---|
| committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
| commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
| tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /src/options | |
| parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) | |
update from the master
Diffstat (limited to 'src/options')
56 files changed, 943 insertions, 592 deletions
diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 8a465c522..643932781 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -206,7 +206,8 @@ liboptions_la_SOURCES = \ arith_propagation_mode.h \ arith_unate_lemma_mode.cpp \ arith_unate_lemma_mode.h \ - argument_extender.cpp \ + argument_extender_implementation.cpp \ + argument_extender_implementation.h \ argument_extender.h \ base_handlers.h \ boolean_term_conversion_mode.cpp \ diff --git a/src/options/argument_extender.cpp b/src/options/argument_extender.cpp deleted file mode 100644 index d55610590..000000000 --- a/src/options/argument_extender.cpp +++ /dev/null @@ -1,74 +0,0 @@ -/********************* */ -/*! \file preempt_get_option.h - ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Utility function for parsing commandline options. - ** - ** Utility function for parsing commandline options. - **/ - -#include "options/argument_extender.h" - -#include <cstdlib> -#include <cstring> -#include <vector> - -#include "base/cvc4_assert.h" -#include "base/output.h" - -namespace CVC4 { -namespace options { - -ArgumentExtender::ArgumentExtender(unsigned additional, size_t length) - : d_additional(additional) - , d_length(length) -{ - AlwaysAssert(d_additional >= 1); - AlwaysAssert(d_length >= 1); -} - -ArgumentExtender::~ArgumentExtender(){} - -unsigned ArgumentExtender::getIncrease() const { return d_additional; } -size_t ArgumentExtender::getLength() const { return d_length; } - -void ArgumentExtender::extend(int& argc, char**& argv, const char* opt, - std::vector<char*>& allocated) -{ - - Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl; - - AlwaysAssert(opt != NULL && *opt != '\0'); - AlwaysAssert(strlen(opt) <= getLength()); - - ++argc; - unsigned i = 1; - while(argv[i] != NULL && argv[i][0] != '\0') { - ++i; - } - - if(argv[i] == NULL) { - unsigned newSize = i + getIncrease(); - argv = (char**) realloc(argv, newSize * sizeof(char*)); - for(unsigned j = i; j < newSize-1; ++j) { - char* newString = (char*) malloc(sizeof(char) * getLength()); - newString[0] = '\0'; - argv[j] = newString; - allocated.push_back(newString); - } - argv[newSize - 1] = NULL; - } - - strncpy(argv[i], opt, getLength() - 1); - argv[i][getLength() - 1] = '\0'; // ensure NULL-termination even on overflow -} - -}/* CVC4::options namespace */ -}/* CVC4 namespace */ diff --git a/src/options/argument_extender.h b/src/options/argument_extender.h index 1f7e3c1dd..6be41fe8e 100644 --- a/src/options/argument_extender.h +++ b/src/options/argument_extender.h @@ -1,79 +1,85 @@ /********************* */ -/*! \file preempt_get_option.h +/*! \file argument_extender.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** - ** \brief Utility function for extending commandline options. + ** \brief Abstract utility class for extending commandline options. ** - ** Utility function for extending commandline options. + ** Abstract utility class for extending commandline options. **/ -#include "cvc4_private.h" +#include "cvc4_public.h" -#ifndef __CVC4__OPTIONS__PREMPT_GET_OPTION_H -#define __CVC4__OPTIONS__PREMPT_GET_OPTION_H +#ifndef __CVC4__OPTIONS__ARGUMENT_EXTENDER_H +#define __CVC4__OPTIONS__ARGUMENT_EXTENDER_H #include <cstddef> -#include <vector> namespace CVC4 { namespace options { - +/** + * Abstract utility class for implementing command line options + * parsing for the Options class. This allows for adding preemption + * arguments. A preemption is effectivly adding a new argument into + * the commandline arguments and must be processed immediately. + */ class ArgumentExtender { - public: +public: + ArgumentExtender(){} + virtual ~ArgumentExtender(){} + /** + * This creates a copy of the current arguments list as a new array. + * The new array is stored in argv. The user of this function is + * expected to own the memory of the string array, but not the + * strings themselves. The length of the new array is + * numArguments() and is stored in argc. + * * Preconditions: - * additional >= 1 - * length >= 1 + * - argc and argv are non-null. */ - ArgumentExtender(unsigned additional, size_t length); - ~ArgumentExtender(); + virtual void getArguments(int* argc, char*** argv) const = 0; + + /** Returns the number of arguments that are . */ + virtual size_t numArguments() const = 0; /** - * This purpose of this function is to massage argc and argv upon the event - * of parsing during Options::parseOptions of an option with the :link or - * :link-alternative attributes. The purpose of the function is to extend argv - * with another commandline argument. - * - * Preconditions: - * opt is '\0' terminated, non-null and non-empty c-string. - * strlen(opt) <= getLength() - * - * Let P be the first position in argv that is >= 1 and is either NULL or - * empty: - * argv[P] == NULL || argv[P] == '\0' - * - * This has a very specific set of side effects: - * - argc is incremented by one. - * - If argv[P] == NULL, this reallocates argv to have (P+additional) - * elements. - * - The 0 through P-1 elements of argv are the same. - * - The P element of argv is a copy of the first len-1 characters of opt. - * This is a newly allocated '\0' terminated c string of length len. - * - The P+1 through (P+additional-2) elements of argv are newly allocated - * empty '\0' terminated c strings of size len. - * - The last element at (P+additional-1) of argv is NULL. - * - All allocations are pushed back onto allocated. + * Inserts a copy of element into the front of the arguments list. + * Preconditions: element is non-null and 0 terminated. + */ + virtual void pushFrontArgument(const char* element) = 0; + + /** + * Inserts a copy of element into the back of the arguments list. + * Preconditions: element is non-null and 0 terminated. + */ + virtual void pushBackArgument(const char* element) = 0; + + /** Removes the front of the arguments list.*/ + virtual void popFrontArgument() = 0; + + /** Adds a new preemption to the arguments list. */ + virtual void pushBackPreemption(const char* element) = 0; + + /** + * Moves all of the preemptions into the front of the arguments + * list. */ - void extend(int& argc, char**& argv, const char* opt, - std::vector<char*>& allocated); + virtual void movePreemptionsToArguments() = 0; - unsigned getIncrease() const; - size_t getLength() const; + /** Returns true iff there is a pending preemption.*/ + virtual bool hasPreemptions() const = 0; - private: - unsigned d_additional; - size_t d_length; -}; +};/* class ArgumentExtender */ }/* CVC4::options namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__OPTIONS__PREMPT_GET_OPTION_H */ +#endif /* __CVC4__OPTIONS__ARGUMENT_EXTENDER_H */ diff --git a/src/options/argument_extender_implementation.cpp b/src/options/argument_extender_implementation.cpp new file mode 100644 index 000000000..0c23434c4 --- /dev/null +++ b/src/options/argument_extender_implementation.cpp @@ -0,0 +1,114 @@ +/********************* */ +/*! \file argument_extender_implementation.cpp + ** \verbatim + ** Top contributors (to current version): + ** Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility class for parsing commandline options. + ** + ** Utility class for parsing commandline options. + **/ + +#include "options/argument_extender_implementation.h" + +#include <cstdlib> +#include <cstring> +#include <list> + +#include "base/cvc4_assert.h" +#include "base/output.h" +#include "options/argument_extender.h" + +namespace CVC4 { +namespace options { + +ArgumentExtenderImplementation::ArgumentExtenderImplementation() + : d_allocated() + , d_preemptions() + , d_arguments() +{ +} + +ArgumentExtenderImplementation::~ArgumentExtenderImplementation(){ + for(CharPointerList::iterator i = d_allocated.begin(), + iend = d_allocated.end(); i != iend; ++i) { + char* current = *i; + Debug("options") << "~ArgumentExtenderImplementation " << current + << std::endl; + free(current); + } + d_allocated.clear(); +} + +size_t ArgumentExtenderImplementation::numArguments() const { + return d_arguments.size(); +} + +char* ArgumentExtenderImplementation::allocateCopy(const char* element) { + Assert(element != NULL); + + char* duplicate = strdup(element); + Assert(duplicate != NULL); + d_allocated.push_back(duplicate); + return duplicate; +} + +bool ArgumentExtenderImplementation::hasPreemptions() const { + return !d_preemptions.empty(); +} + +void ArgumentExtenderImplementation::pushBackPreemption(const char* element) { + d_preemptions.push_back(allocateCopy(element)); +} + +void ArgumentExtenderImplementation::movePreemptionsToArguments() { + d_arguments.splice(d_arguments.begin(), d_preemptions); +} + +void ArgumentExtenderImplementation::popFrontArgument() { + Assert(!d_arguments.empty()); + Debug("options") << "ArgumentExtenderImplementation::popFrontArgument " + << d_arguments.front() << std::endl; + d_arguments.pop_front(); +} + +void ArgumentExtenderImplementation::pushFrontArgument(const char* element) { + d_arguments.push_front(allocateCopy(element)); +} + +void ArgumentExtenderImplementation::pushBackArgument(const char* element) { + d_arguments.push_back(allocateCopy(element)); +} + +void ArgumentExtenderImplementation::getArguments(int* argc, char*** argv) + const { + Assert(argc != NULL); + Assert(argv != NULL); + + *argc = numArguments(); + *argv = copyArguments(); +} + +char** ArgumentExtenderImplementation::copyArguments() const { + int size = numArguments(); + Assert(size >= 0); + + char** array = (char**) malloc( sizeof(char*) * size ); + Assert(array != NULL); + int position = 0; + for(std::list< char* >::const_iterator i = d_arguments.begin(), + iend = d_arguments.end(); i != iend; ++i, ++position) { + char* at_position = *i; + array[position] = at_position; + } + + return array; +} + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ diff --git a/src/options/argument_extender_implementation.h b/src/options/argument_extender_implementation.h new file mode 100644 index 000000000..e948132d7 --- /dev/null +++ b/src/options/argument_extender_implementation.h @@ -0,0 +1,115 @@ +/********************* */ +/*! \file argument_extender_implementation.h + ** \verbatim + ** Top contributors (to current version): + ** Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility class for extending commandline options. + ** + ** Utility class for extending commandline options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H +#define __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H + +#include <cstddef> +#include <list> + +#include "options/argument_extender.h" + +namespace CVC4 { +namespace options { + +/** + * Utility class for implementing command line options parsing for the + * Options class. This allows for adding preemption arguments. + * Preemptions are processed immediately after the current argument. + */ +class ArgumentExtenderImplementation : public ArgumentExtender { + public: + /** Constructs a new empty ArgumentExtender.*/ + ArgumentExtenderImplementation(); + + /** Destroys an ArgumentExtender and frees its associated memory.*/ + ~ArgumentExtenderImplementation(); + + /** + * This creates a copy of the current arguments list as a new array. + * The new array is stored in argv. The user of this function is + * expected to own the memory of the string array, but not the + * strings themselves. The length of the new array is + * numArguments() and is stored in argc. + * + * Preconditions: + * - argc and argv are non-null. + */ + void getArguments(int* argc, char*** argv) const; + + /** Returns the number of arguments that are . */ + size_t numArguments() const; + + /** + * Inserts a copy of element into the front of the arguments list. + * Preconditions: element is non-null and 0 terminated. + */ + void pushFrontArgument(const char* element); + + /** + * Inserts a copy of element into the back of the arguments list. + * Preconditions: element is non-null and 0 terminated. + */ + void pushBackArgument(const char* element); + + /** Removes the front of the arguments list.*/ + void popFrontArgument(); + + /** Adds a new preemption to the arguments list. */ + void pushBackPreemption(const char* element); + + /** + * Moves all of the preemptions into the front of the arguments + * list. + */ + void movePreemptionsToArguments(); + + /** Returns true iff there is a pending preemption.*/ + bool hasPreemptions() const; + +private: + + typedef std::list< char* > CharPointerList; + + /** Creates of copy of the arugments list.*/ + char** copyArguments() const; + + /** Allocates a copy and stores a copy in d_allocated.*/ + char* allocateCopy(const char* element); + + /** Contains a copy of the allocated strings.*/ + CharPointerList d_allocated; + + /** + * A list of all of the preempted arguments. All of these pointers + * in this list should be contained in d_allocated. + */ + CharPointerList d_preemptions; + + /** + * A list of all of the arguments. All of these pointers in this + * list should be contained in d_allocated. + */ + CharPointerList d_arguments; + +};/* class ArgumentExtenderImplementation */ + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H */ diff --git a/src/options/arith_heuristic_pivot_rule.cpp b/src/options/arith_heuristic_pivot_rule.cpp index ff5f2102a..15c340aa8 100644 --- a/src/options/arith_heuristic_pivot_rule.cpp +++ b/src/options/arith_heuristic_pivot_rule.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file arith_heuristic_pivot_rule.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/arith_heuristic_pivot_rule.h b/src/options/arith_heuristic_pivot_rule.h index e44b8105b..9048cb92e 100644 --- a/src/options/arith_heuristic_pivot_rule.h +++ b/src/options/arith_heuristic_pivot_rule.h @@ -1,13 +1,13 @@ /********************* */ /*! \file arith_heuristic_pivot_rule.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/arith_options b/src/options/arith_options index 9f4003004..f38e377ba 100644 --- a/src/options/arith_options +++ b/src/options/arith_options @@ -162,4 +162,7 @@ option pbRewrites --pb-rewrites bool :default false option pbRewriteThreshold --pb-rewrite-threshold int :default 256 threshold of number of pseudoboolean variables to have before doing rewrites +option sNormInferEq --snorm-infer-eq bool :default false + infer equalities based on Shostak normalization + endmodule diff --git a/src/options/arith_propagation_mode.cpp b/src/options/arith_propagation_mode.cpp index 7f18a0356..5baf0b832 100644 --- a/src/options/arith_propagation_mode.cpp +++ b/src/options/arith_propagation_mode.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file arith_propagation_mode.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/arith_propagation_mode.h b/src/options/arith_propagation_mode.h index fa89496f0..dc4b80372 100644 --- a/src/options/arith_propagation_mode.h +++ b/src/options/arith_propagation_mode.h @@ -1,13 +1,13 @@ /********************* */ /*! \file arith_propagation_mode.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/arith_unate_lemma_mode.cpp b/src/options/arith_unate_lemma_mode.cpp index 55fd8a01f..9b683f4c1 100644 --- a/src/options/arith_unate_lemma_mode.cpp +++ b/src/options/arith_unate_lemma_mode.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file arith_unate_lemma_mode.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/arith_unate_lemma_mode.h b/src/options/arith_unate_lemma_mode.h index 5e1362bcb..39664d3aa 100644 --- a/src/options/arith_unate_lemma_mode.h +++ b/src/options/arith_unate_lemma_mode.h @@ -1,13 +1,13 @@ /********************* */ /*! \file arith_unate_lemma_mode.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h index d4137255e..0345f9e10 100644 --- a/src/options/base_handlers.h +++ b/src/options/base_handlers.h @@ -1,13 +1,13 @@ /********************* */ /*! \file base_handlers.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Kshitij Bansal - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/base_options_template.cpp b/src/options/base_options_template.cpp index 2c3d717fa..bdcef6029 100644 --- a/src/options/base_options_template.cpp +++ b/src/options/base_options_template.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file base_options_template.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Contains code for handling command-line options. ** diff --git a/src/options/base_options_template.h b/src/options/base_options_template.h index c8c02ecaa..486b793d0 100644 --- a/src/options/base_options_template.h +++ b/src/options/base_options_template.h @@ -1,13 +1,13 @@ /********************* */ /*! \file base_options_template.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Contains code for handling command-line options. ** diff --git a/src/options/boolean_term_conversion_mode.cpp b/src/options/boolean_term_conversion_mode.cpp index d1466ae14..0673718bb 100644 --- a/src/options/boolean_term_conversion_mode.cpp +++ b/src/options/boolean_term_conversion_mode.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file boolean_term_conversion_mode.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h index 81a0c661a..f2f4a51af 100644 --- a/src/options/boolean_term_conversion_mode.h +++ b/src/options/boolean_term_conversion_mode.h @@ -1,13 +1,13 @@ /********************* */ /*! \file boolean_term_conversion_mode.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp index 99ceb41ee..9cf47fe33 100644 --- a/src/options/bv_bitblast_mode.cpp +++ b/src/options/bv_bitblast_mode.cpp @@ -1,13 +1,13 @@ /********************* */ -/*! \file bitblast_mode.cpp +/*! \file bv_bitblast_mode.cpp ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Liana Hadarean, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Bitblast modes for bit-vector solver. ** diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h index f36021478..4c8c4f626 100644 --- a/src/options/bv_bitblast_mode.h +++ b/src/options/bv_bitblast_mode.h @@ -1,13 +1,13 @@ /********************* */ -/*! \file bitblast_mode.h +/*! \file bv_bitblast_mode.h ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Liana Hadarean, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Bitblasting modes for bit-vector solver. ** diff --git a/src/options/bv_options b/src/options/bv_options index c1180dba3..8edc809e3 100644 --- a/src/options/bv_options +++ b/src/options/bv_options @@ -11,14 +11,14 @@ option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :han choose bitblasting mode, see --bitblast=help # Options for eager bit-blasting - + option bitvectorAig --bitblast-aig bool :default false :predicate abcEnabledBuild setBitblastAig :read-write bitblast by first converting to AIG (implies --bitblast=eager) expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate abcEnabledBuild :read-write :link --bitblast-aig :link-smt bitblast-aig abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") # Options for lazy bit-blasting -option bitvectorPropagate --bv-propagate bool :default true :read-write +option bitvectorPropagate --bv-propagate bool :default true :read-write use bit-vector propagation in the bit-blaster option bitvectorEqualitySolver --bv-eq-solver bool :default true :read-write @@ -28,18 +28,18 @@ option bitvectorEqualitySlicer --bv-eq-slicer=MODE CVC4::theory::bv::BvSlicerMod turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy) -option bitvectorInequalitySolver --bv-inequality-solver bool :default true :read-write +option bitvectorInequalitySolver --bv-inequality-solver bool :default true :read-write turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy) option bitvectorAlgebraicSolver --bv-algebraic-solver bool :default true :read-write turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy) - + expert-option bitvectorAlgebraicBudget --bv-algebraic-budget unsigned :default 1500 :read-write :link --bv-algebraic-solver :link-smt bv-algebraic-solver the budget allowed for the algebraic solver in number of SAT conflicts # General options -option bitvectorToBool --bv-to-bool bool :default false :read-write +option bitvectorToBool --bv-to-bool bool :default false :read-write lift bit-vectors of size 1 to booleans when possible option bitvectorDivByZeroConst --bv-div-zero-const bool :default false :read-write @@ -47,11 +47,11 @@ option bitvectorDivByZeroConst --bv-div-zero-const bool :default false :read-wri expert-option bvExtractArithRewrite --bv-extract-arith bool :default false :read-write enable rewrite pushing extract [i:0] over arithmetic operations (can blow up) - + expert-option bvAbstraction --bv-abstraction bool :default false :read-write - mcm benchmark abstraction + mcm benchmark abstraction -expert-option skolemizeArguments --bv-skolemize bool :default false :read-write +expert-option skolemizeArguments --bv-skolemize bool :default false :read-write skolemize arguments for bv abstraction (only does something if --bv-abstraction is on) expert-option bvNumFunc --bv-num-func=NUM unsigned :default 1 @@ -62,8 +62,8 @@ expert-option bvEagerExplanations --bv-eager-explanations bool :default false :r expert-option bitvectorQuickXplain --bv-quick-xplain bool :default false minimize bv conflicts using the QuickXplain algorithm - + expert-option bvIntroducePow2 --bv-intro-pow2 bool :default false introduce bitvector powers of two as a preprocessing pass - + endmodule diff --git a/src/options/datatypes_options b/src/options/datatypes_options index b44a36e2a..e9578f8d7 100644 --- a/src/options/datatypes_options +++ b/src/options/datatypes_options @@ -23,5 +23,9 @@ option cdtBisimilar --cdt-bisimilar bool :default true do bisimilarity check for co-datatypes option dtCyclic --dt-cyclic bool :default true do cyclicity check for datatypes +option dtInferAsLemmas --dt-infer-as-lemmas bool :default false + always send lemmas out instead of making internal inferences +#option dtRExplainLemmas --dt-rexplain-lemmas bool :default true +# regression explanations for datatype lemmas endmodule diff --git a/src/options/decision_mode.cpp b/src/options/decision_mode.cpp index 0aeae1baa..3a93b0274 100644 --- a/src/options/decision_mode.cpp +++ b/src/options/decision_mode.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file decision_mode.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/decision_mode.h b/src/options/decision_mode.h index 420d00b4c..efc6ca213 100644 --- a/src/options/decision_mode.h +++ b/src/options/decision_mode.h @@ -1,13 +1,13 @@ /********************* */ /*! \file decision_mode.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Kshitij Bansal - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Kshitij Bansal, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/decision_weight.h b/src/options/decision_weight.h index 89ebe8a21..6d01b18cb 100644 --- a/src/options/decision_weight.h +++ b/src/options/decision_weight.h @@ -1,13 +1,13 @@ /********************* */ /*! \file decision_weight.h ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Kshitij Bansal, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Rewriter attributes ** diff --git a/src/options/didyoumean.cpp b/src/options/didyoumean.cpp index 1066c7a1f..d874c7bc7 100644 --- a/src/options/didyoumean.cpp +++ b/src/options/didyoumean.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file didyoumean.cpp ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Kshitij Bansal, Tim King, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief did-you-mean style suggestions ** diff --git a/src/options/didyoumean.h b/src/options/didyoumean.h index 2615f4d0a..71a12e6fc 100644 --- a/src/options/didyoumean.h +++ b/src/options/didyoumean.h @@ -1,13 +1,13 @@ /********************* */ /*! \file didyoumean.h ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Kshitij Bansal, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief did-you-mean style suggestions. ** diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp index af3daa689..8117b57ac 100644 --- a/src/options/didyoumean_test.cpp +++ b/src/options/didyoumean_test.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file didyoumean_test.cpp ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Kshitij Bansal, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/language.cpp b/src/options/language.cpp index 7558c6927..665089e45 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file language.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Definition of input and output languages ** diff --git a/src/options/language.h b/src/options/language.h index 9191a1d59..00328e4ab 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -1,13 +1,13 @@ /********************* */ /*! \file language.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Francois Bobot, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Definition of input and output languages ** diff --git a/src/options/main_options b/src/options/main_options index 7ec4fedb3..0fa799df2 100644 --- a/src/options/main_options +++ b/src/options/main_options @@ -54,8 +54,8 @@ option segvSpin --segv-spin bool :default false spin on segfault/other crash waiting for gdb undocumented-alias --segv-nospin = --no-segv-spin -expert-option tearDownIncremental : --tear-down-incremental int :default 0 - implement PUSH/POP/multi-query by destroying and recreating SmtEngine +expert-option tearDownIncremental : --tear-down-incremental=N int :default 0 + implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries expert-option waitToJoin --wait-to-join bool :default true wait for other threads to join before quitting diff --git a/src/options/mkoptions b/src/options/mkoptions index ad8d7033f..dd5575644 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -604,7 +604,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r for link in $links; do run_links="$run_links #line $lineno \"$kf\" - argumentExtender.extend(extra_argc, extra_argv, \"$link\", allocated);" + extender->pushBackPreemption(\"$link\");" done fi if [ -n "$smt_links" ]; then @@ -623,7 +623,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r for link in $links_alternate; do run_links_alternate="$run_links_alternate #line $lineno \"$kf\" - argumentExtender.extend(extra_argc, extra_argv, \"$link\", allocated);" + extender->pushBackPreemption(\"$link\");" done fi if [ -n "$notifications" ]; then @@ -657,7 +657,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o if [ "$type" = bool ]; then all_modules_option_handlers="${all_modules_option_handlers}${cases} #line $lineno \"$kf\" - assignBool(options::$internal, option, true);$run_links + options->assignBool(options::$internal, option, true);$run_links break; " elif [ -n "$expect_arg" -a "$internal" != - ]; then @@ -690,7 +690,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options }" all_modules_option_handlers="${all_modules_option_handlers}${cases} #line $lineno \"$kf\" - assign(options::$internal, option, optionarg);$run_links + options->assign(options::$internal, option, optionarg);$run_links break; " elif [ -n "$expect_arg" ]; then @@ -733,7 +733,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options if [ "$type" = bool ]; then all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate} #line $lineno \"$kf\" - assignBool(options::$internal, option, false);$run_links_alternate + options->assignBool(options::$internal, option, false);$run_links_alternate break; " else @@ -1013,12 +1013,12 @@ function handle_alias { fi links="$links #line $lineno \"$kf\" - argumentExtender.extend(extra_argc, extra_argv, \"$linkopt\", allocated);" + extender->pushBackPreemption(\"$linkopt\");" if [ "$linkarg" ]; then # include also the arg links="$links #line $lineno \"$kf\" - argumentExtender.extend(extra_argc, extra_argv, optionarg.c_str(), allocated);" + extender->pushBackPreemption(optionarg.c_str());" fi shift done diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp index 4c92d056b..214f148aa 100644 --- a/src/options/open_ostream.cpp +++ b/src/options/open_ostream.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file open_ostream.cpp ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h index ab83427a9..6c00e7dd1 100644 --- a/src/options/open_ostream.h +++ b/src/options/open_ostream.h @@ -1,13 +1,13 @@ /********************* */ -/*! \file open_stream.h +/*! \file open_ostream.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/option_exception.h b/src/options/option_exception.h index c57414026..450eda988 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -1,13 +1,13 @@ /********************* */ /*! \file option_exception.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Options-related exceptions ** diff --git a/src/options/options.h b/src/options/options.h index 8fb52146f..33bd94e46 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -1,13 +1,13 @@ /********************* */ /*! \file options.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal + ** Top contributors (to current version): + ** Tim King, Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Global (command-line, set-option, ...) parameters for SMT. ** @@ -27,6 +27,7 @@ #include "base/listener.h" #include "base/modal_exception.h" #include "base/tls.h" +#include "options/argument_extender.h" #include "options/language.h" #include "options/printer_modes.h" #include "options/option_exception.h" @@ -314,12 +315,18 @@ public: static std::vector<std::string> suggestSmtOptions(const std::string& optionName) throw(); /** - * Initialize the options based on the given command-line arguments. - * The return value is what's left of the command line (that is, the - * non-option arguments). + * Initialize the Options object options based on the given + * command-line arguments given in argc and argv. The return value + * is what's left of the command line (that is, the non-option + * arguments). + * + * This function uses getopt_long() and is not thread safe. + * + * Preconditions: options and argv must be non-null. */ - std::vector<std::string> parseOptions(int argc, char* argv[]) - throw(OptionException); + static std::vector<std::string> parseOptions(Options* options, + int argc, char* argv[]) + throw(OptionException); /** * Get the setting for all options. @@ -528,6 +535,22 @@ public: /** Sends a std::flush to getOut(). */ void flushOut(); + private: + + /** + * Internal procedure for implementing the parseOptions function. + * Initializes the options object based on the given command-line + * arguments. This uses an ArgumentExtender containing the + * command-line arguments. Nonoptions are stored into nonoptions. + * + * This is not thread safe. + * + * Preconditions: options, extender and nonoptions are non-null. + */ + static void parseOptionsRecursive(Options* options, + options::ArgumentExtender* extender, + std::vector<std::string>* nonoptions) + throw(OptionException); };/* class Options */ }/* CVC4 namespace */ diff --git a/src/options/options_get_option_template.cpp b/src/options/options_get_option_template.cpp index b7e5433ee..d50644a5d 100644 --- a/src/options/options_get_option_template.cpp +++ b/src/options/options_get_option_template.cpp @@ -1,13 +1,13 @@ /********************* */ -/*! \file option_handler_get_option_template.cpp +/*! \file options_get_option_template.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Implementation of OptionsHandler::getOption. ** diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 1c48f4bb1..a2809bd67 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file options_handler.cpp ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Interface for custom handlers and predicates options. ** @@ -347,15 +347,21 @@ interleave \n\ const std::string OptionsHandler::s_triggerSelModeHelp = "\ Trigger selection modes currently supported by the --trigger-sel option:\n\ \n\ -default \n\ -+ Default, consider all subterms of quantified formulas for trigger selection.\n\ -\n\ -min \n\ +min | default \n\ + Consider only minimal subterms that meet criteria for triggers.\n\ \n\ max \n\ + Consider only maximal subterms that meet criteria for triggers. \n\ \n\ +all \n\ ++ Consider all subterms that meet criteria for triggers. \n\ +\n\ +min-s-max \n\ ++ Consider only minimal subterms that meet criteria for single triggers, maximal otherwise. \n\ +\n\ +min-s-all \n\ ++ Consider only minimal subterms that meet criteria for single triggers, all otherwise. \n\ +\n\ "; const std::string OptionsHandler::s_prenexQuantModeHelp = "\ Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ @@ -428,7 +434,7 @@ post \n\ "; const std::string OptionsHandler::s_macrosQuantHelp = "\ -Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ +Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ \n\ all \n\ + Infer definitions for functions, including those containing quantified formulas.\n\ @@ -441,6 +447,34 @@ ground-uf \n\ \n\ "; +const std::string OptionsHandler::s_quantDSplitHelp = "\ +Modes for quantifiers splitting, supported by --quant-dsplit-mode:\n\ +\n\ +none \n\ ++ Never split quantified formulas.\n\ +\n\ +default \n\ ++ Split quantified formulas over some finite datatypes when finite model finding is enabled.\n\ +\n\ +agg \n\ ++ Aggressively split quantified formulas.\n\ +\n\ +"; + +const std::string OptionsHandler::s_quantRepHelp = "\ +Modes for quantifiers representative selection, supported by --quant-rep-mode:\n\ +\n\ +ee \n\ ++ Let equality engine choose representatives.\n\ +\n\ +first (default) \n\ ++ Choose terms that appear first.\n\ +\n\ +depth \n\ ++ Choose terms that are of minimal depth.\n\ +\n\ +"; + theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) { if(optarg == "pre-full") { return theory::quantifiers::INST_WHEN_PRE_FULL; @@ -542,8 +576,6 @@ theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option, return theory::quantifiers::QCF_PROP_EQ; } else if(optarg == "partial") { return theory::quantifiers::QCF_PARTIAL; - } else if(optarg == "mc" ) { - return theory::quantifiers::QCF_MC; } else if(optarg == "help") { puts(s_qcfModeHelp.c_str()); exit(1); @@ -574,12 +606,18 @@ theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string } theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "default" || optarg == "all" ) { + if(optarg == "default") { return theory::quantifiers::TRIGGER_SEL_DEFAULT; } else if(optarg == "min") { return theory::quantifiers::TRIGGER_SEL_MIN; } else if(optarg == "max") { return theory::quantifiers::TRIGGER_SEL_MAX; + } else if(optarg == "min-s-max") { + return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX; + } else if(optarg == "min-s-all") { + return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL; + } else if(optarg == "all") { + return theory::quantifiers::TRIGGER_SEL_ALL; } else if(optarg == "help") { puts(s_triggerSelModeHelp.c_str()); exit(1); @@ -686,6 +724,37 @@ theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(std } } +theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none" ) { + return theory::quantifiers::QUANT_DSPLIT_MODE_NONE; + } else if(optarg == "default") { + return theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT; + } else if(optarg == "agg") { + return theory::quantifiers::QUANT_DSPLIT_MODE_AGG; + } else if(optarg == "help") { + puts(s_quantDSplitHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --quant-dsplit-mode: `") + + optarg + "'. Try --quant-dsplit-mode help."); + } +} + +theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none" ) { + return theory::quantifiers::QUANT_REP_MODE_EE; + } else if(optarg == "first" || optarg == "default") { + return theory::quantifiers::QUANT_REP_MODE_FIRST; + } else if(optarg == "depth") { + return theory::quantifiers::QUANT_REP_MODE_DEPTH; + } else if(optarg == "help") { + puts(s_quantRepHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --quant-rep-mode: `") + + optarg + "'. Try --quant-rep-mode help."); + } +} // theory/bv/options_handlers.h void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 9aa037004..baa6cea96 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -1,13 +1,13 @@ /********************* */ /*! \file options_handler.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Interface for custom handlers and predicates options. ** @@ -100,6 +100,8 @@ public: theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException); // theory/bv/options_handlers.h void abcEnabledBuild(std::string option, bool value) throw(OptionException); @@ -199,6 +201,8 @@ public: static const std::string s_iteLiftQuantHelp; static const std::string s_literalMatchHelp; static const std::string s_macrosQuantHelp; + static const std::string s_quantDSplitHelp; + static const std::string s_quantRepHelp; static const std::string s_mbqiModeHelp; static const std::string s_modelFormatHelp; static const std::string s_prenexQuantModeHelp; diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h index f033fd5ad..f33656eb1 100644 --- a/src/options/options_holder_template.h +++ b/src/options/options_holder_template.h @@ -1,13 +1,13 @@ /********************* */ /*! \file options_holder_template.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Global (command-line, set-option, ...) parameters for SMT ** diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 2e86c732e..8f3a63175 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file options_public_functions.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Definitions of public facing interface functions for Options. ** @@ -204,7 +204,7 @@ std::ostream* Options::getOut(){ } std::ostream* Options::getOutConst() const{ -#warning "Remove Options::getOutConst" + // #warning "Remove Options::getOutConst" return (*this)[options::out]; } diff --git a/src/options/options_set_option_template.cpp b/src/options/options_set_option_template.cpp index 04f3800f7..cc068f4e6 100644 --- a/src/options/options_set_option_template.cpp +++ b/src/options/options_set_option_template.cpp @@ -1,13 +1,13 @@ /********************* */ -/*! \file option_handler_set_option_template.cpp +/*! \file options_set_option_template.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Implementation of OptionsHandler::setOption. ** diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 51b2bea5e..f029dfd17 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file options_template.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal + ** Top contributors (to current version): + ** Tim King, Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Contains code for handling command-line options. ** @@ -53,13 +53,14 @@ extern int optreset; #include "base/output.h" #include "base/tls.h" #include "options/argument_extender.h" +#include "options/argument_extender_implementation.h" #include "options/didyoumean.h" #include "options/language.h" #include "options/options_handler.h" ${include_all_option_headers} -#line 63 "${template}" +#line 64 "${template}" #include "options/options_holder.h" #include "cvc4autoconfig.h" @@ -67,7 +68,7 @@ ${include_all_option_headers} ${option_handler_includes} -#line 71 "${template}" +#line 72 "${template}" using namespace CVC4; using namespace CVC4::options; @@ -389,7 +390,7 @@ Options::registerSetReplayLogFilename( ${all_custom_handlers} -#line 393 "${template}" +#line 394 "${template}" #ifdef CVC4_DEBUG # define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true @@ -407,18 +408,18 @@ options::OptionsHolder::OptionsHolder() : ${all_modules_defaults} { } -#line 411 "${template}" +#line 412 "${template}" static const std::string mostCommonOptionsDescription = "\ Most commonly-used CVC4 options:${common_documentation}"; -#line 416 "${template}" +#line 417 "${template}" static const std::string optionsDescription = mostCommonOptionsDescription + "\n\ \n\ Additional CVC4 options:${remaining_documentation}"; -#line 422 "${template}" +#line 423 "${template}" static const std::string optionsFootnote = "\n\ [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ @@ -431,7 +432,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\ cvc4 | presentation | pl CVC4 presentation language\n\ smt1 | smtlib1 SMT-LIB format 1.2\n\ smt | smtlib | smt2 |\n\ - smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\ + smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ tptp TPTP format (cnf and fof)\n\ sygus SyGuS format\n\ @@ -442,7 +443,7 @@ Languages currently supported as arguments to the --output-lang option:\n\ cvc3 CVC3 presentation language\n\ smt1 | smtlib1 SMT-LIB format 1.2\n\ smt | smtlib | smt2 |\n\ - smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\ + smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ tptp TPTP format\n\ z3str SMT-LIB 2.0 with Z3-str string constraints\n\ @@ -497,7 +498,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options} { NULL, no_argument, NULL, '\0' } };/* cmdlineOptions */ -#line 501 "${template}" +#line 502 "${template}" // static void preemptGetopt(int& argc, char**& argv, const char* opt) { @@ -549,178 +550,196 @@ public: * The return value is what's left of the command line (that is, the * non-option arguments). */ -std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { - options::OptionsGuard guard(&s_current, this); +std::vector<std::string> Options::parseOptions(Options* options, + int argc, char* argv[]) + throw(OptionException) { - // Having this synonym simplifies the generation code in mkoptions. - options::OptionsHandler* handler = d_handler; + Assert(options != NULL); + Assert(argv != NULL); - const char *progName = main_argv[0]; + options::OptionsGuard guard(&s_current, options); - ArgumentExtender argumentExtender(s_preemptAdditional, s_maxoptlen); - std::vector<char*> allocated; + const char *progName = argv[0]; - Debug("options") << "main_argv == " << main_argv << std::endl; + // To debug options parsing, you may prefer to simply uncomment this + // and recompile. Debug flags have not been parsed yet so these have + // not been set. + //DebugChannel.on("options"); - // Reset getopt(), in the case of multiple calls to parseOptions(). - // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. - optind = 0; -#if HAVE_DECL_OPTRESET - optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this -#endif /* HAVE_DECL_OPTRESET */ + Debug("options") << "Options::parseOptions == " << options << std::endl; + Debug("options") << "argv == " << argv << std::endl; - // find the base name of the program + // Find the base name of the program. const char *x = strrchr(progName, '/'); if(x != NULL) { progName = x + 1; } - d_holder->binary_name = std::string(progName); + options->d_holder->binary_name = std::string(progName); + + ArgumentExtender* argumentExtender = new ArgumentExtenderImplementation(); + for(int position = 1; position < argc; position++) { + argumentExtender->pushBackArgument(argv[position]); + } + + std::vector<std::string> nonoptions; + parseOptionsRecursive(options, argumentExtender, &nonoptions); + if(Debug.isOn("options")){ + for(std::vector<std::string>::const_iterator i = nonoptions.begin(), + iend = nonoptions.end(); i != iend; ++i){ + Debug("options") << "nonoptions " << *i << std::endl; + } + } + + delete argumentExtender; + return nonoptions; +} + +void Options::parseOptionsRecursive(Options* options, + ArgumentExtender* extender, + std::vector<std::string>* nonoptions) + throw(OptionException) { + + int argc; + char** argv; + + extender->movePreemptionsToArguments(); + extender->pushFrontArgument(""); + extender->getArguments(&argc, &argv); + + if(Debug.isOn("options")) { + Debug("options") << "starting a new parseOptionsRecursive with " + << argc << " arguments" << std::endl; + for( int i = 0; i < argc ; i++ ){ + Assert(argv[i] != NULL); + Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl; + } + } - int extra_argc = 1; - char **extra_argv = (char**) malloc(2 * sizeof(char*)); - extra_argv[0] = NULL; - extra_argv[1] = NULL; + // Having this synonym simplifies the generation code in mkoptions. + options::OptionsHandler* handler = options->d_handler; + options::OptionsHolder* holder = options->d_holder; - int extra_optind = 0, main_optind = 0; + // Reset getopt(), in the case of multiple calls to parseOptions(). + // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. + optind = 0; +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this +#endif /* HAVE_DECL_OPTRESET */ + + + int main_optind = 0; int old_optind; - int *optind_ref = &main_optind; - char** argv = main_argv; - std::vector<std::string> nonOptions; + while(true) { // Repeat Forever + + if(extender->hasPreemptions()){ + // Stop this round of parsing. We now parse recursively + // to start on a new character array for argv. + parseOptionsRecursive(options, extender, nonoptions); + break; + } - for(;;) { - int c = -1; optopt = 0; std::string option, optionarg; - Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind - << ", extra_argc == " << extra_argc << std::endl; - if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) { -#if HAVE_DECL_OPTRESET - if(optind_ref != &extra_optind) { - optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this - } -#endif /* HAVE_DECL_OPTRESET */ - old_optind = optind = extra_optind; - optind_ref = &extra_optind; - argv = extra_argv; - Debug("preemptGetopt") << "in preempt code, next arg is " - << extra_argv[optind == 0 ? 1 : optind] - << std::endl; - if(extra_argv[extra_optind == 0 ? 1 : extra_optind][0] != '-') { - InternalError( - "preempted args cannot give non-options command-line args (found `%s')", - extra_argv[extra_optind == 0 ? 1 : extra_optind]); - } - c = getopt_long(extra_argc, extra_argv, - "+:${all_modules_short_options}", - cmdlineOptions, NULL); - Debug("preemptGetopt") << "in preempt code" - << ", c == " << c << " (`" << char(c) << "')" - << " optind == " << optind << std::endl; - if(optopt == 0 || - ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) { - // long option - option = argv[old_optind == 0 ? 1 : old_optind]; - optionarg = (optarg == NULL) ? "" : optarg; - } else { - // short option - option = std::string("-") + char(optopt); - optionarg = (optarg == NULL) ? "" : optarg; - } - if(optind >= extra_argc) { - Debug("preemptGetopt") << "-- no more preempt args" << std::endl; - unsigned i = 1; - while(extra_argv[i] != NULL && extra_argv[i][0] != '\0') { - extra_argv[i][0] = '\0'; - ++i; - } - extra_argc = 1; - extra_optind = 0; - } else { - Debug("preemptGetopt") << "-- more preempt args" << std::endl; - extra_optind = optind; - } + + optind = main_optind; + old_optind = main_optind; + //optind_ref = &main_optind; + //argv = main_argv; + + // If we encounter an element that is not at zero and does not start + // with a "-", this is a non-option. We consume this element as a + // non-option. + if (main_optind > 0 && main_optind < argc && + argv[main_optind][0] != '-') { + Debug("options") << "enqueueing " << argv[main_optind] + << " as a non-option." << std::endl; + nonoptions->push_back(argv[main_optind]); + ++main_optind; + extender->popFrontArgument(); + continue; } - if(c == -1) { -#if HAVE_DECL_OPTRESET - if(optind_ref != &main_optind) { - optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this - } -#endif /* HAVE_DECL_OPTRESET */ - old_optind = optind = main_optind; - optind_ref = &main_optind; - argv = main_argv; - if(main_optind < argc && main_argv[main_optind][0] != '-') { - do { - if(main_optind != 0) { - nonOptions.push_back(main_argv[main_optind]); - } - ++main_optind; - } while(main_optind < argc && main_argv[main_optind][0] != '-'); - continue; - } - Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; -#if defined(__MINGW32__) || defined(__MINGW64__) - if(optreset == 1 && optind > 1) { - // on mingw, optreset will reset the optind, so we have to - // manually advance argc, argv - main_argv[optind - 1] = main_argv[0]; - argv = main_argv += optind - 1; - argc -= optind - 1; - old_optind = optind = main_optind = 1; - if(argc > 0) { - Debug("options") << "looking at : " << argv[0] << std::endl; - } - /*c = getopt_long(argc, main_argv, + + + Debug("options") << "[ before, main_optind == " << main_optind << " ]" + << std::endl; + Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; + Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]" + << std::endl; + int c = getopt_long(argc, argv, "+:${all_modules_short_options}", cmdlineOptions, NULL); - Debug("options") << "pre-emptory c is " << c << " (" << char(c) << ")" << std::endl; - Debug("options") << "optind was reset to " << optind << std::endl; - optind = main_optind; - Debug("options") << "I restored optind to " << optind << std::endl;*/ - } -#endif /* __MINGW32__ || __MINGW64__ */ - Debug("options") << "[ argc == " << argc - << ", main_argv == " << main_argv << " ]" << std::endl; - c = getopt_long(argc, main_argv, - "+:${all_modules_short_options}", - cmdlineOptions, NULL); - main_optind = optind; - Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" - << std::endl; - Debug("options") << "[ next option will be at pos: " << optind << " ]" - << std::endl; - if(c == -1) { + + while(main_optind < optind) { + main_optind++; + extender->popFrontArgument(); + } + + Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" + << "[ next option will be at pos: " << optind << " ]" + << std::endl; + + // The initial getopt_long call should always determine that argv[0] + // is not an option and returns -1. We always manually advance beyond + // this element. + // + // We have to reinitialize optind to 0 instead of 1 as we need to support + // changing the argv array passed to getopt. + // This is needed as are using GNU extensions. + // From: http://man7.org/linux/man-pages/man3/getopt.3.html + // A program that scans multiple argument vectors, or rescans the same + // vector more than once, and wants to make use of GNU extensions such + // as '+' and '-' at the start of optstring, or changes the value of + // POSIXLY_CORRECT between scans, must reinitialize getopt() by + // resetting optind to 0, rather than the traditional value of 1. + // (Resetting to 0 forces the invocation of an internal initialization + // routine that rechecks POSIXLY_CORRECT and checks for GNU extensions + // in optstring.) + if ( old_optind == 0 && c == -1 ) { + Assert(main_optind > 0); + continue; + } + + if ( c == -1 ) { + if(Debug.isOn("options")) { Debug("options") << "done with option parsing" << std::endl; - break; + for(int index = optind; index < argc; ++index) { + Debug("options") << "remaining " << argv[index] << std::endl; + } } - option = argv[old_optind == 0 ? 1 : old_optind]; - optionarg = (optarg == NULL) ? "" : optarg; + break; } + option = argv[old_optind == 0 ? 1 : old_optind]; + optionarg = (optarg == NULL) ? "" : optarg; + Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "'), " << option << std::endl; switch(c) { ${all_modules_option_handlers} -#line 709 "${template}" +#line 722 "${template}" case ':': // This can be a long or short option, and the way to get at the // name of it is different. - throw OptionException(std::string("option `") + option + "' missing its required argument"); + throw OptionException(std::string("option `") + option + + "' missing its required argument"); case '?': default: - if( ( optopt == 0 || ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} ) ) && - !strncmp(argv[optind - 1], "--thread", 8) && - strlen(argv[optind - 1]) > 8 ) { + if( ( optopt == 0 || + ( optopt >= ${long_option_value_begin} && + optopt <= ${long_option_value_end} ) + ) && !strncmp(argv[optind - 1], "--thread", 8) && + strlen(argv[optind - 1]) > 8 ) + { if(! isdigit(argv[optind - 1][8])) { throw OptionException(formatThreadOptionException(option)); } - std::vector<std::string>& threadArgv = d_holder->threadArgv; + std::vector<std::string>& threadArgv = holder->threadArgv; char *end; long tnum = strtol(argv[optind - 1] + 8, &end, 10); if(tnum < 0 || (*end != '\0' && *end != '=')) { @@ -734,23 +753,24 @@ ${all_modules_option_handlers} } if(*end == '\0') { // e.g., we have --thread0 "foo" if(argc <= optind) { - throw OptionException(std::string("option `") + option - + "' missing its required argument"); + throw OptionException(std::string("option `") + option + + "' missing its required argument"); } Debug("options") << "thread " << tnum << " gets option " << argv[optind] << std::endl; - threadArgv[tnum] += argv[(*optind_ref)++]; + threadArgv[tnum] += argv[main_optind]; + main_optind++; } else { // e.g., we have --thread0="foo" if(end[1] == '\0') { throw OptionException(std::string("option `") + option + "' missing its required argument"); } - Debug("options") << "thread " << tnum << " gets option " << (end + 1) - << std::endl; + Debug("options") << "thread " << tnum << " gets option " + << (end + 1) << std::endl; threadArgv[tnum] += end + 1; } - Debug("options") << "thread " << tnum << " now has " << threadArgv[tnum] - << std::endl; + Debug("options") << "thread " << tnum << " now has " + << threadArgv[tnum] << std::endl; break; } @@ -759,19 +779,10 @@ ${all_modules_option_handlers} } } - Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl; - - free(extra_argv); - for(std::vector<char*>::iterator i = allocated.begin(), iend = allocated.end(); - i != iend; ++i) - { - char* current = *i; - #warning "TODO: Unit tests fail if garbage collection is done here." - //free(current); - } - allocated.clear(); + Debug("options") << "got " << nonoptions->size() + << " non-option arguments." << std::endl; - return nonOptions; + free(argv); } std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() { @@ -787,7 +798,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th static const char* smtOptions[] = { ${all_modules_smt_options}, -#line 790 "${template}" +#line 800 "${template}" NULL };/* smtOptions[] */ @@ -809,7 +820,7 @@ std::vector< std::vector<std::string> > Options::getOptions() const throw() { ${all_modules_get_options} -#line 813 "${template}" +#line 762 "${template}" return opts; } diff --git a/src/options/printer_modes.cpp b/src/options/printer_modes.cpp index b698ed07d..3ca311a96 100644 --- a/src/options/printer_modes.cpp +++ b/src/options/printer_modes.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file printer_modes.cpp ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h index 8ccceb13f..a05ca2470 100644 --- a/src/options/printer_modes.h +++ b/src/options/printer_modes.h @@ -1,13 +1,13 @@ /********************* */ /*! \file printer_modes.h ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp index e87f00d65..a58120974 100644 --- a/src/options/quantifiers_modes.cpp +++ b/src/options/quantifiers_modes.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file quantifiers_modes.cpp ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 540db38ec..5749da972 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -1,13 +1,13 @@ /********************* */ /*! \file quantifiers_modes.h ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** @@ -83,8 +83,6 @@ enum QcfMode { QCF_PROP_EQ, /** use qcf for conflicts, propagations and heuristic instantiations */ QCF_PARTIAL, - /** use qcf for model checking */ - QCF_MC, }; enum UserPatMode { @@ -107,6 +105,12 @@ enum TriggerSelMode { TRIGGER_SEL_MIN, /** only consider maximal terms for triggers */ TRIGGER_SEL_MAX, + /** consider minimal terms for single triggers, maximal for non-single */ + TRIGGER_SEL_MIN_SINGLE_MAX, + /** consider minimal terms for single triggers, all for non-single */ + TRIGGER_SEL_MIN_SINGLE_ALL, + /** consider all terms for triggers */ + TRIGGER_SEL_ALL, }; enum CVC4_PUBLIC PrenexQuantMode { @@ -163,6 +167,24 @@ enum MacrosQuantMode { MACROS_QUANT_MODE_GROUND_UF, }; +enum QuantDSplitMode { + /** never do quantifiers splitting */ + QUANT_DSPLIT_MODE_NONE, + /** default */ + QUANT_DSPLIT_MODE_DEFAULT, + /** do quantifiers splitting aggressively */ + QUANT_DSPLIT_MODE_AGG, +}; + +enum QuantRepMode { + /** let equality engine choose representatives */ + QUANT_REP_MODE_EE, + /** default, choose representatives that appear first */ + QUANT_REP_MODE_FIRST, + /** choose representatives that have minimal depth */ + QUANT_REP_MODE_DEPTH, +}; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index f5a6ee843..74b3011a6 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -37,11 +37,6 @@ option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false aggressive split quantified formulas that lead to variable eliminations option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false split ites with dt testers as conditions -# Whether to CNF quantifier bodies -# option cnfQuant --cnf-quant bool :default false -# apply CNF conversion to quantified formulas -option nnfQuant --nnf-quant bool :default true - apply NNF conversion to quantified formulas # Whether to pre-skolemize quantifier bodies. # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to # forall x. P( x ) => f( S( x ) ) = x @@ -57,6 +52,8 @@ option elimTautQuant --elim-taut-quant bool :default true eliminate tautological disjuncts of quantified formulas option purifyQuant --purify-quant bool :default false purify quantified formulas +option elimExtArithQuant --elim-ext-arith-quant bool :default true + eliminate extended arithmetic symbols in quantified formulas #### E-matching options @@ -67,9 +64,13 @@ option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default which ground terms to consider for instantiation option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching +option inferArithTriggerEq --infer-arith-trigger-eq bool :default false + infer equalities for trigger terms based on solving arithmetic equalities +option inferArithTriggerEqExp --infer-arith-trigger-eq-exp bool :default false + record explanations for inferArithTriggerEq -option smartTriggers --smart-triggers bool :default true - enable smart triggers +option strictTriggers --strict-triggers bool :default false + only instantiate quantifiers with user patterns based on triggers option relevantTriggers --relevant-triggers bool :default false prefer triggers that are more relevant based on SInE style analysis option relationalTriggers --relational-triggers bool :default false @@ -88,20 +89,26 @@ option multiTriggerPriority --multi-trigger-priority bool :default false only try multi triggers if single triggers give no instantiations option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerSelMode selection mode for triggers -option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "options/quantifiers_modes.h" :handler stringToUserPatMode +option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :read-write :include "options/quantifiers_modes.h" :handler stringToUserPatMode policy for handling user-provided patterns for quantifier instantiation option incrementTriggers --increment-triggers bool :default true generate additional triggers as needed during search option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "options/quantifiers_modes.h" :handler stringToInstWhenMode :predicate checkInstWhenMode when to apply instantiation +option instWhenStrictInterleave --inst-when-strict-interleave bool :default true :read-write + ensure theory combination and standard quantifier effort strategies take turns +option instWhenPhase --inst-when-phase=N int :read-write :default 2 :read-write + instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen +option instWhenTcFirst --inst-when-tc-first bool :default true :read-write + allow theory combination to happen once initially, before quantifier strategies are run option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) option instLevelInputOnly --inst-level-input-only bool :default true only input terms are assigned instantiation level zero -option internalReps --quant-internal-reps bool :default true - instantiate with representatives chosen by quantifiers engine +option quantRepMode --quant-rep-mode=MODE CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode + selection mode for representatives in quantifiers engine option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly @@ -167,6 +174,9 @@ option qcfAllConflict --qcf-all-conflict bool :read-write :default false option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed + +option instPropagate --inst-propagate bool :read-write :default false + internal propagation for instantiations for selecting relevant instances ### rewrite rules options @@ -200,6 +210,8 @@ option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50 number of ground terms to generate for model filtering option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false more aggressive merging for universal equality engine, introduces terms +option conjectureGenMaxDepth --conjecture-gen-max-depth=N int :default 3 + maximum depth of terms to consider for conjectures ### synthesis options @@ -283,6 +295,10 @@ option macrosQuant --macros-quant bool :read-write :default false perform quantifiers macro expansion option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "options/quantifiers_modes.h" :handler stringToMacrosQuantMode mode for quantifiers macro expansion +option quantDynamicSplit --quant-dsplit-mode=MODE CVC4::theory::quantifiers::QuantDSplitMode :read-write :default CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler stringToQuantDSplitMode + mode for dynamic quantifiers splitting +option quantAntiSkolem --quant-anti-skolem bool :read-write :default false + perform anti-skolemization for quantified formulas ### recursive function options diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp index f68adbb45..32d3d73ae 100644 --- a/src/options/set_language.cpp +++ b/src/options/set_language.cpp @@ -1,13 +1,13 @@ /********************* */ -/*! \file language.h +/*! \file set_language.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Definition of input and output languages ** diff --git a/src/options/set_language.h b/src/options/set_language.h index 53b0a6a63..c27bb5184 100644 --- a/src/options/set_language.h +++ b/src/options/set_language.h @@ -1,13 +1,13 @@ /********************* */ -/*! \file language.h +/*! \file set_language.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Definition of input and output languages ** diff --git a/src/options/sets_options b/src/options/sets_options index 67bed5fe7..be945e4c9 100644 --- a/src/options/sets_options +++ b/src/options/sets_options @@ -17,4 +17,12 @@ expert-option setsCare1 --sets-care1 bool :default false option setsPropFull --sets-prop-full bool :default true additional propagation at full effort +option setsAggRewrite --sets-agg-rewrite bool :default false + aggressive sets rewriting + +option setsGuessEmpty --sets-guess-empty int :default 0 + when to guess leaf nodes being empty (0...2 : most aggressive..least aggressive) + +option setsSlowLemmas --sets-slow-lemmas bool :default true + endmodule diff --git a/src/options/simplification_mode.cpp b/src/options/simplification_mode.cpp index ab7851ef9..7189dacd1 100644 --- a/src/options/simplification_mode.cpp +++ b/src/options/simplification_mode.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file simplification_mode.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/simplification_mode.h b/src/options/simplification_mode.h index dd02ada5c..d1170f9ad 100644 --- a/src/options/simplification_mode.h +++ b/src/options/simplification_mode.h @@ -1,13 +1,13 @@ /********************* */ /*! \file simplification_mode.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/options/strings_options b/src/options/strings_options index 65c293dbc..5c991a1bb 100644 --- a/src/options/strings_options +++ b/src/options/strings_options @@ -53,6 +53,18 @@ option stringInferSym strings-infer-sym --strings-infer-sym bool :default true strings split on empty string option stringEagerLen strings-eager-len --strings-eager-len bool :default true strings eager length lemmas +option stringCheckEntailLen strings-check-entail-len --strings-check-entail-len bool :default true + check entailment between length terms to reduce splitting +option stringProcessLoop strings-process-loop --strings-process-loop bool :default true + reduce looping word equations to regular expressions +option stringAbortLoop strings-abort-loop --strings-abort-loop bool :default false + abort when a looping word equation is encountered +option stringInferAsLemmas strings-infer-as-lemmas --strings-infer-as-lemmas bool :default false + always send lemmas out instead of making internal inferences +option stringRExplainLemmas strings-rexplain-lemmas --strings-rexplain-lemmas bool :default true + regression explanations for string lemmas +option stringMinPrefixExplain strings-min-prefix-explain --strings-min-prefix-explain bool :default true + minimize explanations for prefix of normal forms in strings endmodule diff --git a/src/options/theoryof_mode.cpp b/src/options/theoryof_mode.cpp index c05f97ede..cf7178042 100644 --- a/src/options/theoryof_mode.cpp +++ b/src/options/theoryof_mode.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file theoryof_mode.cpp + ** \verbatim + ** Top contributors (to current version): + ** Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "options/theoryof_mode.h" diff --git a/src/options/theoryof_mode.h b/src/options/theoryof_mode.h index 5a8723738..98f05a131 100644 --- a/src/options/theoryof_mode.h +++ b/src/options/theoryof_mode.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theoryof_mode.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Option selection for theoryOf() operation ** diff --git a/src/options/ufss_mode.h b/src/options/ufss_mode.h index 6ce05d46a..4a4b8b4c1 100644 --- a/src/options/ufss_mode.h +++ b/src/options/ufss_mode.h @@ -1,13 +1,13 @@ /********************* */ /*! \file ufss_mode.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Custom handlers and predicates for TheoryUF options ** |