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

2021-09-07	Andrew Reynolds	Refactoring of proof manager initialization (#7073)	commit \| commitdiff \| tree
2021-09-07	Andres Noetzli	Use `EnvObj` methods instead of `Theory` methods (...	commit \| commitdiff \| tree
2021-09-07	Aina Niemetz	sygus: Eliminate calls to Rewriter::rewrite. (#7142)	commit \| commitdiff \| tree
2021-09-07	Andrew Reynolds	Refactoring and fixes of set defaults for quantifiers...	commit \| commitdiff \| tree
2021-09-03	Aina Niemetz	EnvObj: Add options(), context(), userContext(). (...	commit \| commitdiff \| tree
2021-09-03	MikolasJanota	Avoiding duplicate search in maps (#7055)	commit \| commitdiff \| tree
2021-09-03	Aina Niemetz	sygus: Make more classes derive from EnvObj. (#7140)	commit \| commitdiff \| tree
2021-09-03	Gereon Kremer	Refactor option sanitizations (#7129)	commit \| commitdiff \| tree
2021-09-03	Andrew Reynolds	Standardize Rewriter::rewriteViaMethod call (#7119)	commit \| commitdiff \| tree
2021-09-03	Gereon Kremer	Check that alternate is only set for bool (#7125)	commit \| commitdiff \| tree
2021-09-03	Gereon Kremer	Refactor options::get() and options::getNames() (#7135)	commit \| commitdiff \| tree
2021-09-03	Andrew Reynolds	Make quantifier module classes derive from EnvObj ...	commit \| commitdiff \| tree
2021-09-03	Aina Niemetz	sygus: Make CeSingleInv derive from EnvObj. (#7136)	commit \| commitdiff \| tree
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
next

RSS Atom