With this the fourth week and the first phase of GSoC 2019 is over. Here I will give you a brief summary of my progress this week.
I started this week by setting up my workspace for profiling the code related to new assumptions. I am using pyinstrument for that. The results of profiler suggests that a significant amount of time is spent in the to_cnf() function which converts the logical expression into their CNF counterparts, to be used by the SAT solver. Also, since this system is built over the SymPy core, a large amount of this time is spent in the core itself (See the graph here). A possible solution to this is to use constructs at a level lower than the SymPy objects, hence removing the overheads.
Also, as suggested in the last blog, there are various ideas proposed for improving the new assumptions mechanism. Some of them have been implemented to some extent in some PRs. Before proceeding for any new strategies, I need to look into these ideas first. I have started an issue-tree to gather them.
Over the end of the week, I also pushed my work on First Order Logic module at #17069. This work is based on #7608 and extends it by adding Equality to it. Currently, there are test failures and some points to decide. I will try to get it done within this week.
I spent most of this week exploring the profiling and benchmarking of code, and I learnt a lot during this. For the coming week, I will focus on speeding up the code in to_cnf. As suggested by Aaron, this seems a good point to start with. Also, I will be working on the FOL module.