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

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	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-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	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 candidate...	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-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
next

RSS Atom