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

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
2018-06-09	Andres Noetzli	Reset decisions at SAT level after solving (#2059)	commit \| commitdiff \| tree
2018-06-08	Mathias Preiner	Disable BV-abstraction in the competition script. ...	commit \| commitdiff \| tree
2018-06-07	Andres Noetzli	Look for cryptominisat5_simple, not cryptominisat5...	commit \| commitdiff \| tree
2018-06-07	Aina Niemetz	Remove invalid assertion (#1993). (#2057)	commit \| commitdiff \| tree
2018-06-07	Andrew Reynolds	Clear pending inferences during datatypes splitting...	commit \| commitdiff \| tree
2018-06-04	Andrew Reynolds	Move assertion. (#2051)	commit \| commitdiff \| tree
2018-06-04	Andres Noetzli	Regressions: Support for requiring CVC4 features (...	commit \| commitdiff \| tree
2018-06-02	Andrew Reynolds	Fix corner case of mixed int/real cegqi. (#2046)	commit \| commitdiff \| tree
2018-06-01	Andrew Reynolds	Fix quantified bv variable elimination (#2039)	commit \| commitdiff \| tree
2018-06-01	Andrew Reynolds	Fix quantifiers conflict lemma handling (#2043)	commit \| commitdiff \| tree
2018-06-01	Andrew Reynolds	Apply preprocessing to counterexample lemmas in CEGQI...	commit \| commitdiff \| tree
2018-05-30	Andres Noetzli	Fix for issue #2002 (#2012)	commit \| commitdiff \| tree
2018-05-30	Andres Noetzli	[SMT-COMP] Print non-(un)sat output to stderr (#2019)	commit \| commitdiff \| tree
2018-05-30	Mathias Preiner	Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV...	commit \| commitdiff \| tree
2018-05-28	Andrew Reynolds	Builtin evaluation functions for sygus (#1991)	commit \| commitdiff \| tree
2018-05-26	Mathias Preiner	Update SymFPU. (#1992)	commit \| commitdiff \| tree
2018-05-25	Andrew Reynolds	Reenable repair const (#1983)	commit \| commitdiff \| tree
2018-05-25	Andres Noetzli	MiniSat: Be more careful about running proof code ...	commit \| commitdiff \| tree
2018-05-25	Andrew Reynolds	Fix various nl assertions. (#1980)	commit \| commitdiff \| tree
2018-05-25	Andrew Reynolds	Fix (#1979)	commit \| commitdiff \| tree
2018-05-24	Andres Noetzli	Fix compiler warnings (#1959)	commit \| commitdiff \| tree
2018-05-24	Andrew Reynolds	Fix (#1975)	commit \| commitdiff \| tree
2018-05-24	Andrew Reynolds	Fixes for non-linear check model (#1974)	commit \| commitdiff \| tree
next

RSS Atom