projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
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
2018-06-01
Andrew Reynolds
Fix quantifiers conflict lemma handling (#2043)
commit
|
commitdiff
|
tree
2018-06-01
Andrew Reynolds
Apply preprocessing to counterexample lemmas in CEGQI...
commit
|
commitdiff
|
tree
2018-06-01
Andrew Reynolds
Use monomial sum utility to solve for quantifiers...
commit
|
commitdiff
|
tree
2018-06-01
Andrew Reynolds
Reduce before preregister. (#2025)
commit
|
commitdiff
|
tree
2018-05-31
Mathias Preiner
Fix bv-abstraction check for AND with non bit-vector...
commit
|
commitdiff
|
tree
2018-05-30
Aina Niemetz
Ignore license key in set-info command. (#2021)
commit
|
commitdiff
|
tree
2018-05-30
Andres Noetzli
Fix for issue #2002 (#2012)
commit
|
commitdiff
|
tree
2018-05-30
Andrew Reynolds
Fixes for quantifiers + incremental (#2009)
commit
|
commitdiff
|
tree
2018-05-30
Andres Noetzli
[SMT-COMP] Print non-(un)sat output to stderr (#2019)
commit
|
commitdiff
|
tree
2018-05-30
Mathias Preiner
Normalize negated bit-vector terms over equalities...
commit
|
commitdiff
|
tree
2018-05-30
Mathias Preiner
Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFB...
commit
|
commitdiff
|
tree
2018-05-30
Andrew Reynolds
Draft run script for strings smt comp 2018. (#2016)
commit
|
commitdiff
|
tree
2018-05-29
Andres Noetzli
Make user's SMT2 version override file version (#2004)
commit
|
commitdiff
|
tree
2018-05-29
Andrew Reynolds
Disable minisat elimination when nonlinear is enabled...
commit
|
commitdiff
|
tree
2018-05-29
Andres Noetzli
Track input language in a single place (#2003)
commit
|
commitdiff
|
tree
2018-05-28
Andrew Reynolds
Builtin evaluation functions for sygus (#1991)
commit
|
commitdiff
|
tree
2018-05-27
Andrew Reynolds
Fix cegqi assertions for quantified non-linear cases...
commit
|
commitdiff
|
tree
2018-05-27
Andres Noetzli
Fix no-cbqi-innermost option name in run script (#1994)
commit
|
commitdiff
|
tree
2018-05-26
Mathias Preiner
Update SymFPU. (#1992)
commit
|
commitdiff
|
tree
2018-05-25
Andrew Reynolds
Reenable repair const (#1983)
commit
|
commitdiff
|
tree
2018-05-25
Andres Noetzli
MiniSat: Be more careful about running proof code ...
commit
|
commitdiff
|
tree
2018-05-25
Mathias Preiner
Add QF_BV configuration for SMTCOMP'18. (#1981)
commit
|
commitdiff
|
tree
2018-05-25
Andrew Reynolds
Fix various nl assertions. (#1980)
commit
|
commitdiff
|
tree
2018-05-25
Andrew Reynolds
Fix (#1979)
commit
|
commitdiff
|
tree
2018-05-24
Andrew Reynolds
Improve simple constant symmetry breaking for sygus...
commit
|
commitdiff
|
tree
2018-05-24
Andres Noetzli
Fix compiler warnings (#1959)
commit
|
commitdiff
|
tree
2018-05-24
Andrew Reynolds
Fix (#1975)
commit
|
commitdiff
|
tree
2018-05-24
Andrew Reynolds
Fixes for non-linear check model (#1974)
commit
|
commitdiff
|
tree
2018-05-24
Andrew Reynolds
Fix nl regression for unsat cores. (#1973)
commit
|
commitdiff
|
tree
2018-05-24
Andrew Reynolds
Remove spurious assertion in nonlinear extension (...
commit
|
commitdiff
|
tree
2018-05-23
Haniel Barbosa
Towards better symbolic enumeration in SyGuS (#1971)
commit
|
commitdiff
|
tree
2018-05-23
Andrew Reynolds
Add notions of evaluated kinds in TheoryModel (#1947)
commit
|
commitdiff
|
tree
2018-05-23
Andres Noetzli
Remove ProofProxy (#1965)
commit
|
commitdiff
|
tree
2018-05-23
Andrew Reynolds
Generalize check-model in NonLinearExtension for quadra...
commit
|
commitdiff
|
tree
2018-05-23
Andres Noetzli
Set same options for proofs as for unsat cores (#1957)
commit
|
commitdiff
|
tree
2018-05-23
Andrew Reynolds
Repair constants using symbolic constructors (#1960)
commit
|
commitdiff
|
tree
2018-05-22
Andrew Reynolds
Parse error for sygus grammar term with multiple let...
commit
|
commitdiff
|
tree
2018-05-22
Andres Noetzli
Disable symmetry breaker for unsat cores (#1958)
commit
|
commitdiff
|
tree
2018-05-22
Andrew Reynolds
Make sygus infer find function definitions (#1951)
commit
|
commitdiff
|
tree
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
next