summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-02-09Do not traverse quantifiers in term formula removal (#5859)Andrew Reynolds
2021-02-09cmake: Make Python3 default and improve toml error messages. (#5884)Mathias Preiner
2021-02-09Eliminating dependencies from inst utils (#5882)Andrew Reynolds
2021-02-09Make term database optionally SAT-context-dependent (#5877)Andrew Reynolds
2021-02-09google test: expr: Migrate node_manager_black. (#5857)Aina Niemetz
2021-02-09google test: main: Migrate interactive_shell_black. (#5878)Aina Niemetz
2021-02-09google test: expr: Migrate type_cardinality_black. (#5871)Aina Niemetz
2021-02-09google test: expr: Migrate node_self_iterator_black. (#5865)Aina Niemetz
2021-02-09[quantifiers] Fix prenex computation (#5879)Haniel Barbosa
2021-02-08google test: expr: Migrate type_node_white. (#5872)Aina Niemetz
2021-02-08Use quantifiers inference manager for lemma management (#5867)Andrew Reynolds
2021-02-08Fix disequality between seq.unit terms (#5880)Andrew Reynolds
2021-02-08google test: expr: Migrate node_white. (#5869)Aina Niemetz
2021-02-08Fix dumping of assertions for monolithic preprocessing passes (#5866)Haniel Barbosa
2021-02-08Remove support for inst closure (#5874)Andrew Reynolds
2021-02-08Use consistent names for fixtures in unit tests. (#5863)Aina Niemetz
2021-02-08google test: expr: Migrate node_traversal_black. (#5868)Aina Niemetz
2021-02-08Avoid spurious traversal of terms during preregistration (#5860)Andrew Reynolds
2021-02-05Do not combine theories if theory engine needs check (#5861)Andrew Reynolds
2021-02-05google test: expr: Migrate symbol_table_black. (#5870)Aina Niemetz
2021-02-05Minor cleaning of quantifiers engine (#5858)Andrew Reynolds
2021-02-05google test: expr: Migrate node_manager_white. (#5864)Aina Niemetz
2021-02-05Remove obsolete include from node_black unit test. (#5862)Aina Niemetz
2021-02-05google test: expr: Migrate node_builder_black. (#5855)Aina Niemetz
2021-02-05Miscellaneous cleaning in theory engine (#5854)Andrew Reynolds
2021-02-04Adding an option to optimize polite combination for datatypes (#5856)yoni206
2021-02-04Introduce quantifiers registry utility (#5829)Andrew Reynolds
2021-02-04Clarifying documentation of `--static-binary` (#5844)yoni206
2021-02-04Eliminate equality query dependence on quantifiers engine (#5831)Andrew Reynolds
2021-02-04[proof-new] Catch trivial cycles in SAT proof generation (#5853)Haniel Barbosa
2021-02-03Add BV solver bitblast. (#5851)Mathias Preiner
2021-02-03[proof-new] Fix MACRO_RESOLUTION expansion for singleton clause corner case (...Haniel Barbosa
2021-02-02(proof-new) Miscellaneous fixes and regressions (#5841)Andrew Reynolds
2021-02-02(proof-new) Refactor theory preprocessing (#5835)Andrew Reynolds
2021-02-02Remove quantifiers regression from decision folder (#5830)Andrew Reynolds
2021-02-02Cleanup some includes (#5847)Andrew Reynolds
2021-02-02Improvements for NL traces (#5846)Andrew Reynolds
2021-02-02[proof-new] Fix bug in expansion of MACRO_RESOLUTION (#5845)Haniel Barbosa
2021-02-01Eliminate PREPROCESS lemma property (#5827)Andrew Reynolds
2021-02-01Simplify alpha equivalence module (#5839)Andrew Reynolds
2021-02-01Avoid calling the printers while converting sexpr to string. (#5842)Abdalrhman Mohamed
2021-02-01Fix BagsRewriter::rewriteUnionDisjoint (#5840)mudathirmahgoub
2021-01-30Fix unguarded call to get representative (#5838)Andrew Reynolds
2021-01-29[proof-new] Connecting new unsat cores (#5834)Haniel Barbosa
2021-01-29Add bag inferences for operators: intersection, duplicate_removal, and empty ...mudathirmahgoub
2021-01-29(proof-new) Distinguish pre vs post rewrites in term conversion proof generat...Andrew Reynolds
2021-01-28Reorganize calls to quantifiers engine from SmtEngine layer (#5828)Andrew Reynolds
2021-01-28Remove regex header from cvc4cpp.cpp (#5826)mudathirmahgoub
2021-01-28Simplify lemma interface (#5819)Andrew Reynolds
2021-01-28Use standard equality engine information in quantifiers state (#5824)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback