summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2021-05-10Remove header for option modules (#6514)Gereon Kremer
2021-05-10Remove read_only from options. (#6513)Gereon Kremer
2021-05-10Unify top-level substitutions and model substitutions (#6499)Andrew Reynolds
2021-05-10Add doc to Kind.java (#6498)mudathirmahgoub
2021-05-08Adding functions to the python API and testing them (#6477)yoni206
2021-05-07Add support for datatype update (#6449)Andrew Reynolds
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-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-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-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-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-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
2021-04-26New design in DOT representation, nodes colored based on visions(basic and pr...Diego Della Rocca de Camargos
2021-04-26Ensure dependency is tracked for all substitutions (#6438)Andrew Reynolds
2021-04-26Enable print-inst-full by default (#6435)Andrew Reynolds
2021-04-26Fix assertions in SAT solver (#6443)Haniel Barbosa
2021-04-26Do not process looping word equations over sequences (#6434)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback