| Age | Commit message (Collapse) | Author |
|---|
|
|
|
We previously incorrectly allowed this, leading to problems that were unsolvable but where we would not warn the user this combination is not supported.
FYI @polgreen
|
|
|
|
This eliminates the old option "inst format mode" and makes proof output for TPTP organized as an ordinary proof output format.
|
|
This PR refactors part of the arithmetic theory to use the options via the Env object.
|
|
Reverts a change from #7031, which changed the contract for when the proof CNF stream is handling propagations. When doing unsat cores with sat proofs (but not full proofs), theory engine will not be proof producing but the proof cnf stream still needs to connect theory lemmas with their clausified equivalents in the SAT solver.
|
|
This PR moves the collectAssertedTerms utility function from the model manager to the theory class. This allows to use the utility also when we are not currently building the model.
|
|
PR #7017 fixed the policy for eliminating quantifiers but introduced
some minor issues, which this commit fixes:
the InstantiationEngine::checkOwnership() method was changed to look
for patterns in the wrong node.
the PR changed the modes of the --user-pat=MODE method but reused
one of the names. This commit fixes the name and adds a check in the
options script.
fixing the policy caused cvc5 to answer unsat instead of the
expected unknown for regress0/use_approx/bug812_approx.smt2. The
commit updates the expected result.
|
|
This simplifies our management of how/when proofs are enabled in the PropEngine.
|
|
Because we are now using C++17, we can get rid of Maybe and instead
use std::optional, which offers the same functionality.
|
|
Also moves d_filename to Env.
|
|
No behavior changes in this PR, just code reorganization.
|
|
This also consolidates the option strictTriggers into userPatMode.
Fixes #6996.
|
|
|
|
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).
|
|
Mainly just indentation / formatting changes. In preparation for playing around with heuristics to datatypes theory motivated by Facebook benchmarks.
|
|
Work towards a new expression miner for caching satisfiability queries.
|
|
This commit starts to carve out better control flow structure in setDefaults.
It makes setDefaults contained in a class, and moves a few blocks of code to their own functions.
This class also makes options manager obsolete, it is deleted in this PR.
There should be no behavior change in this PR.
|
|
This PR is a follow-up to #7011, making the Env object available in the TheoryState base class.
|
|
This PR refactors the ExtTheory class to use a given inference manager instead of a given output channel.
|
|
This PR changes the Theory base class and the constructors of all theories to use the Env class to access contexts, logic information and the proof node manager.
|
|
Currently, our check for whether an inference is a fact or a lemma
involves checking whether the kind of the conclusion is a conjunction or
a disjunction. However, this does not take into account inferences of
other kinds such as ites, which is a problem because they require a
decision from the SAT solver. This commit changes the condition to check
the theory of the conclusion. If the conclusion belongs to the theory of
strings, it considers it as a fact.
|
|
This commit adds a check for CryptoMiniSat's static dependencies when configuring CryptoMiniSat. It changes a build-time failure into a configure-time failure.
`find_library` in CMake > 3.18 supports `REQUIRED`; as `cvc5` targets 3.10, I've implemented a check for what `find_library` returns.
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
In `master`, starting `cvc5` interactively will give you:
```
glpk-cut-log - a modified version of GPLK, the GNU Linear Programming Kit
See http://github.com/timothy-king/glpk-cut-log for copyrightinformation
```
Notice: there's a double-space after the dash following the library name, and there's no space between "copyrightinformation".
This commit corrects this print such that it gives:
```
glpk-cut-log - a modified version of GPLK, the GNU Linear Programming Kit
See http://github.com/timothy-king/glpk-cut-log for copyright information
```
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
This commit refactors the `setDefaults` method to accept an `Options` object as argument instead of using the current (static) `Options` object.
|
|
This commit adds `-fno-extern-tls-init` to the list of compiler flags to
tell the compiler that it can assume that there is no dynamic
initialization of thread-local variables in non-defining translation
units. This option should result in better performance and works around
crashing issues with our Windows build.
|
|
This commit simplifies both the code that generates the option modules and the generated code itself. It removes placeholders in the templates that are no longer used, gets rid of the option holder types (and replaces them by simple inline functions) and does some clean up on the related code in the `mkoptions.py` script.
|
|
Currently, it seems that `cvc5` has no tests that get anywhere near close to exercising the code in `approx_simplex`, which means that the GLPK integration is effectively untested in CI:
* https://cvc4.cs.stanford.edu/downloads/builds/coverage/cvc5-2021-08-02/index.src_theory_arith_approx_simplex.cpp.html
(which is at 2.8% at the time of writing!)
Indeed, if you run the whole of `ctest`, none of the code near GLPK is exercised; and, worse, there are *no* regression tests that use `--use-approx`!
This commit adds a selection of simple tests that have been derived (using `cvc5`'s existing regression suite and ddSMT) to reach code inside of `approx_simplex`; namely:
- `solveRelaxation`, and
- `solveMIP`
This is (hopefully) an initial start that will allow us to grow more regression tests exercising GLPK (e.g., following the same process of reduction, but using the SMTLIB benchmarks vs. only `cvc5`'s regression suite).
The folder structure has been named such that I can do `ctest -R "use_approx"` to run only the tests that (should) reach GLPK.
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
Fixes #7001. Commit c8bc488 introduced the use
of list(PREPEND ...) which was only introduced in version 3.15. We require
CMake 3.9 or later and this commit makes our build system compatible with older
CMake versions again. It also changes our CI to have two builds with Ubuntu
18.04 and two builds with Ubuntu 20.04 to better cover different versions of
build tools (including CMake 3.10).
|
|
This PR removes options/CMakeLists.txt and merges its contents into src/CMakeLists.txt and does some generalization in the mkoptions.py script. This prepares the whole setup so that we can also generate options code in other directories than options/ easily in the future: parts of the options code will be moved to the main folder.
|
|
This PR moves the remaining responsibilities from the options manager into option predicates. They belong there anyway, given that this code shall be executed immediately when an option is set. This also allows to remove the infrastructure for an options listener.
|
|
Fixes cpp API's mkBitVector(val_str, base) constructor.
|
|
Initial work towards rewrite rule reconstruction.
|
|
For some configurations, the unit test `solver_black` was unable to find
the correct variant `std::find()`. This commit adds an explicit include
of `<algorithm>`, which declares the `std::find()` as required by the
unit test.
|
|
This PR simplifies our rewriter for string equalities. We do not try to rewrite equalities to true/false by default.
This prevents cases where lemmas may contain vacuous premises that rewrite to false, hence making a lemma rewrite to true.
This PR reorganizes the interplay between the rewrite and the post-processing of rewrites via extended equality rewriting.
Fixes #6913. Also adds benchmarks from #6101 which appear related but were fixed in previous commits, thus fixes #6101 as well.
|
|
This PR removes calls to the Solver constructor with an Options object, and instead uses the setOption() method.
|
|
This PR consolidates the two different reset implementations into a single function.
|
|
|
|
This makes it so that we replace subproof A with subproof B if A and B prove the same thing, and B contains no assumptions. This is independent of the scope that A and B are in.
The previous policy replaced subproof A with subproof B if A and B prove the same thing and were in the same scope. This is not safe if A occurs in multiple scopes, where free assumptions can escape.
The new policy is more effective and safer than the previous one.
|
|
This PR fixes the escaped characters in the dot printer. The output is now a valid DOT.
Signed-off-by: Diego Della Rocca de Camargos diegodellarocc@gmail.com
|
|
Now, all inferences throughout cvc5 in our regression are properly marked with an InferenceId.
This PR includes minor simplifications to the interface for sygus modules. In particular it changes the behavior to send inferences via the inference manager instead of passing them around as a vector.
|
|
Addresses #6979.
|
|
Adds the datatype values as debug information for dumping instantiations produced by --sygus-inst.
|
|
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))))
)
|
|
|
|
Work towards making our policy for subproof merging safer.
|
|
This PR introduces a new ManagedStream class that replaces the previous ManagedOstream. It allows to directly store the (wrapped) stream objects in the options. Handling the stream options is moved from the options manager to option predicates and the different options for input and output streams are combined into a single one.
Some associated utilities (open_ostream.h and update_ostream.h) are now obsolete and thus removed.
|
|
This PR adds a new API function api::Solver::getOptionNames() that exposes a list of all option names as strings. This PR will be followed by another that adds a method to further inspect a particular option by name, and thereby allows to inspect the solver options in a sensible way.
|
|
This PR replaces some option predicates by explicit minimum and maximum values. This allows us to export information about an options domain/range in the future.
|
|
The only remaining unknown inferences covered by our regressions are from the sygus solver, will address in later PR.
|
