summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-11-11Support older bash versionsAndres Noetzli
2021-11-11Remove `ConstantMap<Rational>`Andres Noetzli
This is in preparation of having two different kinds (`CONST_RATIONAL` and `CONST_INT`) share the same payload. To do so, we cannot rely on `ConstantMap<Rational>` anymore to map the payload type to a kind. This commit extends support in the `mkmetakind` script to deal with such payloads by adding a `+` suffix to the type. The commit also does some minor refactoring of `NodeManager::mkConst()` and `NodeManager::mkConstInternal()` to support setting the kind explicitly. Finally, the commit addresses all instances where `mkConst<Rational>()` is used, including the API.
2021-11-09[proofs] Alethe: Translate Further Equality rules (#7606)Lachnitt
Implementation of the translation of FALSE_INTRO, FALSE_ELIM, TRUE_INTRO and TRUE_ELIM rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-11-09[proofs] Alethe: Translate Equality rules (#7605)Lachnitt
Implementation of the translation of SYMM, TRANS and CONG rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-11-09Only eliminate lambdas in higher-order elimination if ho-elim is enabled (#7603)Andrew Reynolds
Required for lazy lambdas in HO. Also properly guards the case when the preprocessing pass is a no-op.
2021-11-09Minor optimizations for term database (#7600)Andrew Reynolds
A few minor optimizations for term database. Also collects private/public blocks in quantifiers engine.
2021-11-09Clean up ctest configuration and CI test configuration. (#7620)Aina Niemetz
Previously, on CI, unit tests and api tests were run twice since we use a ctest exclude rule based on labels (-LE) which includes unit and api tests, but then run them separately again. This cleans up the CI test configuration. Further, unit gtest unit tests were added with gtest_add_tests, which adds every test of a unit test binary as a single test target to ctest. In theory, this may speed up testing (because more parallelism) but in practice it slows it down due to the start up overhead. It also clutters CI output. This cleans up the gtest configuration to add the gtest unit tests per test binary rather then per test of a test binary.
2021-11-09[proofs] Generalize trivial cycle detection in LazyCDProofChain (#7619)Haniel Barbosa
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.
2021-11-09[proofs] Alethe: Translate REORDERING rule (#7533)Lachnitt
Implementation of the translation of REORDERING rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-11-09sets: Update theory reference and smt2 examples. (#7602)Aina Niemetz
2021-11-09Preparation for non-constant lambda models (#7604)Andrew Reynolds
This makes our core model construction amenable to (non-constant) lambdas as assignments to function equivalence classes for higher-order. We currently only generate almost constant functions for values of functions. After this PR, we allow explicitly provided lambdas as representatives provided by a theory, which will be used by the higher-order extension. It also makes some improvements to debug check models regarding checking when representatives are equal to their model values.
2021-11-09Make secant points user context dependent (#7567)Gereon Kremer
This PR fixes an issue where the secant points associated with certain transcendental lemmas were not properly cleared when leaving a user context. Closes #4694.
2021-11-09Remove redundant rules for generating Java and Python kinds. (#7616)Abdalrhman Mohamed
This PR addresses an issue where the Ninja build generator errors when either Java or Python bindings are enabled. As shown in the error message below, the error occurs because the build.ninja file generated by CMake contains multiple rules for generating OUTPUT and BYPRODUCTS files.
2021-11-09Add LFSC signature for strings (#7523)Andrew Reynolds
This includes the currently supported rules and cases, although it is highly incomplete.
2021-11-09regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match SMT-LIB. (#7609)Aina Niemetz
This renames kinds REGEXP_EMPTY to REGEXP_NONE and REGEXP_SIGMA to REGEXP_ALLCHAR to match their SMT-LIB representation (re.none, re.allchar). It further renames api::Solver::mkRegexpEmpty() to mkRegexpNone and api::Solver::mkRegexpSigma to mkRegexpAllchar.
2021-11-09Remove `CVC5Message` (#7610)Gereon Kremer
This PR removes the few remaining usages of the CVC5Message() and gets rid of the whole thing.
2021-11-09Remove antlr_tracing.h (#7608)Gereon Kremer
This PR removes the long obsolete antlr_tracing.h. The file contains an ugly hack to make lexer tracing work for ANTLR 3.2. It has been obsolete since ANTLR 3.3 (April 2011). Note that the code is only enabled with -DCVC5_TRACE_ANTLR, a flag that is never used.
2021-11-09Remove more static option accesses (#7582)Gereon Kremer
This PR removes more than half of the remaining static option accesses options::foo() from the theory solvers.
2021-11-09Remove command-verbosity option (#7581)Gereon Kremer
This PR removes the command-verbosity option. It is implemented as a weird special case, and nobody seems to use it anyway.
2021-11-09cmake: Use fastcov for generating coverage reports. (#7594)Mathias Preiner
fastcov is a parallelized gcov wrapper.
2021-11-08Improve rendering of expert options. (#7589)Gereon Kremer
The way expert-only options have been rendered in the documentation emphasized those options, which is exactly what should not be done. This PR changes the rendering to make those options slightly opaque instead.
2021-11-08expand bag.choose operator (#7481)mudathirmahgoub
This PR expands bag.choose operator as a preprocessing step. It also refactors the implementation of choose operator for sets
2021-11-08Add lambda lift utility (#7601)Andrew Reynolds
Towards a lazy approach for handling lambdas in the higher-order extension.
2021-11-08sets: Rename kinds with a more consistent naming scheme. (#7595)Aina Niemetz
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.'.
2021-11-08Evaluate cast-to-real operator (#7599)Andrew Reynolds
Fixes cvc5/cvc5-projects#341.
2021-11-08[proofs] Adding NoSubtype node converter to Alethe (#7587)Haniel Barbosa
Initial version. It'll be improved on demand according to new cases that may lead to issues.
2021-11-08[proofs] Method to convert node representation of Alethe rule (#7598)Haniel Barbosa
2021-11-06Integrate java unit tests into ctest (#7593)Gereon Kremer
This PR properly integrates the java api unit tests into ctest.
2021-11-06Print `unsupported` for unrecognized flags. (#7384)Abdalrhman Mohamed
Fixes #7374.
2021-11-06better traces in node converter (#7590)Haniel Barbosa
2021-11-06Do not use extended rewrites on recursive function definitions (#7549)Andrew Reynolds
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.
2021-11-06Only run regress0 for static build (#7592)Gereon Kremer
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.
2021-11-06Remove `Notice()` in favor of new `verbose()` (#7588)Gereon Kremer
This PR removes the remaining usages of the Notice() macros and uses verbose() instead.
2021-11-06Disable regress2 test. (#7591)Mathias Preiner
2021-11-05Fix exclusion criteria for codatatype model values (#7546)Andrew Reynolds
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.
2021-11-05[proofs] Fix open sat proof (#7509)Haniel Barbosa
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
2021-11-05Eliminate a level of nesting of traversals in theory preprocessing (#7345)Andrew Reynolds
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.
2021-11-05Remove `Chat()` in favor of new `verbose()` (#7586)Gereon Kremer
This PR completely removes the first of several logging macros. Instead of Chat(), we now use verbose(2).
2021-11-05Move functions and lambdas from builtin to uf (#7570)Andrew Reynolds
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.
2021-11-05[FP] Do not assert that model has shared term (#7585)Andres Noetzli
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.
2021-11-05Fix some issues with the java api (#7583)Gereon Kremer
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).
2021-11-05Alethe: Translate CNF rules (#7532)Lachnitt
Implementation of the translation of various CNF rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-11-05Minor changes to circuit propagator (#7584)Haniel Barbosa
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.
2021-11-05Remove many static calls to rewrite (#7580)Andrew Reynolds
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).
2021-11-05Remove quadratic solving in NlModel (#7542)Gereon Kremer
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.
2021-11-05Eliminate `Warning` macro in favor of `EnvObj::warning` (#7575)Gereon Kremer
This PR eliminates almost all usages of the Warning macro, replacing it mostly by calling EnvObj::warning.
2021-11-05Remove a bunch of debugging/logging code from the linear solver (#7576)Gereon Kremer
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.
2021-11-04Add -o sygus-grammar to print auto-generated SyGuS grammars (#7573)Andrew Reynolds
Fixes #5341.
2021-11-04Improve defaults for sygus default grammars (#7553)Andrew Reynolds
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.
2021-11-04Replace the old dump infrastructure (#7572)Andrew Reynolds
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback