| Age | Commit message (Collapse) | Author |
|---|
|
This includes support for some trusted rules (whose use is to come). It also modifies THEORY_REWRITE so that it is a "trusted" rule, that is, it is not re-checked. The reason for this is that TheoryRewriter is not deterministic. An example of non-determinism in TheoryRewriter are rules that introduce bound variables (e.g. quantifiers rewriter) since these bound variables are fresh each time it is invoked. Non-deterministic theory rewriters cannot be rechecked, which was leading to failures on proof-new at proof check time. The other way to fix this would be to cache TheoryRewriter responses, but then the checker would only be verifying that the caching was being done properly. This is not worthwhile.
|
|
This makes the theory preprocessor proof producing in the new infrastructure, which involves updating its interfaces to TrustNode in a few places.
|
|
This class is responsible for the connection between terms and their witness form in the final proof.
|
|
This adds proof support in the term formula removal pass.
It also refactors this class heavily so that its interface is more intuitive and does not depend on AssertionPipeline.
|
|
This commit changes UninterpretedConstant to use TypeNode instead of
Type.
|
|
This adds support for skeleton proofs in the rewriter (REWRITE -> THEORY_REWRITE).
It adds "extended equality rewrite" as a new method of the rewriter/theory rewriters.
The unit test of this feature should be added on a followup PR.
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
|
|
This commit changes ArrayStoreAll to use Node/TypeNode instead of
Expr/Type.
|
|
This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine.
It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.
|
|
This includes 4 changes:
Theory constructor takes a ProofNodeManager,
Theory::explain returns a TrustNode (of kind PROP_EXP),
Theory::expandDefinitions returns a TrustNode (of kind REWRITE),
Theory::ppRewrite returns a TrustNode (of kind REWRITE).
These are all currently planned updates to the interface of Theory.
This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support.
This PR is also contingent on the performance tests for proof-new on SMT-LIB.
|
|
Fixes #4685.
A recent commit #4661 added assertions for checking whether a witness rewrite corresponded to a legal elimination. #4685 demonstrates that these assertions can be violated and hence should be checked to ensure the rewrite is sound.
|
|
Previously, the proof rule checkers were run on witness form for convenience. However, it is more flexible for the sake of the internal calculus to run on Skolem forms. The main reason is that the conversion to/from witness form does not preserve terms that contain witness. Our preprocessing steps rely on using witness terms. This design change additionally simplifies a lot of the code of the builtin proof rule checker.
Instead, witness forms can be queried on an as-needed basis, e.g. in MACRO_SR_PRED_TRANSFORM.
|
|
Proof checking failures revealed that we are not rewriting witness for Boolean variables (witness ((x Bool)) x) ---> true and (witness ((x Bool)) (not x)) ---> false.
Also adds 2 assertions that are required for elimination (witness ((x T)) (= x t)) ---> t. These assertions should always hold due to the witness terms we construct.
|
|
|
|
This makes the conversion between lambdas and arrays, done in the theory builtin rewriter and used in higher-order model construction, robust to function definitions in terms of AND/OR.
This also improves tracing and makes a few parts of the code adhere to code guidelines.
|
|
This is a common class for adding steps for theory-specific proof rules into a ProofStepBuffer.
|
|
This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing.
This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form.
Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler.
Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal.
|
|
This adds the proof checker for TheoryBuiltin, which handles the core proof rules (SCOPE and ASSUME) and all proof rules corresponding to generic operations on Node objects. This includes proof rules for rewriting and substitution, which are added in this PR.
|
|
When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.
This PR ensures we only eliminate variables when v contains only evaluated operators.
Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.
Fixes #4500.
|
|
Renamed operator CHOICE to WITNESS, and removed it from the front end
|
|
This commit adds statistics for string rewrites. This is work towards proof
support in the string solver. At a high level, this commit adds a pointer to a
`SequenceStatistics` in the rewriters and modifies
`SequencesRewriter::returnRewrite()` to count the rewrites done. In practice,
to make this work requires a couple of changes, some of them temporary:
- We can't have a single `Rewriter` instance shared between different
`SmtEngine` instances anymore. Thus the `Rewriter` is now owned by the
`SmtEngine` and calling the rewriter retrieves the rewriter associated with
the current `SmtEngine`. This is a temporary workaround before we get rid of
singletons.
- Methods in the `SequencesRewriter` and the `StringsRewriter` are made
non-`static` because they need access to the statistics instance.
- `StringsEntail` now has non-`static` methods because it needs a reference to
the sequences rewriter that it can call.
- The interaction between the `StringsRewriter` and the `SequencesRewriter`
changed: the `StringsRewriter` is now a proper `TheoryRewriter` that inherits
from `SequencesRewriter` and calls its `postRewrite()` before applying its
own rewrites (this is essentially a reversal of roles from before: the
`SequencesRewriter` used to call `static` methods in the `StringsRewriter`).
- The theory rewriters are now owned by the individual theories. This design
mirrors the `EqualityEngine`s owned by the individual theories.
|
|
Fixes #4170.
|
|
Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).
|
|
Added the operator choice to Smt2.g and Cvc.g.
Removed the unused parameter hasBoundVars from TheoryModel::getModelValue
|
|
This standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up.
This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps).
Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans).
|
|
The lambda rewriter was not robust to the case where the lambda of the
array representation contained a disequality, e.g. `not(x = 1))`. It
would process it as `ite(not(x = 1), true, false)` instead of `ite(x =
1, false, true)`, which meant that it wasn't able to turn it into an
array representation when checking const-ness. Additionally, the
rewriter had issues when the lambda was of the form `ite((= x c1), true,
(= y c2))` (after turning it into an array and then into a lambda)
because it is expecting the false branch of the `ite` to not contain `y`
variables, making it non-constant despite the array being constant. This
commit solves that issue by normalizing `ite(not(c), x, y) ---> ite(c,
y, x)`.
|
|
|
|
Fixes #3536. The type checker for the chain operator was calling the
rewriter. However, the floating-point rewriter was expecting
`TheoryFp::expandDefinition()` to be applied before rewriting. If the
chain operator had subterms that were supposed to be removed by
`TheoryFp::expandDefinition()`, the FP rewriter was throwing an
exception. This commit fixes the issue by not calling the full rewriter
in the type checker but by just expanding the chain operator. This is a
bit less efficient than before because the rewriter does not cache the
result of expanding the chain operator anymore but assuming that there
are no long chains, the performance impact should be negligible. It also
seemed like a reasonable assumption that the rewriter can expect to run
after `expandDefinition()` because otherwise the rewriter has to expand
definitions, which may be too restrictive.
|
|
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.
|
|
|
|
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
|
|
|
|
The rewriter for lambda is currently too aggressive, there are cases like:
lambda xy. x = y
that are converted into an array representation that when indexing based on x gives (store y true false), which is subsequently converted to:
lambda fv_1 fv_2. fv_1 = y
where fv_1 and fv_2 are canonical free variables. Here, y is used as index but was not substituted hence is incorrectly made free.
To make things simpler, this PR disables any rewriting for lambda unless the array representation of the lambda is a constant, which hardcodes/simplifies a previous argument (reqConst=true). This fixes a sygus issue I ran into yesterday (regression added in this PR).
Some parts of the code were formatted as a result.
|
|
|
|
Adds missing override keywords.
|
|
|
|
|
|
Includes:
- Basic rewriting for choice functions in the builtin rewriter,
- Do not consider more than one equal term in ceg instantiator (helps cases where we have a
repeated pattern of duplicate instantiations),
- Do not introduce dummy extract equalities in the cbqi-bv-rm-extract pass (dummy concat
equalities suffice).
- Do not consider extracts in nested quantified formulas in the cbqi-bv-rm-extract pass.
|
|
* Implement enumerator for functions.
* Address review.
* Minor
* Format
* Improve comment.
* Format
|
|
* Initial support for Hilbert choice operator.
* Clang format.
* Fix
* Minor
|
|
* Remove restrictions about function types
* Introduce notion of first-class type, improve assertions, add comment on equality type rule.
* Update comment
|
|
* Remove unhandled subtypes, which consequently makes typing rules uniformly stricter based on weakening the subtype relation. Ensure coercions in the smt2 and cvc parser for Real decimal constants whose type is Integer. Ensure type annotations are computed during preRewrite to ensure rewriting (which does not preserve types) does not impact term construction for parametric datatypes. This fixes issue #1048 (we now give an type exception).
* Update unit test for parametric datatypes to reflect new subtyping relation.
* Remove deprecated test.
* Make array construction for lambdas work with new subtype relations to handle lambdas like (lambda ((x Int) (y Int)) (ite (= x 0) 0.5 0.0)).
|
|
Add isConst check for lambda expressions by conversions to and from an Array representation where isConst is implemented. This enables check-model to succeed on higher-order benchmarks. Change the builtin rewriter for lambda to attempt to put lambdas into constant form. Update regression.
|
|
Disable support for subrange and predicate subtypes (which were only partially supported previously).
|
|
|
