| Age | Commit message (Collapse) | Author |
|---|
|
improvements to robustness of sygus parsing.
|
|
Minor changes to sygus type registration. Print sygus let solutions assuming fixed variable names.
|
|
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.
|
|
|
|
|
|
|
|
towards parsing non-flattened sygus grammars.
|
|
|
|
|
|
|
|
fmf mbqi=gen-ev for interpreted operators.
|
|
--fmf-fun.
|
|
Morgan's proof branch).
|
|
Parser dont tokenize
|
|
delta lemmas.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
utilities more robust. Fix bug in conjecture generation for non-parameterized operators.
|
|
|
|
|
|
implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
|
|
Refactor.
|
|
refactor of previous commit.
|
|
|
|
|
|
|
|
Add sygus regressions.
|
|
construction of sygus datatypes. Expand define-fun in evaluators.
|
|
|
|
integer numerals. Refactor to smt2.cpp.
|
|
declare-var vs synth-fun arguments. Handle ground properties in sythesis conjectures.
|
|
sygus parser.
|
|
|
|
|
|
|
|
disabled string literal test case for smtlib v2.5
|
|
enumerating elements to meet cardinality lower bounds.
|
|
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
