| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
The build system (cmake) will automatically generate an export header
cvc4_export.h, which makes sure that the correct export features are
defined depending on the compiler and target platform. The macro CVC4_EXPORT
replaces CVC4_PUBLIC and its usage is reduced by 2/3.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
|
|
Adds a dot printer for proof nodes. Also adds an option to choose the proof format (as a mode).
Signed-off-by: Diego Della Rocca de Camargos <diegodellarocc@gmail.com>
|
|
Refactoring out the code from `inst_strategy_enumerative` into a separate
class. Some additional tricks to avoid duplicate instantiations, most
notably, before instantiation, a tuple is checked if it's not a
super-tuple of some tuple that had earlier resulted in a useless
instantiation.
Signed-off-by: mikolas <mikolas.janota@gmail.com>
|
|
|
|
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
|
|
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
|
|
Also moves several proof-specific options to proof_options.
|
|
Previously, it was optional whether to put length constraints in conclusion for deq string inferences. However, due to optimizations in skolem caching, it is now required to guard these length constraints.
It furthermore changes the policy to not ignore the lengths for the registered skolem, since it may be shared elsewhere.
Fixes #5940.
Notice that proof-new already requires this option to be enabled when proofs are enabled. Hence, this will simplify proof-new when merged.
|
|
Adds an option to optionally print conclusion in the AST proof.
|
|
This was used in the old method for unsat core tracking for instantiation lemmas, which will soon be subsumed.
This is also work towards eliminating the dependencies on quantifiers engine from Instantiate.
|
|
./configure.sh will now fail if Python3 is not installed on the system. Since Python2 is now deprecated the user has to explicitly enable it via --python2. This commit also removes the --python3 configure flag.
|
|
This makes the terms registered to the term database (those considered by E-matching) optionally stored in a SAT-context-dependent manner. The motivation is to have a more flexible/fine-grained set of terms considered by E-matching, e.g. if preregistration becomes lazier in the future.
This uncovered 2 issues:
The induction techniques in "conjecture generator" were using private interfaces, this PR removes the friend relaionship and cleans the code
The conflict-based instantiation module was accessing the signature tables for BOUND_VARIABLES when an operator of an APPLY_UF was a BOUND_VARIABLE. This is possible when options::ufHo is enabled. This makes conflict-based instantiation skip such terms.
|
|
This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database.
It also simplifies the TermDatabase::addTerm method (which changed indentation).
|
|
This PR makes the optimization introduced in bbca987 optional.
|
|
This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.
|
|
Allows one to generate unsat cores from the new proof infrastructure. For new this is controlled by a new option, --check-unsat-cores-new.
|
|
(#5814)
This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).
Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.
|
|
|
|
In preparation for splitting trigger.h/cpp into multiple files.
This updates the code to conform to guidelines. No major changes, apart from a heuristic related to "pure theory triggers" is deleted and simplified.
|
|
We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.
This PR is the third and final step. It adds the user-facing option that turn this feature on, as well as regression tests.
|
|
Previously we were not printing unsat cores when passing the option to dump them if we used the check-sat-assuming command or the QUERY command. This commit fixes this.
It also kills the redundant dump-synth option, as it simplifies a bit what is going on in the command executor.
|
|
This was an experimental option used in combination with separation logic.
|
|
This was a hack to improve the QF arithmetic solver by ensuring that certain instantiation lemmas were preregistered. This is no longer needed and will be a hindrance to the currently line of refactoring.
|
|
This simplifies preprocessing so that the only call to theory-preprocess and ite-removal is at the very end. (One exception is early-theory-pp which is used by default in combination with ite-simp to maintain the performance on QF_LIA/nec).
This is in preparation for making theory preprocessing happen lazily, post-CNF conversion.
@HanielB has done SMT-LIB performance runs, see below.
|
|
This is required to avoid failures in the planned refactoring of check-models.
This removes the SMT-LIB 2.5 semantics option for bvdiv/bvrem.
It still remains to merge the BITVECTOR_UDIV / BITVECTOR_UDIV_TOTAL kinds, calling the total version "BITVECTOR_UDIV", and analogously for UREM.
FYI @barrettcw
|
|
This ensures that datatype selectors are properly handled as triggers in E-matching.
This is challenging since selectors in quantified formulas are of kind APPLY_SELECTOR but are theory-preprocessed to APPLY_SELECTOR_TOTAL/APPLY_UF. Hence, we must match on 2 possible operators, and ones that do not match the operator of the trigger. This adds a custom candidate generator for this case.
It also removes a deprecated option that is no longer used (in part due to our use of shared selectors).
This is in preparation for further work on optimizing cvc4 on benchmarks from Facebook.
Note that there is not a convienient way to call expandDefinitions currently (which is required to get the proper operators to match). This PR calls smt::getCurrentSmtEngine() to do this, although we should find a better solution soon, e.g. adding expandDefinitions to the rewriter.
FYI @barrettcw
|
|
The current help message for --bv-div-zero-const only mentions bvudiv (in which the result is -1) and not bvurem (in which the result is the first argument).
I think this is a bit misleading, because in practice, this option controls also the behavior of bvurem:
CVC4/src/theory/bv/theory_bv.cpp
Line 134 in 0309ef4
if (options::bitvectorDivByZeroConst())
This PR is an attempt to provide a more accurate help message.
|
|
Fixes #5370, #5462.
|
|
This was caused by the quantifiers rewriting eliminating extended arithmetic operators, which was required due to the way counterexample-guided quantifier instantiation used to work with preprocessing. The technique is now more robust and this option can be deleted.
This fixes a debug assertion failure from UFNIA SMT-LIB, a minimized benchmark is included as a regression.
|
|
Signed-off-by: Everett Maus <evmaus@google.com>
|
|
This PR relates to #4987 .
Our plan is to:
delete the model keyword (done in #5415 )
avoid printing extra declarations by default (done in #5432 )
wrap UF values with as expressions.
This PR does step 3, fixes a regression accordingly, and adds the formula from #4987 and a variant of it to the regressions.
|
|
This further removes obsolete explicit includes of stdint.h.
|
|
The main goal of the resource limitation mechanism (via `--rlimit`) is to have a deterministic limitation on runtime. The ultimate goal would be that the actual runtime grows linearly with the spent resources.
To achieve this, this PR does the following:
- introduce new resources spent in places that are not yet covered
- find resource weights that best approximate the runtime
It provides a contrib script `learn_resource_weights.py` that uses statistics from a given benchmark run and uses linear regression to find good resource weights. The script also evaluates this estimate and identifies outliers, benchmarks for which this approximation is particularly bad. This probably indicates that on such a benchmark, some part of the code takes a significant amount of time but is not yet represented by a resource.
Eventually, we should use the resulting resource weights as defaults for the options like `--rewrite-step`, `--theory-check-step`, etc.
|
|
This PR relates to #4987 .
Our plan is to:
delete the model keyword
avoid printing extra declarations by default
wrap UF values with as expressions.
This PR is step 2. It allows the user to choose the model printing style in case of uninterpreted elements: either using datatypes, or using declare-sorts and declare-funs or just using declare-funs.
The default option, which is closest to the standard, is just using declare-funs. In step 3, these will be replaced by abstract values using as.
|
|
This improves trace/error messages for proof-new-pedantic, and also merges the proof-new-pedantic-eager with the proof-new-eager-checking option.
|
|
This removes infrastructure for stream property related to printing type annotations on all variables.
This is towards refactoring the printers.
|
|
This PR disables the `--nl-cad` option by default. It was erroneously enabled with #5345 but leads to errors on, e.g., QF_NIA. Enabling for QF_NRA is done in set_defaults.
|
|
This PR enables `--nl-cad` for QF_NRA (and QF_UFNRA) by default to improve nonlinear arithmetic solving.
Furthermore, it takes care of disabling it when libpoly is not available. It also adds a fix to the CadSolver that avoids incorrect SATs in the presence of theory combination.
|
|
This option has a number of subtle bugs, it should be reimplemented if/when finite-model-find is refactored. It is not high priority enough to maintain.
This does some additional cleaning of the uf cardinality extension, some methods changed indentation.
Fixes #5239, fixes #4872, fixes #4865.
|
|
This PR adds three instantiation modes to the SyGuS instantiation module.
|
|
This makes it so that an "unknown" response in a CEGIS verification step causes the sygus solver to exclude the current solution and mark incomplete. Previously, the sygus solver was non-terminating in such cases, trying the same solution continously.
This also removes the option "sygusVerifySubcall", as this option should always be used. It also makes --nl-ext-tplanes enabled by default when sygus is enabled.
|
|
This PR adds options to add additional ground terms to the SyGuS instantiation grammars.
|
|
While the CAD subsolver already provided for a way to use the linear model to seed the model search, it was not actually used yet.
This PR now does use it, though it is disabled by a Boolean flag.
|
|
Currently, (bvand x y) is translated into a sum of ITEs.
This PR introduces two more options for the translation of (bvand x y):
bv: cast the integer translations of x and y back to bit-vectors, do a bvand, and cast the result to integers.
iand: use the builtin iand operator.
These options are added to many of the tests, and some new tests are added.
In addition, some tests are cleaned up (e.g., removing --no-check-unsat-cores for satisfiable benchmarks).
Finally, some tests are moved from regress0 to regress2 because they take several seconds to complete (2 -- 10 seconds).
|
|
This PR adds a simple BV solver that sends bit-blasting lemmas to the internal MiniSat.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This PR adds a new icp-based solver to be integrated into the nonlinear extension.
It is not meant to be used as a stand-alone ICP solver. It does not implement splits (only propagations) and implements a rather aggressive budget mechanism that aims to quickly stop propagation to allow other solvers to take over. Additionally, it enforces a maximum bit size to avoid divergence.
|
