Age | Commit message (Collapse) | Author |
|
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.
|
|
|
|
|
|
|
|
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.
|