| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Adds support for global assumptions in sygus files.
Also guards against cases of declare-const, which should be prohibited in sygus.
|
|
|
|
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`.
|
|
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().
|
|
|
|
This PR refactors the code generation for options::getInfo()
|
|
This PR adds main/options.cpp to cmake. Also, it removes the old (now obsolete and unused) options script.
|
|
This PR reorders some options generation code that is out of order after some merges.
|
|
This PR refactors the code for options parsing.
|
|
This commit better integrates the StatisticsRegistry with the environment. It makes the registry an `EnvObj` itself and adds a getter to `EnvObj` to get the registry. It also refactors parts of cvc5 to use this new mechanism to obtain the registry instead of using the (global, static) `smtStatisticsRegistry()` function.
|
|
Add comment that partial operators are one reason that the current
assertion cannot be checked.
|
|
IsPowerOfTwo rule is specific to the BvIntroPow2 preprocessing pass and should not be a general bit-vector rewrite rule.
|
|
|
|
|
|
This PR is based on #7171
|
|
|
|
Fixes #7002.
|
|
This commit adds Op.java OpTest.java and cvc5_Op.cpp to the java api.
|
|
Currently, we are using non-standard attributes. With C++17, all the
attributes that we use regularly are now standardized. This commit
replaces the compiler-specific attributes with standard ones.
|
|
This moves a large portion of the `finalizeLogic` method to more appropriate places.
It also fixes an issue : `opts.datatypes.dtSharedSelectorsWasSetByUser` was checked with wrong polarity, making a previous commit not effective.
|
|
|
|
This PR refactors how we generate the command-line help message.
|
|
This PR is the first step in replacing options access via options::foo() to using the environment (via EnvObj and options().module.foo). It replaces all such options accesses in the preprocessing passes.
|
|
|
|
|
|
Allow access to the Output() macro via the API.
|
|
Towards supporting a (get-difficulty) command.
This tracks an estimate of the difficulty of preprocessed assertions during solving. It will be connected to TheoryEngine (via RelevanceManager) in a followup PR.
|
|
This is work towards supporting a (get-difficulty) command.
This is a helper class for transforming the difficulty of preprocessed assertions to difficulty of the input assertions.
|
|
The use of shared selectors may have fairly negative effects when combined with E-matching. The issue is that it allows too many things to match. When shared selectors are disabled, a selector trigger like s(x) will only match terms that access the field of the constructor associated with s. When we use shared selectors, s(x) is converted to e.g. shared_selector_D_Int_1(x), which in turn matches applications of selectors of the same type over any constructor.
This PR disables shared selectors when quantifiers are present and SyGuS is not used.
It also disables shared selectors in single invocation subcalls, thus fixes #3109.
It further makes a minor fix to the datatypes rewriter to ensure that rewritten form does not depend on options.
|
|
This commit removes TheoryState::options() by changing more classes to
EnvObjs.
|
|
This was a predecessor to the evaluator and TermDbSygus::rewriteNode that is no longer necessary.
This refactors the code so that evaluateWithUnfolding is replaced by rewriteNode as necessary throughout the SyGuS solver.
Note that in a few places, the extended rewriter was being used where TermDbSygus::rewriteNode (which also evaluates recursive function definitions) should have been used.
|
|
These are utilities used for two-pass printing of LFSC proofs.
|
|
This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache.
It makes minor cleanup to the dependencies of this method.
|
|
This PR refactors the code generation and the generate code for options::set().
|
|
This PR fixes / improves the comments in the options scripts.
|
|
This PR does a couple of minor cleanups related to options.
|
|
This PR refactors the options code generation for the options/options.h/.cpp files.
|
|
This PR:
Adds extendedRewrite to EnvObj and Rewriter.
Eliminates static calls to Rewriter::rewrite from within the extended rewriter. Instead, the use of extended rewriter is always through Rewriter, which passes itself to the ExtendedRewriter.
Make most uses of extended rewriter non-static. I've added a placeholder method Rewriter::callExtendedRewrite for places in the code that call the extended rewriter are currently difficult to eliminate.
|
|
The method for discarding assertions based on bound inference is quite expensive (40% of runtime) for some benchmarks with quantified formulas from Facebook. This adds an option to disable this, which is done by default for quantified logics.
|
|
Required for automatic generation of side conditions from DSL rewrite rules.
|
