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

2018-08-07	Andrew Reynolds	Make flat form inferences optional in strings (#2277)	commit \| commitdiff \| tree
2018-08-07	Andrew Reynolds	Add RegLan to smt2/sygus parsers. (#2276)	commit \| commitdiff \| tree
2018-08-07	Andrew Reynolds	Move sygus quantifier elimination step for non-ground...	commit \| commitdiff \| tree
2018-08-06	Andrew Reynolds	Fixes and improvements for single invocation inference...	commit \| commitdiff \| tree
2018-08-06	Andrew Reynolds	Fix degenerate case of sygus grammar construction for...	commit \| commitdiff \| tree
2018-08-04	Aina Niemetz	Add rewrite for nested BITVECTOR_ITE with cond_outer...	commit \| commitdiff \| tree
2018-08-04	Aina Niemetz	Add rewrite for BITVECTOR_ITE with const children....	commit \| commitdiff \| tree
2018-08-03	Aina Niemetz	Add rewrite for BITVECTOR_ITE with term_then == term_else...	commit \| commitdiff \| tree
2018-08-03	Andrew Reynolds	Eliminate option for sygus UF evaluation functions...	commit \| commitdiff \| tree
2018-08-03	Aina Niemetz	Add timer for BV inequality solver. (#2265)	commit \| commitdiff \| tree
2018-08-02	Andrew Reynolds	Parse standard separation logic inputs (#2257)	commit \| commitdiff \| tree
2018-08-02	Andrew Reynolds	Improve CEGQI heuristics involving equality and multiple...	commit \| commitdiff \| tree
2018-08-02	Andrew Reynolds	Fix candidate rewrite utilities for non-first-class...	commit \| commitdiff \| tree
2018-08-02	Aina Niemetz	Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with...	commit \| commitdiff \| tree
2018-08-02	Andrew Reynolds	Remove references to deprecated propagate as decision...	commit \| commitdiff \| tree
2018-08-02	Andrew Reynolds	Fix API call for reg exp. (#2248)	commit \| commitdiff \| tree
2018-08-02	Andrew Reynolds	Fix issues with printing parametric datatypes in smt2...	commit \| commitdiff \| tree
2018-08-01	Mathias Preiner	Fix bool-to-bv preprocessing pass for non-{bv,bool...	commit \| commitdiff \| tree
2018-08-01	Aina Niemetz	InteractiveShell: Remove redundant options argument...	commit \| commitdiff \| tree
2018-08-01	Aina Niemetz	New C++ API: Fixed ownership of options object. (#2243)	commit \| commitdiff \| tree
2018-08-01	Mathias Preiner	Remove hasAssertions() method from eager BV solver...	commit \| commitdiff \| tree
2018-07-31	Mathias Preiner	Fix option handler for lazy/bv-sat-solver combinations...	commit \| commitdiff \| tree
2018-07-30	Mathias Preiner	Add support for incremental eager bit-blasting. (#1838)	commit \| commitdiff \| tree
2018-07-27	Mathias Preiner	Require argument description for non-{bool,void} options...	commit \| commitdiff \| tree
2018-07-27	Andres Noetzli	Fix issues related to cxxtest in configure.ac (#2226)	commit \| commitdiff \| tree
2018-07-27	Mathias Preiner	Fix CryptoMiniSat config to allow system versions....	commit \| commitdiff \| tree
2018-07-26	yoni206	Disabling bvLazyRewriteExtf in the right place (#2214)	commit \| commitdiff \| tree
2018-07-26	Andrew Reynolds	Fix a few issues in the sygus sampler related to evaluation...	commit \| commitdiff \| tree
2018-07-26	Aina Niemetz	New C++ API: Third batch of commands (SMT-LIB). (#2212)	commit \| commitdiff \| tree
2018-07-26	Aina Niemetz	New C++ API: Second batch of commands (SMT-LIB). (...	commit \| commitdiff \| tree
2018-07-25	Andrew Reynolds	Move reg exp rewrites from prerewrite to postrewrite...	commit \| commitdiff \| tree
2018-07-25	Mathias Preiner	Use CryptoMiniSat 5.6.3. (#2205)	commit \| commitdiff \| tree
2018-07-24	Andrew Reynolds	Improvements to sets + cardinality + quantifiers (...	commit \| commitdiff \| tree
2018-07-24	Aina Niemetz	New C++ API: First batch of commands (SMT-LIB and...	commit \| commitdiff \| tree
2018-07-23	Andrew Reynolds	Improve rewriter for regular expression concatenation...	commit \| commitdiff \| tree
2018-07-23	Andrew Reynolds	Generalize symmetry detection for 1 symmetry variable...	commit \| commitdiff \| tree
2018-07-23	Aina Niemetz	New C++ API: Implementation of Solver class: OpTerm...	commit \| commitdiff \| tree
2018-07-23	Aina Niemetz	New C++ API: declare-datatype. (#2166)	commit \| commitdiff \| tree
2018-07-23	Andrew Reynolds	sygusComp2018: add regressions (#2191)	commit \| commitdiff \| tree
2018-07-23	Andrew Reynolds	Fix warning in sygus PBE (#2190)	commit \| commitdiff \| tree
2018-07-21	Andrew Reynolds	Optimizations and fixes for computing whether a type...	commit \| commitdiff \| tree
2018-07-21	Andrew Reynolds	sygusComp2018: refactor and improve sygus io utility...	commit \| commitdiff \| tree
2018-07-20	Andrew Reynolds	Cleanup and additions for candidate generator (#2173)	commit \| commitdiff \| tree
2018-07-20	Andrew Reynolds	sygusComp2018: minor changes to repair constant utility...	commit \| commitdiff \| tree
2018-07-17	Andrew Reynolds	sygusComp2018: pbe multi-enumerator fairness option...	commit \| commitdiff \| tree
2018-07-17	yoni206	Refactor sep-pre-skolem-emp preprocessing pass	commit \| commitdiff \| tree
2018-07-17	Andrew Reynolds	Minor cleanup and fixes for conflict-based instantiation...	commit \| commitdiff \| tree
2018-07-17	Andrew Reynolds	Do extended rewrite on results of quantifier elimination...	commit \| commitdiff \| tree
2018-07-17	Andrew Reynolds	Purify applications of exp to transcendental arguments...	commit \| commitdiff \| tree
2018-07-17	Andrew Reynolds	sygusComp2018: update policies for solution reconstruction...	commit \| commitdiff \| tree
2018-07-17	Andrew Reynolds	sygusComp2018: Improvements to datatypes sygus solver...	commit \| commitdiff \| tree
2018-07-17	Andrew Reynolds	sygusComp 2018: updates to sygus term database (#2170)	commit \| commitdiff \| tree
2018-07-14	Andrew Reynolds	sygusComp2018: update semantics for declare-fun in...	commit \| commitdiff \| tree
2018-07-13	Andrew Reynolds	Fix and improve grammar normalization for any constant...	commit \| commitdiff \| tree
2018-07-13	Andres Noetzli	Properly clean up assertion stack in CnfProof (#2147)	commit \| commitdiff \| tree
2018-07-13	Andrew Reynolds	sygusComp2018: optimization for collect model info...	commit \| commitdiff \| tree
2018-07-13	Aina Niemetz	New C++ API: Minor reorder. (#2163)	commit \| commitdiff \| tree
2018-07-13	Aina Niemetz	New C++ API: Implementation of datatype classes. (...	commit \| commitdiff \| tree
2018-07-13	Aina Niemetz	New C++ API: Implementation of Solver class: Consts...	commit \| commitdiff \| tree
2018-07-08	Andres Noetzli	Add more sophisticated floating-point sampler (#2155)	commit \| commitdiff \| tree
2018-07-06	Andrew Reynolds	Split ext theory to own file and document (#1809)	commit \| commitdiff \| tree
2018-07-06	Aina Niemetz	New C++ API: Implementation of Solver class: Sort handling...	commit \| commitdiff \| tree
2018-07-04	Andrew Reynolds	More cleanup in strings (#2138)	commit \| commitdiff \| tree
2018-07-04	Aina Niemetz	New C++ API: Implementation of datatype declaration...	commit \| commitdiff \| tree
2018-07-04	Aina Niemetz	New C++ API: Implementation of OpTerm. (#2132)	commit \| commitdiff \| tree
2018-07-03	Aina Niemetz	New C++ API: Implementation of Term. (#2131)	commit \| commitdiff \| tree
2018-07-03	Aina Niemetz	New C++ API: Implementation of Kind maps. (#2130)	commit \| commitdiff \| tree
2018-07-03	Aina Niemetz	Fix datatypes example: nil constructor was missing...	commit \| commitdiff \| tree
2018-07-03	Andrew Reynolds	sygusComp2018: update sygus-related options setting...	commit \| commitdiff \| tree
2018-07-03	Andrew Reynolds	Remove miscellaneous dead and unused code from quantifiers...	commit \| commitdiff \| tree
2018-07-03	Andres Noetzli	Add regression test for issue #1986 (#2114)	commit \| commitdiff \| tree
2018-07-02	Aina Niemetz	Refactor ApplySubsts preprocessing pass. (#2120)	commit \| commitdiff \| tree
2018-07-02	Aina Niemetz	New C++ API: Implementation of Sort. (#2122)	commit \| commitdiff \| tree
2018-07-02	Andrew Reynolds	Remove some dead code from theory strings (#2125)	commit \| commitdiff \| tree
2018-07-02	Andrew Reynolds	Modify cegqi heuristic for finite datatypes (#2126)	commit \| commitdiff \| tree
2018-07-02	Andrew Reynolds	Improve error message. (#2124)	commit \| commitdiff \| tree
2018-06-29	Andrew Reynolds	Use evaluator in sygus sampler. (#2117)	commit \| commitdiff \| tree
2018-06-29	Aina Niemetz	New C++ API: Implementation of Result. (#2112)	commit \| commitdiff \| tree
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	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	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-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-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-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
next

RSS Atom