projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2018-07-17
Andrew Reynolds
Minor cleanup and fixes for conflict-based instantiatio...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
Do extended rewrite on results of quantifier eliminatio...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
Purify applications of exp to transcendental arguments...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
sygusComp2018: update policies for solution reconstruc...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
sygusComp2018: Improvements to datatypes sygus solver...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
sygusComp 2018: updates to sygus term database (#2170)
commit
|
commitdiff
|
tree
2018-07-15
Andres Noetzli
Avoid ambiguous overloads in BitVector (#2169)
commit
|
commitdiff
|
tree
2018-07-14
Andres Noetzli
exportTo only if needed for --sygus-rr-synth-check...
commit
|
commitdiff
|
tree
2018-07-14
Andrew Reynolds
sygusComp2018: update semantics for declare-fun in...
commit
|
commitdiff
|
tree
2018-07-13
Andrew Reynolds
Fix and improve grammar normalization for any constant...
commit
|
commitdiff
|
tree
2018-07-13
Andres Noetzli
Properly clean up assertion stack in CnfProof (#2147)
commit
|
commitdiff
|
tree
2018-07-13
Andrew Reynolds
sygusComp2018: optimization for collect model info...
commit
|
commitdiff
|
tree
2018-07-13
Aina Niemetz
New C++ API: Minor reorder. (#2163)
commit
|
commitdiff
|
tree
2018-07-13
Aina Niemetz
New C++ API: Implementation of datatype classes. (...
commit
|
commitdiff
|
tree
2018-07-13
Aina Niemetz
New C++ API: Implementation of Solver class: Consts...
commit
|
commitdiff
|
tree
2018-07-11
Caleb Donovick
Move rewrite to pass (#2128)
commit
|
commitdiff
|
tree
2018-07-08
Andres Noetzli
Add more sophisticated floating-point sampler (#2155)
commit
|
commitdiff
|
tree
2018-07-07
Andrew Reynolds
sygusComp2018: improve extended rewriter for Bool...
commit
|
commitdiff
|
tree
2018-07-06
Andrew Reynolds
Split ext theory to own file and document (#1809)
commit
|
commitdiff
|
tree
2018-07-06
Martin
Feature/fp rewrite improvement (#2154)
commit
|
commitdiff
|
tree
2018-07-06
Aina Niemetz
New C++ API: Implementation of Solver class: Term handl...
commit
|
commitdiff
|
tree
2018-07-06
Aina Niemetz
New C++ API: Implementation of Solver class: Sort handl...
commit
|
commitdiff
|
tree
2018-07-06
Andres Noetzli
Add option for timeout for rewrite candidate check...
commit
|
commitdiff
|
tree
2018-07-06
Andrew Reynolds
sygusComp2018: simplify beta reduction in uf rewriter...
commit
|
commitdiff
|
tree
2018-07-05
Andrew Reynolds
Make string length lemmas more robust to rewriting...
commit
|
commitdiff
|
tree
2018-07-05
Andrew Reynolds
Minor changes to sygus-rr utilities to support floating...
commit
|
commitdiff
|
tree
2018-07-05
Andres Noetzli
sygusComp2018: Improve string rewriter (#2141)
commit
|
commitdiff
|
tree
2018-07-04
Andrew Reynolds
More cleanup in strings (#2138)
commit
|
commitdiff
|
tree
2018-07-04
Aina Niemetz
New C++ API: Implementation of datatype declaration...
commit
|
commitdiff
|
tree
2018-07-04
Andrew Reynolds
Reorganize candidate rewrite rule filtering (#2116)
commit
|
commitdiff
|
tree
2018-07-04
Andres Noetzli
Remove unused CDVector (#2139)
commit
|
commitdiff
|
tree
2018-07-04
Aina Niemetz
New C++ API: Implementation of OpTerm. (#2132)
commit
|
commitdiff
|
tree
2018-07-04
Andrew Reynolds
Fix fmf-fun for non-equality function definitions ...
commit
|
commitdiff
|
tree
2018-07-03
Aina Niemetz
New C++ API: Implementation of Term. (#2131)
commit
|
commitdiff
|
tree
2018-07-03
Aina Niemetz
New C++ API: Implementation of Kind maps. (#2130)
commit
|
commitdiff
|
tree
2018-07-03
Aina Niemetz
Fix datatypes example: nil constructor was missing...
commit
|
commitdiff
|
tree
2018-07-03
Andrew Reynolds
sygusComp2018: update sygus-related options setting...
commit
|
commitdiff
|
tree
2018-07-03
Andrew Reynolds
Remove miscellaneous dead and unused code from quantifi...
commit
|
commitdiff
|
tree
2018-07-03
Andres Noetzli
Add regression test for issue #1986 (#2114)
commit
|
commitdiff
|
tree
2018-07-02
Aina Niemetz
Refactor ApplySubsts preprocessing pass. (#2120)
commit
|
commitdiff
|
tree
2018-07-02
Aina Niemetz
New C++ API: Implementation of Sort. (#2122)
commit
|
commitdiff
|
tree
2018-07-02
Andrew Reynolds
Remove some dead code from theory strings (#2125)
commit
|
commitdiff
|
tree
2018-07-02
Caleb Donovick
Add missing include (#2127)
commit
|
commitdiff
|
tree
2018-07-02
Andrew Reynolds
Modify cegqi heuristic for finite datatypes (#2126)
commit
|
commitdiff
|
tree
2018-07-02
Andrew Reynolds
Improve error message. (#2124)
commit
|
commitdiff
|
tree
2018-06-29
Andrew Reynolds
Use evaluator in sygus sampler. (#2117)
commit
|
commitdiff
|
tree
2018-06-29
Aina Niemetz
New C++ API: Implementation of Result. (#2112)
commit
|
commitdiff
|
tree
2018-06-28
Andrew Reynolds
Remove comment about model value hack (#2118)
commit
|
commitdiff
|
tree
2018-06-28
Andrew Reynolds
sygusComp2018: optimization for invariance test (...
commit
|
commitdiff
|
tree
2018-06-28
Andres Noetzli
Fix stale reference in MiniSat when generating UC ...
commit
|
commitdiff
|
tree
2018-06-28
Andrew Reynolds
Do not rename uninterpreted constants (#2098)
commit
|
commitdiff
|
tree
2018-06-28
Andrew Reynolds
Split and document ceg theory instantiators (#2094)
commit
|
commitdiff
|
tree
2018-06-27
Aina Niemetz
Header for new C++ API. (#1697)
commit
|
commitdiff
|
tree
2018-06-27
Andrew Reynolds
Synthesize candidate-rewrites from standard inputs...
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
sygusComp2018: add scripts. (#2103)
commit
|
commitdiff
|
tree
2018-06-26
Andres Noetzli
sygusComp2018: Add evaluator (#2090)
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
Add casc j9 tfn script (#2100)
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
Disable uf symmetry breaker in incremental mode (...
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
Fix assertion for relational triggers (#2096)
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
Do not dagify printing over binders (#2093)
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
Remove unnecessary code in register quantifier internal...
commit
|
commitdiff
|
tree
2018-06-26
Andres Noetzli
Minor improvements in SMT2 and CVC printers (#2089)
commit
|
commitdiff
|
tree
2018-06-26
Aina Niemetz
Bump library version to 1.7-prerelease.
commit
|
commitdiff
|
tree
2018-06-26
Aina Niemetz
Cutting release 1.6.
commit
|
commitdiff
|
tree
2018-06-25
Aina Niemetz
More updates to NEWS for 1.6.
commit
|
commitdiff
|
tree
2018-06-25
Aina Niemetz
Update AUTHORS, NEWS, README, RELEASE-NOTES and THANKS...
commit
|
commitdiff
|
tree
2018-06-25
Aina Niemetz
Bump library version.
commit
|
commitdiff
|
tree
2018-06-25
Aina Niemetz
Update copyright year in configuration.cpp:copyright().
commit
|
commitdiff
|
tree
2018-06-25
Aina Niemetz
Updated copyright headers.
commit
|
commitdiff
|
tree
2018-06-25
Aina Niemetz
Do not use git blame -C in get-authors (too many false...
commit
|
commitdiff
|
tree
2018-06-25
Aina Niemetz
Fix update-copyright script for files without a header.
commit
|
commitdiff
|
tree
2018-06-25
Aina Niemetz
Added Makai and Yoni to get-authors script.
commit
|
commitdiff
|
tree
2018-06-25
Andres Noetzli
Remove parentheses for prefix ops without args (#2082)
commit
|
commitdiff
|
tree
2018-06-21
Andres Noetzli
Fix warnings and enable -Wnon-virtual-dtor warning...
commit
|
commitdiff
|
tree
2018-06-21
Andres Noetzli
Check unsat cores in regressions also without LFSC...
commit
|
commitdiff
|
tree
2018-06-21
Aina Niemetz
Updated installation instructions to mention autogen...
commit
|
commitdiff
|
tree
2018-06-20
Andres Noetzli
Resolve CVC4_USE_SYMFPU in headers at config-time ...
commit
|
commitdiff
|
tree
2018-06-15
Andrew Reynolds
Disable solving non-linear BV literals by default ...
commit
|
commitdiff
|
tree
2018-06-13
Andres Noetzli
Workaround for incremental unsat cores (#1962)
commit
|
commitdiff
|
tree
2018-06-13
Andrew Reynolds
Fix simple regexp consume (#2066)
commit
|
commitdiff
|
tree
2018-06-13
Andres Noetzli
Disable unconstrainedSimp pass when proofs enabled...
commit
|
commitdiff
|
tree
2018-06-12
Andrew Reynolds
Fix strip constant endpoint for ITOS in strings rewrite...
commit
|
commitdiff
|
tree
2018-06-11
Andrew Reynolds
Fix equality conflicts reported by FP (#2064)
commit
|
commitdiff
|
tree
2018-06-10
Andres Noetzli
Disable test that fails in competition mode (#2063)
commit
|
commitdiff
|
tree
2018-06-09
Andres Noetzli
Add flag to skip regression if feature enabled (#2062)
commit
|
commitdiff
|
tree
2018-06-09
Andres Noetzli
Reset decisions at SAT level after solving (#2059)
commit
|
commitdiff
|
tree
2018-06-08
Mathias Preiner
Disable BV-abstraction in the competition script. ...
commit
|
commitdiff
|
tree
2018-06-07
Andres Noetzli
Look for cryptominisat5_simple, not cryptominisat5...
commit
|
commitdiff
|
tree
2018-06-07
Aina Niemetz
Remove invalid assertion (#1993). (#2057)
commit
|
commitdiff
|
tree
2018-06-07
Andrew Reynolds
Clear pending inferences during datatypes splitting...
commit
|
commitdiff
|
tree
2018-06-05
Andres Noetzli
Only enable transcendentals if logic is N[I]RAT (#2052)
commit
|
commitdiff
|
tree
2018-06-04
Andrew Reynolds
Move assertion. (#2051)
commit
|
commitdiff
|
tree
2018-06-04
Andres Noetzli
[SMT-COMP] Add new logics to run-scripts (#2022)
commit
|
commitdiff
|
tree
2018-06-04
Andrew Reynolds
Enable cegqi (with model values) for floating point...
commit
|
commitdiff
|
tree
2018-06-04
Andres Noetzli
Regressions: Support for requiring CVC4 features (...
commit
|
commitdiff
|
tree
2018-06-02
Andrew Reynolds
Fix assertion involving unassigned Boolean eqc in...
commit
|
commitdiff
|
tree
2018-06-02
Andrew Reynolds
Fix corner case of mixed int/real cegqi. (#2046)
commit
|
commitdiff
|
tree
2018-06-02
Mathias Preiner
Fix BV-abstraction check to consider SKOLEM. (#2042)
commit
|
commitdiff
|
tree
2018-06-02
Andrew Reynolds
Fix preinitialization pass for finite model finding...
commit
|
commitdiff
|
tree
2018-06-01
Andrew Reynolds
Fix quantified bv variable elimination (#2039)
commit
|
commitdiff
|
tree
next