projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2018-05-22
Andrew Reynolds
Infrastructure for strings strategies (#1883)
commit
|
commitdiff
|
tree
2018-05-22
Mathias Preiner
Add SymFPU licensing information. (#1952)
commit
|
commitdiff
|
tree
2018-05-21
Andrew Reynolds
Improvements in parsing and printing related to mixed...
commit
|
commitdiff
|
tree
2018-05-21
Andrew Reynolds
Infrastructure to mark unused sygus strategies (#1950)
commit
|
commitdiff
|
tree
2018-05-21
makaimann
Handle IMPLIES in bool-to-bv and test it in regress0...
commit
|
commitdiff
|
tree
2018-05-21
Andrew Reynolds
Refactor sygus eval unfold (#1946)
commit
|
commitdiff
|
tree
2018-05-21
Andres Noetzli
Remove Eclipse project files (#1928)
commit
|
commitdiff
|
tree
2018-05-21
Andres Noetzli
Fix compiler warning in hashsmt example (#1927)
commit
|
commitdiff
|
tree
2018-05-21
Haniel Barbosa
Assign weight 1 for Boolean variables in SyGuS default...
commit
|
commitdiff
|
tree
2018-05-21
Caleb Donovick
Fix file extension (#1919)
commit
|
commitdiff
|
tree
2018-05-19
Haniel Barbosa
changing default (#1944)
commit
|
commitdiff
|
tree
2018-05-18
Andrew Reynolds
Cache isInterpretedFinite (#1943)
commit
|
commitdiff
|
tree
2018-05-18
Andrew Reynolds
Cegis unif defaults to cegis when no unif (#1942)
commit
|
commitdiff
|
tree
2018-05-18
Andrew Reynolds
Unified fairness scheme for cegis unif (#1941)
commit
|
commitdiff
|
tree
2018-05-17
Andrew Reynolds
Catch type errors in sygus grammars for lambda (define...
commit
|
commitdiff
|
tree
2018-05-17
Andrew Reynolds
Fix debugPrint and add regress. (#1934)
commit
|
commitdiff
|
tree
2018-05-17
Haniel Barbosa
Option to force return values of Bool functions to...
commit
|
commitdiff
|
tree
2018-05-17
Andrew Reynolds
Cegis-specific infrastructure (#1933)
commit
|
commitdiff
|
tree
2018-05-17
Andrew Reynolds
Internal propagation for refinement lemmas (#1932)
commit
|
commitdiff
|
tree
2018-05-16
Andrew Reynolds
Improve the separation resolution scheme in cegis unif...
commit
|
commitdiff
|
tree
2018-05-16
yoni206
Refactor static learning preprocessing pass (#1857)
commit
|
commitdiff
|
tree
2018-05-15
Andrew Reynolds
Refactoring get enumerator values in construct candidat...
commit
|
commitdiff
|
tree
2018-05-15
Haniel Barbosa
adding regressions (#1925)
commit
|
commitdiff
|
tree
2018-05-15
Haniel Barbosa
Building and refining solutions with dynamic condition...
commit
|
commitdiff
|
tree
2018-05-15
Andrew Reynolds
Fix free variables in cbqi preregister inst. (#1921)
commit
|
commitdiff
|
tree
2018-05-15
Andrew Reynolds
Fix annotations in regress2. (#1917)
commit
|
commitdiff
|
tree
2018-05-15
Andrew Reynolds
Minor improvements to --nl-ext-purify (#1896)
commit
|
commitdiff
|
tree
2018-05-15
Andrew Reynolds
Incorporating dynamic condition enumeration into cegis...
commit
|
commitdiff
|
tree
2018-05-14
Martin
Floating point theory solver based on SymFPU (#1895)
commit
|
commitdiff
|
tree
2018-05-14
Mathias Preiner
Add contrib/get-symfpu for downloading symfpu. (#1905)
commit
|
commitdiff
|
tree
2018-05-14
Haniel Barbosa
Fix purification in SygusUnifRL (#1912)
commit
|
commitdiff
|
tree
2018-05-14
Andrew Reynolds
Add regressions, change defaults. (#1911)
commit
|
commitdiff
|
tree
2018-05-14
Andrew Reynolds
Flag to check invariance of entire values in sygus...
commit
|
commitdiff
|
tree
2018-05-14
Florian Schanda
Small change for more sensible line breaking in the...
commit
|
commitdiff
|
tree
2018-05-11
Aina Niemetz
Remove obsolete unit test for ackermannization. (#1906)
commit
|
commitdiff
|
tree
2018-05-11
Aina Niemetz
Fix ackermannize preprocessing pass. (#1904)
commit
|
commitdiff
|
tree
2018-05-11
Andres Noetzli
Support multiple sets of command line args in regs...
commit
|
commitdiff
|
tree
2018-05-11
Haniel Barbosa
Also exclude ITEs from ITE conditions in SygusUnifStrat...
commit
|
commitdiff
|
tree
2018-05-10
Andrew Reynolds
Exclude Boolean connectives from ITE conditions in...
commit
|
commitdiff
|
tree
2018-05-10
Andrew Reynolds
Sygus repair constants (#1812)
commit
|
commitdiff
|
tree
2018-05-10
Haniel Barbosa
Static learn redundant operators in CegisUnif (#1899)
commit
|
commitdiff
|
tree
2018-05-10
Andrew Reynolds
Add ITE to default Boolean sygus grammar (#1898)
commit
|
commitdiff
|
tree
2018-05-10
Aina Niemetz
Refactored BVAckermann preprocessing pass. (#1889)
commit
|
commitdiff
|
tree
2018-05-10
Andrew Reynolds
Fix priority of decisions for cegis unif (#1897)
commit
|
commitdiff
|
tree
2018-05-09
Haniel Barbosa
Piecing solutions together in CegisUnif (#1894)
commit
|
commitdiff
|
tree
2018-05-09
yoni206
Reorder class members in bv-to-bool and bool-to-bv...
commit
|
commitdiff
|
tree
2018-05-09
Andrew Reynolds
Better option names for PBE (#1891)
commit
|
commitdiff
|
tree
2018-05-09
Andrew Reynolds
Make symmetry-breaker-exp into a preprocessing pass...
commit
|
commitdiff
|
tree
2018-05-09
PaulMeng
Add the symmetry breaker module (#1847)
commit
|
commitdiff
|
tree
2018-05-08
Mathias Preiner
Refactor bv-abstraction preprocessing pass. (#1860)
commit
|
commitdiff
|
tree
2018-05-08
Andrew Reynolds
Infrastructure for approximations in model output ...
commit
|
commitdiff
|
tree
2018-05-08
Andrew Reynolds
Support for str.<= and str.< (#1882)
commit
|
commitdiff
|
tree
2018-05-08
Aina Niemetz
Fix order of preprocessing pass registration. (#1887)
commit
|
commitdiff
|
tree
2018-05-08
Haniel Barbosa
Classifying data in SygusUnifRL (#1886)
commit
|
commitdiff
|
tree
2018-05-08
Andrew Reynolds
Infrastructure for CEGQI handled status (#1873)
commit
|
commitdiff
|
tree
2018-05-08
Haniel Barbosa
only lazy trie changes (#1885)
commit
|
commitdiff
|
tree
2018-05-07
Andrew Reynolds
Add support for str.code (#1821)
commit
|
commitdiff
|
tree
2018-05-05
Andrew Reynolds
Fix handling of TO_REAL in cvc printer (#1876)
commit
|
commitdiff
|
tree
2018-05-05
Andrew Reynolds
Remove special case for record selector printing. ...
commit
|
commitdiff
|
tree
2018-05-04
Andrew Reynolds
Cegis unif register evaluation points (#1878)
commit
|
commitdiff
|
tree
2018-05-04
Andres Noetzli
Make --output-lang consistent with --lang (#1877)
commit
|
commitdiff
|
tree
2018-05-04
Andrew Reynolds
Do not print tuples. (#1874)
commit
|
commitdiff
|
tree
2018-05-04
Mathias Preiner
Refactor bv-intro-pow2 preprocessing pass. (#1851)
commit
|
commitdiff
|
tree
2018-05-04
Andres Noetzli
Fix printing of multiple datatypes (#1872)
commit
|
commitdiff
|
tree
2018-05-04
Haniel Barbosa
Move Lazy trie datastructure to its own file (#1871)
commit
|
commitdiff
|
tree
2018-05-04
Andrew Reynolds
Initialize cegis unif strategy (#1861)
commit
|
commitdiff
|
tree
2018-05-04
Andrew Reynolds
Document datatypes sygus (#1818)
commit
|
commitdiff
|
tree
2018-05-04
Andrew Reynolds
Sets subtypes (#1095)
commit
|
commitdiff
|
tree
2018-05-03
Mathias Preiner
Fix redundant internalPush calls. (#1865)
commit
|
commitdiff
|
tree
2018-05-03
Andres Noetzli
Fix warnings in proof code (#1850)
commit
|
commitdiff
|
tree
2018-05-03
Andrew Reynolds
Interleave quantifiers checks with ground theory checks...
commit
|
commitdiff
|
tree
2018-05-03
Andrew Reynolds
Option to interleave tangent plane inferences (#1833)
commit
|
commitdiff
|
tree
2018-05-03
Andrew Reynolds
Link cegis unif with the enumeration manager (#1859)
commit
|
commitdiff
|
tree
2018-05-03
Haniel Barbosa
Make CegisUnif default to Cegis when no unif used ...
commit
|
commitdiff
|
tree
2018-05-03
Andrew Reynolds
Fix cvc printer for nullary constructors (#1856)
commit
|
commitdiff
|
tree
2018-05-03
Andres Noetzli
Remove (dummy) SMT1 printer (#1854)
commit
|
commitdiff
|
tree
2018-05-03
Andrew Reynolds
Support HORN logic string (#1849)
commit
|
commitdiff
|
tree
2018-05-03
Andrew Reynolds
Initial support for string standard in smt lib 2.6...
commit
|
commitdiff
|
tree
2018-05-01
Andrew Reynolds
Cegis unif enumerator manager (#1837)
commit
|
commitdiff
|
tree
2018-05-01
Andrew Reynolds
Improve tangent planes for transcendental functions...
commit
|
commitdiff
|
tree
2018-04-30
Haniel Barbosa
Refactor real2int (#1813)
commit
|
commitdiff
|
tree
2018-04-30
Andres Noetzli
Remove dead code in bv-to-bool preprocessing pass ...
commit
|
commitdiff
|
tree
2018-04-30
Andrew Reynolds
Remove subsort symmetry breaking (#1807)
commit
|
commitdiff
|
tree
2018-04-30
Andrew Reynolds
Fix 1156 (#1830)
commit
|
commitdiff
|
tree
2018-04-30
Andres Noetzli
Disable unsat-cores/proofs for slow regression (#1835)
commit
|
commitdiff
|
tree
2018-04-30
Andrew Reynolds
Allow multiple functions in sygus unif approaches ...
commit
|
commitdiff
|
tree
2018-04-30
Andrew Reynolds
Make factoring inference more aggressive (#1825)
commit
|
commitdiff
|
tree
2018-04-30
Andrew Reynolds
Refactor nonlinear check (#1814)
commit
|
commitdiff
|
tree
2018-04-30
Andrew Reynolds
Improvements to simple transcendental function check...
commit
|
commitdiff
|
tree
2018-04-28
Haniel Barbosa
Initial implementation of SygusUnifRL (#1829)
commit
|
commitdiff
|
tree
2018-04-28
Andrew Reynolds
Make construct solution behavior specific to SygusIO...
commit
|
commitdiff
|
tree
2018-04-27
Andrew Reynolds
Print function for equality status. (#1826)
commit
|
commitdiff
|
tree
2018-04-27
Andrew Reynolds
Simplify tangent plane direction (#1824)
commit
|
commitdiff
|
tree
2018-04-27
Haniel Barbosa
New module for synthesizing functions in a data-driven...
commit
|
commitdiff
|
tree
2018-04-27
Andrew Reynolds
Core improvements to extended rewriter (#1820)
commit
|
commitdiff
|
tree
2018-04-26
Andrew Reynolds
Fix subgoal generation context (#1816)
commit
|
commitdiff
|
tree
2018-04-25
yoni206
Refactor array-proofs and uf-proofs (#1655)
commit
|
commitdiff
|
tree
2018-04-25
Andrew Reynolds
Equality resolution in the extended rewriter (#1811)
commit
|
commitdiff
|
tree
2018-04-25
yoni206
Refactor bv-to-bool and bool-to-bv preprocessing passes...
commit
|
commitdiff
|
tree
2018-04-25
Andrew Reynolds
Move candidate rewrite code to own file (#1804)
commit
|
commitdiff
|
tree
next