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

2020-09-26	Gereon Kremer	Use inference manager for nl_solver (#5125)	commit \| commitdiff \| tree
2020-09-26	Andrew Reynolds	Connect the shared solver to theory engine (#5103)	commit \| commitdiff \| tree
2020-09-26	Andrew Reynolds	Use original quantified formula for single invocation...	commit \| commitdiff \| tree
2020-09-26	Aina Niemetz	Restrict bvxnor to only allow two operands (was n-ary...	commit \| commitdiff \| tree
2020-09-25	Andrew Reynolds	Make sygus refinement step more robust to unevaluatable...	commit \| commitdiff \| tree
2020-09-25	Haniel Barbosa	Cleaning and documenting cnf stream (#5134)	commit \| commitdiff \| tree
2020-09-24	Aina Niemetz	SyGuS: Add default grammar for FP. (#5133)	commit \| commitdiff \| tree
2020-09-24	Andrew Reynolds	Function definition fmf preprocessing pass (#5064)	commit \| commitdiff \| tree
2020-09-24	Andrew Reynolds	Modify lemma vs fact policy for datatype equalities...	commit \| commitdiff \| tree
2020-09-23	Andrew Reynolds	Disable cegqi-bv when using sygus (#5124)	commit \| commitdiff \| tree
2020-09-23	Gereon Kremer	Make IAND solver use inference manager. (#5126)	commit \| commitdiff \| tree
2020-09-23	yoni206	bv2int: new options for bvand translation (#5096)	commit \| commitdiff \| tree
2020-09-23	Andrew Reynolds	Allow E-matching by default when strings are enabled...	commit \| commitdiff \| tree
2020-09-23	Aina Niemetz	New C++ API: Catch and throw recoverable exception...	commit \| commitdiff \| tree
2020-09-23	Aina Niemetz	FP: Use Assert instead of AlwaysAssert in traits::...	commit \| commitdiff \| tree
2020-09-23	Abdalrhman Mohamed	Refactor Commands to use the Public API. (#5105)	commit \| commitdiff \| tree
2020-09-23	Andrew Reynolds	Fix type issue with term formula removal (#5107)	commit \| commitdiff \| tree
2020-09-23	Andres Noetzli	[Python API] Conversion to/from Unicode strings (#5120)	commit \| commitdiff \| tree
2020-09-22	Aina Niemetz	FP: Use Assert instead of PRECONDITION macro in converter...	commit \| commitdiff \| tree
2020-09-22	Mathias Preiner	Add simple BV solver (#5065)	commit \| commitdiff \| tree
2020-09-22	mudathirmahgoub	Add skeleton for theory of bags (multisets) (#5100)	commit \| commitdiff \| tree
2020-09-22	Andres Noetzli	Fix compilation without LibPoly (#5118)	commit \| commitdiff \| tree
2020-09-22	makaimann	Add method to get Python object from constant value...	commit \| commitdiff \| tree
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	commit \| commitdiff \| tree
2020-09-22	Gereon Kremer	ICP-based solver for nonlinear arithmetic (#5017)	commit \| commitdiff \| tree
2020-09-22	yoni206	Require dumping in a dumping test (#5108)	commit \| commitdiff \| tree
2020-09-21	Andrew Reynolds	(proof-new) Add the arrays proof checker (#5047)	commit \| commitdiff \| tree
2020-09-20	Andrew Reynolds	More flexible design for model manager distributed...	commit \| commitdiff \| tree
2020-09-19	Andrew Reynolds	Standardize equality engine notifications in sets ...	commit \| commitdiff \| tree
2020-09-18	Andrew Reynolds	Fix assertion list for globally defined recursive functions...	commit \| commitdiff \| tree
2020-09-18	Andrew Reynolds	Add the shared solver (#4982)	commit \| commitdiff \| tree
2020-09-18	yoni206	bv2int: quantifiers support (#5080)	commit \| commitdiff \| tree
2020-09-18	Andres Noetzli	Fix muzzled builds (#5093)	commit \| commitdiff \| tree
2020-09-18	Haniel Barbosa	[proof-new] Proof utilities for normalizing clauses...	commit \| commitdiff \| tree
2020-09-18	Andrew Reynolds	Logic exception for arrays indexed by arrays (#5073)	commit \| commitdiff \| tree
2020-09-18	Andres Noetzli	[Strings] Fix extended equality rewriter (#5092)	commit \| commitdiff \| tree
2020-09-18	Andrew Reynolds	(proof-new) Updates to proof node updater algorithm...	commit \| commitdiff \| tree
2020-09-18	Andrew Reynolds	(proof-new) Rewrites involving operators in term conversion...	commit \| commitdiff \| tree
2020-09-17	Andrew Reynolds	(proof-new) Fixes for theory engine proof generator...	commit \| commitdiff \| tree
2020-09-17	Haniel Barbosa	[proof-new] Have mkScope agnostic to True assumptions...	commit \| commitdiff \| tree
2020-09-17	Gereon Kremer	(cad-solver) Fix square-free-basis computation (#5085)	commit \| commitdiff \| tree
2020-09-17	Andrew Reynolds	Reduce recursion in term formula removal (#5052)	commit \| commitdiff \| tree
2020-09-17	Gereon Kremer	Use new inference manager in transcendental solver...	commit \| commitdiff \| tree
2020-09-17	Andrew V. Jones	Do not allow to build Python bindings if building statically...	commit \| commitdiff \| tree
2020-09-17	Andrew Reynolds	Further standardization of datatypes (#5076)	commit \| commitdiff \| tree
2020-09-17	yoni206	Dumping internal define-funs with no arguments (#5077)	commit \| commitdiff \| tree
2020-09-16	Andres Noetzli	Only rewrite replace_re(_all) if regexp is const (...	commit \| commitdiff \| tree
2020-09-16	Abdalrhman Mohamed	Dump commands in internal code using command printing...	commit \| commitdiff \| tree
2020-09-16	Andrew Reynolds	Add buffered inference manager to TheorySep (#5038)	commit \| commitdiff \| tree
2020-09-16	Haniel Barbosa	[proof-new] Adds Lazy CDProof chain data-structure...	commit \| commitdiff \| tree
2020-09-16	Andrew Reynolds	Refactor collectModelInfo in TheoryArith (#5027)	commit \| commitdiff \| tree
2020-09-16	yoni206	bv2int: support models in tests (#5068)	commit \| commitdiff \| tree
2020-09-16	Haniel Barbosa	[proof-new] Extending eqproof conversion to HO congruence...	commit \| commitdiff \| tree
2020-09-16	Haniel Barbosa	[proof-new] Resolution rules and checkers (#5070)	commit \| commitdiff \| tree
2020-09-16	Haniel Barbosa	[proof-new] A simple proof generator for buffered proof...	commit \| commitdiff \| tree
2020-09-16	Andrew Reynolds	(proof-new) Make proofs mandatory in proof equality...	commit \| commitdiff \| tree
2020-09-15	Andrew Reynolds	Move sets member propagation to SolverState (#5045)	commit \| commitdiff \| tree
2020-09-15	Aina Niemetz	Rename system tests to api tests and remove obsolete...	commit \| commitdiff \| tree
2020-09-15	Andrew Reynolds	Move quantifiers engine private to own file (#5053)	commit \| commitdiff \| tree
2020-09-15	Andrew Reynolds	Fix needsModel method for CEGQI (#5048)	commit \| commitdiff \| tree
2020-09-15	Andrew Reynolds	Standard equality engine notify class for Theory (...	commit \| commitdiff \| tree
2020-09-15	Andres Noetzli	Fix ABC build (#5061)	commit \| commitdiff \| tree
2020-09-15	Ying Sheng	Interpolation: Add implementation for SyGuS interpolation...	commit \| commitdiff \| tree
2020-09-14	yoni206	bv2int: simpler translation for plus and times (#5055)	commit \| commitdiff \| tree
2020-09-14	Andrew Reynolds	Refactoring the rewriter of sets (#4856)	commit \| commitdiff \| tree
2020-09-14	Andres Noetzli	Fix type for Windows build (#5062)	commit \| commitdiff \| tree
2020-09-14	Andrew Reynolds	Standardize uses of inference manager in datatypes...	commit \| commitdiff \| tree
2020-09-12	Andrew Reynolds	(proof-new) Add SMT proof manager (#5054)	commit \| commitdiff \| tree
2020-09-12	Andrew Reynolds	(proof-new) Update TheoryEngine lemma and conflict...	commit \| commitdiff \| tree
2020-09-11	Andrew Reynolds	Move finite model minimization to UF last call effort...	commit \| commitdiff \| tree
2020-09-11	Andrew Reynolds	(proof-new) Handle mismatched assumptions in proof...	commit \| commitdiff \| tree
2020-09-11	Andrew Reynolds	(proof-new) Use deep copy for final lemma step in proof...	commit \| commitdiff \| tree
2020-09-11	Andrew Reynolds	Add witness to cvc printer. (#5057)	commit \| commitdiff \| tree
2020-09-10	yoni206	bv2int: refactoring the main translation loop (#5051)	commit \| commitdiff \| tree
2020-09-10	Andrew Reynolds	Parser error for wrong number of datatypes (#5049)	commit \| commitdiff \| tree
2020-09-10	yoni206	bv2int: improvement in lazy failures (#5020)	commit \| commitdiff \| tree
2020-09-10	Andrew Reynolds	Use state and inference manager in UF CardinalityExtension...	commit \| commitdiff \| tree
2020-09-09	Andrew Reynolds	(proof-new) Minor changes to proof node updater (#5011)	commit \| commitdiff \| tree
2020-09-09	Andrew Reynolds	(proof-new) Make proofs in term formula removal term...	commit \| commitdiff \| tree
2020-09-09	Andrew Reynolds	(proof-new) Generalize single step helper in eager...	commit \| commitdiff \| tree
2020-09-09	Andrew Reynolds	Fixes for regular expressions + sygus (#5044)	commit \| commitdiff \| tree
2020-09-09	mudathirmahgoub	Add is_singleton operator to the theory of sets (#5033)	commit \| commitdiff \| tree
2020-09-09	Andrew Reynolds	Split term registry from theory state in sets (#5037)	commit \| commitdiff \| tree
2020-09-08	Mathias Preiner	Fix printing of fp values. (#5041)	commit \| commitdiff \| tree
2020-09-08	Andres Noetzli	Make CVC/API BV div/mod semantics match SMT-LIB (#4997)	commit \| commitdiff \| tree
2020-09-08	Andrew Reynolds	Eliminate a custom use of TheorySep in quantifiers...	commit \| commitdiff \| tree
2020-09-04	Andrew Reynolds	Add asLemma flag to theory inference process (#5030)	commit \| commitdiff \| tree
2020-09-04	Haniel Barbosa	[Regressions] Fix regression issues related to BV proofs...	commit \| commitdiff \| tree
2020-09-04	Andrew Reynolds	(new theory) Update TheoryBV to new standard for collectMode...	commit \| commitdiff \| tree
2020-09-04	Haniel Barbosa	Fix non-lib-poly-build issues (#5028)	commit \| commitdiff \| tree
2020-09-04	Abdalrhman Mohamed	Use Result::Sat instead of BenchmarkStatus in printers...	commit \| commitdiff \| tree
2020-09-04	Gereon Kremer	Use arith::InferenceManager for CAD lemmas (#5015)	commit \| commitdiff \| tree
2020-09-04	Malte Mues	Change the unavailable ABC mercury repository for the...	commit \| commitdiff \| tree
2020-09-04	Mathias Preiner	Split lazy bit-vector solver from TheoryBV (#5009)	commit \| commitdiff \| tree
2020-09-04	Andrew Reynolds	Add interfaces for making trust nodes in TheoryInferenceMana...	commit \| commitdiff \| tree
2020-09-03	Andrew Reynolds	Update sets inference manager to inherit from InferenceManag...	commit \| commitdiff \| tree
2020-09-03	Gereon Kremer	Added a new rule to simplify (bvugt (bvurem T x) x...	commit \| commitdiff \| tree
2020-09-03	Andrew Reynolds	Minor cleanup of quantifiers engine (#4994)	commit \| commitdiff \| tree
2020-09-03	yoni206	Changing the handled operators in bv2int preprocessing...	commit \| commitdiff \| tree
2020-09-03	Gereon Kremer	Basic integration of arith::InferenceManager (#4999)	commit \| commitdiff \| tree
next

RSS Atom