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

2021-09-23	Gereon Kremer	Eliminate Output macro in favor of simple Env functions...	commit \| commitdiff \| tree
2021-09-23	Lachnitt	[proofs[ Alethe: Fix Order of Arguments of addAletheStepFrom...	commit \| commitdiff \| tree
2021-09-23	Lachnitt	[proofs] Alethe: Translate THEORY_REWRITE (#7236)	commit \| commitdiff \| tree
2021-09-23	Lachnitt	[proofs] Alethe: Add Alethe Files to be Compiled ...	commit \| commitdiff \| tree
2021-09-23	Gereon Kremer	Refactor check interface of nonlinear extension (#7235)	commit \| commitdiff \| tree
2021-09-23	Andrew Reynolds	More uses of EnvObj (#7230)	commit \| commitdiff \| tree
2021-09-23	Lachnitt	[proofs] Alethe: Translate SCOPE rule (#7224)	commit \| commitdiff \| tree
2021-09-23	Abdalrhman Mohamed	Use `\|` to print quoted strings in `set-info` command...	commit \| commitdiff \| tree
2021-09-23	Andrew Reynolds	Implement alpha equivalence proofs (#7066)	commit \| commitdiff \| tree
2021-09-22	Andrew Reynolds	Make cegqi subsolvers EnvObj (#7205)	commit \| commitdiff \| tree
2021-09-22	Mathias Preiner	Remove CVC language support (#7219)	commit \| commitdiff \| tree
2021-09-22	Andrew Reynolds	Towards standard usage of evaluator (#7189)	commit \| commitdiff \| tree
2021-09-22	Ouyancheng	Fix solver_black unit test (#7233)	commit \| commitdiff \| tree
2021-09-22	Andrew Reynolds	Add extensionality option for strings disequalities...	commit \| commitdiff \| tree
2021-09-22	Aina Niemetz	arrays: Use EnvObj::rewrite and EnvObj::options. (...	commit \| commitdiff \| tree
2021-09-22	Aina Niemetz	arrays: Move type enumerator implementation to .cpp...	commit \| commitdiff \| tree
2021-09-22	Gereon Kremer	Eliminate arithmetic proof macros (#7226)	commit \| commitdiff \| tree
2021-09-22	Andrew Reynolds	Minimal fixing version for tuple update parsing (#7228)	commit \| commitdiff \| tree
2021-09-21	Lachnitt	[Proofs] Alethe: Translate ASSUME rule (#7213)	commit \| commitdiff \| tree
2021-09-21	Lachnitt	[proofs] Alethe: Implementation of AletheProofPostprocessCal...	commit \| commitdiff \| tree
2021-09-21	Aina Niemetz	README: Fix link to INSTALL.rst. (#7222)	commit \| commitdiff \| tree
2021-09-21	Andres Noetzli	Fix handling of conversions between FP and reals (...	commit \| commitdiff \| tree
2021-09-20	Alex Ozdemir	Start python API Solver documentation (#7064)	commit \| commitdiff \| tree
2021-09-20	Haniel Barbosa	[proofs] Alethe: adds a node converter	commit \| commitdiff \| tree
2021-09-20	Andrew Reynolds	Add the LFSC proof post-processor (#7134)	commit \| commitdiff \| tree
2021-09-20	Aina Niemetz	TheoryModel: Use EnvObj::rewrite instead of Rewriter...	commit \| commitdiff \| tree
2021-09-20	Andres Noetzli	Optionally enable interprocedural optimization (#7209)	commit \| commitdiff \| tree
2021-09-20	Gereon Kremer	Add anchors to cmdline options (#7210)	commit \| commitdiff \| tree
2021-09-18	Andrew Reynolds	Fix printer for datatype udpater (#7208)	commit \| commitdiff \| tree
2021-09-18	Gereon Kremer	Refactor tag suggestion mechanism (#7199)	commit \| commitdiff \| tree
2021-09-17	Andres Noetzli	Use a single `NodeManager` per thread (#7204)	commit \| commitdiff \| tree
2021-09-17	Lachnitt	[proofs] Alethe: Added Proof Postprocessor to alethe_proof_p...	commit \| commitdiff \| tree
2021-09-17	Lachnitt	[proofs] Alethe: Added Final Callback Function to alethe_pro...	commit \| commitdiff \| tree
2021-09-17	Gereon Kremer	Replace write access to options by a local variable...	commit \| commitdiff \| tree
2021-09-17	Gereon Kremer	Minor cleanup related to EnvObj (#7206)	commit \| commitdiff \| tree
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
next

RSS Atom