| Age | Commit message (Collapse) | Author |
|---|
|
Fixes cvc5/cvc5-projects#341.
|
|
Initial version. It'll be improved on demand according to new cases that may lead to issues.
|
|
|
|
This PR properly integrates the java api unit tests into ctest.
|
|
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.
|
|
It is surprisingly tricky to call ctest properly with multiple -LE arguments (and I actually doubt that the CI version of ctest adheres to its documentation). This PR avoid calling make check (which sets -LE regress[3-4] as a default) and calls ctest directly.
|
|
This PR removes the remaining usages of the Notice() macros and uses verbose() instead.
|
|
|
|
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.
|
|
This PR completely removes the first of several logging macros. Instead of Chat(), we now use verbose(2).
|
|
This is in preparation for adding better native support for handling lambdas in the higher-order extension of the UF theory.
We require that LAMBDA and function types belong to theory UF so that the theory solver is properly notified.
This also splits the utility methods for computing whether a function is "constant" to its own file.
This PR is code move only.
|
|
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 fixes two issues with the java api:
- the JNI_HEADERS variable was set to a non-existent file, which caused the generate-jni-headers target to always rebuilt.
- the directory structure was unnecessarily nested (probably because we use CMAKE_CURRENT_BINARY_DIR instead of CMAKE_BINARY_DIR).
|
|
Implementation of the translation of various CNF rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Previously in a given part of the code a proof would be retrieved only so that it'd be printed. This commit guards that part of the code with whether the trace is on and gives more information in what is printed.
Also changes the style of a call.
|
|
This is the result of a global replace Rewriter::rewrite( -> rewrite( + patching the results.
It makes several classes into EnvObj. Many calls to Rewriter::rewrite remain (that are embedded in classes that should not be EnvObj).
|
|
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.
|
|
This PR eliminates almost all usages of the Warning macro, replacing it mostly by calling EnvObj::warning.
|
|
This PR removes old debugging code from the linear solver.
The removed code was either redundant, already in comments, or manually disabled by a constant false.
|
|
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 simplifies the cmake setup to only build either shared or statically. It also attempts to fix windows builds, both shared and static.
|
|
This PR fixes links to releases and nightly builds. Fixes #7016.
|
|
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 PR makes the collection of trace and debug tags more flexible by allowing for "special tag collectors". They can be used to inject tags that are not used as constant strings, but only assembled dynamically at runtime.
One example is the set of assertions::pre-X and assertions::post-X tags. They are currently handled by Dump, and will be migrated to Trace.
|
|
This does a bit of cleanup by properly calling the option handler instead of trying to manually replicating it. This is way more robust in the face of modifications to the option handlers.
|
|
Now that theories have been refactored to use common interfaces, they
should not access Theory::get() anymore because facts are consumed by
Theory::check().
|
|
This renames Solver::getSeparationHeap to Solver::getValueSepHeap,
Solver::getSeparationNilTerm to Solver::getSepNil and
Solver::declareSeparationHeap to Solver::declareSepHeap.
@mudathirmahgoub @alex-ozdemir @yoni206
|
|
Fixes #5893.
|
|
This PR enables CI for java tests by adding --java-bindings to ci.yml.
It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface.
The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun.
|
|
A debug trace on miplib referred to a possibly out of bounds child.
|
|
This makes all methods for constructing skolems local to SkolemManager.
It removes infrastructure for node manager listeners being notified when skolems are constructed. This was used for 2 things:
(1) The old dumping infrastructure, where skolems could contribute in part to traces to print benchmarks. This code will be deleted soon.
(2) The miplib preprocessing pass, which used this functionality to listen to what skolems were constructed, and subsequently assumed these skolems coincided with what Boolean variables appeared in assertions. This is highly error prone, and has been replaced by a simple traversal to collect Boolean variables in assertions.
This is in preparation for a lazy lambda lifting technique, which will require more infrastructure in SkolemManager.
|
|
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.
|
|
When we eagerly bitblast to the main SAT solver, we have to make sure that we don't use the equality engine in order to not start propagating equalities below BITVECTOR_EAGER_ATOM predicates.
Fixes the nightly failure.
|
|
The code for printing fmf.card does not run in its current location. This PR moves the code to a different switch statement to ensure that it runs.
|
|
This PR is a step towards enabling -o raw-benchmark. It adds printing methods for some of the new commands and fixes some other miscellaneous issues.
|
|
This is an experimental extension of smt2.
|
|
Also includes a fix for the Boolean signature. After the strings PR and this one, the initial LFSC signature is complete.
|
|
|
|
|
|
Fixes #4813
|
|
There is 1 remaining call to Rewriter::rewrite in the bags type enumerator which is not straightforward to eliminate; it should perhaps call an intermediate call to a normal form utility instead of the full rewriter.
|
|
The assertion can be violated in mixed Int/Real arithmetic. The instantiator utility nevertheless safe guards Int vs Real subtyping.
Fixes #7537.
|
