| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
|
|
|
|
space based on commutative operators.
|
|
|
|
|
|
Add sygus regressions.
|
|
construction of sygus datatypes. Expand define-fun in evaluators.
|
|
declare-var vs synth-fun arguments. Handle ground properties in sythesis conjectures.
|
|
sygus parser.
|
|
|
|
|
|
|
|
|
|
fixed a bug for empty string in regex
|
|
datatypes rewriter
|
|
trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.
|
|
|
|
pre-model.
|
|
|
|
enumerating elements to meet cardinality lower bounds.
|
|
|
|
|
