| Age | Commit message (Collapse) | Author |
|---|
|
Review comments by @nafur from #5304.
|
|
Our first support for seq.nth eliminated it eagerly during expandDefinitions.
This PR changes that, by eliminating it lazily, as done with other extended string operators.
|
|
This moves the CLN implementation of member functions of class Integer from
the header to the .cpp file. This only moves code, and adds documentation for
previously undocumented or poorly documented functions.
Analogous to #5190.
|
|
Previously the binary resolution checker was:
- Checking applications in which for a pivot (not l) the literal (not l) would be eliminated from the first clause and l from the second because double negation was handled implicitly. Now whether the binary resolution is such that the pivot is removed as is from the first clause and negated from the second, or the other way around, is marked via an argument.
- Not producing false the remaining set of literals after resolution was empty.
This commit also updates the informal description of the rule accordingly, as well as to clarify the behavior when the pivot does not occur properly in the clauses (in which case the rule application corresponds to weakening).
Co-authored-by: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
|
|
This updates and improves assertions pipeline and preprocess generator so that they avoid cyclic proofs and have better infrastructure for catching pedantic failures.
This is in preparation for making the non-clausal-simplification pass proof producing.
|
|
This sets up the preprocessing pass context in preparation for proof production.
This PR makes the top level substitutions map into a TrustSubstitutionMap, the data structure that applies substitutions in a way that tracks proofs.
This PR also makes the "apply subst" preprocessing pass proof producing.
|
|
|
|
This ensures we don't segfault if the pending lemma vector is cleared while we are processing it. This is potentially possible in datatypes currently. Fixes #5236.
|
|
This PR makes it so that cyclic checks are only performed eager when proofNewEagerChecking is true.
It refactors the existing cyclic check in ProofNodeToSExpr to have a more consistent style, and adds a cyclic check to getFreeAssumptions.
|
|
This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify.
This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager.
|
|
Trust substitution is a data structure that is used throughout preprocessing for proofs.
This adds its implementation.
|
|
This updates the SMT proof postprocessor with additional stats. It also adds the feature to handle conjunctions as substitution, e.g. a child proof concluding (and (= x t) (= y s)) is interpreted as a substitution for x, y, whereas previously we insisted they must be provided separately.
|
|
Avoids use of macro rules in a few places.
|
|
This refactors the SMT-level model object so that it is a wrapper around TheoryModel instead of a base class. This inheritance was unnecessary.
Moreover, it removes the virtual base models of the SMT-level model which were based on Expr. Now the interface is more minimal and in terms of Node only.
This PR further simplifies a few places in the code that interface with the SmtEngine with things related to models.
|
|
Fixes #5280.
Previously we were checking for nested recursive datatypes in expandDefinitions. This does not catch cases where the only terms of a malformed nested recursive datatype are variables. The proper place to check is in preRegisterTerm. The benchmark from that issue now gives an error.
|
|
The bv-to-int preprocessing pass has a cache that maps each BV node to its translated integer node.
In case the BV node is a function symbol, it's translated integer node is a fresh function symbol.
On current master, if we later process this fresh function symbol in the preprocessing pass, we again create a fresh function symbol as its translation. This is unsound, and was discovered in #5281, whose benchmark is added to regressions.
Closes #5281 if merged.
|
|
This adds an inference enumeration for datatypes, which is analogous to what is done in strings and non-linear arithmetic. Inferences are informal identifiers that serve the purpose of (1) debugging the code, (2) providing hints on how proofs can be reconstructed.
This PR also splits the InferenceManager file in datatypes into 2.
|
|
Use a farkas proof to prove one of arithmetic's lemmas.
These changes were checked-out directly from proof-new, without modification.
|
|
This PR fixes issue #5269 of unnecessary calling TheorySetsRels::areEqual in a product relation (which compares the rightmost element of the first child with the leftmost element in the second child). This may violate an assertion in TheorySetsRels::areEqual that the types of the 2 elements should be the same
|
|
There are 3 potential modes to lazily treat the iand operator:
(1) by value (typical CEGAR loop)
(2) by sum (lazily expanding each iand node into a sum of ITEs)
(3) by bit-wise equalities (lazily expanding each iand node into bit-wise equalities)
This PR implements (2).
The relevant option is added to existing tests, and a new test is added. In a few other tests, some options are removed to make them run faster.
|
|
|
|
Very simple, just threading the proofs through.
|
|
Errors with these methods were encountered while working on new techniques for arithmetic preprocessing.
Also, there is obvious inefficiency since approximations for constants are being computed when certain traces are disabled.
|
|
Threads conflict proofs through TheoryArithPrivate.
Mostly just wiring things up.
|
|
This commit fixes several issues with bv-to-int preprocessing pass, mostly raised by @ajreynol:
1. make sure to rewrite the processed node before and after processing it
2. use the new `mkAnd` function
3. remove `--no-check-unsat-cores` from tests whenever possible
4. add new tests from #5230 . These tests now pass, and so this PR closes #5230 if merged. This also makes #5253 redundant.
5. remove an unused test
|
|
|
|
Includes:
T/F splitting lemmas for any arith constraint
Unate lemmas produced early on
The hard part is proving the unate lemmas. In general, they are all implied by 2-constraint farkas proofs, so we ultimately map them all down to proveOr, which constructs that proof.
make check was happy with this change. Hopefully the CI agrees :).
|
|
This class is of general use, not just as the overall maintainer of proofs of preprocessing, but also locally within preprocessing passes. This generalizes the interface slightly and also does some minor cleaning.
|
|
Some of the interfaces in the proof rule checker are unnecessary now and can be deleted.
This also updates STRING_TRUST to have pedantic level 2.
|
|
files. (#5241)
|
|
This adds 2 new rules for convenience to the Boolean checker.
|
|
This updates the proof node updater with a mergeSubproofs field which automatically merges subproofs in the same SCOPE that prove the same thing. This is currently enabled by default, it is now configurable and disabled by default.
|
|
The bv-to-int preprocessing pass introduces large ite terms that correspond to truth tables of bvand for various bit-widths.
Previously there were two inefficiencies in those tables:
They weren't being cached
The ite was not optimized
This PR adds a cache for the tables that induce the ite terms.
In addition, it computes smaller ite terms by computing the most common value of each table and using it as the default value of the ite.
|
|
This option has a number of subtle bugs, it should be reimplemented if/when finite-model-find is refactored. It is not high priority enough to maintain.
This does some additional cleaning of the uf cardinality extension, some methods changed indentation.
Fixes #5239, fixes #4872, fixes #4865.
|
|
This eliminates all use of Expr in the SmtEngine except in a few interfaces (setUserAttribute, getAssignment) whose signature is currently in question.
The next steps will be to (1) eliminate Expr from the smt/model.h interface, (2) replace Type by TypeNode in Sort.
|
|
enabled. (#5248)
This ensures that arrays is not the owner of uninterpreted sorts if uf-ho or finite-model-find are enabled. In these cases, the UF solver implements special techniques (cardinality, ho reasoning) that should take priority.
Fixes #5233.
|
|
This PR adds three instantiation modes to the SyGuS instantiation module.
|
|
This PR adds a new utility function to convert a poly::Polynomial back to a cvc4 Node.
|
|
This PR provides an SMT version of the following SMT commands:
get-instantiations
block-model
block-model-values
get-qe
get-qe-disjunct
command.cpp now calls those functions instead of their SmtEngine counterparts. In addition, SEXPR is now an API kind.
|
|
This PR is essentially a code move.
It moves the code that translates bvand from the bv_to_int preprocessing pass to a new class IAndHelper, in the new files nl_iand_utils.{h,cpp}. The goal is to have this code in a place which can be shared between the bv2int preprocessing pass and the iand solver.
Future PRs will:
Optimize this utility
Make use of it in the iand solver
The code in nl_iand_utils.{h,cpp} is almost completely a move from bv_to_int.{h,cpp}. The changes are all minor, and include, e.g., the following changes:
the node manager is no longer a member, and so is the constant 0.
using the oneBitAnd function directly, without a function pointer.
|
|
Use the Node-returning variants of
Constraint::externalExplainByAssertions in TheoryArithPrivate locations
that aren't computing proofs.
The problem is that the TrustNode returning variant requires that arith
has stored an externally valid literal for the constraint, which is not
always the case.
This is what we did on proof-new, I just forgot.
|
|
Threads proofs through arith::Constraint's machinery for explaining
constraints. Changes, by function:
externalExplainByAssertions:
introduce scope to prove the implication
externalExplainForPropagation:
introduce scope to prove the implication
externalExplainConflict:
use other machinery to prove conflicting constraints
use the CONTRA rule
introduce scope to close the conflict proof
Future commits will pick up these proofs in theory_arith_private.cpp.
Future commits will prove the "split" lemmas produced in constraint.cpp
|
|
Fixes #5163. When `:global-declarations` is disabled (the default), then
`(reset-assertions)` should remove all declared and defined symbols. Before
this commit, we would remove the defined function from `SmtEngine` but the
parser would not remove it from its symbol table because the symbol was defined
at (what it considered) level 0. Level 0, however, is reserved for global
symbols that we never want to remove.
This commit adds an additional global `pushScope()`/`popScope()`, similar to
what we have in `SmtEngine`. As a result, user-defined symbols are now defined
at level 1 and get removed from the `SymbolTable` when `(reset-assertions)` is
called. The commit also makes sure that symbols defined by the logic are
asserted at level 0, so that they are not removed by `(reset-assertions)`. It
adds a flag to `defineType` to ignore duplicate definitions because some
symbols are defined by multiple logics, which leads to a failing assertion when
inserting them both at level 0 in the hashmap of the `SymbolTable`. E.g.
strings and integer arithmetic both define `Int`. The commit also fixes
existing unit tests that fail with these stricter semantics of
`(reset-assertions)`.
Signed-off-by: Andres Noetzli <noetzli@amazon.com>
|
|
(#5223)
This simplifies the approach for wrongly-applied selectors whose range type involves e.g. uninterpreted sorts. These cases are particularly tricky since uninterpreted constants should never appear in facts or lemmas.
Previously, the rewriter had special cases for either making a ground term or value, and a purify step was used to eliminate the occurrences of uninterpreted sorts afterwards.
This PR leverages mkGroundTerm in this inference instead, and makes the rewriter uniformly use mkGroundValue.
This also required making the type enumerator for datatypes more uniform. In particular, we require that the first value enumerated by the type enumerator is of the same shape as the term required by mkGroundTerm, or else debug-check-model will fail. This is due to the fact that now the inference for wrongly applied selectors uses terms while the rewriter uses values. The type enumerator is updated so that recursive codatatypes also first take mkGroundValue as the zero term, when they are well-founded. Previously this was skipped since the codatatype enumerator uses a different algorithm for computing its ground terms.
This is in preparation for further work on optimizations and proofs for datatypes.
|
|
This is a common pattern that is required in several places in preprocessing.
|
|
This completes proof support in TheoryEngine.
The main addition in this PR is to make its getExplanation method proof producing.
|
|
This includes several subtle issues encountered in the past month based on our regressions.
It also improves the expansion forms of MACRO_ rules to use EQ_RESOLVE instead of a TRUE_INTRO/TRUE_ELIM scheme. This is both more compact and avoids cyclic proofs for some corner cases of proofs with Boolean constant equalites.
|
|
Gets the correct `NodeManagerScope` for getting the `toString` of a term, op, or sort. The following program had strange output:
```
#include "cvc4/api/cvc4cpp.h"
using namespace CVC4::api;
using namespace std;
int main()
{
Solver s;
Term x = s.mkConst(s.getIntegerSort(), "x");
cout << "x = " << x << endl;
Solver s2;
cout << "x = " << x << endl;
return 0;
}
```
It was outputting:
```
x = x
x = var_267
```
Fixing the scope makes the output `x = x` both times, as expected.
|
|
Threads proofs through the flow of information from the equality engine
into the theory of arithmetic.
Pretty straightforward. You just have to bundle up information from the EE.
|
|
|
