Age | Commit message (Collapse) | Author |
|
signature. Add regressions.
|
|
|
|
|
|
This reverts commit d2b44175c45a6d2c2fa9c3f8ec1ca1c433cb399b.
|
|
regressions.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
|
|
|
|
Making sure the CVC4 flags do not get overwritten after being set.
|
|
|
|
refactoring.
|
|
Refactor.
|
|
|
|
|
|
|
|
|
|
Heuristics to fit syntax.
|
|
|
|
Tim regarding Trace.isOn
|
|
syntax for single inv properties.
|
|
|
|
partial inst variables for LTE.
|
|
|
|
--cegqi-si. Minor improvements to syntax-guided case, refactoring. Do not apply exhaustive tester inference for sygus datatypes.
|
|
ITE handling in sygus.
|
|
|
|
|
|
Minor improvements to sygus splitting.
|
|
Preparation for single invocation properties. Set output lang to SMT2 for sygus.
|
|
|
|
quantifiers module. Refactor QuantifiersEngine registration and check.
|
|
conflict lemmas.
|
|
|
|
|
|
enabled. Simplify option names.
|
|
|
|
refactor of previous commit.
|
|
|
|
quantifiers check for sat.
|
|
inside splitting lemmas for sygus.
|
|
|
|
applied selectors.
|