| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.
|
|
|
|
Fixes a solution soundness issue caused by allowing ineligible terms of kind BOOLEAN_TERM_VARIABLE to appear in instantiations.
This also corrects the expected solution on a benchmark that had an incorrect status.
Fixes #6603.
|
|
|
|
|
|
This is to make it consistent with the name of the SMT-LIB operator
(fp.add).
|
|
This commit fixes an assertion failure in the rewriter on some of the
SMT-LIB QF_ABVFP benchmarks (the regression in this commit is the
minified version of
`non_incremental/QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_klee.x86_64/query.14.smt2`).
The problem was that after applying the `BvComp` rewrite, the bit-vector
rewriter was returning `REWRITE_DONE` instead of `REWRITE_AGAIN`. The
rewrite simplifies expressions of the form `bvcomp(t, c)` where `c` is a
constant of bit-width 1. If `c` is zero, then the rewrite returns
`bvnot(t)`. This node can potentially be rewritten further, e.g., if `t`
is `bvnot(x)`. This commit fixes the response and adds the corresponding
tests.
|
|
We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).
The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.
|
|
Fixes followup issues from #6604.
|
|
Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.
|
|
This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.
It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").
|
|
Fixes #6604.
Previously, re-elim was solution unsound for cases where the LHS and a component of the RHS were both empty. This ensures a length requirement is given for the LHS to ensure proper containment.
|
|
Fixes #6545.
An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.
|
|
This replaces our previous formalization of RE unfolding skolems with a more explicit one that is amenable to external proof conversion. It adds a few associated utility methods to SkolemManager required for LFSC proof conversion for RE_UNFOLD_POS.
It also changes the order of equalities in the RE_UNFOLD_POS rule, which simplifies LFSC proof checking.
|
|
In a handcrafted case, one can make the body of quantified formula another quantified formula when special attributes are used. The relevant domain utility was not robust to this case, leading to instantiations with free variables.
This fixes the issue and also updates its style to use a term context stack, which also avoids a tree traversal of the bodies of quantified formulas in this utility.
Fixes #6476. The benchmark from that issue now times out.
|
|
|
|
|
|
This PR does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.
It also removes the unused command GetSynthSolutionCommand.
|
|
This commit adds support for braced-init-lists in calls to `mkNode()`,
e.g., `mkNode(REGEXP_EMPTY, {})`. Previously, such a call would result
in a node of kind `REGEXP_EMPTY` with a single null node as a child
because the compiler chose the `mkNode(Kind kind, TNode child1)` variant
and converted `{}` to a node using the default constructor. This commit
adds an overload of `mkNode()` that takes an `initializer_list<TNode>`
to allow this use case. It also adds a `mkNode()` overload with zero children
for convenience and removes the 4- and 5-children variants because they
saw little use. Finally, it makes the default constructor of `NodeTemplate`
explicit to avoid accidental conversions.
|
|
|
|
This commit removes the remaining old proof code and the code to produce unsat cores based on it.
|
|
reflects that it is a macro, which we will eliminate
|
|
Fixes #6567.
|
|
The strings inference id STRINGS_INFER_EMP is a rare inference that currently leads to a segfault when proof reconstruction is tried for it. This PR makes it unhandled.
This was caught by a new regression on the soon-to-be-merged jh-new branch.
|
|
Fixes #6561.
Previously we missed a case where a rewrite fired for (re.range x x) where x is not a character.
|
|
This also makes the relations solver use the inference manager in the standard way.
|
|
This PR adds support for handling --bitblast=eager in the new bitblast solver.
|
|
Fixes #6560.
|
|
Fixes #6561. That benchmark now gives an error:
(error "expecting a single constant string term in regexp range").
This PR also makes isConstRegExp do a non-recursive dag traversal.
|
|
This PR modifies the rcons algorithm to loop over terms to reconstruct instead of obligations. It also modifies the Obs data structure to reflect this change. The rest of the PR is mostly updating documentation and refactoring the affected code.
|
|
Fixes #6483. The benchmark in the issue was performing the following
incorrect rewrite:
Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP.
The rewrite RPL_X_Y_X_SIMP rewrites terms of the form (str.replace x y x), where x is of length one and (= y "") rewrites to a
conjunction of equalities of the form (= y_i "") where y_i is some
term. The function responsible for collecting the terms y_i from this
conjunction, collectEmptyEqs(), returns a bool and a vector of
Nodes. The bool indicates whether all equalities in the conjunction
were of the form (= y_i ""). The rewrite RPL_X_Y_X_SIMP only applies
if this is true. However, collectEmptyEqs() had a bug where it would
not return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
collectEmptyEqs() and adds tests.
|
|
This includes:
(1) The type rule for `re.range` no longer insists on constant arguments, or a non-empty range. This is required for LFSC proof conversion, where re.range terms take arguments that are not (cvc5 internal) constants.
(2) Simplifications to reductions for indexof, which fixes proof checking errors in LFSC.
|
|
Fixes #6520. The `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites were
applied too aggressively. Those rewrites attempt to rewrite string
equalities between concatenations where the prefix on one side is
provably shorter than the prefix on the other side. The length of the
shorter prefix is then stripped from the longer prefix. However, cvc5
was not checking whether it was able to strip the length of the full
prefix. If cvc5 cannot strip the full length of the shorter prefix, then
the rewrite does not apply because parts of the shorter prefix would
have to be kept. This commit adds an additional condition that checks
whether the length of the full prefix was stripped.
|
|
This PR improves the integration of the CAD solver with the nl-ext solver in a simple way: we simply use a few of the simple linearization lemmas in combination with CAD by default, significantly improving the performance on QF_NRA.
|
|
The bitblast solver currently uses solving under assumptions for all facts that are sent to the bit-vector solver. For input facts on user-level 0 we can however assert the fact to the SAT solver, which allows the SAT solver to do more preprocessing. This PR adds the option to assert user-level 0 input facts, which is disabled by default.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
applicable (#6529)
Fixes #6510.
This PR also eliminates a deprecated variant mkBooleanTermVariable from SkolemManager.
|
|
This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions.
The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model.
There is no reason to have these two things be separate.
|
|
This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
|
|
This removes the expandOnly flag from expandDefinitions.
The use of expandOnly = true is equivalent to applying top-level substitutions only, which should be done explicitly via Env::getTopLevelSubstitutions. It updates the trust substitutions utility to distinguish apply vs applyTrusted for convenience for this purpose.
This also breaks several dependencies in e.g. expand definitions module.
|
|
|
|
Fixes #6495.
|
|
This is work towards unifying top-level substitutions with model substitutions.
Currently, for model evaluation, BV eager atom preprocessing pass adds mappings (BV_EAGER_ATOM X) -> X to say how (BV_EAGER_ATOM X) should be evaluated in the model. This is not necessary since a rewrite rule (BV_EAGER_ATOM c) -> c for constant c would suffice.
This eliminates the call to addModelSubstitution in that preprocessing pass.
It also makes it so that we don't make true/false themselves into eager atoms.
|
|
This is work towards making the initialization of theory engine, theory models, quantifiers engine more flexible.
This makes it so that the specialized quantifiers models classes (FirstOrderModel) do not inherit from TheoryModel. There is no longer any reason for this, since FirstOrderModel does not have any override methods.
As a result of this PR, there is only one kind of TheoryModel and it is constructed immediately when ModelManager is constructed.
This required refactoring the initialization of when FirstOrderModel is constructed in ModelBuilder classes in quantifiers.
This also avoids the need for casting TheoryModel to FirstOrderModel.
|
|
This is work towards eliminating singletons.
Also, TheoryModel should use the same substitution map as the preprocessor. This is work towards unifying these things, which will be done in a future PR.
|
|
|
|
|
