Age | Commit message (Collapse) | Author |
|
Implementation of the translation of SCOPE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
This PR is a step towards enabling raw-benchmark for cvc5 regressions. cvc5 fails to reparse 57 regressions (in regress0) printed be raw-benchmark because they contain multi-line strings in set-info that we don't print between vertical bars right now. This PR fixes that bug and removes 2 commands (derived from set-info commands) that are not used by the parsers anymore.
|
|
This is a modified version of #6137 which accounts for extended rewriting between quantified formulas that are considered alpha equivalent.
It also generalizes the proof rule ALPHA_EQUIV. Notice that if we were to make this rule more pedantic, we would check for variable shadowing during substitution, although this is not currently done.
|
|
Makes a few places do multiplication for Rational directly instead of invoking the rewriter.
|
|
This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.
|
|
This makes the evaluator accessible via EnvObj through the Rewriter. It furthermore removes Rewriter::rewrite from inside the evaluator itself.
Construction of Evaluator utilities is now discouraged.
The include dependencies were cleaned slightly in this PR, leading to more precise includes throughout.
This is work towards having a configurable cardinality for strings, as well as eliminating SmtEngineScope.
|
|
In file `test/unit/api/solver_black.cpp` line 1499,
`for (const std::pair<Term, Term>& t : dmap)` is not the correct way of iterating through the element pairs,
it should be `for (const std::pair<const Term, Term>& t : dmap)` as the keys are immutable.
This triggers a warning on LLVM clang 12.0.1 (not AppleClang) on macOS.
|
|
Towards the strings array solver.
Extensionality for disequalities is disabled by default, but will be used when the strings array solver is enabled.
|
|
This does not yet clean up the usage of Rewriter::rewrite in the arrays
type enumerator yet. Will be cleaned up in a follow-up PR.
|
|
This further cleans up the class declaration in the header to comply
with code style guidelines.
|
|
This PR eliminates some macros for arithmetic proofs, that only slightly simplified access to the produce-proofs option. Now that static access is deprecated, these checks needed to be implemented differently anyway.
|
|
This takes the essential changes from #7218 so that the current ANTLR issues are avoided.
|
|
Implementation of the translation of ASSUME rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of addAletheStep and addAletheStepFromOr. Added stub for AletheProofPostprocessCallback update function that will be populated by subsequent PRs.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
|
|
Fixes #7056. Currently, we introduce a UF for conversions between FP
numbers and reals. This is done as part of `ppRewrite()`. The problem is
that terms sent to `ppRewrite()` are not fully preprocessed yet and the
FP theory solver was storing terms that were not fully preprocessed in a
map for later lookup. For the issue at hand, the conversion term
contained an `ite`, which was later removed. As a result, the theory
solver did not consider the term to be relevant when refining
abstractions. This commit changes the handling of conversion functions
to instead adding purification lemmas for conversion terms when they are
registered. The purification lemmas are needed, because otherwise, we
can't retrieve the model values for the term without the rewriter
interferring.
|
|
|
|
Currently the only transformation it applies is removing attributes from quantifiers. Others may be added later.
|
|
Includes the necessary conversions to LFSC for the core rules of the internal calculus.
|
|
|
|
This commit adds support for enabling interprocedural optimization. The
option is enabled by default for --best builds and cuts down our
executable size from about 33M to 20M.
|
|
This PR adds anchors to the auto-generates command line option documentation. This allows to link to specific options from other parts of the documentation.
|
|
|
|
This refactors the internal tag suggestion mechanism to no longer rely on C-style char arrays, but use a C++ vector of strings instead.
|
|
This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.
One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.
|
|
Added proof postprocessor class to alethe_proof_processor header file.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Added final callback class to alethe_proof_processor header file.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
This PR replaces a write to the options object by a local variable in the simplex procedure base class. The write was used to temporarily lower a limit for a single simplex call.
|
|
This PR does a bit of cleanup in the nonlinear arithmetic code related to the usage of EnvObj.
|
|
Fixes #6531.
This issue also occurs when using `--full-saturate-quant` on facebook benchmarks that combine multiple sequence types.
It does some cleanup on relevant domain in the process.
|
|
Added alethe_proof_processor header file and introduced callback class.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
|
|
This PR removes a handful of options that are no longer used anywhere.
|
|
Implementation file for Alethe proof rules.
|
|
Adds header for Alethe proof rules
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
|
|
Adds smt2 parsing, printing and API support for get-difficulty. Adds unit tests.
|
|
This PR does some final cleanup on the options generation code.
|
|
Before, cvc5 was returning with --parse-only before the code could
reach the code responsible for dumping the raw benchmark. This moves the
check for --parse-only to the appropriate place and updates the
run_regression.py script to use --parse-only.
|
|
Adds support for global assumptions in sygus files.
Also guards against cases of declare-const, which should be prohibited in sygus.
|
|
This adds a few utilities in preparation for the print benchmark utility, which will replace our own dumping infrastructure.
|
|
This method will be called from SmtEngine in the implementation for (get-difficulty).
|
|
This PR refactors the code generation for options/<module>_options.(h|cpp).
|
|
This PR refactors the generation of the command line help for sphinx to a function, just like all the other code generation methods.
|
|
This refactor additionally removes the caching for urem/udiv cases when
bit-blasting udiv/urem and eliminates the only rewrite() calls in the
bit-blaster. Caching is not required since repeated calls to udiv/urem
with the same arguments will produce the same circuit. Further, the rewrite()
calls during bit-blasting would further complicate the recording of
bit-blasting proofs and hence is removed.
|
|
This commit refactors the proof bit-blaster to properly track the pre- and post-rewrites in bbAtom(). The individual bit-blast steps are recorded in a term conversion proof generator. The overall bit-blast proof is stored in a BitblastProofGenerator, which tracks the pre- and post-rewrite and includes the bit-blast proof of the TCPG.
|
|
Printing the original benchmark is simple, as it is exactly the commands we execute.
This removes the previous code from SmtEngine, which is currently broken.
|
|
This removes TheoryState::getSatContext() and
TheoryState::getUserContext().
|
|
This also introduces the produceDifficulty option which is analogous to produceUnsatCores.
It requires another unsat cores mode PP_ONLY, indicating that we are only tracking proofs of preprocessing. This option should perhaps be renamed to proofMode instead of unsatCoresMode, since its use is more general than for unsat cores. This will be addressed in a future refactoring.
|
|
This PR adds a new api::Solver::isOutputOn() method, including unit tests for both isOutputOn() and getOutput().
|