summaryrefslogtreecommitdiff
path: root/src/smt/process_assertions.cpp
AgeCommit message (Expand)Author
2021-10-25Fix support for global declarations (#7480)Andrew Reynolds
2021-10-22Remove `--uf-ho` option (#7463)Andrew Reynolds
2021-10-12Clean up occurrences of SmtEngine in comments. (#7349)Aina Niemetz
2021-10-12Get rid of unused member d_smtStats in ExpandDefs. (#7346)Aina Niemetz
2021-10-11Rename SmtEngineStatistics to SolverEngineStatistics. (#7339)Aina Niemetz
2021-10-09Remove static accesses to options where EnvObj is used (#7330)Gereon Kremer
2021-10-07Move preprocessor to smt solver (#7321)Andrew Reynolds
2021-10-07Eliminate more circular dependencies on solver engine (#7311)Andrew Reynolds
2021-09-30Rename SmtEngine to SolverEngine. (#7282)Aina Niemetz
2021-09-30Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)Aina Niemetz
2021-07-06Integrate learned rewrite preprocessing pass (#6840)Andrew Reynolds
2021-04-30Use substitutions for implementing defined functions (#6437)Andrew Reynolds
2021-04-19Fully incorporate quantifiers macros into ppAssert / non-clausal simplificati...Andrew Reynolds
2021-04-12Refactor resource manager (#6322)Gereon Kremer
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-10Fix term registration and non-theory-preprocessed terms in substitutions (#6080)Andrew Reynolds
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
2021-01-15Implement --no-strings-lazy-pp as a preprocessing pass (#5777)Andrew Reynolds
2021-01-14Updates to theory preprocess equality (#5776)Andrew Reynolds
2021-01-12Foreign theory rewrite option (#5763)yoni206
2020-12-24[proof-new] Only use old proofs for unsat cores if no proof new (#5725)Haniel Barbosa
2020-12-22Make theory preprocess rewrite equalities a preprocessing pass (#5711)Andrew Reynolds
2020-12-21Move ownership of theory preprocessor to TheoryProxy (#5690)Andrew Reynolds
2020-12-16Simplify preprocessing (#5647)Andrew Reynolds
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-12-02Update copyright headers.Aina Niemetz
2020-11-26Move expand definitions to its own file (#5528)Andrew Reynolds
2020-11-18Minor cleanup of SmtEngine (#5450)Andrew Reynolds
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
2020-10-19(proof-new) Update preprocessing pass context for proofs (#5298)Andrew Reynolds
2020-10-06bv-to-int: change order of passes (#5208)yoni206
2020-10-01(proof-new) Preprocessing passes use proper interfaces to assertions pipeline...Andrew Reynolds
2020-09-24 Function definition fmf preprocessing pass (#5064)Andrew Reynolds
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-16Dump commands in internal code using command printing functions. (#5040)Abdalrhman Mohamed
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-08-21Remove BV equality slicer (#4928)Andrew Reynolds
2020-08-13Split SmtSolver from SmtEngine (#4880)Andrew Reynolds
2020-08-11Split SmtEngineState from SmtEngine (#4855)Andrew Reynolds
2020-08-05Split Assertions from SmtEngine (#4788)Andrew Reynolds
2020-07-11Changing bv_to_int options (#4721)yoni206
2020-07-10(proof-new) Update Theory interface for proof-new (#4648)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-04-08Split ProcessAssertions module from SmtEngine (#4210)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback