| Age | Commit message (Collapse) | Author |
|---|
|
This fixes a segfault in the evaluator for substitutions of the form x -> t where t is not constant.
This consolidates 2 cases where we did not evaluate children (when we are variable or are an application term with an unevaluated child). This was problematic previously since we would access children of currNode instead of currNodeVal.
This also makes our handling of APPLY_UF more consistent, so that it is added to the main switch statement.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
|
|
This adds basic support for string/sequence updating, which has a semantics that is length preserving.
|
|
This will be required to separate "evaluation steps" from "rewrite steps" when reconstructing proofs of rewrites.
|
|
|
|
Work towards support for the strings standard.
This updates the string solver and parser such that:
The internal representation of strings is vectors of code points,
Generation of the previous internal representation of strings has been relegated to the type enumerator. This is the code that ensures that "A" is the first character chosen for values of strings in models,
The previous ad-hoc escape sequence handling is moved from the String class to the parser. It will live there for at least one version of CVC4, until we no longer support non-smt-lib complaint escape sequences or non-printable characters in strings,
Handle unicode escape sequences according to the SMT-LIB standard in String,
Simplify a number of calls to String utility functions, since the conversion between the previous internal format and code points is now unnecessary,
Fixed a bug in the handling of TO_CODE: it should be based on the alphabet cardinality, not the number of internal code points.
|
|
This commit adds support for `str.from_code`. This is work towards
supporting the new strings standard. The code currently just does an
eager expansion of the operator. The commit also renames `STRING_CODE`
to `STRING_TO_CODE` to better reflect the names of the operators in the
new standard.
|
|
|
|
Improves performance on ground conjectures with recursive functions. We use the evalutator to (partially) evaluate bodies of recursive functions, instead of relying on substitution+rewriting.
|
|
This ensures that the Evaluator always returns the result of substitution + rewriting for constant substitutions.
This requires a few further extensions to the code, namely:
(1) Applying substutitions to operators,
(2) Reconstructing all nodes that fail to evaluate by taking into account evaluation of their 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`.
|
|
|
|
|
|
|
|
|
|
|
|
This should fix Coverity issue 1470214.
|
|
|
|
|
|
This commit adds the Evaluator class that can be used to quickly
evaluate terms under a given substitution without going through the
rewriter. This has been shown to lead to significant performance
improvements on SyGuS PBE problems with a large number of inputs because
candidate solutions are evaluated on those inputs. With this commit, the
evaluator only gets called from the SyGuS solver but there are
potentially other places in the code that could profit from it.
|
