Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
Fixes #3537.
This benchmark triggers a potential unsoundness caused by instantiating with an uninterpreted constant (which is unsound).
|
|
This commit changes theory rewriters to be non-static. This refactoring
is needed as a stepping stone to making our rewriter configurable: If we
have multiple solver objects with different rewrite configurations, we
cannot use `static` variables for the rewriter table in the BV rewriter
for example. It is also in line with our goal of getting rid of
singletons in general. Note that the `Rewriter` class is still a
singleton, which will be changed in a future commit.
|
|
|
|
|
|
Previously, we were using UFs to encode substrings in the
`str.to.int`/`int.to.str` reductions. Our experiments have shown,
however, that using `str.substr` is more efficient instead.
|
|
|
|
This commit adds a lemma to our encoding of `str.to.int` and
`int.to.str` that relates the integer value in the encodings to the
value of partial results.
|
|
This makes it so that we don't construct intermediate unfoldings of applications of DT_SYGUS_EVAL, which wastes time in node construction. It makes the sygusToBuiltin utility in TermDbSygus use this implementation.
|
|
|
|
|
|
* [proof] Eliminate the side condition in er.plf
By tweaking the axioms a bit, I got rid of the lone SC in the Extended
Resolution signature.
* [proof] Changed er_proof.cpp in line with signature
The new signature requires slightly different proof printing.
* [proof] clang-format er_proof.cpp
* Fix tests
* [proof] Actually delete the SC
* Apply suggestions from code review
Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Add LFSC-checking unit test for ER proof
* Gate the lfsc invocation on the build system
* Properly gate the lfsc check on the build system
* gate the plf_signatures forward def on the build system
|
|
|
|
This adds classes corresponding to the Node-level Datatype API "DType", which is a specification for a datatype type. It does not enable the use of this layer yet. A followup PR will update the Expr-level Datatype to use the Node-level code, which is currently verified to be functional on this branch: https://github.com/ajreynol/CVC4/tree/dtype-integrate. Futher PRs will make the internal (Node-level) code forgo the use of the Expr-layer datatype, which will then enable the Expr-layer to be replaced by the Term-layer datatype.
Most of the documentation for the methods in DType/DTypeConstructor/DTypeSelector was copied from Datatype/DatatypeConstructor/DatatypeConstructorArg.
|
|
solver (#3525)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit fixes a corner case in the model construction of strings:
For a given length, we were assuming that for each equivalence class, we
could always find an initial guess for a constant to assign to it. This
was not always true, however, because a preceding equivalence class
could use up all constants and get assigned the last remaining one, so
we wouldn't have a constant remaining for the current class. This
resulted in an assertion failure (in debug) or a crash (in production).
This commit fixes the issue by checking whether we've run out of
constants before assigning an initial constant for an equivalence class.
|
|
|
|
More recent clang version introduce an extra flag AfterCaseLabel for brace wrapping after case labels. Default is false, with the effect opening braces after case labels will be aligned on the same line as the label. Our style requires it to be set to true.
|
|
|
|
CVC4_API_CHECK_NOT_NULL (#3520)
|
|
|
|
|
|
API (#3355)
* Treat uninterpreted functions as a child in Term iteration
* Remove unnecessary const_iterator constructor
* Add parameter comments to const_iterator constructor
* Use operator[] instead of storing a vector of Expr children
* Switch pos member variable from int to uint32_t
* Add comment about how UFs are treated in iteration
* Allow OpTerm to contain a single Kind, update OpTerm construction
* Update mkTerm to use only an OpTerm (and not also a Kind)
* Remove unnecessary function checkMkOpTerm
* Update mkOpTerm comments to not use _OP Kinds
* Update examples to use new mkTerm
* First pass on fixing unit test
* Override kind for Constructor and Selector Terms
* More fixes to unit tests
* Updates to parser
* Remove old assert (for Kind, OpTerm pattern which was removed)
* Remove *_OP kinds from public API
* Add hasOpTerm and getOpTerm methods to Term
* Add test for UF iteration
* Add unit test for getOpTerm
* Move OpTerm implementation above Term implemenation to match header file
Moved in header because Term::getOpTerm() returns an OpTerm and the compiler complains
if OpTerm is not defined earlier. Simply moving the declaration is easier/cleaner than
forward declaring within the same file that it's declared.
* Fix mkTerm in datatypes-new.cpp example
* Use helper function for creating term from Kind to avoid nested API calls
* Rename: OpTerm->Op in API
* Update OpTerm->Op in examples/tests/parser
* Add case for APPLY_TESTER
* operator term -> operator
* Update src/api/cvc4cpp.h
Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Comment comment suggestion
Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Add not-null checks and implement Op from a single Kind constructor
* Undo sed mistake for OpTerm replacement
* Add 'd_' prefix to member vars
* Fix comment and remove old commented-out code
* Formatting
* Revert "Formatting"
This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9.
* More fixes for sed mistakes
* Minor formatting
* Undo changes in CVC parser
* Add isIndexed and prefix with d_
* Create helper function for isIndexed to avoid calling API functions in other API functions
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Refactor compute model value for nl
* Format
|
|
|
|
|
|
|