git.libre-soc.org Git - cvc5.git/search

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-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	Haniel Barbosa	Also exclude ITEs from ITE conditions in SygusUnifStrat...	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	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-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	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-07	Andrew Reynolds	Add support for str.code (#1821)	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	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-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	Andrew Reynolds	Support HORN logic string (#1849)	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	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	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	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
2018-04-25	Andrew Reynolds	Add benchmark requiring subgoal generation with induction...	commit \| commitdiff \| tree
2018-04-25	Andrew Reynolds	Remove nl solve subs option. (#1803)	commit \| commitdiff \| tree
2018-04-25	Andrew Reynolds	Fix issue with multi-triggers that include variable...	commit \| commitdiff \| tree
2018-04-23	Andrew Reynolds	Draft smt comp 2018 for quantifiers and non-linear...	commit \| commitdiff \| tree
2018-04-21	Andrew Reynolds	Improve sygus sampling for strings (#1802)	commit \| commitdiff \| tree
2018-04-21	Andres Noetzli	Remove unused cache.h (#1795)	commit \| commitdiff \| tree
2018-04-20	yoni206	Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...	commit \| commitdiff \| tree
2018-04-20	Andrew Reynolds	Reenable filtering based on ordering in sygus sampler...	commit \| commitdiff \| tree
2018-04-20	Andrew Reynolds	Draft of casc j9 scripts (#1800)	commit \| commitdiff \| tree
2018-04-19	yoni206	Adding config/tap-driver.sh to .gitignore (#1792)	commit \| commitdiff \| tree
2018-04-19	Andres Noetzli	Refactor pbRewrites preprocessing pass (#1767)	commit \| commitdiff \| tree
2018-04-19	Andres Noetzli	Remove tap-driver.sh (#1791)	commit \| commitdiff \| tree
2018-04-17	Andres Noetzli	Add timeout (option) to regression script (#1786)	commit \| commitdiff \| tree
2018-04-16	Andres Noetzli	Disable check proofs/unsat cores for two regs (#1785)	commit \| commitdiff \| tree
2018-04-16	Andrew Reynolds	Make 256 the default cardinality for strings (#1783)	commit \| commitdiff \| tree
2018-04-16	Andrew Reynolds	Skolemize candidate rewrite rule checks (#1777)	commit \| commitdiff \| tree
2018-04-16	Andrew Reynolds	Make strings fmf apply to all but internally generated...	commit \| commitdiff \| tree
2018-04-15	Andrew Reynolds	Fix type error with regexp (#1778)	commit \| commitdiff \| tree
2018-04-14	Andrew Reynolds	Another fix for sygus rr stats. (#1768)	commit \| commitdiff \| tree
2018-04-14	Andres Noetzli	[Reg] Make status/unsat-core detection more robust...	commit \| commitdiff \| tree
2018-04-14	Andres Noetzli	Fix get-unsat-core detection in regression script ...	commit \| commitdiff \| tree
2018-04-14	yoni206	allowing --bool-to-bv without quantifiers (#1771)	commit \| commitdiff \| tree
2018-04-14	Andres Noetzli	Fix use-after-free in eager bitblaster (#1772)	commit \| commitdiff \| tree
2018-04-14	Andrew Reynolds	Disable split for negative contains. (#1774)	commit \| commitdiff \| tree
2018-04-13	Andres Noetzli	Fix issue in regression script when proofs enabled...	commit \| commitdiff \| tree
2018-04-13	Andrew Reynolds	Fix alpha equivalence for higher-order (#1769)	commit \| commitdiff \| tree
2018-04-12	Andrew Reynolds	Fixes for free variables in assertions (#1762)	commit \| commitdiff \| tree
2018-04-11	Aina Niemetz	Refactored BVGauss preprocessing pass. (#1766)	commit \| commitdiff \| tree
2018-04-11	Andrew Reynolds	Properly implement function extensionality based on...	commit \| commitdiff \| tree
2018-04-10	Andrew Reynolds	Improve accuracy of stats for sygus sampler (#1755)	commit \| commitdiff \| tree
2018-04-10	Andres Noetzli	Remove unused arith options (#1758)	commit \| commitdiff \| tree
2018-04-10	Andrew Reynolds	Fix hasSubterm calls for higher-order (#1760)	commit \| commitdiff \| tree
2018-04-10	Andrew Reynolds	Fix higher-order term indexing. (#1754)	commit \| commitdiff \| tree
2018-04-09	Andrew Reynolds	Fix sygus substr static symmetry breaking (#1761)	commit \| commitdiff \| tree
2018-04-08	Andrew Reynolds	Allow predetermined first-order variables when constructing...	commit \| commitdiff \| tree
2018-04-08	Andrew Reynolds	Check free variables in assertions (#1737)	commit \| commitdiff \| tree
2018-04-08	Andrew Reynolds	Do not introduce uinterpreted constants in TPTP parser...	commit \| commitdiff \| tree
2018-04-08	Andrew Reynolds	Add quantifier name attribute. (#1756)	commit \| commitdiff \| tree
2018-04-06	Andres Noetzli	Python regression script (#1662)	commit \| commitdiff \| tree
2018-04-05	Mathias Preiner	Add more general SignExtendUltConst rewriting. (#1385)	commit \| commitdiff \| tree
2018-04-05	Andres Noetzli	Make Python bindings example compatible w/ Python3...	commit \| commitdiff \| tree
2018-04-05	Andres Noetzli	Update README for regression tests (#1746)	commit \| commitdiff \| tree
2018-04-04	Andrew Reynolds	Fix for corner case of higher-order matching (#1708)	commit \| commitdiff \| tree
2018-04-04	Andrew Reynolds	Do not debug check models when unknown (#1748)	commit \| commitdiff \| tree
2018-04-04	Andrew Reynolds	Fix sygus infer (#1747)	commit \| commitdiff \| tree
2018-04-04	Andres Noetzli	Refactor IntToBV preprocessing pass (#1716)	commit \| commitdiff \| tree
2018-04-04	Andres Noetzli	[BVMiniSat] Avoid duplicates in conflicts (#1745)	commit \| commitdiff \| tree
2018-04-03	Andrew Reynolds	Make sygus unif I/O an subclass of sygus unif (#1741)	commit \| commitdiff \| tree
next

RSS Atom