| Age | Commit message (Collapse) | Author |
|---|
|
Before, cvc5 was returning with `--parse-only` before the code could
reach the code responsible for dumping the raw benchmark. This moves the
check for `--parse-only` to the appropriate place and updates the
`run_regression.py` script to use `--parse-only`.
|
|
This PR refactors the generation of the command line help for sphinx to a function, just like all the other code generation methods.
|
|
Printing the original benchmark is simple, as it is exactly the commands we execute.
This removes the previous code from SmtEngine, which is currently broken.
|
|
This PR refactors the code for options parsing.
|
|
This PR refactors how we generate the command-line help message.
|
|
When using --editline, our interactive_shell_black unit test was not
working because the unit test was redirecting std::cin and std::cout
to std::stringstreams, which does not work with Editline. This commit
refactors our InteractiveShell class to explicitly take the input and
output streams as arguments, which fixes the issue because we do not use
Editline for input streams that are not std::cin. Additionally, the
commit updates the unit test to use SMT-LIB syntax instead of the
deprecated CVC language.
|
|
This PR does some cleanup in the driver and the options. It removes the now obsolete public attribute that allowed using the options in the driver, and removes a bunch of includes from the driver that are no longer necessary.
|
|
This changes our implementation of GetModelCommand so that we use the API to print the model.
It simplifies smt::Model so that this is a pretty printing utility, and not a layer on top of TheoryModel.
It adds getModel as an API method for returning the string representation of the model, analogous to our current support for getProof.
This eliminates the last call to getSmtEngine() from the command layer.
|
|
This makes the `driver::totalTime` statistic a `TimerStat`. This eliminates the need to obtain the overall runtime in the driver and write it to the statistics towards the end of the runtime. This not only eliminates some code in the driver, but also gets rid of the call to `getSmtEngine()` that goes around the API.
One disclaimer: The statistics output changes from seconds as a double (i.e. `1.234`) to milliseconds (i.e. `1234ms`).
|
|
This PR refactors the driver to no longer directly access the Options object, but instead use Solver::getOption() or Solver::getOptionInfo().
|
|
This PR simplifies how we store the current input file name and handle setting and getting it.
It is now an option, that can also be set and get via setInfo() and getInfo().
|
|
This PR adds a new API function Solver::getDriverOptions() which is used to communicate special options that (a) can not be properly communicated via getOption() and (b) need to be available in the driver (in a type-safe manner).
As of now, this concerns the input stream and output streams.
Furthermore, this PR refactors the driver to obtain them via the driver options instead of using the (deprecated) Solver::getOptions() method.
|
|
This PR moves the first chunk of code in the driver to use the proper options API for the language options. It is now handled as a string.
|
|
This fixes a minor issue where models should be dumped for "not entailed" results. This fix was required when preparing the submission to CASC this year.
|
|
This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.
|
|
This PR moves the code responsible for parsing the command line to the main folder. Note that the options themselves, and converting strings to the options proper types, calling predicates etc, stays in libcvc5. The PR also slightly refactors the options code to get rid of the assign_* functions.
|
|
Fix competition mode by accessing options in the correct way in main functions.
|
|
This PR removes explicit ownership of the options object from the main function and replaces it by an api::Solver object. To achieve this, it does a number of minor changes:
- api::Solver not takes a unique_ptr<Options> in its constructor
- CommandExecutor only holds a reference to (a unique ptr of) the api::Solver
- the main functions accesses options via the solver
|
|
This PR adds the new CVC5ApiOptionException. While the driver does not (and can not) do anything special for the two existing api exceptions, it can (and should) properly inform the user about incorrect command line option usage.
The PR also removes the UnrecognizedOptionException. It is purely internal now, and immediately catched by the API wrapper. Having a separate exception for this is no longer useful.
The additional catch block in main.cpp is only temporary until option parsing has been migrated to the driver and setting the options is done properly via the API.
|
|
This option is mostly redundant: It offers a way to access the
interactive shell without any copyright information or cvc5> prompt
being printed. However, --no-interactive offers the same experience
(except for the features offered by libedit).
|
|
This PR consolidates the two different reset implementations into a single function.
|
|
This complete the implementation of dump-instantiations-debug.
With this option, we can print the source of instantiations. For example:
$ cvc5 regress1/quantifiers/dump-inst-proof.smt2 --dump-instantiations-debug --produce-proofs
unsat
(instantiations (forall ((x Int)) (or (P x) (Q x)))
(! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (P x) true))))
)
(instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))))
(! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (S x) false))))
)
|
|
This PR fixes an issue that was introduced with fda4613 where printing the statistics would only show non-defaulted and non-expert options.
|
|
This PR changes how the command executor prints the statistics by moving stuff around a bit, eventually using only proper API methods of api::Solver. This PR also removes the smt_engine.h include from command_executor.cpp.
|
|
This PR improves the check when we use libedit: only when the input is an interactive terminal.
This is motivated by a change to the unit test for the interactive mode that now properly redirects standard input (and output).
|
|
This PR moves the remaining special purpose functions out of the Options class. This set of functions is only used to implement API functions in the smt engine (getting and setting options by string), and by the main driver for parsing and printing usage information.
|
|
This PR makes the CommandExecutor class use the options object from its SmtEngine instead of the driver one. This makes sure that options that are set via (set-option ...) are in effect for the CommandExecutor. It still stores the driver options, though, as they are used for resets.
The PR also does some minor cleanups along the way (remove unused pOptions, make things const).
Fixes #2376.
|
|
Recent experiments have shown that `--tear-down-incremental` is actually
not really helping anymore and it has always been a bit of a workaround.
It is also broken on current master. This commit removes the option.
|
|
This PR gets rid of almost all remaining public option wrappers. It does so by
- making base, main and parser options public such that they can directly be used from the driver and the parser
- moving incremental and the resource limiting options to base
- moving dumping options to main
After this PR, the only option wrapper left is becoming obsolete as well after (the follow-up of) #6697.
|
|
This PR pushes a rather complex check from the CommandExecutor inside the GetInstantiationsCommand.
The aim is to only use the instFormatMode option in the library (command.cpp) but not the main driver (command_executor.cpp).
|
|
The binary_name is solely used as a temporary storage to pass the data from the options parser back to the runCvc5 method where it is put in a static variable. This PR gets rid of the option and the public option getter in favor of directly storing the program name in the static variable using an additional argument to parseOptions().
|
|
This PR adds the possibility to make option modules public. As shown on the example of the main driver options, this allows to get rid of the wrappers from options_public.h. We plan to make only very few option modules public (i.e. main and parser).
|
|
|
|
This PR fixes the driver which used an incorrect variable name in competition mode.
|
|
This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.
|
|
This commit decouples the creation of a `Parser` instance from creating
an `Input` and setting the `Input` on the parser. This is a first step
in refactoring the parser infrastructure. A future PR will split the
parser class into three classes: `Parser`, `ParserState`, and
`InputParser`. The `Parser` and `InputParser` classes will be the
public-facing classes. The new `Parser` class will have methods to
create `InputParser`s from files, streams, and strings. `InputParser`s
will have methods to get commands/exprs from a given input. The
`ParserState` class will keep track of the state of the parser and will
be the internal interface for the parsers. The current `Parser` class is
used both publicly and internally, which is messy.
|
|
When cvc5 was compiled in competition mode (but not for the application
track), then it had a special behavior when reading from stdin. When it
received input from stdin, it would read all of stdin and then parse the
input as a string because it assumed that the full input is directly
available on stdin. However, the non-application tracks of SMT-COMP do
not use stdin anymore. They pass a filename to the solver. This special
case is not used as a result. Usually, cvc5 parses from stdin using the
line buffer, so this commit makes it so that this is always the case,
which simplifies the code.
|
|
As discussed in #6484 (and https://www.gnu.org/software/libc/manual/html_node/Termination-in-Handler.html), simply calling std::abort at the end of a custom signal handler seems to be bad practice. As suggested, this PR changes these calls to instead first reset to the default signal handler for the given signal, and then calling it.
Fixes #6484.
|
|
This PR removes two headers for exceptions from options.h, and instead pushes the includes to a couple of source files.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
|
|
This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
|
|
|
|
|
|
|
|
|
|
CMake 3.10.2 (default on Ubuntu 18.04) does not allow target_link_libraries on object libraries.
|
|
This PR does some minor refactorings in preparation for the new statistics: some renamings, removal of now obsolete code and usage of references instead of pointers.
|
|
This PR migrates CLN to a new Find script and adds the possibility to install CLN if not found in the system.
Also, it does a bit of cleanup.
|
|
|
