| Age | Commit message (Collapse) | Author |
|---|
|
This commit unifies abstract values and "uninterpreted constants" into a
single kind. Note that "uninterpreted constants" is a bit of a misnomer
in the context of the new API, since they do not correspond to the
equivalent of a `declare-const` command, but instead are values for
symbols of an uninterpreted sort (and thus special cases of abstract
values). Instead of treating "uninterpreted constants" as a separate
kind, this commit extends abstract values to hold a type (instead of
marking their type via attribute in `NodeManager::mkAbstractValue()`)
and uses the type of the abstract values to determine whether they are a
value for a constant of uninterpreted sort or not. Unifying these
representations simplifies code and brings the terminology more in line
with the SMT-LIB standard.
This commit also updates the APIs to remove support for creating
abstract values and "uninterpreted constants". Users should never create
those. They can only be returned as a value for a term after a
satisfiability check.
Finally, the commit removes code in the parser for parsing abstract
values and updates the code for getting values involving abstract
values. Since the parser does not allow the declaration/definition of
abstract values, and determining whether a symbol is an abstract value
was broken (not all symbols starting with an `@` are abstract values),
the code was effectively dead. Getting values involving "uninterpreted
constants" now no longer requires parsing the string of the values, but
instead, we can use existing API functionality.
|
|
|
|
|
|
|
|
|
|
|
|
SMT-LIB indicates that abstract values can appear in terms as arguments to `get-value`. This is not currently the case, as pointed out by #6908.
This updates our parser so that bindings are added to the symbol table for all uninterpreted constants in the model whenever we parse a `get-value` term.
Fixes #6908.
|
|
With -o raw-benchmark, The command:
(echo """")
was printed as
(echo """""""")
because we run the quote-escaping procedure twice on it. This PR fixes the issue by ensuring that we only run it once.
|
|
We are currently using an attribute to mark "rewritten with proofs". This is incorrect as attributes are global, but proofs of rewrites are local to the solver instance.
This enables applications of proofs within internal subsolvers, and is required for a new internal fuzzing technique.
|
|
The lack of a type enumerator for regular expressions makes certain things impossible e.g. sygus-based sampling for RE queries.
It is trivial to support a basic RE enumerator that takes singleton languages of strings. This commit adds this utility as the type enumerator for RE.
|
|
MACRO_SR_PRED_TRANSFORM (#7412)
Fixes a proof checking failure during post-processing.
Fixes a rare case where the RHS of equality resolve step requires a symmetry step.
|
|
The only open case is dynamic cardinality types (e.g. uninterpreted sorts when FMF is enabled).
|
|
We now insist that we sanity check integer models in linear logics. Previously, we could trigger an assertion failure in Minisat if a user asked for a model in a state where the linear solver had assigned a real value to an integer variable, as we would be sending a lemma during collectModelValues in a state where we had already terminated with "sat".
This also changes an assertion to warning, to allow the regression to pass.
Fixes #6774 (This PR fixes a followup issue after the original bad model reported there was fixed by sanity checks).
As the assertion failure is downgraded to a warning, fixes #6988, fixes #7252.
|
|
This PR removes some auto-generated utility methods to set an option if it has not been set by the user. It was once added as we thought it might be useful, but we do not actually use it.
|
|
Fixes #6653.
The third benchmark on that issue is no longer an issue, this adds it as a regression, which is the last open benchmark on the referenced issue.
|
|
Check for experimental array features was done at the parser module, which meant that users of the API could use them without calling Solver::setOption("arrays-exp"). This PR fixes that by moving the check to the internal theory module.
|
|
PR #6848 disabled relevancy order by default, but for QF_NIA, it helps
us solve significantly more benchmarks (17525 vs. 16889 with a 20 minute
timeout using the updated SMT-COMP script). This also updates the
options for `QF_AUFBV` and `QF_ALIA` to use `--decision=stoponly`,
following the name change of the option.
|
|
This PR adds documentation to the python class Op, Grammar, Result, and for API enums.
Additionally, documentation for isNull functions in the datatype classes is added for the python API, and a small change in the cpp API documentation is introduced.
|
|
Fixes #6535, Fixes #6475, Fixes #5660, Fixes #6607, Fixes #6638, Fixes #6642, Fixes #6775.
|
|
This PR improves our docs-ci mechanism to properly upload documentation for tags.
|
|
|
|
(#7366)
This makes string proof construction more robust by maintaining two separate proof inference constructors, one for facts and one for lemmas/conflicts. This avoids issues where 2 lemmas with the same conclusion (but possibly different explanations) are added in the same call to check.
This fixes one of the two issues related to proofs for #6973.
|
|
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
|
|
|
|
|
|
|
|
|
|
|
