Age | Commit message (Collapse) | Author |
|
|
|
|
|
Adds missing override keywords.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Previously, we computed an inverse for s1 o x, x o s2, s1 o x o s2 while disregarding that invertibility
depends on si. This adds this handling as an optional heuristic for concats over (dis)equality since it improves performance on a considerable number of benchmarks.
|
|
This refactors and simplifies solveBvLit() and fixes the following:
- generate side conditions for BITVECTOR_NEG, BITVECTOR_NOT, BITVECTOR_PLUS,
BITVECTOR_XOR over inequalities and disequality
- fix CONCAT handling (generate side conditions rather then computing an inverse which was incorrect)
- fix SIGN_EXTEND handling (same as with CONCATs)
|
|
|
|
|
|
|
|
|
|
Removing more miscellaneous throw specifiers.
|
|
|
|
|
|
|
|
|
|
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).
|
|
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.
|
|
|
|
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 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).
|
|
|
|
|
|
* 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
|
|
* Higher-order instantiation.
* Add missing files.
* Document inst match generators, make collectHoVarApplyTerms iterative.
* More documentation.
* More documentation.
* More documentation.
* More documentation
* Refactoring, documentation.
* More documentation.
* Fix comment, reference issue.
* More documentation. Fix ho trigger for the changes from master.
* Minor
* More documentation.
* More documentation.
* More
* More documentation, make indexing and lookup in TriggerTrie iterative instead of recursive.
* More
* Minor improvements to comments.
* Remove an unimplemented optimization from an old version of cached multi-trigger matching. Update and improve documentation in inst match generator.
* Improve documentation for ho_trigger.
* Update ho trigger to not access now private member of TermDb.
* Address comments.
* Address
* Clang format
|
|
This adds a deterministic (seeded) random number generator (RNG). It implements the xorshift* generator (see S. Vigna, An experimental exploration of Marsaglia's xorshift generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016).
|
|
* Disable qe preprocessing for sygus by default, add option.
* Fix bug
* Unnest one
* Format
|
|
|
|
* Remove front end hack for sygus.
* Remove other hack, add sygus solution output mode.
* Clang format
* Minor
* Fix
* Minor
* Remove unused field.
|
|
* Multi-instantiation heuristic for cbqi bv.
* New clang format.
* Minor
* Minor.
* Minor
|
|
* Add mode for cbqi bv inequality handling.
* Implement the mode.
* Clang format
* Apply new clang format.
* Revert "Apply new clang format."
This reverts commit 1fec0ed999e45daacc4c756f11b5ecb4690f6561.
* Revert "Clang format"
This reverts commit 17042edb82d64c159aeddfe0264cd663998d0471.
* Clang format, second try.
* Revert "Clang format, second try."
This reverts commit f862c47c34bc313f5bc49a26b7586a4824e5aae0.
* Apply clang format, try 3.
|
|
This adds inverse handling for ULT(BV), SLT(BV) and disequalities. Rewriting of inequalities and disequalities to equalities with slack can now be disabled with an option (--cbqi-bv-inv-in-dis-eq). Function solve_bv_constraint is now merged into solve_bv_lit.
|
|
* Add option sygus-abort-size, which tells the enumerative SyGuS solver to abort when it reaches a given term size.
* Apply clang format.
|
|
Adds two heuristics for cbqi-bv, both disabled by default.
The first optimistically solves for boundary points of inequalities.
The second randomly interleaves inversion and value instantiations.
Adds some newly solved regressions from SMT LIB.
|
|
This adds option --copyright which displays copyright information for CVC4. It further extends --show-config with copyright information and adds a banner with copyright information in interactive mode.
|
|
Quantifiers utilities for higher-order.
This makes the term indexing mechanisms in Term Database take into account equalities between functions, in which case the term indices for the two functions merges.
Also adds required options and a minor utility for implementing app completion.
|
|
Also removed obsolete CUDD related code.
|
|
* Refactor conjecture class in ce guided instantiation, move to own file. In preparation for sygus streaming mode.
* Infrastructure for streaming guards, more cleanup.
* Do explicit exclusion to move to next solution for sygus streaming option, now functional. More cleanup.
* More cleanup, add comments.
* Update comments
* Optimizations for invariant synthesis. Fix corner case for single invocation inference, more encapsulation in single inv utility. Minor fix for variable elimination in quantifiers rewriter.
* Fix makefile.
* Cleanup.
* Remove unused includes.
* Minor
|
|
* Initial work on BV CEGQI, still working on avoid circular dependencies with inversion skolems.
* Guard by option, minor notes.
* Minor
* Minor fixes.
* Minor
|
|
* Extend quantifier-free UF solver to higher-order. This includes an extensionality inference, and lazy conversion from APPLY_UF to HO_APPLY terms.Implements collectModelInfo and theory combination for HO_APPLY terms.
* Update comments, minor changes to functions. Update APPLY_UF skolem to be user-context dependent.
* Remove unused NodeList
|