| Age | Commit message (Collapse) | Author |
|---|
|
inside splitting lemmas for sygus.
|
|
|
|
applied selectors.
|
|
|
|
|
|
|
|
space based on commutative operators.
|
|
|
|
|
|
Add sygus regressions.
|
|
construction of sygus datatypes. Expand define-fun in evaluators.
|
|
Fixing bug where (- 1).0 was printed by get-value. Thanks to Christoph Sticksel for the bug report.
|
|
the cxxtest git repository.
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
fixed a bug for empty string in regex
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.
|
|
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.
|
|
|
