Age | Commit message (Collapse) | Author |
|
|
|
default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.
|
|
Start grammar. Add regression.
|
|
Add regression.
|
|
grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression.
|
|
within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
tff script. Minor additions to sygus.
|
|
|
|
fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.
|
|
fmf mbqi=gen-ev for interpreted operators.
|
|
--fmf-fun.
|
|
|
|
(mostly whitespace differences).
|
|
Morgan's proof branch).
|
|
Parser dont tokenize
|
|
|
|
|
|
|
|
|
|
https://www.starexec.org/starexec/secure/details/job.jsp?id=6972
The plot is bit misleading. Those not on x=y, are from QF_BV/asp which are segfaulting (see bugzilla 623). No performance impact on other logics it was tested on.
|
|
|
|
|
|
simplification.
|
|
|
|
|
|
signature. Add regressions.
|
|
regressions.
|
|
implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
|
|
|
|
|
|
Add sygus regressions.
|
|
Fixing bug where (- 1).0 was printed by get-value. Thanks to Christoph Sticksel for the bug report.
|
|
|
|
|
|
disabled string literal test case for smtlib v2.5
|
|
|
|
datatypes rewriter
|
|
Added "ignoring negative membership" option (fragment checking is not provided,
and users must make sure the constraint is in the fragment;
otherwise, the solution may not be correct).
|
|
|
|
|
|
instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs.
|
|
Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine.
|
|
|