summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-02-17TheoryIds for UF theory. (#5901)Gereon Kremer
2021-02-17Add InferenceIds for theory of arrays (#5910)Gereon Kremer
2021-02-17Add InferenceId to buffered inference manager (#5911)Gereon Kremer
2021-02-17Add new IntegralHistogramStat (#5898)Gereon Kremer
2021-02-16Add bit-level propagation support to BV bitblast solver. (#5906)Mathias Preiner
2021-02-16google test: parser: Migrate parser_builder_black. (#5896)Aina Niemetz
2021-02-15Remove now obsolete sendLemmas and inferences stat from arith::nl (#5903)Gereon Kremer
2021-02-13Moving methods from quantifiers engine to quantifiers state (#5881)Andrew Reynolds
2021-02-13Properly set up equality engine for BV bitblast solver. (#5905)Mathias Preiner
2021-02-12Simplify and fix decision engine's handling of skolem definitions (#5888)Andrew Reynolds
2021-02-12(proof-new) Option to not automatically consider symmetry in CDProof (#5895)Andrew Reynolds
2021-02-11google test: parser: Migrate parser_black. (#5886)Aina Niemetz
2021-02-11Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)Gereon Kremer
2021-02-11Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)Gereon Kremer
2021-02-11[proof-new] Adding a proof-producing ensure literal method (#5889)Haniel Barbosa
2021-02-11Merge InferenceIds into one enum (#5892)Gereon Kremer
2021-02-11Fix spurious assertion failure in regexp normalization (#5852)Andrew Reynolds
2021-02-11Simplify interface for preprocessor (#5890)Andrew Reynolds
2021-02-10Refactor term registration visitors (#5875)Andrew Reynolds
2021-02-10Fix open proof for factoring lemma (#5885)Andrew Reynolds
2021-02-10Simplify method for inferring proxy lemmas in strings (#5789)Andrew Reynolds
2021-02-09Remove track instantiations infrastructure (#5883)Andrew Reynolds
2021-02-09Optimize get skolems method (#5876)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback