| Age | Commit message (Collapse) | Author |
|---|
|
This would add tracing options to print the decision tree in [org-mode](https://orgmode.org/) format which can be viewed with emacs or [vim-orgmode](https://github.com/jceb/vim-orgmode).
In the raw format, the number of asterisks denote the decision level of a decision, and within a propagation node, the number of spaces denote the level. Most viewers render the asterisks as indented bullets.
There are some options for controlling verbosity:
`dtview` - prints the decisions (basic option)
`dtview::command` - also prints smt-lib commands as they're issued
`dtview::conflict` - also prints conflicts
`dtview::prop` - also prints propagations
Example usage:
`cvc4 -t dtview -t dtview::command -t dtview::conflict -t dtview::prop <example smt2 file> &> example-trace.org`
The resulting file when opened with an org-mode viewer has collapsible nodes, where "..." marks a node with children.
|
|
Fixes a bug where we don't return the partially evaluated version (for unevaluatable nodes). Also adds `NONLINEAR_MULT` whose semantics is identical to `MULT`.
|
|
In some SyGuS applications, the bottleneck is the rewriter. This PR makes a few simple optimizations to the core rewriter, namely:
(1) Minimize the overhead of `theoryOf` calls, which take about 10-15% of the runtime in the rewriter. This PR avoids many calls to `theoryOf` by the observation that nodes with zero children never rewrite, hence we can return the node itself immediately. Furthermore, the `theoryOf` call can be simplified to hardcode the context under which we were using it: get the theory (based on type) where due to the above, we can assume that the node is not a variable.
The one (negligible) change in behavior due to this change is that nodes with more than one child for which `isConst` returns true (this is limited to the case of `APPLY_CONSTRUCTOR` in datatypes) lookup their theory based on the Kind, not their type, which should always be the same theory unless a theory had a way of constructing constant nodes of a type belonging to another theory.
(2) Remove deprecated infrastrastructure for a "neverIsConst" function, which was adding about a 1% of the runtime for some SyGuS benchmarks.
This makes SyGuS for some sets of benchmarks roughly 3% faster.
|
|
|
|
|
|
|
|
The word-blasting function `FpConverter::convert` used a `std::stack` with `deque` as an underlying data structure (default) for node traversal. Previous experiments suggested that using `std::stack<T, std::deque<T>>` performs worse than using `std::vector<T>`, and we decided, as a guideline, to always use `std::vector` for stacks: https://github.com/CVC4/CVC4/wiki/Code-Style-Guidelines#stack.
This PR refactors `FpConverter::convert` to use `std::vector`. Runs on all incremental and non-incremental FP logics in SMT-LIB showed a slight improvement over the previous (`std::stack<T, std::deque<T>>`) implementation, and an even greater (albeit still slight) improvement over using `std::stack<T, std::vector<T>>`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
