| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits).
|
|
|
|
When compiling the Java bindings on macOS, the linker complained about
CVC4::ExprManager::mkConst<CVC4::TypeConstant>() and
CVC4::Expr::getConst<CVC4::TypeConstant>() being undefined. After some
research, I found that the issue has been introduced by commit
36bf9f8bcb2a1a3aea1f90eb4d13aed3bbf6da8f. It looks like adding the
-no-undefined flags resulted in the symbols in question being omitted
due to TypeConstant not being exported. This commit makes TypeConstant
CVC4_PUBLIC, which fixes the issue.
|
|
Adds support for linearizing additions w.r.t. to a variable.
For example,
a * x + b + c * d * -x = e + x
is rewritten to
x * (a - c * d - 1) = e - b.
This also adds an additional rewriting rule x * x = x --> x < 2.
|
|
This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL,
BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL.
It refactors side condition generation for better readability and unit testing.
It further adds unit tests for all side conditions we generate in order to check if they too weak
or to restrictive (which may result in unsound behavior).
This is achieved by checking the following two implications:
not (exists x. s * x = t => SC) ... if sat, SC is too restrictive
not (SC => exists x. s * x = t) ... if sat SC is too weak
This simplifies to checking not (SC <=> exists x. s * x = t).
|
|
|
|
|
|
|
|
|
|
Also, moved implementation of BVMinisatSatSolver::MinisatNotify::notify to .cpp file.
|
|
|
|
Now prints each tag in a separate line.
|
|
|
|
|
|
|
|
|
|
This is another step towards addressing #1304 and #1344. This pull request:
- Refactors SygusGrammarNorm
- Makes SyGusGrammarNorm a default component in the construction of grammar. The linearization of grammars however only occurs if the option --sygus-grammar-norm is used.
- Performs a "chain transformation" in the application of the PLUS operator in integer grammars
- Removes redundant expansions of definitions from TermDbSygus
- Adds a default empty print callback to SygusEmptyPrintCallback
This lays the basis for more general linearizations.
|
|
|
|
|
|
This commit fixes two issues with reset-assertions:
- pending pops were not done in SmtEngine, resulting in the following
assertion failure:
d_userLevels.size() == 0 && d_userContext->getLevel() == 1
- all definitions were erased on reset-assertion in an SMT2 file,
leading to errors about undefined types
|
|
|
|
|
|
My last commit for the Valgrind instrumentation contained a typo that
made the nightlies fail. This commit fixes the issue.
|
|
This commit adds two configuration options that help debugging memory
issues with allocations in the ContextMemoryManager:
--enable/disable-valgrind: This flag enables/disables Valgrind
instrumentation of the ContextMemoryManager. Enabled by default for
debug builds if the Valgrind headers are available.
--enable/disable-context-memory-manager: This flag enables/disables the
use of the ContextMemoryManager. If the flag is disableda dummy
ContextMemoryManager is used that does single allocations instead of
chunks. The flag is enabled by default.
|
|
This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur.
|
|
|
|
|
|
This
makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables.
Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default
Allows cbqiNestedQE to be used in the BV logic.
Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic).
|
|
|
|
|
|
|
|
This enables building CVC4 from a source release with Cryptominisat support.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
lambdas (#1403)
This partially solves issue #1344. Definitions are expanded when the grammar normalizer is called. When this becomes default then the code that expands definitions elsewhere will be removed.
The PR also contains minor changes to the PrintCallback and SygusGrammarNormalize module.
|
|
|
|
|
|
* minor
Using string previously computed
* adding option
* starting module for simplifying grammars
* more
* more
* fix
* fix
* fix
* fix
* fix
* removing unused command
* removing unused command
* removing unnecessary quantifier engine
* adding lambda support
* transient
* reverting changes
* starting normalization of integers
* removing unnecessary objects
* using for_each
* rebuilding given datatypes
* recrating types as given
* bug fixing
* minor
* reverting space changes
* addressing review
* addressing review
|
|
* Preprocess extract -> concat pass for cegqi bv.
* Add sygus bench
* Fixes, infrastructure.
* Minor fixes.
* Try
* Minor
* Minor
* Document
* Format
* Improving debug messages.
* Address
* Format
* Overlapping extracts.
* Format
* Minor
* Address review.
* Format
* Comment
* Format
|
|
|
|
|
