Split ProcessAssertions module from SmtEngine (#4210)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 9 Apr 2020 01:26:11 +0000 (20:26 -0500)
committerGitHub <noreply@github.com>
Thu, 9 Apr 2020 01:26:11 +0000 (20:26 -0500)
commit2f8caabd570dd5bb2936d9f094b7b302a510aa6d
tree5ae3497d2dcd9bf39cc0686a1a0d23b0113571d2
parentdf1ea6b9cdc1f424073151d0f7fda639d4405622
Split ProcessAssertions module from SmtEngine (#4210)

This is a step towards refactoring the SmtEngine. It splits several core components of SmtEnginePrivate to its own independent module, ProcessAssertions which is responsible for applying preprocessing passes , simplification and expand definitions.

The main change involved moving these functions from SmtEnginePrivate to this new class. A few other minor changes were done to make this move:

A few things changed order within processAssertions to allow SmtEnginePrivate-specific things to happen outside of the main scope of processAssertions.
processAssertions had some logic to catch incompatible options and silently disable options. This was moved to setDefaults.
A few data members in SmtEngine were moved to ProcessAssertions.
Two utilities that were sitting in smt_engine.cpp were moved to their own files.
Another refactoring step will be to make ProcessAssertions take only the utilities it needs instead of taking a SmtEngine reference. This requires further detangling of Options.
src/CMakeLists.txt
src/options/arith_options.toml
src/smt/defined_function.h [new file with mode: 0644]
src/smt/process_assertions.cpp [new file with mode: 0644]
src/smt/process_assertions.h [new file with mode: 0644]
src/smt/set_defaults.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/smt/smt_engine_stats.cpp [new file with mode: 0644]
src/smt/smt_engine_stats.h [new file with mode: 0644]