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

2021-09-03	Andrew Reynolds	Eliminate backwards ref to SmtEngine from abduction...	commit \| commitdiff \| tree
2021-09-03	Aina Niemetz	theory: Have more classes in theory with reference...	commit \| commitdiff \| tree
2021-09-03	Aina Niemetz	theory: Have Theory and TheoryArith* derive from EnvObj...	commit \| commitdiff \| tree
2021-09-03	Gereon Kremer	Remove "experimental" options (#7124)	commit \| commitdiff \| tree
2021-09-03	Aina Niemetz	pp: Have PreprocessingPassContext derive from EnvObj...	commit \| commitdiff \| tree
2021-09-02	Andrew Reynolds	Add LFSC node converter (#6944)	commit \| commitdiff \| tree
2021-09-02	Gereon Kremer	Refactor options handlers (#7080)	commit \| commitdiff \| tree
2021-09-02	Andres Noetzli	[Unit Tests] Fix shell test for Editline (#7117)	commit \| commitdiff \| tree
2021-09-02	Aina Niemetz	Disable sygus-inst for regression close to time limit...	commit \| commitdiff \| tree
2021-09-02	Aina Niemetz	EnvObj: Restrict access. (#7121)	commit \| commitdiff \| tree
2021-09-02	Gereon Kremer	Add API check whether option in getOptionInfo() exists...	commit \| commitdiff \| tree
2021-09-02	Gereon Kremer	Driver & Options cleanup (#7109)	commit \| commitdiff \| tree
2021-09-02	Andrew Reynolds	Remove more instances of ufHo (#7087)	commit \| commitdiff \| tree
2021-09-02	Gereon Kremer	Remove options::getAll() (#7111)	commit \| commitdiff \| tree
2021-09-02	Andres Noetzli	[CI] Add step for running unit/API tests (#7116)	commit \| commitdiff \| tree
2021-09-02	Andrew Reynolds	Implement lazy proof checking modes (#7106)	commit \| commitdiff \| tree
2021-09-02	Aina Niemetz	Remove PreprocessingPassContext::getSmt(). (#7118)	commit \| commitdiff \| tree
2021-09-02	Andres Noetzli	Remove unused `Backtracker` (#7115)	commit \| commitdiff \| tree
2021-09-02	Andres Noetzli	[Unit Tests] Fix bags rewrite test (#7114)	commit \| commitdiff \| tree
2021-09-02	Aina Niemetz	pp: Derive PreprocessingPass from EnvObj. (#7112)	commit \| commitdiff \| tree
2021-09-02	Aina Niemetz	Enable sygus-inst for FP, NIA and NRA. (#7098)	commit \| commitdiff \| tree
2021-09-02	Aina Niemetz	rewriter: Make rewriteEqualityExt non-static. (#7110)	commit \| commitdiff \| tree
2021-09-02	Aina Niemetz	Add class EnvObj. (#7113)	commit \| commitdiff \| tree
2021-09-02	Andres Noetzli	Update CI to macOS 11 (#7104)	commit \| commitdiff \| tree
2021-09-01	Aina Niemetz	Clean up and document PP context. (#7102)	commit \| commitdiff \| tree
2021-09-01	Aina Niemetz	Clean up TheoryEngine header according to code style...	commit \| commitdiff \| tree
2021-09-01	Haniel Barbosa	[proof] [sat] Fix lost reference to reason when processing...	commit \| commitdiff \| tree
2021-09-01	Andrew Reynolds	Print response to get-model using the API (#7084)	commit \| commitdiff \| tree
2021-09-01	Aina Niemetz	rewriter: Make registerTheoryRewriter non-static. ...	commit \| commitdiff \| tree
2021-09-01	mudathirmahgoub	Fixed TestTheoryWhiteBagsRewriter.map failure (#7103)	commit \| commitdiff \| tree
2021-09-01	Andrew Reynolds	Fix issues with cyclic proofs due to double SYMM application...	commit \| commitdiff \| tree
2021-09-01	Gereon Kremer	Make driver::totalTime a TimerStat (#7089)	commit \| commitdiff \| tree
2021-09-01	Gereon Kremer	No longer use direct access to options in driver (...	commit \| commitdiff \| tree
2021-09-01	Aina Niemetz	rewriter: Make clearCaches non-static. (#7100)	commit \| commitdiff \| tree
2021-09-01	Andrew Reynolds	Lazy proof reconstruction for strings theory solver...	commit \| commitdiff \| tree
2021-08-31	Aina Niemetz	bv: Remove dump=bv-rewrites. (#7099)	commit \| commitdiff \| tree
2021-08-31	Gereon Kremer	Make sure modes are sorted in ModeInfo (#7097)	commit \| commitdiff \| tree
2021-08-31	yoni206	bv-to-int-module: implementations and stubs for translating...	commit \| commitdiff \| tree
2021-08-31	Andrew Reynolds	Fix normal forms context-dependent simplification for...	commit \| commitdiff \| tree
2021-08-31	Andrew Reynolds	Make regular expression sort not closed enumerable...	commit \| commitdiff \| tree
2021-08-30	Gereon Kremer	Add API function to obtain information about a single...	commit \| commitdiff \| tree
2021-08-30	mudathirmahgoub	Add kind BAG_MAP and its type rule to bags (#6503)	commit \| commitdiff \| tree
2021-08-30	Andrew Reynolds	Further refactoring of set defaults for incompatibility...	commit \| commitdiff \| tree
2021-08-30	Gereon Kremer	Refactor filename handling (#7088)	commit \| commitdiff \| tree
2021-08-30	Andrew Reynolds	Fix proof equality engine for "no-explain" premises...	commit \| commitdiff \| tree
2021-08-30	yoni206	python docs for Datatype-related classes (#7058)	commit \| commitdiff \| tree
2021-08-30	Andrew Reynolds	Fix quantifiers dynamic split module for parametric...	commit \| commitdiff \| tree
2021-08-27	Gereon Kremer	Add Driver options (#7078)	commit \| commitdiff \| tree
2021-08-27	Gereon Kremer	Handle languages as strings in driver (#7074)	commit \| commitdiff \| tree
2021-08-27	Andrew Reynolds	Expand definitions in sygus operators at the SMT level...	commit \| commitdiff \| tree
2021-08-27	Andrew Reynolds	Add n-ary match trie utility (#6909)	commit \| commitdiff \| tree
2021-08-27	Andrew Reynolds	Add missing methods to Solver API for models (#7052)	commit \| commitdiff \| tree
2021-08-27	yoni206	Add `isNull` to cpp api tests, python api, and python...	commit \| commitdiff \| tree
2021-08-26	Gereon Kremer	Fix a subtle issues with squashing the docs-ci history...	commit \| commitdiff \| tree
2021-08-26	Andrew Reynolds	Eliminate currentSmtEngine for subsolver calls (#7068)	commit \| commitdiff \| tree
2021-08-26	Andrew Reynolds	Dump models for isNotEntailed results (#7071)	commit \| commitdiff \| tree
2021-08-26	Andrew Reynolds	Make datatype selector expansion to its own accessible...	commit \| commitdiff \| tree
2021-08-26	Gereon Kremer	Improve integration of nonlinear arithmetic into the...	commit \| commitdiff \| tree
2021-08-26	Mathias Preiner	int2bv: Fix conversion of signed bit-vector values...	commit \| commitdiff \| tree
2021-08-26	Gereon Kremer	Consolidate language types (#7065)	commit \| commitdiff \| tree
2021-08-25	Gereon Kremer	Add missing include (#7067)	commit \| commitdiff \| tree
2021-08-25	Andrew Reynolds	Eliminate calls to currentSmtEngine (#7060)	commit \| commitdiff \| tree
2021-08-24	Andrew Reynolds	Split higher-order term database (#7045)	commit \| commitdiff \| tree
2021-08-24	Andrew Reynolds	Refactor enumerator management in synth conjecture...	commit \| commitdiff \| tree
2021-08-24	yoni206	bv-to-int: more implementations (#7051)	commit \| commitdiff \| tree
2021-08-24	Andrew Reynolds	Top-level structure for set defaults (#7047)	commit \| commitdiff \| tree
2021-08-24	Andrew Reynolds	Uniform treatment of trusted theory inferences in proofs...	commit \| commitdiff \| tree
2021-08-24	Andrew Reynolds	Miscellaneous changes from proof-new (#7042)	commit \| commitdiff \| tree
2021-08-23	Andrew Reynolds	Fix non-deterministism in quantified datatypes expansion...	commit \| commitdiff \| tree
2021-08-23	Andrew Reynolds	Purify substitutions in strings proof reconstruction...	commit \| commitdiff \| tree
2021-08-23	Andrew Reynolds	Generalize inequality elimination in quantifiers rewriter...	commit \| commitdiff \| tree
2021-08-23	Andrew Reynolds	Fix single invocation partition for higher-order (...	commit \| commitdiff \| tree
2021-08-23	Gereon Kremer	Move options parsing code to main (#7054)	commit \| commitdiff \| tree
2021-08-23	yoni206	Adding parameters to Datatype python API documentation...	commit \| commitdiff \| tree
2021-08-23	Aina Niemetz	api: Require size argument for mkBitVector. (#6998)	commit \| commitdiff \| tree
2021-08-23	Gereon Kremer	Use options correctly in competition mode (#7053)	commit \| commitdiff \| tree
2021-08-22	Andrew Reynolds	Simplify model printing modes (#7049)	commit \| commitdiff \| tree
2021-08-22	Andrew Reynolds	Prenex quantified formulas with user annotations by...	commit \| commitdiff \| tree
2021-08-20	Gereon Kremer	Make driver use options from the solver (#6930)	commit \| commitdiff \| tree
2021-08-20	Andrew Reynolds	Simplify how user-provided quantifier attributes are...	commit \| commitdiff \| tree
2021-08-20	mudathirmahgoub	Add Term.java to the Java API (#6330)	commit \| commitdiff \| tree
2021-08-20	Andrew Reynolds	More refactoring of set defaults (#7043)	commit \| commitdiff \| tree
2021-08-20	Andrew Reynolds	Support sygus standard command syntax set-feature ...	commit \| commitdiff \| tree
2021-08-20	Andrew Reynolds	Eliminate eager model building (#7038)	commit \| commitdiff \| tree
2021-08-20	Gereon Kremer	Use Env class in nonlinear extension (#7039)	commit \| commitdiff \| tree
2021-08-20	Gereon Kremer	Add CVC5ApiOptionException (#6992)	commit \| commitdiff \| tree
2021-08-19	yoni206	Make the python quickstart example run using ctest...	commit \| commitdiff \| tree
2021-08-19	yoni206	Add python quick start guide (#7024)	commit \| commitdiff \| tree
2021-08-19	Andres Noetzli	Remove `--(no-)interactive-prompt` (#7022)	commit \| commitdiff \| tree
2021-08-19	Andrew Reynolds	Catch cases where recursive functions reference functions...	commit \| commitdiff \| tree
2021-08-19	Andrew Reynolds	Split proof final callback to its own file (#6984)	commit \| commitdiff \| tree
2021-08-19	Andrew Reynolds	Refactor proof output for TPTP (#7029)	commit \| commitdiff \| tree
2021-08-19	Gereon Kremer	Start using Options via Env in arithmetic (#7032)	commit \| commitdiff \| tree
2021-08-19	Haniel Barbosa	[unsat cores] [proofs] Revert test about when to explain...	commit \| commitdiff \| tree
2021-08-18	Gereon Kremer	move collectAssertedTerms back to the theory class...	commit \| commitdiff \| tree
2021-08-18	Andres Noetzli	Minor fixes of policy for eliminating quantifiers ...	commit \| commitdiff \| tree
2021-08-18	Andrew Reynolds	Make TheoryProxy use Env, simplify initialization of...	commit \| commitdiff \| tree
2021-08-17	Andres Noetzli	Replace `Maybe` with `std::optional` (#7005)	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Make SmtEngineState use Env (#7028)	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Refactoring theory-specific variable elimination in...	commit \| commitdiff \| tree
next

RSS Atom