| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
SymFPU does not allow to_fp conversion from signed bv of size 1. This
adds rewrites for this case.
Rewrites for the constant and the non-constant cases were tested in
isolation.
|
|
This PR adds --auto-download for the CI job that builds the documentation. Also makes sure that the documentation workflow never fails.
|
|
This PR adds CI jobs to automatically build documentation for branches on the main repository and for pull request.
The first job builds the documentation for every push and pr and stores the generated documentation in cvc5.github.io/docs-ci. All versions are stored and for every branch and PR a symbolic link to the most recent version is maintained.
Note that the PR jobs are run by the pull_request_target trigger that allows access to repository secrets, but runs in the context of the target branch and we thus need to (carefully!) pull in the relevant changes manually.
The second job runs once a week and prunes the docs-ci repository: all directories that have not been touched for a month are removed, and all commits older than a month are squashed into a single commit. This retains the full history for the last month, but effectively removes everything older than that.
|
|
This automatically applies @martin-cs's working patch from 2020-11-14.
It fixes several issues, all covered open issues are added as
regression tests.
Fixes #3582.
Fixes #5511.
Fixes #6164.
|
|
This PR removes the old python api tests for terms from test/api/python/test_term.py and replaces it with a new test file test/python/unit/api/test_term.py. The new test file is obtained by translating test/unit/api/term_black.cpp.
In this PR I only include the tests that pass without requiring any change to the python API. The next PR will add functions to the python API that are currently not supported, along with corresponding tests.
Comment: This was originally done in #6460 on the wrong fork. Now it is re-opened, and addresses all comments given there.
|
|
This PR refactors ppAssert from the lazy BV solver and moves it to TheoryBV.
|
|
|
|
for multiple objectives (#6459)
This PR is one part of multiple.
Preliminary support means currently only supports single objective.
It supports queue-ing up objectives and it always optimizes the first.
Multiple-obj optimization algorithm will be up next.
* Refactor optimization result and objective classes
* Add preliminary support for multiple objectives
* The unit tests are now comparing node values instead of node addresses
|
|
This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions.
In other words, the effect of:
(define-fun f X t)
is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when
(= f (lambda X t)) was an equality solved by non-clausal simplification
The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula.
In this PR:
define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline.
Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit.
The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions.
The proof manager does not require a special case of using the define-function maps.
Define-function maps are eliminated from SmtEngine.
Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.
|
|
|
|
This PR simplifies the generated code for Options::getOption() and Options::setOption(). It now uses less string streams, less temporary vectors and the new options[...] syntax (instead of options::...().
|
|
This PR fixes an issue with one of our nightlies.
|
|
This PR fixes an issue that can lead to an exponential explosion of a rational constant for repeated calls to the cegqi instantiation strategy. The d_small_const variable was squared regularly, we now simply multiply it with its original value.
|
|
(#6452)
If lb = ub + 1 then (lb+ub)/2 =pivot == lb since it's rounding to -infinity.
and lb <= x < pivot will always be UNSAT.
We need to handle this differently.
And this only happens in minimization.
|
|
This PR refactors how the resource manager options are used. It moves options relevant for the resource manager into its own file (making the number of smt options a bit smaller) and uses the Options object directly instead of using the old static accessors.
|
|
This PR removes two headers for exceptions from options.h, and instead pushes the includes to a couple of source files.
|
|
This PR adds a reset() method to the ReferenceStat class. It then uses it to properly reset such statistics in the minisat solvers where lifetime is an issue.
|
|
This PR does some cleanup on the options class: it puts the option defaults into the member declaration and removes the explicit constructor; it puts the holder into a unique_ptr; it uses the regular struct copy operation instead of reconstructing the holder object; it moves some macros required for option defaults into the option holder header.
Also, this PR removes some obsolete code related to suggestions for typos.
|
|
This PR does a bit of cleanup on our didyoumean code.
|
|
|
|
Benchmark is taking 40 seconds on production, due to the configuration that tests --check-unsat-cores.
|
|
This bug can be triggered by define-fun, quantifier macros or inferred substitutions whose RHS contain quantified formulas.
This corrects the issue by ensuring that bound variables introduced for prenexing are fresh for distinct quantified formula subterms that may share quantified variables.
This was reported by Geoff Sutcliffe via a TPTP run.
|
|
Previously, we were conditionally checking whether a function was "flat" e.g. did not have a function type as the range type.
The original motivation for this was to catch cases where the user made a declare-fun that had function return type, which is not permitted. All these checks are already done at the API level https://github.com/CVC4/CVC4/blob/master/src/api/cpp/cvc5_checks.h#L441.
However, internally we should have no such restriction. This is required for simplifying the LFSC term processor.
|
|
This PR adds the basic setup for including the python API in our sphinx documentation and shows how it works using the Datatype class as an example. In detail
- it enables sphinx.ext.autodoc and makes sure the generated pycvc5 is in the search path
- adds a index page for the python API
- adds a page for the Datatype class
- adds docstrings for the Datatype class
- does some finetuning (remove source locations, but adds signature information)
|
|
This PR replaces all api::*HashFunction objects by specializations of std::hash. std::hash is meant to be extended in this way, and it allows for a much cleaner usage of std::unordered_set and std::unordered_map with these types.
|
|
|
|
This PR makes cmake generate the sphinx configuration file. This will simplify dynamically modifying this file in the future, for example to add custom paths within the build directory (for the python API).
|
|
This PR protects two methods of the IntStat class in case statistics are disabled.
|
|
This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular
- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()
The removed methods are only used in few places with are changed to using Options::current().X() instead.
In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.
|
|
Required for fixing a bug in CNF stream's ensureLiteral, which was crashing when combined with unsat-cores-mode=assumptions.
With this PR, we assign a formula like (= (= x y) (= z w)) to have theoryOf THEORY_BOOL. Previously, it mistaken was assigned THEORY_UF if e.g. x,y z, w were terms whose type was an uninterpreted sort.
We should retest unsat-cores-mode=assumptions after this PR is merged.
|
|
propositional) (#6423)
Conclusion and rule are placed on the same node (records nodes in the dot format).
Nodes are colored based on the view they will belong to.
Signed-off-by: Diego Della Rocca de Camargos diegodellarocc@gmail.com
|
|
This ensures that dependencies are tracked for all inferred substitutions, even if a trusted step is added.
This is required to ensure unsat cores are sound when we use e.g. non-clausal simplification + unsat cores.
|
|
This makes dump-instantiations print instantiations for all quantified formulas by default, regardless of whether they had an associated identifier.
|
|
Due to our recent changes in the unsat core infrastructure we were doing a couple assertions wrong during conflict analysis. This commit fixes them.
|
|
|
|
This updates the policy of when to apply smart enumeration: we do so if the grammar has ITE or admits Boolean connective terms. Previously, we applied smart enumeration for ITE and all Boolean grammars. However, this is misguided since e.g. partial evaluation unfolding has no opportunity to be effective if the enumerated terms are only Boolean literals.
This significantly improves run time on a challenge benchmark from @makaimann.
|
|
|
|
This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.
This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
|
|
This PR adds an assumption-based unsat cores option. If enabled it will
disable proof logging in the SAT solver and adds input assertions as
assumptions to the SAT solver. When an unsat core is requested we
extract the unsat core in terms of the unsat assumption in the SAT
solver. Assumption-based unsat cores use the proof infrastructure to map
the input assumptions back to the original assertions.
|
|
This PR adds the dependency of the CaDiCaL cmake target on the external project CaDiCaL-EP if it is not found in the system.
|
|
This adds proofs for sets purification lemmas, which are of the form (= t (skolem t)) and (member t (skolem (singleton t))). Each can be trivially justified in the internal calculus by MACRO_SR_PRED_INTRO.
|
|
This adds various methods for applying substitution as an options to MACRO_SR_* rules. It extends the proof checker and the proof post processor to eliminate based on these types.
It updates the trust substitutions utility used by non-clausal simplification to use fixed-point semantics for substitution, which is highly important for efficiency.
As a result of this PR, we are orders of magnitude faster for checking proofs for problems where non-clausal substitution infers many substitutions. It also makes our regressions noticeably faster:
|
|
This PR fixes a very subtle issue with setting the values a ReferenceStat refers to.
ReferenceStat::set() would take a variable by const& and then store the pointer to it. When giving it a different, but implicitly convertible, type, the pointer would assume the wrong type and consequently read incorrect values from it.
This PR makes set() a template function that explicitly checks that the given type is the correct one.
As we can only export int64_t to the API, this forces users of ReferenceStat to use int64_t stats.
|
|
One of the main motivations for this PR is to simplify our process for doing SMT-LIB wide runs.
|
|
|
|
|
|
This is work towards addressing a bottleneck when generating proofs for substitutions from non-clausal simplification.
This makes the proof generation in trust substitution map lazy.
Further work is required to allow an alternative fixpoint semantics for substitutions in the proof checker instead of the current sequential one.
|
|
In preparation for using this class as part of our proof checker.
This removes an option that was previously used as a hack to try to make check-models work for quantifiers. It also makes supplying a context optional.
|
