| Age | Commit message (Collapse) | Author |
|---|
|
This further renames kind SET_INTERSECTION to SET_INTER.
|
|
Required for lazy lambdas in HO.
Also properly guards the case when the preprocessing pass is a no-op.
|
|
Previously the trivial cycle check only covered the case in which the currently-being-expanded assumption `A` had as its stored proof node `pf` an assumption proof justifying itself. However, it can be the case that `pf` is not an assumption proof, but a proof that nevertheless has `A` as one of its free assumptions. This commit generalizes the trivial cycle check to account for this.
|
|
This PR removes the command-verbosity option. It is implemented as a weird special case, and nobody seems to use it anyway.
|
|
This PR expands bag.choose operator as a preprocessing step.
It also refactors the implementation of choose operator for sets
|
|
This prefixes sets kinds with SET_ and relation kinds with
RELATION_. It also prefixes the corresponding SMT-LIB operators with
'set.' and relation operators with 'rel.'.
|
|
Fixes #7374.
|
|
Leads to potential non-idempotent behavior in the rewriter.
The issue cannot be replicated on master, but this safe guards this case anyways.
Fixes #5278.
|
|
|
|
This fixes codatatype model value construction.
Model construction for codatatypes is non-standard since it requires analyzing whether (possibly recursively defined) terms are alpha equivalent to others during model construction. This is currently handled as a special case within the theory model builder. (This should eventually be moved somewhere more appropriate via a new callback to theory).
This fixes the criteria which was too permissive about which values can be used in models. We now exclude values that match the skeleton of representative codatatype terms. Previously we additionally required that the terms were bisimilar.
Fixes #4851.
|
|
Improves how LazyCDProofChain handles cycles, which fixes a particular case triggered by the added regression. Also makes LazyCDProofChain::getProofFor more robust in that when it can't connect the requested fact it yields an assumption proof node.
Fixes cvc5/cvc5-projects#324
|
|
This simplifies the theory preprocessor so that it does not rely on the term formula removal to do a nested traversal. Instead, it only relies on its "runCurrent" method.
Notice that this PR essentially replaces TheoryPreprocessor's theoryPreprocess method with TermFormulaRemoval's runInternal method, while adding the required call to rewriteWithProof and preprocessWithProof as post-rewrites. This is far simpler than the previous method, which invoked nested traversals using TermFormulaRemoval::run.
There are two things that will be improved in follow up PRs:
The initial full rewrite step in the theory preprocessor can be merged into the main traversal of theory preprocess (I believe this is why we are slower on nec benchmark than we were previously),
We should eliminate the traversal methods from TermFormulaRemoval altogether, as they are now subsumed by the theory preprocessors main traversal. This will require refactoring how "early ITE removal" works, as this is the only user now of TermFormulaRemoval::run.
Note we should probably performance test this change.
This incidentally fixes #6973, as the previous theory preprocessing code was to blame for that issue.
|
|
Fixes #7569. Currently, the FP solver asserts that
m->hasTerm(sharedTerm) is always true for the real term in the
conversion from real to floating-point value. This is not necessarily
the case because the arithmetic solver computes values for the variables
in the shared terms but not necessarily for the terms themselves. This
commit removes the assertion and instead relies on the fact that a later
assertion checks that m->getValue(sharedTerm).isConst(), which is the
property that we are actually interested in.
|
|
This PR removes obsolete code from NlModel concerned with solving quadratic equations. This code is only used on nonlinear real problems where the cad solver is not used.
|
|
Fixes #5341.
|
|
We now add constants from the conjecture to default grammars by default. We also ensure that integer constants are used as real constants when applicable.
|
|
This deletes the old dumping infrastructure, which due to changes in our usage of SolverEngine does not print valid benchmarks.
This eliminates the concept of a "NodeManagerListener" which has been problematic to maintain.
This PR reimplements the --dump=assertions:pre-X and --dump=assertions:post-X as -t assertions::pre-X and -t assertions::post-X. This is done in a self contained utility method in ProcessAssertions using smt::PrintBenchmark and does not require keeping the rest of the code in sync.
The other dumping tags are deleted for now, and will be reimplemented as needed.
|
|
This PR does the first step in consolidating our various output mechanisms. The goal is to have only three major ways to output information:
- verbose(level) prints log-like information to the user via stderr, -v and -q increase and decrease the verbosity, respectively.
- output(tag) prints structured information (as s-expressions) to the user via stdout, -o enables individual tags.
- Trace(tag) prints log-like information to the developer via stdout, -t enables individual tags.
While Debug and Trace (and eventually Dump) will be combined within Trace, all of Warning, Message, Notice and Chat will be combined into verbose.
|
|
This PR enables the CDCAC solver for quantified logics with reals, but no integers. Also, it disables SyGuS if no integers are used. The regression is a benchmark that is only solved with this new configuration.
|
|
This properly formalizes all string skolems used in reduction and preprocessing. This avoids proof checking failures due to non-deterministism when checking steps for these modules.
Fixes cvc5/cvc5-projects#334. Fixes cvc5/cvc5-projects#331.
|
|
Preregistering terms must always add them to the equality engine of TheoryFp, otherwise there may be preregistered terms that do not occur in the equality engine of TheoryFp, thus leading to crashes during theory combination.
Fixes cvc5/cvc5-projects#329.
|
|
This is an experimental extension of smt2.
|
|
Fixes #4813
|
|
The assertion can be violated in mixed Int/Real arithmetic. The instantiator utility nevertheless safe guards Int vs Real subtyping.
Fixes #7537.
|
|
This commit removes the old bit-vector solver code.
|
|
This PR fixes an issue where we did compute upwards closure (for join, product, etc.) on equivalence classes whose membership cache had already been initialized (perhaps recursively from the computation of upwards/downwards closures on other terms).
It also generalizes the fix from #7511. Instead of doing explicit splitting, we mark shared terms and let theory combination (when necessary) do splitting. This is required to fix a more general version of the benchmark from the previous PR, where instead now a term c+1 is used in a position that is relevant to a join.
It disables a regression that times out after these fixes, and does further cleanup.
|
|
This PR fixes soundness issues found by cvc5 fuzzy sygus when it answers unsat for sat problems.
One error was with the rewrite rule (bag.count x (bag x c) = c which did not account for cases when c is negative.
This conflicts with fact that all multiplicities are non-negative.
Another error was that the difference_remove inference rule didn't consider the negative case for (count e B)
(= (count e (difference_remove A B)) (ite (= (count e B) 0) (count e A) 0))) ; not enough
(= (count e (difference_remove A B)) (ite (<= (count e B) 0) (count e A) 0))) ; the right rule
|
|
This PR fixes a bug found by cvc5 fuzzy sygus.
|
|
This PR fixes the proof generated for the nonlinear monomial bounds check lemmas. In some cases, it implies an equality (multiplied by a monomial) not from the equality but from the two weak inequalities. We now properly detect this special case and add a rather involved proof.
Fixes cvc5/cvc5-projects#326.
|
|
(#7526)
This fixes a bug in HO model construction where we were communicating information about irrelevant function terms to the model, leading to incorrect models.
|
|
This PR fixes another double negation issue in the circuit propagator.
Fixes cvc5/cvc5-projects#332.
|
|
Also improves a few traces.
Fixes cvc5/cvc5-projects#330
|
|
This PR is step towards enabling -o raw-benchmark for regressions. It creates a define-fun command for each named term. This allows us to reparse dumped benchmarks containing named terms, but we still lose track of those terms and do not print them in response to (get-assignment) and (get-unsat-core) commands. This PR also simplifies the interface for DefineFunCommand interface and removes support for (define ...) command.
|
|
Given
```smt2
(set-info :source (0 1 True False x ""))
```
`cvc5` currently prints the command below with `-o raw-benchmark`
```smt2
(set-info : |(0 1 True False x )|)
```
This PR ensures that `cvc5` correctly prints the command by
- Parsing and storing keywords eagerly before parsing their values.
- Removing pre-processing steps done to symbols and string literals.
|
|
Fixes cvc5/cvc5-projects#307.
|
|
Fixes #7504.
|
|
Fixes cvc5/cvc5-projects#316.
|
|
Since we apply a lazy schema for app completion, this may omit terms from the care graph that are relevant for theory combination. This corrects the care graph for UF when higher-order is enabled by considering the HO_APPLY version of all partially and fully applied prefixes of APPLY_UF terms during TheoryUF::computeCareGraph.
Fixes #5741. Fixes #5744. Fixes #5201. Fixes #5078. Fixes #4758.
|
|
This fixes a model unsoundness issue in the theory solver for relations.
|
|
These rewrites introduce the possibility of non-termination in the rewriter, as demonstrated in the included regression.
Instead, these rewrites are now moved to the extended rewriter.
|
|
Fixes #6766.
|
|
This PR adds the missing handler declaration for the --version option.
Fixes #7505.
|
|
Previously the check for whether the original conclusion of the MACRO_RESOULTION step was a singleton was incomplete. Now the test is made the proper way.
Depends on #7497.
Fixes cvc5/cvc5-projects#318
|
|
Fixes cvc5/cvc5-projects#317
|
|
This avoids cyclic proofs in a rare case where theory explanations involve an equality and its symmetric form.
This PR disables auto-symmetry on lazy proofs used for theory explanations, which is slightly less convenient but avoids potentials for cyclic proofs. Note this complication would not arise if the theory engine did not allow non-rewritten equalities to be propagated between theories.
Fixes cvc5/cvc5-projects#311.
|
|
Fixes cvc5/cvc5-projects#319
|
|
Fixes #4656. Fixes #5234. These do not occur on master.
|
|
Fixes #7385.
Option --sygus-inst relies on the quantifier-free sygus extension of datatypes, which does not support incremental mode. Updating it to support incremental is a long term project.
Until this is complete, --sygus-inst should not be run in incremental mode.
|
|
This adds a new option for --sygus-query-gen=unsat to generate unsat queries (previously, only satisfiable queries were supported).
The algorithm can be seen as a variant of abduction where we conjoin predicates that both (1) refine the current model and (2) avoid repeated unsat cores.
It does some minor refactoring of ExprMinerManager to support the new module.
|
|
Previously, we asserted global declarations as substitutions/formulas just before check-sat. This is not ideal since the current set of assertions can be preprocessed without having knowledge of definitions of defined functions. Moreover, this could lead to model unsoundness if it were the case that a defined symbol was solved during preprocessing.
Fixes #7479. In that example, y was solved for true and then we failed to overwrite y with its definition (> x 0), hence dropping the definition. Now, y is defined as (> x 0) before we preprocess.
|
