| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This derives sygus unification utility objects from EnvObj where
necessary. There's one remaining occurrence of Rewriter::rewrite in
sygus_unif_rl.cpp, which is a bit tricky to address and thus subject to
a future PR.
|
|
This PR further refactors set defaults for incompatibility issues related to quantifiers.
It adds a new restriction that was discovered recently: --nl-rlv should not be used in quantified logics. Some regressions are modified that are impacted by this restriction.
Also does minor rearrangements to the order in which default options are set.
|
|
This removes the methods `getEnv()`, `options()`, `getSatContext()`, and
`getUserContext()` from the `Theory` class because they are now part of
`EnvObj`. Additionally, this commit converts the inference managers to
`EnvObj` because of there were some calls to retrieve the contexts from
`Theory` in those classes.
|
|
This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.
|
|
This commit identifies a couple of scenarios where an operation required
2 searches into a map/hashmap and replaces them with a single search.
This also makes the code shorter.
Signed-off-by: Mikolas Janota <mikolas.janota@gmail.com>
|
|
|
|
This PR refactors the code that performs sanity checks on the parsed option data.
|
|
This moves the standard method for rewrites in proofs from TheoryBuiltinProofRuleChecker to Rewriter. The motivation for this change is to make various kinds of rewrite methods (standard rewrite, extended rewrite, extended equality rewrite, evaluate) accessible throughout the code in a standard way. After this PR, it is possible to know variants of the REWRITE proof rule application by having access to the rewriter, instead of having to get the builtin proof rule checker. Note that TheoryBuiltinProofRuleChecker::applyRewrite *cannot* be static since access to the rewriter is not longer permitted to be static.
It also removes some unused infrastructure from Rewriter.
Followup PRs will remove applyRewrite for TheoryBuiltinProofRuleChecker in favor of calling the rewriter directly.
|
|
This PR slightly changes how the alternate option property is handled and explicitly checks that alternate is only set for bool options.
|
|
This PR refactors the code generation and the generated code for options::get() and options::getNames().
|
|
|
|
This further reorders the header according to the code style guidelines.
|
|
|
|
EnvObj. (#7130)
|
|
Note: the diff in theory.h is only huge because of small changes that caused huge reformat. The effective change is only that it now derives from EnvObj, does not have a member d_env (because it inherits it) and does not need getLogicInfo (because that's in EnvObj).
|
|
This PR changes all options from experimental to expert and adds a check that only the well-defined option categories are used (common, regular, expert, undocumented).
|
|
|
|
This utility converts from terms used in the internal calculus to terms that capture how they should be printed in LFSC.
|
|
This PR does a major refactoring to the default option handlers (i.e. the piece of code that converts strings to the respective option types). It gets rid of the current multi-layer template specialization in favor of a simple overloaded template function.
|
|
When using --editline, our interactive_shell_black unit test was not
working because the unit test was redirecting std::cin and std::cout
to std::stringstreams, which does not work with Editline. This commit
refactors our InteractiveShell class to explicitly take the input and
output streams as arguments, which fixes the issue because we do not use
Editline for input streams that are not std::cin. Additionally, the
commit updates the unit test to use SMT-LIB syntax instead of the
deprecated CVC language.
|
|
|
|
This makes all members of EnvObj protected in order to prevent creating
EnvObj instances and call member functions. It further uses protected
inheritance (instead of public) for derived classes in order to disallow
`EnvObj* a = new DerivedObj();`.
|
|
This PR adds a missing check in the API for getOptionInfo().
|
|
This PR does some cleanup in the driver and the options. It removes the now obsolete public attribute that allowed using the options in the driver, and removes a bunch of includes from the driver that are no longer necessary.
|
|
Towards replacing that option with a logic check throughout.
|
|
options::getAll() returns a list of all options and their current values as strings. The same functionality can be obtained by using options::getNames() and options::get(). This PR does exactly this replacement, getting rid of a large chunk of generated code. Calling getInfo("all-options") may suffer a minor performance hit, but not noticeable in practice.
|
|
Currently, we configure one of our builds to include unit tests but then
do not compile and run them. This commit adds a step to compile and run
the unit/API tests.
|
|
This implements several variants of lazy proof checking in the core proof checker.
Note this extends the ProofNode class with an additional Boolean d_provenChecked indicating whether the d_proven field was checked by the underlying proof checker.
This PR updates the default proof checking mode to lazy. The previous default can now be enabled by --proof-check=eager-simple.
|
|
|
|
backtrackable.h was defining a datastructure Backtracker, which was
a member in ArrayInfo and Info but it was not doing anything.
|
|
PR #7103 did not quite fix the unit test: The types of the lambda and
the expected bags were still off. This fixes the unit test.
|
|
|
|
|
|
More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
|
|
This class will serve as base class for classes that need access to the
environment. This does not yet have classes derive from this base class.
Will update #7110 and #7112 to use this after this is in.
|
|
`macos-latest` is currently using macOS 10.15, so this updates the CI to use `mac-11` (Big Sur).
|
|
This marks methods const where possible and adds missing documentation.
|
|
|
|
literals (#7108)
Similarly to the issue when explaining literals, it's necassary to save the
reference to the reason for propagating a redundant literal, as adding
explanations that may be added to the SAT solver during the recursive
elimination of redundant literals may change the original reference.
|
|
This changes our implementation of GetModelCommand so that we use the API to print the model.
It simplifies smt::Model so that this is a pretty printing utility, and not a layer on top of TheoryModel.
It adds getModel as an API method for returning the string representation of the model, analogous to our current support for getProof.
This eliminates the last call to getSmtEngine() from the command layer.
|
|
More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
|
|
Fixed TestTheoryWhiteBagsRewriter.map failure
|
|
Our way of constructing proofs from the equality engine in very rare cases may cause cyclic proofs due to constructing double applications of SYMM, which are not recognized as assumptions in CDProof. This is due to an interplay between LazyProofChain using an underlying CDProof as its default proof generator, where the proof chain would use the proofs from the CDProof to form a cyclic proof.
This was encountered in 9 SMT-LIB benchmarks in QF_SLIA.
This makes us safer in several places related to double SYMM steps.
|
|
This makes the `driver::totalTime` statistic a `TimerStat`. This eliminates the need to obtain the overall runtime in the driver and write it to the statistics towards the end of the runtime. This not only eliminates some code in the driver, but also gets rid of the call to `getSmtEngine()` that goes around the API.
One disclaimer: The statistics output changes from seconds as a double (i.e. `1.234`) to milliseconds (i.e. `1234ms`).
|
|
This PR refactors the driver to no longer directly access the Options object, but instead use Solver::getOption() or Solver::getOptionInfo().
|
|
This works towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
|
|
This makes it so that we call the strings::InferProofCons::convert lazily, instead deferring to a temporary, trusted STRING_INFERENCE rule.
This decreases our average proof overhead on commonly solved instances from 64% to 58% on QF_S + QF_SLIA. It also reduces timeouts significantly, from 2010 to 1460. (Note these numbers were with a slightly extended version of this branch that includes other pending PRs for proofs).
Also fixes one subtle issue where proof reconstruction was misusing sequential substitutions (leading to warnings during proof post-processing).
|
|
This is work towards eliminating calls to currentSmtEngine.
This dump mode will become obsolete with the DSL, and is thus now
removed.
|
|
This PR ensures that the possible modes returned in getOptionInfo() are always sorted. Their order would depend on the python dictionary ordering, which changed with a somewhat recent python version and thereby breaks our tests.
|
