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

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
2021-08-17	Andrew Reynolds	Fix policy for eliminating quantified formulas (#7017)	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Make theory BV use central eq engine when option is...	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Cosmetic improvements to theory datatypes (#7020)	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Improve conversion to skolems in expression miner ...	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Initial refactoring of set defaults (#7021)	commit \| commitdiff \| tree
2021-08-17	Gereon Kremer	Push Env class into TheoryState (#7012)	commit \| commitdiff \| tree
2021-08-16	Gereon Kremer	Use InferenceManager in ExtTheory (#7006)	commit \| commitdiff \| tree
2021-08-16	Gereon Kremer	Make Theory class use Env (#7011)	commit \| commitdiff \| tree
2021-08-16	Andres Noetzli	[Strings] Make fact detection more robust (#7007)	commit \| commitdiff \| tree
2021-08-16	Andrew V. Jones	Add check for static libraries when compiling CryptoMiniSat...	commit \| commitdiff \| tree
2021-08-16	Andrew V. Jones	Correct copyright print for GLPK (#7015) See http://github.com/timothy-king/glpk-cut-log... See http://github.com/timothy-king/glpk-cut-log...	commit \| commitdiff \| tree
2021-08-13	Gereon Kremer	Refactor setDefaults to use an options object (#6994)	commit \| commitdiff \| tree
2021-08-10	Andres Noetzli	Disable external initialization of `thread_local` variables...	commit \| commitdiff \| tree
2021-08-10	Gereon Kremer	Simplify generation of option module code. (#6995)	commit \| commitdiff \| tree
2021-08-09	Andrew V. Jones	Create grouping of tests that exercise '--use-approx...	commit \| commitdiff \| tree
2021-08-09	Andres Noetzli	Support older CMake versions (#7003)	commit \| commitdiff \| tree
2021-08-06	Gereon Kremer	Merge options cmake into general cmake file (#6989)	commit \| commitdiff \| tree
2021-08-06	Gereon Kremer	Clear options manager (#6991)	commit \| commitdiff \| tree
2021-08-05	Alex Ozdemir	Normalize val in BitVector(val_str, base) (#6955)	commit \| commitdiff \| tree
2021-08-05	Andrew Reynolds	Generalize term canonizer for type classes (#6895)	commit \| commitdiff \| tree
2021-08-05	Andres Noetzli	[Unit Tests] Add missing include (#6990)	commit \| commitdiff \| tree
2021-08-05	Andrew Reynolds	Fix policy for rewriting string equalities (#6916)	commit \| commitdiff \| tree
2021-08-05	Gereon Kremer	No longer call solver constructor with an options object...	commit \| commitdiff \| tree
2021-08-04	Gereon Kremer	Consolidate solver resets (#6986)	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Proper printing of proofs in the internal calculus...	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Fix policy for merging subproofs (#6981)	commit \| commitdiff \| tree
2021-08-04	Diego Della Rocca...	[proof] [dot] Fix comments on dot printer (#6983)	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Add inference ids for remainder of sygus solver (#6977)	commit \| commitdiff \| tree
2021-08-04	Haniel Barbosa	Improve error messages for UF catching higher-order...	commit \| commitdiff \| tree
2021-08-04	Mathias Preiner	syqi: Add debug information for dumping instantiations...	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Add optional debug information for dumping instantiations...	commit \| commitdiff \| tree
2021-08-04	Aina Niemetz	Update bug_report.md	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Add containsAssumption proof utility (#6953)	commit \| commitdiff \| tree
2021-08-04	Gereon Kremer	Refactor managed streams (#6934)	commit \| commitdiff \| tree
2021-08-04	Gereon Kremer	Add API function to get list of option names (#6971)	commit \| commitdiff \| tree
2021-08-04	Gereon Kremer	Replace numeric predicates by explicit minimum and...	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Add missing inference identifiers (#6962)	commit \| commitdiff \| tree
2021-08-04	Haniel Barbosa	[proof] Add getProof to API and use it in GetProofCommand...	commit \| commitdiff \| tree
2021-08-04	Alex Ozdemir	Add IEEE-BV-to-FP to external-to-internal mapping in...	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Remove dependencies on smt engine in smt solver (#6965)	commit \| commitdiff \| tree
2021-08-03	Gereon Kremer	Use int64_t, uint64_t or double for all numeric options...	commit \| commitdiff \| tree
2021-08-03	Andrew Reynolds	Refactor shared solver to use theory builtin inference...	commit \| commitdiff \| tree
2021-08-03	Andrew Reynolds	Remove "inUnsatCore" flag throughout (#6964)	commit \| commitdiff \| tree
2021-08-03	Gereon Kremer	Properly honor --stats-all and --stats-expert when...	commit \| commitdiff \| tree
2021-08-02	Aina Niemetz	Add 'REQUIRES: poly' to regression. (#6966)	commit \| commitdiff \| tree
2021-08-02	Mathias Preiner	bv: Enable equality engine for bitblast-internal. ...	commit \| commitdiff \| tree
2021-07-31	Gereon Kremer	Perform statistics printing via the API (#6952)	commit \| commitdiff \| tree
2021-07-30	Gereon Kremer	Allow changing certain options while solving (#6945)	commit \| commitdiff \| tree
2021-07-30	Andrew Reynolds	Simplify smt2 printer (#6954)	commit \| commitdiff \| tree
2021-07-29	Gereon Kremer	Integrate installation instructions into documentation...	commit \| commitdiff \| tree
2021-07-29	Aina Niemetz	quickstart: Add python example to docs. (#6949)	commit \| commitdiff \| tree
2021-07-29	Haniel Barbosa	[proofs] Set BV solver to better proof-producing one...	commit \| commitdiff \| tree
2021-07-29	yoni206	Python quick start example (#6939)	commit \| commitdiff \| tree
2021-07-29	Andrew Reynolds	Integrate central equality engine approach into theory...	commit \| commitdiff \| tree
2021-07-29	Andrew Reynolds	Minor updates to shared terms database for central...	commit \| commitdiff \| tree
2021-07-28	makaimann	Fixes for building python wheels on manylinux2014 ...	commit \| commitdiff \| tree
2021-07-28	Andrew Reynolds	Minor changes to arrays in preparation for central...	commit \| commitdiff \| tree
2021-07-28	Gereon Kremer	Only use libedit on tty inputs (#6946)	commit \| commitdiff \| tree
2021-07-28	Andres Noetzli	Print link to docs preview (#6922)	commit \| commitdiff \| tree
2021-07-28	Andrew Reynolds	Make extended rewriter methods const (#6948)	commit \| commitdiff \| tree
2021-07-27	Mathias Preiner	bv: Refactor getEqualityStatus and use for both bitblasting...	commit \| commitdiff \| tree
2021-07-27	Mathias Preiner	proof: Add eqrange expansion rule. (#6936)	commit \| commitdiff \| tree
next

RSS Atom