| Age | Commit message (Collapse) | Author |
|---|
|
This goes back to the new cmake setup and makes it compatible again with cmake 3.9.
It mostly means we can not link object libraries and also not link other libraries to object libraries.
I've tested these changes within docker on `ubuntu:18-04` with a manually installed `cmake-3.9.6`.
|
|
This introduces a new versioning mechanism that allows for better automation.
|
|
We already created two dependency targets `GMP_SHARED` and `GMP_STATIC`, as we could not use `libgmp.a` for shared linking (as it is built without `-fPIC`). This PR fixes our handling of CLN and Poly: they would always link with `GMP_STATIC`, leading to having both `GMP_SHARED` and `GMP_STATIC` in the linker command line in certain situations. We now also have `*_SHARED` and `*_STATIC` for both CLN and Poly.
|
|
This PR changes --dump-unsat-cores-full to --print-unsat-cores-full.
It also makes it so that solely having --dump-unsat-cores-full no longer automatically prints unsat cores.
|
|
This PR modifies our CI builds to have two static production builds. These binaries will be used as release artifacts later.
|
|
Some cleanup on the option handlers, starting with handlers for base and main options.
|
|
|
|
This is in preparation for renaming SmtEngine to SolverEngine.
|
|
This PR does a major refactoring on how we organize our builds to allow both shared and static builds. We now build the libraries using object libraries to allow building the libraries both dynamically and statically in the same build folder, though the static library is optional (ENABLE_STATIC_LIBRARY). The binary is linked either dynamically or statically (depending on ENABLE_STATIC_BINARY).
|
|
Support for the CVC language was removed in #7219 but the help message
for languages was not updated. This removes the mention of CVC from the
help message.
|
|
This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.
|
|
This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.
One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.
|
|
Adds smt2 parsing, printing and API support for get-difficulty. Adds unit tests.
|
|
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.
|
