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

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
2018-04-03	Andrew Reynolds	Use choice when expanding definitions for inverse transcende...	commit \| commitdiff \| tree
2018-04-03	Andrew Reynolds	Internal sygus type checking (#1734)	commit \| commitdiff \| tree
2018-04-03	Andrew Reynolds	Improvements to extended rewriter for Booleans and...	commit \| commitdiff \| tree
2018-04-02	Andrew Reynolds	Make sygus unif utility use sygus unif strategies ...	commit \| commitdiff \| tree
2018-04-02	yoni206	a formula should be an instance of itself (#1668)	commit \| commitdiff \| tree
2018-03-30	Andrew Reynolds	Disable regression (#1731)	commit \| commitdiff \| tree
2018-03-30	Andrew Reynolds	Split strategy representation from SygusUnif (#1730)	commit \| commitdiff \| tree
2018-03-30	Andrew Reynolds	Do not use factoring inference for transcendental functions...	commit \| commitdiff \| tree
2018-03-29	Andrew Reynolds	Simplify sygus unif so that it is one-to-one with functions...	commit \| commitdiff \| tree
2018-03-27	Andrew Reynolds	Make sygus pbe use sygus unif utility (#1724)	commit \| commitdiff \| tree
2018-03-27	Andrew Reynolds	Fix for --sygus-rr-synth (#1723)	commit \| commitdiff \| tree
2018-03-27	Andrew Reynolds	Make sygus unif utility (#1720)	commit \| commitdiff \| tree
2018-03-27	Andrew Reynolds	Filter candidate rewrites based on matching (#1682)	commit \| commitdiff \| tree
2018-03-27	Andrew Reynolds	Documentation and simplifications for PBE (#1677)	commit \| commitdiff \| tree
2018-03-26	Andres Noetzli	Regression level 0 for distcheck on Travis (#1714)	commit \| commitdiff \| tree
2018-03-26	Andres Noetzli	Add support for filtering regressions with regex (...	commit \| commitdiff \| tree
2018-03-26	Andres Noetzli	Fix memory leak in bvminisat (#1710)	commit \| commitdiff \| tree
2018-03-26	Andres Noetzli	Make Java bindings work with newer build envs (#1709)	commit \| commitdiff \| tree
2018-03-26	Andrew Reynolds	Synth-check and accelerate options for sygus-rr (#1691)	commit \| commitdiff \| tree
2018-03-26	Andrew Reynolds	Abort when sygus-verify finds unsoundness. (#1717)	commit \| commitdiff \| tree
2018-03-26	Andres Noetzli	Rewrites for substr of strings of length one (#1712)	commit \| commitdiff \| tree
2018-03-23	Andrew Reynolds	Add a few quantifiers regressions to improve coverage...	commit \| commitdiff \| tree
2018-03-23	Andrew Reynolds	Remove unused code (#1700)	commit \| commitdiff \| tree
2018-03-23	Andrew Reynolds	Minor reorganization for ematching (#1701)	commit \| commitdiff \| tree
2018-03-23	Andrew Reynolds	Enable post-condition strenghtening by default for...	commit \| commitdiff \| tree
2018-03-21	Andres Noetzli	Fix 'make regress' (#1683)	commit \| commitdiff \| tree
2018-03-21	Mathias Preiner	Refactor mkoptions (#1631)	commit \| commitdiff \| tree
2018-03-21	Andrew Reynolds	More rewrites for indexof (#1648)	commit \| commitdiff \| tree
2018-03-21	Andres Noetzli	Move regression tests to single Makefile.am (#1658)	commit \| commitdiff \| tree
2018-03-21	Andres Noetzli	Fix various regression tests (#1657)	commit \| commitdiff \| tree
2018-03-21	Andrew Reynolds	Fix for string disequality processing (#1679)	commit \| commitdiff \| tree
2018-03-20	Mathias Preiner	Add support for CaDiCaL as eager BV SAT solver. (#1675)	commit \| commitdiff \| tree
2018-03-20	Andrew Reynolds	Internally remove redundant assertions and infer equalities...	commit \| commitdiff \| tree
2018-03-20	Andrew Reynolds	Minor fix and addition to sygus sampler (#1678)	commit \| commitdiff \| tree
2018-03-20	Andrew Reynolds	Enable CEGQI for non-linear (#1674)	commit \| commitdiff \| tree
2018-03-19	Andrew Reynolds	Document inferences for strings (#1642)	commit \| commitdiff \| tree
2018-03-13	Mathias Preiner	Use Cryptominisat version 5.0.2 (instead of 4.2.0)...	commit \| commitdiff \| tree
2018-03-13	Aina Niemetz	SmtEngine::getModel() is now public. (#1665)	commit \| commitdiff \| tree
2018-03-09	Aina Niemetz	Printers are now managed as unique_ptr (fix mem leak...	commit \| commitdiff \| tree
2018-03-09	Aina Niemetz	Some minor cleanup in bv::utils. (#1663)	commit \| commitdiff \| tree
2018-03-09	Aina Niemetz	Add support for SMT-LIB v2.5 command get-unsat-assumptions...	commit \| commitdiff \| tree
2018-03-09	Mathias Preiner	Cleanup Cryptominisat SAT wrapper. (#1652)	commit \| commitdiff \| tree
2018-03-09	Mathias Preiner	Fix Travis for unit test compilation errors. (#1651)	commit \| commitdiff \| tree
2018-03-07	Mathias Preiner	Make statistics output consistent. (#1647)	commit \| commitdiff \| tree
2018-03-06	Andrew Reynolds	Simplify initialization of quantifiers engine (#1641)	commit \| commitdiff \| tree
2018-03-06	Andrew Reynolds	Refactor symmetry breaking in datatypes sygus (#1640)	commit \| commitdiff \| tree
2018-03-06	Andrew Reynolds	Update semantics for string indexof and replace (#1630)	commit \| commitdiff \| tree
2018-03-05	Mathias Preiner	Enable -Wsuggest-override by default. (#1643)	commit \| commitdiff \| tree
2018-03-05	Andrew Reynolds	Fix for sampler. (#1639)	commit \| commitdiff \| tree
2018-03-05	Aina Niemetz	Add support for check-sat-assuming. (#1637)	commit \| commitdiff \| tree
2018-03-05	Aina Niemetz	Add CVC4_PUBLIC keyword to overloads of << for Expr...	commit \| commitdiff \| tree
2018-03-05	Aina Niemetz	Add uniform way to serialize containers of Expr to...	commit \| commitdiff \| tree
2018-03-02	Andrew Reynolds	Optimization for sygus streaming mode (#1636)	commit \| commitdiff \| tree
2018-03-02	Andrew Reynolds	Simplify sygus wrt miniscoping (#1634)	commit \| commitdiff \| tree
2018-03-02	Andrew Reynolds	Print candidate rewrites in terms of original grammar...	commit \| commitdiff \| tree
2018-03-02	Andrew Reynolds	Create infrastructure for sygus modules (#1632)	commit \| commitdiff \| tree
2018-02-28	Aina Niemetz	SmtEngine::getAssignment now returns a vector of assignments...	commit \| commitdiff \| tree
2018-02-28	Andrew Reynolds	Minor fixes for rec-fun (#1616)	commit \| commitdiff \| tree
2018-02-28	Aina Niemetz	Remove unused code in pushDefineFunRecScop in smt2...	commit \| commitdiff \| tree
2018-02-27	Andrew Reynolds	Improve rewriter for string indexof (#1592)	commit \| commitdiff \| tree
2018-02-27	Andrew Reynolds	Option to not use partial function semantics for arithmetic...	commit \| commitdiff \| tree
2018-02-27	Andrew Reynolds	Improvements to sygus sampling (#1621)	commit \| commitdiff \| tree
2018-02-24	Andres Noetzli	Add unit tests for BitVector, minor BV rewrite fix...	commit \| commitdiff \| tree
2018-02-23	Aina Niemetz	Split and document bitvector.h. (#1615)	commit \| commitdiff \| tree
2018-02-23	Andrew Reynolds	Fix cd-simplification for strings (#1624)	commit \| commitdiff \| tree
2018-02-22	Andrew Reynolds	Minor improvements to string rewriter (#1572)	commit \| commitdiff \| tree
2018-02-22	Aina Niemetz	Fixed disabling the BV equality slicer for quantifiers...	commit \| commitdiff \| tree
2018-02-22	Aina Niemetz	Disable BV equality slicer if not pure QF_BV. (#1619)	commit \| commitdiff \| tree
2018-02-20	Aina Niemetz	Improve documentation of bv::utils::isCoreTerm (#1617)	commit \| commitdiff \| tree
2018-02-20	Aina Niemetz	Moved and simplified bv::utils::intersect. (#1614)	commit \| commitdiff \| tree
2018-02-20	Aina Niemetz	Unrecursified and merged bv::utils::is(Core\|Equality...	commit \| commitdiff \| tree
2018-02-17	Aina Niemetz	bv::utils::mk(And\|Or) Do not return true if size of...	commit \| commitdiff \| tree
2018-02-16	Aina Niemetz	Removed bv::utils::mkConjunction (redundant). (#1610)	commit \| commitdiff \| tree
2018-02-15	Andrew Reynolds	Fix corner case for rewrite of mult by pow 2 (#1601)	commit \| commitdiff \| tree
2018-02-14	Andrew Reynolds	Quantifiers subdirectories (#1608)	commit \| commitdiff \| tree
next

RSS Atom