| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
Also adds a call to get proof in a unit test.
|
|
Without this, you can't make terms with that kind.
|
|
This is work towards eliminating circular dependencies on SmtEngine.
This simplifies several interfaces and makes it so that SmtSolver does not take a pointer to its parent SmtEngine.
It is also work towards eliminating the output manager, which is now subsumed by Env.
|
|
This PR further simplifies the option setup by only using int64_t or uint64_t for integer options.
|
|
This ensures that e.g. COMBINATION_SPLIT shows up under theory::builtin::inferencesLemmas, and -t im. It also removes outdated interfaces from OutputChannel, and makes the feature TheoryEngine::ensureLemmaAtoms more modular, which was required for making these interfaces more consistent.
It also ensures that TheoryBuiltin has an inference manager, which will simplify special casing in #6956.
|
|
The internal solver no longer cares about what assertions are named / are in the unsat core.
This simplifies the code so that the (now unused) `inUnsatCore` flag is removed from all interfaces.
This eliminates another external use of `getSmtEngine`.
|
|
This PR fixes an issue that was introduced with fda4613 where printing the statistics would only show non-defaulted and non-expert options.
|
|
This regression times out without libpoly.
|
|
|
|
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 allows changing some select options ever after the smt engine has been fully initialized, following the SMT-LIB standard (section 4.1.7).
|
|
The common case of printing function applications is to print the kind in smt2 format, this makes this the default case and removes spurious cases. It also makes a few minor fixes.
|
|
This PR migrates the current INSTALL.md to an rst file and then includes it in the documentation. It also does some minor improvements to this file, in particular it now mentions --dep-path
|
|
|
|
Since the internal bitblaster can be way slower, the regressions that would have slow runs when --check-proofs is passed now have the command line that forces the use of the default bitblaster.
|
|
This is a translation of quickstart.cpp to python.
|
|
and regressions (#6943)
This commit makes TheoryEngine take into account whether theories are using the central equality engine.
With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.
|
|
Includes proper set up of the proof equality engine it uses (which may be shared over multiple theories). Also makes its assertEquality method robust to non-equality atoms.
|
|
This PR makes several fixes to the wheel building infrastructure for manylinux2014.
don't statically link to Python (see: this section of PEP-513)
use standard 'build' directory. I noticed that the wheel infrastructure uses directory 'build' to prepare the wheel anyway, so it doesn't make a lot of sense for us to use a separate working directory. I tried changing the name of the build directory in setuptools by setting member variables in initialize_options but that didn't seem to work and I decided it wasn't worth the effort. The wheel should be built in a clean environment anyway, i.e., docker.
find the correct include directory and python library paths for building on manylinux2014 using skbuild. manylinux2014 has several versions of python installed in /opt/python. The CMake infrastructure can't find the necessary information (plus the libraries are deleted from the docker image to save space -- the library is just set to a generic libpython<version>.a). Instead, this PR would manually set them via CMake options.
to allow setting the python information, I extended the configure.sh script to allow directly setting CMake options. There are definitely other options here if you'd rather not change configure.sh. My reasoning was that it could be useful in other situations and I just marked it as an advanced feature. Another approach would be to use skbuild directly in the CMake infrastructure. I didn't like that solution because it would make the CMakeLists.txt more complicated and it wouldn't follow the standard CMake/Cython/Python approach which means we won't benefit from future improvements to that CMake infrastructure. Plus, this issue should only come up on systems with non-standard installations of Python, such as manylinux. This approach (setting CMake options) is basically what scikit-build does automatically if we had used that infrastructure directly.
|
|
Makes arrays more robust to the order in which terms can be added to the equality engine vs. when they are preregistered.
We should probably performance test this.
FYI @barrettcw
|
|
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 commit adds a message to the `docs` target with a link to a preview
of the documentation, e.g.:
```
Preview docs in browser: file://localhost/home/noetzli/repos/cvc5_win/build-docs/docs/sphinx/index.html
```
|
|
|
|
This commit refactors the getEqualityStatus handling for bitblast and bitblast-internal.
|
|
Adds proof support for the eqrange operator.
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
This adds optional arguments to INSTANTIATE steps in proofs to track fine-grained reasons for relevant instantiations.
Also simplifies an old argument modEq which was unused.
FYI @MikolasJanota
|
|
Adds basic utilities in preparation for the LFSC proof conversion.
Depends on #6881, review that first.
|
|
Work towards integrating the enumerator callback into the fast enumerator.
|
|
Previously we provided a bogus (self) explanation in a rare case of setting up the term database for higher order. This is incompatible with cases where central equality engine = master equality engine.
|
|
Although it works on most machines, it times out in the nightly builds.
|
|
This allows one to use a fast enumerator without having access to sygus term database, statistics, etc.
|
|
This will be used in the LFSC printer. It may be of general use to other proof printers.
|
|
Fixes #6639. The issue cannot be reproduced on current master and git bisect suggests that commit adf497a
fixed the issue.
|
