Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
Added a flag to enable/disbale this feature (enabled by default).
Also, added some infrastructure for proving rewrite rules.
|
|
Merge from proof branch
|
|
--dt-blast-splits.
|
|
Added support for the BV case
|
|
the decl_bblast step, instead of having an individual "with alias" rule for each BV operation
|
|
intersection.
|
|
|
|
|
|
The assignment
d_exprToVariableName[*it] = assignAlias(*it)
Creates an empty value for *it in d_exprToVariableName, causing the assertion in assignAlias to fail
|
|
|
|
|
|
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
|
|
|
|
|
|
Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.
|
|
|
|
|
|
|
|
|
|
|
|
instantiations of non-registered quantifiers in sygus.
|
|
uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.
|
|
|
|
|
|
graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.
|
|
|
|
Minor fixes for inst max level.
|
|
|
|
|