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

2020-12-17	Andrew Reynolds	Simplify and fix check models (#5685)	commit \| commitdiff \| tree
2020-12-17	Haniel Barbosa	[proof-new] Only use old proof code for unsat cores...	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	Simplify preprocessing (#5647)	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	Mark quantifier instantiations as needs justify (#5684)	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	Simplify synth-fun printer (#5682)	commit \| commitdiff \| tree
2020-12-16	mudathirmahgoub	Renamed InferInfo::getAntecedant to InferInfo::getAntecedent...	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	(proof-new) Use bound variable manager (#5679)	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	Move ownership of term formula removal to theory preprocesso...	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	Use uint64 utility when parsing tuple selectors in...	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Move trigger trie to own file (#5680)	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Improvements related to quantifiers printing (#5678)	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Proper expand definitions for sets (#5676)	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Consolidate basic sygus utilities regarding sygus conjecture...	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Fix datatypes compute ground value (#5671)	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Remove bv divide by zero option (#5672)	commit \| commitdiff \| tree
2020-12-15	Gereon Kremer	Add getters to retrieve constants from api::Term (...	commit \| commitdiff \| tree
2020-12-14	Haniel Barbosa	[proof-new] Making the CDCL(T) Minisat proof producing...	commit \| commitdiff \| tree
2020-12-14	Haniel Barbosa	[proof-new] Make prop engine proof producing (#5667)	commit \| commitdiff \| tree
2020-12-14	Andrew Reynolds	Properly implement datatype selector triggers (#5624)	commit \| commitdiff \| tree
2020-12-14	Haniel Barbosa	[proof-new] Updating interfaces between prop engine...	commit \| commitdiff \| tree
2020-12-14	Andrew Reynolds	(proof-new) Add bound variable manager (#5655)	commit \| commitdiff \| tree
2020-12-14	Andrew Reynolds	Fix and improve evaluator (#5563)	commit \| commitdiff \| tree
2020-12-14	Andrew Reynolds	Fix SAT-context dependent issue in strings preregistration...	commit \| commitdiff \| tree
2020-12-12	Andrew Reynolds	Flush statistics through NodeManager in SmtEngine ...	commit \| commitdiff \| tree
2020-12-11	yoni206	bv-to-int: new tests from an issue (#5654)	commit \| commitdiff \| tree
2020-12-11	Haniel Barbosa	[proof-new] Updating theory proxy to new proof infrastructu...	commit \| commitdiff \| tree
2020-12-11	Andrew Reynolds	Fix length assumption for deq norm emp rule (#5623)	commit \| commitdiff \| tree
2020-12-10	Gereon Kremer	Refactor KindMap (#5646)	commit \| commitdiff \| tree
2020-12-10	Aina Niemetz	google test: expr: Migrate node_algorithm_black. (...	commit \| commitdiff \| tree
2020-12-10	Andrew Reynolds	Refactor regressions (#5639)	commit \| commitdiff \| tree
2020-12-10	Aina Niemetz	google test: expr: Migrate kind_black. (#5634)	commit \| commitdiff \| tree
2020-12-10	Gereon Kremer	Fixed a bunch of clang warnings. (#5637)	commit \| commitdiff \| tree
2020-12-09	Aina Niemetz	Fix compiler warnings. (#5644)	commit \| commitdiff \| tree
2020-12-09	Andrew Reynolds	(proof-new) Make theory preprocessor proofs self contained...	commit \| commitdiff \| tree
2020-12-09	Aina Niemetz	google test: expr: Migrate kind_map_black. (#5640)	commit \| commitdiff \| tree
2020-12-09	Aina Niemetz	kind_map: Remove unused Accessor class. (#5641)	commit \| commitdiff \| tree
2020-12-09	Aina Niemetz	google test: expr: Migrate attribute_white. (#5632)	commit \| commitdiff \| tree
2020-12-09	Andrew Reynolds	Make decision engine independent of AssertionsPipeline...	commit \| commitdiff \| tree
2020-12-09	Andrew Reynolds	Remove obsolete regressions (#5633)	commit \| commitdiff \| tree
2020-12-09	Aina Niemetz	google test: context: Migrate context_white. (#5630)	commit \| commitdiff \| tree
2020-12-09	Gereon Kremer	Split initial exp lemma into separate lemmas. (#5622)	commit \| commitdiff \| tree
2020-12-09	Aina Niemetz	Delete obsolete unit tests for Expr and ExprManager...	commit \| commitdiff \| tree
2020-12-09	Andrew Reynolds	Ensure CEGQI is applied for parametric datatypes when...	commit \| commitdiff \| tree
2020-12-09	Andrew Reynolds	Do not check FP at last call if not necessary (#5627)	commit \| commitdiff \| tree
2020-12-09	Aina Niemetz	ite_utilities: Fix infinite loop in compressTerm. ...	commit \| commitdiff \| tree
2020-12-09	yoni206	update doc (#5619)	commit \| commitdiff \| tree
2020-12-08	Aina Niemetz	google test: context: Migrate context_mm_black. (#5592)	commit \| commitdiff \| tree
2020-12-08	Aina Niemetz	google test: context: Migrate context_black. (#5587)	commit \| commitdiff \| tree
2020-12-08	Gereon Kremer	Add regression from #1978. (#5552)	commit \| commitdiff \| tree
2020-12-08	Abdalrhman Mohamed	Fix a bug with synth-fun printer (#5512)	commit \| commitdiff \| tree
2020-12-08	Haniel Barbosa	[proof-new] Updating SAT proof to use MACRO_RESOLUTION...	commit \| commitdiff \| tree
2020-12-08	yoni206	bv-to-int: Expand definitions of bvudiv and bvurem...	commit \| commitdiff \| tree
2020-12-08	Andrew Reynolds	Make term indices in the strings base solver aware...	commit \| commitdiff \| tree
2020-12-08	Andrew Reynolds	Proper implementation of expand definitions for sequences...	commit \| commitdiff \| tree
2020-12-08	Andrew Reynolds	Fix collect model values for sequences of sequences...	commit \| commitdiff \| tree
2020-12-08	Haniel Barbosa	[proof-new] Adding MACRO_RESOLUTION rule and updating...	commit \| commitdiff \| tree
2020-12-08	Mathias Preiner	Add support for BV proofs with the simple bitblasting...	commit \| commitdiff \| tree
2020-12-08	Mathias Preiner	Disable algebraic BV subtheory by default and make...	commit \| commitdiff \| tree
2020-12-07	Andrew Reynolds	Fix and reenable fact vs lemma optimization in datatypes...	commit \| commitdiff \| tree
2020-12-07	makaimann	Add bitwise refinement mode for IAND (#5328)	commit \| commitdiff \| tree
2020-12-07	Andrew Reynolds	Fix issue with free variables introduced by quantifier...	commit \| commitdiff \| tree
2020-12-07	Gereon Kremer	Refactor initial phase of transcendental solver (#5599)	commit \| commitdiff \| tree
2020-12-07	Andrew Reynolds	Do not expand theory definitions at the beginning of...	commit \| commitdiff \| tree
2020-12-07	Andrew Reynolds	(proof-new) Split proof ensure closed checks to own...	commit \| commitdiff \| tree
2020-12-07	Gereon Kremer	Add regression from #4927 (#5556)	commit \| commitdiff \| tree
2020-12-07	Andrew Reynolds	Fix bugs in getFreeVariables (#5601)	commit \| commitdiff \| tree
2020-12-05	Everett Maus	Change generated options to be thread_local. (#5583)	commit \| commitdiff \| tree
2020-12-04	Aina Niemetz	google test: expr: Migrate attribute_black. (#5598)	commit \| commitdiff \| tree
2020-12-04	Aina Niemetz	google test: context: Migrate cdo_black. (#5586)	commit \| commitdiff \| tree
2020-12-04	Aina Niemetz	google test: context: Migrate cdmap_white. (#5585)	commit \| commitdiff \| tree
2020-12-04	Andrew Reynolds	Fix bug in hasBoundVar (#5600)	commit \| commitdiff \| tree
2020-12-04	Aina Niemetz	google test: api: Migrate sort_black. (#5594)	commit \| commitdiff \| tree
2020-12-04	Aina Niemetz	google test: context: Migrate cdmap_black. (#5584)	commit \| commitdiff \| tree
2020-12-04	Aina Niemetz	google test: context: Migrate cdlist_black. (#5582)	commit \| commitdiff \| tree
2020-12-04	Alex Ozdemir	Use NodeDfsIterable for makeBinary (#5595)	commit \| commitdiff \| tree
2020-12-04	Mathias Preiner	update-copyright: Preserve file permissions. (#5597)	commit \| commitdiff \| tree
2020-12-03	Andrew Reynolds	(proof-new) Updates to SMT proof manager and SmtEngine...	commit \| commitdiff \| tree
2020-12-03	Aina Niemetz	google test: api: Migrate solver_black. (#5570)	commit \| commitdiff \| tree
2020-12-03	Gereon Kremer	Use mkAnd where the number of children may be less...	commit \| commitdiff \| tree
2020-12-03	yoni206	Models as (#5581)	commit \| commitdiff \| tree
2020-12-03	Aina Niemetz	google test: Add fixture for context tests. (#5590)	commit \| commitdiff \| tree
2020-12-03	Andrew Reynolds	Refactor handling of global declarations (#5577)	commit \| commitdiff \| tree
2020-12-03	Gereon Kremer	Make run_regression.py executable. (#5588)	commit \| commitdiff \| tree
2020-12-03	Aina Niemetz	google test: base: Migrate map_util_black. (#5580)	commit \| commitdiff \| tree
2020-12-02	Aina Niemetz	Fix RoundingMode mapping in API. (#5578)	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Remove Record object and convert to Node-level API...	commit \| commitdiff \| tree
2020-12-02	Aina Niemetz	Rename macro Message to CVC4Message. (#5576)	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Remove dagification visitor (#5574)	commit \| commitdiff \| tree
2020-12-02	Aina Niemetz	google test: api: Migrate term_black. (#5571)	commit \| commitdiff \| tree
2020-12-02	Aina Niemetz	google test: api: Use individual fixture for datatype_black...	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Add associative utilities to node manager (#5530)	commit \| commitdiff \| tree
2020-12-02	Aina Niemetz	google test: api: Migrate op_black. (#5567)	commit \| commitdiff \| tree
2020-12-02	Aina Niemetz	google test: api: Migrate grammar_black. (#5566)	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Use new let binding for cvc printer (#5561)	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	(proof-new) Proofs for expand definitions (#5562)	commit \| commitdiff \| tree
2020-12-02	Gereon Kremer	Add regressions from #3687. (#5553)	commit \| commitdiff \| tree
2020-12-02	Aina Niemetz	google test: api: Migrate result_black. (#5569)	commit \| commitdiff \| tree
2020-12-02	Aina Niemetz	Remove use of this-> in FP literal. (#5565)	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Remove assertion related to CEGQI dependency lemmas...	commit \| commitdiff \| tree
2020-12-02	Aina Niemetz	google test: Infrastructure and first api test. (#5548)	commit \| commitdiff \| tree
next

RSS Atom