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

2020-12-01	Gereon Kremer	Refactor transcendental solver (#5539)	commit \| commitdiff \| tree
2020-12-01	Gereon Kremer	Add regressions from #5099 (#5557)	commit \| commitdiff \| tree
2020-12-01	Gereon Kremer	Add regression for #4335. (#5554)	commit \| commitdiff \| tree
2020-12-01	Gereon Kremer	Add regressions for #4707. (#5555)	commit \| commitdiff \| tree
2020-12-01	Andrew Reynolds	More fixes for quantifier elimination (#5533)	commit \| commitdiff \| tree
2020-12-01	yoni206	fix metadata for a test (#5546)	commit \| commitdiff \| tree
2020-11-30	Aina Niemetz	fp_converter: Properly separate out symbolic glue code...	commit \| commitdiff \| tree
2020-11-30	Andrew Reynolds	Use new let binding in AST printer (#5529)	commit \| commitdiff \| tree
2020-11-30	Aina Niemetz	floatingpoint: Use unique_ptr for FloatingPointLiteral...	commit \| commitdiff \| tree
2020-11-30	Abdalrhman Mohamed	Eliminate uses of SExpr from the parser. (#5496)	commit \| commitdiff \| tree
2020-11-30	Andrew Reynolds	Remove includes for old API from internal code (#5536)	commit \| commitdiff \| tree
2020-11-30	Andrew Reynolds	(proof-new) Proofs for regular expression elimination...	commit \| commitdiff \| tree
2020-11-26	Gereon Kremer	Make CAD solver work for empty set of assertions (...	commit \| commitdiff \| tree
2020-11-26	Andrew Reynolds	Removing infrastructure related to SMT model (#5527)	commit \| commitdiff \| tree
2020-11-26	Andrew Reynolds	Move expand definitions to its own file (#5528)	commit \| commitdiff \| tree
2020-11-26	Andrew Reynolds	Fully decouple SmtEngine and the Expr layer (#5532)	commit \| commitdiff \| tree
2020-11-26	Andrew Reynolds	Fix missed case of theory preprocessing (#5531)	commit \| commitdiff \| tree
2020-11-26	Andrew Reynolds	Disable fact vs lemma optimization in datatypes for...	commit \| commitdiff \| tree
2020-11-25	Andrew Reynolds	Add regressions for closed issues (#5526)	commit \| commitdiff \| tree
2020-11-25	Gereon Kremer	Fix transcendental secant plane lemmas (#5525)	commit \| commitdiff \| tree
2020-11-25	Andrew Reynolds	Use symbol manager for printing responses get-model...	commit \| commitdiff \| tree
2020-11-25	Andrew Reynolds	Allow printing of null node in let binder (#5523)	commit \| commitdiff \| tree
2020-11-25	Gereon Kremer	Refactor transcendental solver (#5514)	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	Fix regular expression consume for nested star (#5518)	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	Change UF ho to ppRewrite instead of expand definition...	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	Fix for sygusToBuiltinEval for non-ground composite...	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	(proof-new) Miscellaneous changes from proof-new (...	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	Add declare model symbol methods to SymbolManager and...	commit \| commitdiff \| tree
2020-11-23	Gereon Kremer	Add get-info :time. (#5485)	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	Fix quantifiers scope issue in strings preprocessor...	commit \| commitdiff \| tree
2020-11-21	mudathirmahgoub	Add posRewriteEqual to bags rewriter (#5498)	commit \| commitdiff \| tree
2020-11-21	Aina Niemetz	Rename symfpu_literal.(h.in\|cpp) -> floatingpoint_literal_sy...	commit \| commitdiff \| tree
2020-11-21	Aina Niemetz	Rename floatingpoint.h.in -> floatingpoin.h. (#5500)	commit \| commitdiff \| tree
2020-11-20	Andrew Reynolds	Fix remove term formula policy for terms beneath quantifiers...	commit \| commitdiff \| tree
2020-11-20	Aina Niemetz	RoundingMode: Rename enum values to conform to code...	commit \| commitdiff \| tree
2020-11-20	Aina Niemetz	FloatingPoint: Separate out symFPU glue code. (#5492)	commit \| commitdiff \| tree
2020-11-20	Aina Niemetz	Fix #5493. (#5495)	commit \| commitdiff \| tree
2020-11-20	Andrew Reynolds	Support nested quantifier elimination for get-qe command...	commit \| commitdiff \| tree
2020-11-20	Andrew Reynolds	Updates to API in preparation for using symbol manager...	commit \| commitdiff \| tree
2020-11-20	Aina Niemetz	Fix compiler warnings. (#5493)	commit \| commitdiff \| tree
2020-11-20	Andrew Reynolds	Fix use of declaration sequence command in cvc parser...	commit \| commitdiff \| tree
2020-11-20	Gereon Kremer	(proof-new) Replace LazyCDProofSet by generic CDProofSet...	commit \| commitdiff \| tree
2020-11-20	Gereon Kremer	Allow to pass ProofGenerator to arithmetic inference...	commit \| commitdiff \| tree
2020-11-19	Andrew Reynolds	Enable new implementation of CEGQI based on nested...	commit \| commitdiff \| tree
2020-11-19	Aina Niemetz	floatingpoint.h: Split in preparation to cleanly separate...	commit \| commitdiff \| tree
2020-11-19	Andrew Reynolds	Use new let binding utility in smt2 printer (#5472)	commit \| commitdiff \| tree
2020-11-19	Aina Niemetz	Include stddef.h (needed for size_t) in cvc4_public...	commit \| commitdiff \| tree
2020-11-19	Andrew Reynolds	Add nested quantifier elimination module (#5422)	commit \| commitdiff \| tree
2020-11-19	Andrew Reynolds	Fix issues related to eliminating extended arithmetic...	commit \| commitdiff \| tree
2020-11-19	Andrew Reynolds	Use symbol manager for unsat cores (#5468)	commit \| commitdiff \| tree
2020-11-18	Mathias Preiner	Add -> operator overload for cd* iterators. (#5464)	commit \| commitdiff \| tree
2020-11-18	Andrew Reynolds	Disable slow nl regression (#5467)	commit \| commitdiff \| tree
2020-11-18	Andrew Reynolds	Add let binding utility (#5444)	commit \| commitdiff \| tree
2020-11-18	Andrew Reynolds	Minor cleanup of SmtEngine (#5450)	commit \| commitdiff \| tree
2020-11-18	Andrew Reynolds	Do not expand definitions of extended arithmetic operators...	commit \| commitdiff \| tree
2020-11-18	Andrew Reynolds	Use symbol manager for get assignment (#5451)	commit \| commitdiff \| tree
2020-11-18	Andrew Reynolds	Fix asan issues related to solver and symbol manager...	commit \| commitdiff \| tree
2020-11-18	Aina Niemetz	FloatingPoint: Use uint32_t instead of unsigned. (...	commit \| commitdiff \| tree
2020-11-18	Aina Niemetz	FloatingPoint: Clean up and document header, format...	commit \| commitdiff \| tree
2020-11-18	Mathias Preiner	ci: Simplify Python dependency installs for Linux and...	commit \| commitdiff \| tree
2020-11-17	Gereon Kremer	Fix tangent plane lemmas (#5455)	commit \| commitdiff \| tree
2020-11-16	Gereon Kremer	Refactor tangent plane lemmas (#5449)	commit \| commitdiff \| tree
2020-11-16	Andrew Reynolds	Cleaning up scopes in preparation for symbol manager...	commit \| commitdiff \| tree
2020-11-16	Gereon Kremer	Improve accuracy of resource limitation (#4763)	commit \| commitdiff \| tree
2020-11-14	Andrew Reynolds	Fix double conflict in extended string solver (#5435)	commit \| commitdiff \| tree
2020-11-14	Andrew Reynolds	(proof-new) Proofs for non-clausal simplification ...	commit \| commitdiff \| tree
2020-11-13	Andrew Reynolds	(proof-new) Enable proofs for datatypes (#5436)	commit \| commitdiff \| tree
2020-11-13	yoni206	Model declarations printing options (#5432)	commit \| commitdiff \| tree
2020-11-13	Andrew Reynolds	Add more features to symbol manager (#5434)	commit \| commitdiff \| tree
2020-11-13	Andrew Reynolds	Make regular expression difference left associative...	commit \| commitdiff \| tree
2020-11-12	Andrew Reynolds	Simplify sygus solver and sygus stream (#5389)	commit \| commitdiff \| tree
2020-11-12	Andrew Reynolds	Fix printing of define named function (#5425)	commit \| commitdiff \| tree
2020-11-12	yoni206	Models standard (#5415)	commit \| commitdiff \| tree
2020-11-12	Andrew Reynolds	(proof-new) Separate explanation stages in proof equality...	commit \| commitdiff \| tree
2020-11-12	Andrew Reynolds	Fix redundant refinement lemma in sygus solver (#5399)	commit \| commitdiff \| tree
2020-11-12	Andrew Reynolds	(proof-new) Proofs for skolemization (#5339)	commit \| commitdiff \| tree
2020-11-12	Andrew Reynolds	(proof-new) Fix true explanations of propagations in...	commit \| commitdiff \| tree
2020-11-12	Andrew Reynolds	(proof-new) Improve printing and debugging for pedantic...	commit \| commitdiff \| tree
2020-11-12	Andrew Reynolds	(proof-new) Add datatypes inference to proof constructor...	commit \| commitdiff \| tree
2020-11-12	Andrew Reynolds	Make symbol manager context dependent (#5424)	commit \| commitdiff \| tree
2020-11-11	Andrew Reynolds	Move symbol manager to src/expr/ (#5420)	commit \| commitdiff \| tree
2020-11-11	Andrew Reynolds	Rewrite witness terms at prerewrite (#5419)	commit \| commitdiff \| tree
2020-11-11	Andrew Reynolds	Add simple substitution utility (#5397)	commit \| commitdiff \| tree
2020-11-11	Andrew Reynolds	Pass symbol manager to commands (#5410)	commit \| commitdiff \| tree
2020-11-11	Andrew Reynolds	Fix preregistration in TheorySep before declare-heap...	commit \| commitdiff \| tree
2020-11-10	Andrew Reynolds	Do not mark extended functions as reduced based on...	commit \| commitdiff \| tree
2020-11-10	Alex Ozdemir	Pin LFSC version (#5412)	commit \| commitdiff \| tree
2020-11-10	Andrew Reynolds	Make mkGroundTerm deterministic (#5347)	commit \| commitdiff \| tree
2020-11-10	Andrew Reynolds	Add getSubtermKinds to node algorithm (#5398)	commit \| commitdiff \| tree
2020-11-10	Andrew Reynolds	Add proper support for the declare-heap command for...	commit \| commitdiff \| tree
2020-11-10	Andrew Reynolds	Migrate some documentation about attributes (#5390)	commit \| commitdiff \| tree
2020-11-09	Andrew Reynolds	Add symbol manager (#5380)	commit \| commitdiff \| tree
2020-11-09	Andrew Reynolds	Simplify handling of subtypes in smt2 printer (#5401)	commit \| commitdiff \| tree
2020-11-09	Gereon Kremer	Properly clear interrupt for solve() as well. (#5403)	commit \| commitdiff \| tree
2020-11-09	Andrew Reynolds	Do not regress explanations of datatype lemmas (#5376)	commit \| commitdiff \| tree
2020-11-06	mudathirmahgoub	Fix issue #5342 (#5349)	commit \| commitdiff \| tree
2020-11-06	Andrew Reynolds	(proof-new) Miscellaneous changes to strings for proofs...	commit \| commitdiff \| tree
2020-11-06	Andrew Reynolds	Split sygus template inference to its own file (#5388)	commit \| commitdiff \| tree
2020-11-06	Andrew Reynolds	Simplify printing with respect to expression types...	commit \| commitdiff \| tree
2020-11-05	mudathirmahgoub	Remove mkSingleton from the API (#5366)	commit \| commitdiff \| tree
next

RSS Atom