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

2021-09-16	Andrew Reynolds	Fix relevant domain for parametric operators (#7198)	commit \| commitdiff \| tree
2021-09-15	Lachnitt	[proofs] Alethe: Added Callback Function to alethe_proof_pro...	commit \| commitdiff \| tree
2021-09-15	Andrew Reynolds	Minor changes to E-matching utilities (#7062)	commit \| commitdiff \| tree
2021-09-15	Gereon Kremer	remove options that are no longer used (#7197)	commit \| commitdiff \| tree
2021-09-15	Lachnitt	[proof] Added printer for proof rule names (#7185)	commit \| commitdiff \| tree
2021-09-15	Lachnitt	[proof] Alethe proof rules (#7180)	commit \| commitdiff \| tree
2021-09-15	Andrew Reynolds	Eliminate global access to options:: from quantifiers...	commit \| commitdiff \| tree
2021-09-14	Andrew Reynolds	Add get-difficulty to the API (#7194)	commit \| commitdiff \| tree
2021-09-14	Gereon Kremer	Final cleanup (#7193)	commit \| commitdiff \| tree
2021-09-14	Andres Noetzli	Make `-o raw-benchmark` work with `--parse-only` (...	commit \| commitdiff \| tree
2021-09-14	Andrew Reynolds	Support sygus version 2.1 command assume (#7081)	commit \| commitdiff \| tree
2021-09-14	Andrew Reynolds	Utilities in preparation for print benchmark utility...	commit \| commitdiff \| tree
2021-09-14	Andrew Reynolds	Add proof manager method to translate difficulty map...	commit \| commitdiff \| tree
2021-09-14	Gereon Kremer	Refactor code generation for option modules (#7182)	commit \| commitdiff \| tree
2021-09-14	Gereon Kremer	Turn sphinx generation into a function (#7181)	commit \| commitdiff \| tree
2021-09-14	Mathias Preiner	bv: Unify bit-blasting code for udiv and urem. (#7188)	commit \| commitdiff \| tree
2021-09-14	Mathias Preiner	proofs: Properly track pre- and post-rewrites in bbAtom...	commit \| commitdiff \| tree
2021-09-14	Andrew Reynolds	Reimplement `--dump=raw-benchmark` as `-o raw-benchmark...	commit \| commitdiff \| tree
2021-09-13	Andres Noetzli	Remove context getters from `TheoryState` (#7174)	commit \| commitdiff \| tree
2021-09-13	Andrew Reynolds	Connect difficulty manager to TheoryEngine (#7161)	commit \| commitdiff \| tree
2021-09-13	Gereon Kremer	Add Solver::isOutputOn() (#7187)	commit \| commitdiff \| tree
2021-09-13	Aina Niemetz	FP: Rename FpConverter to FpWordBlaster. (#7170)	commit \| commitdiff \| tree
2021-09-13	Gereon Kremer	Refactor generation code for getInfo() (#7176)	commit \| commitdiff \| tree
2021-09-13	Gereon Kremer	Add main options to cmake (#7178)	commit \| commitdiff \| tree
2021-09-13	Gereon Kremer	Reorder code (#7175)	commit \| commitdiff \| tree
2021-09-13	Gereon Kremer	Refactor options parsing (#7143)	commit \| commitdiff \| tree
2021-09-11	Gereon Kremer	Use StatisticsRegistry from Env (#7166)	commit \| commitdiff \| tree
2021-09-11	Aina Niemetz	checkModel: Extend documentation. (#7177)	commit \| commitdiff \| tree
2021-09-11	Mathias Preiner	bv: Move IsPowerOfTwo rule to preprocessing pass and...	commit \| commitdiff \| tree
2021-09-11	Andrew Reynolds	Add casc 28 scripts (#7070)	commit \| commitdiff \| tree
2021-09-10	Aina Niemetz	FP: Enable caching in the theory inference manager...	commit \| commitdiff \| tree
2021-09-10	Mathias Preiner	bv: Use EnvObj::rewrite() and EnvObj::options() in...	commit \| commitdiff \| tree
2021-09-10	Aina Niemetz	FP: Use EnvObj::rewrite() and options() in theory_fp...	commit \| commitdiff \| tree
2021-09-10	Aina Niemetz	FP: Do not send trivial lemmas. (#7167)	commit \| commitdiff \| tree
2021-09-10	mudathirmahgoub	Add Op.java to the java API (#6387)	commit \| commitdiff \| tree
2021-09-10	Andres Noetzli	Use C++17 attributes (#7154)	commit \| commitdiff \| tree
2021-09-10	Andrew Reynolds	More refactoring of set defaults (#7160)	commit \| commitdiff \| tree
2021-09-10	Mathias Preiner	bv: Use EnvObj::rewrite() and EnvObj::options() in...	commit \| commitdiff \| tree
2021-09-10	Gereon Kremer	Refactor command-line help (#7157)	commit \| commitdiff \| tree
2021-09-10	Gereon Kremer	Use EnvObj-based options in preprocessing (#7165)	commit \| commitdiff \| tree
2021-09-09	Aina Niemetz	pp passes: Use EnvObj::rewrite() instead of Rewriter...	commit \| commitdiff \| tree
2021-09-09	Andres Noetzli	Remove `TheoryState::getEnv()` (#7163)	commit \| commitdiff \| tree
2021-09-09	Gereon Kremer	Add Solver::getOutput() (#7162)	commit \| commitdiff \| tree
2021-09-09	Andrew Reynolds	Add difficulty manager (#7151)	commit \| commitdiff \| tree
2021-09-09	Andrew Reynolds	Add difficulty post-processor (#7150)	commit \| commitdiff \| tree
2021-09-09	Andrew Reynolds	Disable shared selectors for quantified logics without...	commit \| commitdiff \| tree
2021-09-09	Andres Noetzli	Remove `TheoryState::options()` (#7148)	commit \| commitdiff \| tree
2021-09-09	Andrew Reynolds	Remove deprecated SyGuS method evaluateWithUnfolding...	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Add Lfsc print channel utilities (#7123)	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Improve pre-skolemization, move quantifiers preprocess...	commit \| commitdiff \| tree
2021-09-08	Gereon Kremer	Refactor options::set() (#7138)	commit \| commitdiff \| tree
2021-09-08	Gereon Kremer	Work on comments (#7139)	commit \| commitdiff \| tree
2021-09-08	Gereon Kremer	A couple of minor cleanups (#7141)	commit \| commitdiff \| tree
2021-09-08	Gereon Kremer	Refactor code generation for options.h/.cpp (#7126)	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Towards standard usage of ExtendedRewriter (#7145)	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Add option for using bound inference for relevant assertions...	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Add LFSC side condition conversion utility for list...	commit \| commitdiff \| tree
2021-09-08	mudathirmahgoub	Add Datatype.java to the Java API (#6389)	commit \| commitdiff \| tree
2021-09-08	mudathirmahgoub	Add DatatypeConstructor.java, DatatypeConstructorDecl...	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Use rewriteViaMethod instead of accessing builtin proof...	commit \| commitdiff \| tree
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
next

RSS Atom