| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
smt_engine.cpp:1992: Rewriter::rewrite(d_assertions[i]) == d_assertions[i]
when --ite-simp and --repeat-simp are on
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Manually confirmed that runscripts were not touched during merge.
- redoes Tim's bug fix
- Andy's commits (mostly related to sygus)
|
|
not negBack is already in conflict. This is needed as it can be called multiple times on the same constraint.
|
|
improvements to robustness of sygus parsing.
|
|
Minor changes to sygus type registration. Print sygus let solutions assuming fixed variable names.
|
|
|
|
|
|
|
|
|
|
|
|
sat-solvers
|
|
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.
|
|
|
|
for non-UF logics. Update SMT COMP scripts accordingly.
|
|
|
|
|
|
--cbqi-sat whether to disable sat for quantified arith.
|
|
|
|
|
|
towards parsing non-flattened sygus grammars.
|
|
|
|
|
|
|
|
|
|
Added missing LogicException to throws in method lemma.
|
|
|
|
|
|
|
|
|
|
for sygus.
|
|
moved Minisat namespace into CVC4
|
|
|
