diff --git a/lib/assertion_set.txt b/lib/assertion_set.txt deleted file mode 100644 index b8d49f7e6..000000000 --- a/lib/assertion_set.txt +++ /dev/null @@ -1,78 +0,0 @@ - -The assertion_set class is essentially a set of formulas. -The assertion_set copy() method is constant time. They use persistent -arrays for "sharing" common parts. -The goal is to provide functors (strategies) that apply transformations to these sets. -Examples of transformations are: - - simplification - - gaussian elimination - - CNF, NNF, OCNF transformation - - bit-blasting - - abstraction - - grobner basis computation - - completion - - term rewriting - - bound propagation - - contextal simplification - - if-then-else lifting - - quantifier elimination - - etc - -A functor/strategy is essentially updating an assertion set. It may -also provide a model_converter to convert a model for the resultant -assertion_set into a model for the original assertion_set. See -gaussian_elim.cpp for an example of model_converter. A functor may -return a vector of assertion sets. It may also return a -proof_converter for converting proofs for the resultant assertion -set(s) into a proof for the original assertion_set. The -functor/strategy user is responsible for "plumbing" the -model_converter(s) and proof_converter(s). In the future we may have -tacticals for combining these functors/strategies. This is not needed -now. - -The idea is to provide assertion_set_solvers. They are essentially end-game -strategies. The abstract API for them is defined at assertion_set_solver.h. -Currently, the only assertion_set_solver is based on smt_context.h. -The next one will be based on a pure SAT solver. I also have plans for -one based on linear programming. - -The main goals of the new design are: - - increase modularity. - - expose assertion_set abstraction to external users. - - expose these functor/strategies to external users. - - allow us to combine problem specific solvers in a modular way. - - everything can be interrupted. - - some actions may be resumed. - - clean parallel_z3 implementation. - - support non-satisfiability preserving transformations. - the basic idea is: - * if the transformation is an over-approximation, - then the model_converter must throw an exception if it - can't convert the model into a model for the original assertion_set. - * if the transformation is an under-approximation, - then the proof_converter must throw an exception if it - can't convert the proof(s) into a proof for the original assertion_set. - I don't expect us to provide extensive support for proofs. - So, under-approximations will never really be used to show that - an assertion_set is unsatisfiable. - -Another goal is to a solver object that is essentially invoking an -external solver (process). I expect the external solver (in most cases) to be -Z3 itself. The main advantages are: the main process is safe from crashes, -and we can even invoke solvers in remote machines. - -The new functor/strategy design is not meant for incremental solving. -We may still have solvers that are incremental such as smt_context.h. - -Additional remarks: - -Failures and interruptions are reported using exceptions. -Each functor must provide a cancel() method that can be invoked to -interrupt it. A resume() method is optional. It is a must have if the -functor/strategy may be too time consuming. Each functor may have its -own set of parameters. See rewriter_params.h for an example. The -parameters may have options such as m_max_memory for blocking the -executiong of the functor. Each functor should have a cleanup() -method that must reclaim (almost) all memory consumed by the functor. - - diff --git a/lib/array_property_expander.cpp b/src/dead/array_property_expander.cpp similarity index 100% rename from lib/array_property_expander.cpp rename to src/dead/array_property_expander.cpp diff --git a/lib/array_property_expander.h b/src/dead/array_property_expander.h similarity index 100% rename from lib/array_property_expander.h rename to src/dead/array_property_expander.h diff --git a/lib/array_property_recognizer.cpp b/src/dead/array_property_recognizer.cpp similarity index 100% rename from lib/array_property_recognizer.cpp rename to src/dead/array_property_recognizer.cpp diff --git a/lib/array_property_recognizer.h b/src/dead/array_property_recognizer.h similarity index 100% rename from lib/array_property_recognizer.h rename to src/dead/array_property_recognizer.h diff --git a/lib/big_rational.h b/src/dead/big_rational.h similarity index 100% rename from lib/big_rational.h rename to src/dead/big_rational.h diff --git a/lib/dummy_big_rational.h b/src/dead/dummy_big_rational.h similarity index 100% rename from lib/dummy_big_rational.h rename to src/dead/dummy_big_rational.h diff --git a/lib/gl_tactic.cpp b/src/dead/gl_tactic.cpp similarity index 100% rename from lib/gl_tactic.cpp rename to src/dead/gl_tactic.cpp diff --git a/lib/gl_tactic.h b/src/dead/gl_tactic.h similarity index 100% rename from lib/gl_tactic.h rename to src/dead/gl_tactic.h diff --git a/lib/gmp_big_rational.cpp b/src/dead/gmp_big_rational.cpp similarity index 100% rename from lib/gmp_big_rational.cpp rename to src/dead/gmp_big_rational.cpp diff --git a/lib/gmp_big_rational.h b/src/dead/gmp_big_rational.h similarity index 100% rename from lib/gmp_big_rational.h rename to src/dead/gmp_big_rational.h diff --git a/lib/arith_simplifier_params.cpp b/src/old_params/arith_simplifier_params.cpp similarity index 100% rename from lib/arith_simplifier_params.cpp rename to src/old_params/arith_simplifier_params.cpp diff --git a/lib/rewriter.txt b/src/rewriter/rewriter.txt similarity index 100% rename from lib/rewriter.txt rename to src/rewriter/rewriter.txt