| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #4393. Fixes #3966.
These issues do not occur on current master.
|
|
This PR fixes calling (get-info :authors). It used to (try to) print the whole about() information, but failed to do so because the string needed to be turned into an s-expression. However, about() is not properly escaped.
We now simply print the cvc5 authors.
It also fixes isValidGetInfoFlag() which was missing filename.
Fixes #7362.
|
|
This PR addresses #7361, but also a more general issue about regular-output-channel being able to hold stderr and diagnostic-output-channel being able to hold stdout.
It therefore changes how non-owned streams are stored: beforehand, an explicit stream would always be owned by the ManagedStream (through a std::shared_ptr) and a nullptr implicitly stood for stdout, stderr or stdin. Now we explicitly hold a pointer to a non-owned stream for these special values.
Fixes #7361.
|
|
Fixes #6845.
This issue does not occur in current master.
|
|
|
|
Towards addressing some bottlenecks on Facebook benchmarks.
|
|
This PR generally improves the new CI job to test different cmake versions. It extends the tested versions back to 3.8 and also sets the minimum required version (cmake_minimum_required) to the version that is tested. This allows to check compatibility with changing cmake policies.
It also modifies the run-tests action to get the regression options from explicit inputs instead of the build matrix. As the cmake job had no build matrix, it used to build regress3-4 as well.
|
|
Fixes #7353.
|
|
While #7341 added cmake-3.9 compatible linking for GLPK, it did not actually remove the line that triggers the error on older cmake versions. This commit does.
|
|
These files define how terms and sorts are represented. It also adds basic utilities used throughout.
|
|
Also simplifies slightly how rewritten forms of operators in sygus grammars are obtained.
|
|
|
|
This tightens the interface of the sygus solver, which was a product of not using subsolver calls in the original design.
|
|
The remaining calls to smt::currentResourceManager are in the bitblasters, which should probably update to Env. FYI @mpreiner .
|
|
|
|
|
|
This further renames d_smtStats to d_slvStats in ProcessAssertions.
|
|
|
|
This PR makes the cmake integration of GLPK compatible with cmake 3.9.
Also, it adds a missing BUILD_BYPRODUCT for antlr.
|
|
Towards making theory preprocessing a single pass.
|
|
Also fixes a bug in the quantifiers macro utility which did not compute the instantiation constant body of a quantified formula properly.
This is work towards a major refactoring of conflict-based instantiation / entailment checks.
|
|
The core sygus solver predates the use of subsolvers. When doing verification checks in the CEGIS loop, we previously added unique lemmas to the main solver with fresh skolem variables. We now call subsolvers only, meaning that the set of skolem variables used in verification calls can be fixed.
|
|
When compiling cvc5 with clang-13, it will emit lots of warnings of usages of `std::iterator` as it's deprecated since C++17.
The recommended implementation of iterators is to manually define the following five types:
```
template< class Iter >
struct iterator_traits;
difference_type Iter::difference_type
value_type Iter::value_type
pointer Iter::pointer
reference Iter::reference
iterator_category Iter::iterator_category
```
And the iterator-related types could be accessed by for example `typename std::iterator_traits<Iter>::value_type value`.
This pull request performs the fix, and the program is semantically equivalent before and after the fix.
References:
https://en.cppreference.com/w/cpp/iterator/iterator_traits
https://en.cppreference.com/w/cpp/iterator/iterator
|
|
|
|
|
|
|
|
|
|
|
|
|
|
For static builds, there was a mixup of variable naming in FindANTLR3 (RUNTIME vs LIBRARIES).
|
|
|
|
This PR reverts #7257 and restores compatibility with ancient glibc versions.
|
|
This refactors the CI setup by moving parts of the CI workflow into new composite actions. This allows to reuse this parts in a new workflow that tests against many different cmake versions. It is mostly useful after modifying our cmake setup to check compatibility with older cmake versions.
The workflow is not triggered automatically, but can be started manually.
|
|
This adds the option --proof-format=lfsc.
It adds an initial regression to test the LFSC printer. This will be followed up with a more comprehensive plan for regression tests.
|
|
This class will be used to replace the `fmf.card` operator with a 0-ary indexed parameterized nullary predicate for representing cardinality constraints for UF.
This is in preparation for eliminating hacks in the core of theory combination for e.g. not considering the dummy arguments of cardinality constraints to be shared terms.
|
|
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 PR removes a bunch of static accesses in places where EnvObj is used now, and we can thus use options().
|
|
This led to a model soundness issue in a development branch that reorganizes theory preprocessing.
This ensures that skolem definition manager looks for skolems that appear in operators.
This is important for inputs like:
(declare-fun h (Int) Int)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= h (ite A f g)))
(assert (= (h 0) ...)))
|
|
Work towards virtual clause deletion, where lemmas will be SAT-context dependent.
This adds an argument to the decision engine so it can distinguish lemmas from input assertions.
|
|
|
|
This fixes the diff mechanism to detect whether the current PR changes the documentation. It ignores zip files now, i.e. the javadoc search index files.
|
|
This adds another step to our CI pipeline that uploads the binary build by some of the jobs to a release.
|
|
This breaks the circular dependency of preprocessing pass context of solver engine.
It also moves the preprocessor to be owned by SMT solver, instead of Solver engine.
It also changes the behavior of reset assertions: now, the preprocessing pass context is reset, whereas previously it was not. I believe this is the right behavior, as it eliminates stale data (e.g. learned literals, symbols in assertion cache).
|
|
This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example.
|
|
This adds the remaining implementation of the LFSC printer.
It also corrects a bug introduced during merging the last PR.
The printer will be connected to the proof manager in a follow up PR. It will also be extended with support for DSL proof rule printing when the infrastructure is added.
|
|
|
|
This introduces a new versioning mechanism that allows for better automation.
|
|
This adds an option to change the cardinality of the alphabet of strings. The alphabet of strings is always a prefix of the interval of unicode code points in the string standard.
|
|
This adds recent API functions that were added to terms.
It also uses BigInteger now for integer terms.
|
|
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.
|
