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

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
2018-02-14	Aina Niemetz	Provide a uniform way to serialize node containers...	commit \| commitdiff \| tree
2018-02-13	Aina Niemetz	Moved (unrecursified) bv::utils::collectVars. (#1602)	commit \| commitdiff \| tree
2018-02-13	Aina Niemetz	Skip header for determining top contributors list....	commit \| commitdiff \| tree
2018-02-13	Andrew Reynolds	Option to use extended rewriter as a preprocessing...	commit \| commitdiff \| tree
2018-02-12	Andrew Reynolds	Minor improvements to sygus sampler (#1598)	commit \| commitdiff \| tree
2018-02-11	Aina Niemetz	Move (unrecursified) bv::utils::numNodes to lazy_bitblaster...	commit \| commitdiff \| tree
2018-02-11	Andrew Reynolds	More minor improvements to synth-rr (#1597)	commit \| commitdiff \| tree
2018-02-10	Aina Niemetz	Move BitVector specific funs from bv::utils to util...	commit \| commitdiff \| tree
2018-02-09	Andrew Reynolds	Class to reduce printing of redundant candidate rewrites...	commit \| commitdiff \| tree
2018-02-09	Tim King	Replacing an incorrect reference to an injected class...	commit \| commitdiff \| tree
2018-02-08	Aina Niemetz	Clean up bv utils (part one). (#1580)	commit \| commitdiff \| tree
2018-02-08	Andrew Reynolds	Minor improvements to sygus sampling. (#1577)	commit \| commitdiff \| tree
2018-02-08	Tim King	Removing an unused variable. (#1576)	commit \| commitdiff \| tree
2018-02-08	Aina Niemetz	Reduce number of Travis builds. (#1578)	commit \| commitdiff \| tree
2018-02-07	Aina Niemetz	Use template for bv::utils::mkOr. (#1570)	commit \| commitdiff \| tree
2018-02-07	Andrew Reynolds	Add remaining transcendental functions (#1551)	commit \| commitdiff \| tree
2018-02-07	Aina Niemetz	Use template for bv::utils::mkAnd. (#1569)	commit \| commitdiff \| tree
2018-02-07	Aina Niemetz	Renamed bv::utils::isBVGroundTerm to isBvConstTerm...	commit \| commitdiff \| tree
2018-02-07	Aina Niemetz	Split and document theory_bv_utils. (#1566)	commit \| commitdiff \| tree
2018-02-07	Mathias Preiner	Use separate shell script for common get-* script parts...	commit \| commitdiff \| tree
2018-02-06	Andrew Reynolds	Fix two multiply-by-constant corner cases for bv rewriter...	commit \| commitdiff \| tree
2018-02-06	Andrew Reynolds	Fix rewrite for string replace (#1537)	commit \| commitdiff \| tree
2018-02-06	Tim King	Using getOperator() directly instead of using -1. CID...	commit \| commitdiff \| tree
2018-02-06	Andrew Reynolds	Statically eliminate redundant sygus constructors ...	commit \| commitdiff \| tree
2018-02-05	Tim King	Removing references to __gnu_cxx. (#1541)	commit \| commitdiff \| tree
2018-02-04	Andrew Reynolds	Sample based on sygus grammar by default (#1558)	commit \| commitdiff \| tree
2018-02-03	Andrew Reynolds	Option to use sampling for CEGIS (#1555)	commit \| commitdiff \| tree
2018-02-02	Andrew Reynolds	Fix remaining synthesis solution regressions (#1557)	commit \| commitdiff \| tree
2018-02-01	Andrew Reynolds	Add interface in sygus to get synthesis solution Nodes...	commit \| commitdiff \| tree
2018-02-01	Andrew Reynolds	Use sygus to synthesize/verify rewrite rules (#1547)	commit \| commitdiff \| tree
2018-01-30	Andrew Reynolds	Further clean and document datatypes rewriter (#1548)	commit \| commitdiff \| tree
2018-01-29	Andrew Reynolds	Generalize explanations for PBE sygus strings based...	commit \| commitdiff \| tree
2018-01-28	Andrew Reynolds	Sort children of all commutative operators for sygus...	commit \| commitdiff \| tree
2018-01-25	Tim King	Commenting out throw specifiers on SmtEngine. These...	commit \| commitdiff \| tree
2018-01-25	Aina Niemetz	Added unit tests for PLUS, NEG, NOT ICs for CBQI BV...	commit \| commitdiff \| tree
2018-01-23	Aina Niemetz	Fix MULT handling for CBQI BV. (#1531)	commit \| commitdiff \| tree
2018-01-23	Tim King	Commenting out throw specifiers for DeltaRationExceptions...	commit \| commitdiff \| tree
2018-01-22	Aina Niemetz	Add previous concat handling for CBQI BV as heuristic...	commit \| commitdiff \| tree
2018-01-22	Aina Niemetz	Refactor and fix solveBvLit for CBQI BV. (#1526)	commit \| commitdiff \| tree
2018-01-22	Andrew Reynolds	Only push/pop around check-sat if it is associated...	commit \| commitdiff \| tree
2018-01-17	Tim King	Removes yet more throw specifiers. Updating the documentatio...	commit \| commitdiff \| tree
2018-01-16	Tim King	Removing more miscellaneous throw specifiers. (#1509)	commit \| commitdiff \| tree
2018-01-15	Tim King	Removing throw specifiers from Type. (#1511)	commit \| commitdiff \| tree
2018-01-12	Andrew Reynolds	Improvements for CBQI BV (#1504)	commit \| commitdiff \| tree
2018-01-10	Aina Niemetz	Removed division by constant handling for CBQI BV ...	commit \| commitdiff \| tree
2018-01-10	Tim King	Removing throw specifiers from type enumerators. (...	commit \| commitdiff \| tree
2018-01-10	Mathias Preiner	Fix linearization for terms where the solve variable...	commit \| commitdiff \| tree
next

RSS Atom