summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-05-07Fix and add missing REQUIRE labels for FP regression tests. (#6506)Aina Niemetz
2021-05-07Integrate documentation build with the regular CI workflow (#6490)Gereon Kremer
2021-05-07Properly printing INST_PATTERN_LIST by itself (#6507)Haniel Barbosa
2021-05-07Simplifications to expand definitions (#6487)Andrew Reynolds
2021-05-07Fix for toPythonObj of integer value with real sort (#6505)makaimann
2021-05-06[proof-new] Updating documentation for Subs/Rw ids (#6502)Haniel Barbosa
2021-05-06Discard duplicate terms in patterns (#6501)Andrew Reynolds
2021-05-06Update README.md and remove last CVC4 references. (#6497)Mathias Preiner
2021-05-06Use constant folding for evaluating BV eager atom (#6494)Andrew Reynolds
2021-05-05Do not have quantifiers model inherit from theory model (#6493)Andrew Reynolds
2021-05-05Save block comments associated with each kind when parsing kinds file (#6489)makaimann
2021-05-05Add helper functions for multi-objective optimization + refactoring (#6473)Ouyancheng
2021-05-04Move current decision engine to decision engine old (#6466)Andrew Reynolds
2021-05-04Move env into smt solver, theory engine, prop engine (#6486)Andrew Reynolds
2021-05-04Do not use proof CNF stream with assumptions-based cores (#6488)Haniel Barbosa
2021-05-04Use proper commit hash for PRs (#6485)Gereon Kremer
2021-05-04cmake: Fix ninja build. (#6481)Mathias Preiner
2021-05-04Improve generation of python API documentation (#6482)Gereon Kremer
2021-05-04FP: Move removal of generic to_fp operations to rewriter. (#6480)Aina Niemetz
2021-05-04FP: Move type check from expandDefinitions. (#6479)Aina Niemetz
2021-05-03FP: Rewrite to_fp conversion from signed bit-vector. (#6472)Aina Niemetz
2021-05-03Add missing --auto-download in CI (#6478)Gereon Kremer
2021-05-03Add CI jobs to build docs (#6413)Gereon Kremer
2021-05-03SymFPU: Automatically apply patch from 2020-11-14. (#6471)Aina Niemetz
2021-05-03Python API tests for terms -- Part 1 (#6468)yoni206
2021-04-30bv: Refactor ppAssert and move to TheoryBV. (#6470)Mathias Preiner
2021-04-30Add parameter name for argument `isPreRewrite` for FP rewrites. (#6469)Aina Niemetz
2021-04-30Refactor optimization result and objective classes + add preliminary support ...Ouyancheng
2021-04-30Use substitutions for implementing defined functions (#6437)Andrew Reynolds
2021-04-29Add assertion list utility for justification heuristic (#6414)Andrew Reynolds
2021-04-29Simplify generated code for getOption() and setOption() (#6462)Gereon Kremer
2021-04-29Add missing include. (#6463)Gereon Kremer
2021-04-29Avoid exponential explosion of small constant in CEGQI (#6461)Gereon Kremer
2021-04-28Fix BV Optimization Boundary Condition when lower bound = upper bound + 1 (#6...Ouyancheng
2021-04-28Refactor resource manager options (#6446)Gereon Kremer
2021-04-28Remove exception headers from options.h (#6456)Gereon Kremer
2021-04-28Make sure reference stats are reset properly (#6457)Gereon Kremer
2021-04-28Clean up options holder class (#6458)Gereon Kremer
2021-04-28Cleanup DidYouMean (#6454)Gereon Kremer
2021-04-27Add internal support for datatype update (#6450)Andrew Reynolds
2021-04-27Move slow regression to regress3 (#6451)Andrew Reynolds
2021-04-27Fix refutational soundness bug in quantifier prenexing (#6448)Andrew Reynolds
2021-04-27Simplify making function types (#6447)Andrew Reynolds
2021-04-27Initial setup for docs of python API (#6445)Gereon Kremer
2021-04-27Use std::hash for API types (#6432)Gereon Kremer
2021-04-27Bool: Move implementation of type rules to cpp. (#6420)Aina Niemetz
2021-04-26Generate docs conf.py by cmake (#6441)Gereon Kremer
2021-04-26Protect int stats methods (#6442)Gereon Kremer
2021-04-26First part of options refactoring (#6428)Gereon Kremer
2021-04-26Fix theoryOf for Boolean equalities (#6444)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback