update description for signature of the theory solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/theory_finite_set.h

@@ -57,20 +57,42 @@ Abstract:
    -----------------------------------------------
         x in v3 <=> p(x) and x in v4
 
+Rules are encoded in src/ast/rewriter/finite_set_axioms.cpp as clauses.
+
 The central claim is that the above rules are sufficient to
-decide satisfiability of finite set constraints.
+decide satisfiability of finite set constraints for a subset
+of operations, namely union, intersection, difference, singleton, membership.
 Model construction proceeds by selecting every set.in(x_i, v) for a 
 congruence root v. Then the set of elements { x_i | set.in(x_i, v) } 
 is the interpretation.
 
-This approach, however, does not work with ranges, or is impractical.
-For ranges, we are going to extract an interpretation for set variable v
-directly from a set of range expressions.
-Inductively, the interpretation of a range expression is given by the
-range itself. It proceeds by taking unions, intersections and differences of range
-interpretations. 
+This approach for model-construction, however, does not work with ranges, or is impractical.
+For ranges we can adapt a different model construction approach.
+
+When introducing select and map, decidability can be lost.
 
 For Boolean lattice constraints given by equality, subset, strict subset and union, intersections, 
 the theory solver uses a stand-alone satisfiability checker for Boolean algebras to close branches.
 
+Instructions for copilot:
+
+1. Override relevant methods for smt::theory. Add them to the signature and add stubs or implementations in
+theory_finite_set.cpp.
+2. In final_check_eh add instantiation of theory axioms following the outline in the inference rules above.
+   An example of how to instantiate axioms is in theory_arrays_base.cpp and theroy_datatypes.cpp and other theory files.
 --*/
+
+#pragma once
+
+#include "ast/ast.h"
+#include "ast/ast_pp.h"
+#include "smt/smt_theory.h"
+
+namespace smt {
+    class theory_finite_set : public theory {
+    public:
+        theory_finite_set(ast_manager & m);
+        ~theory_finite_set() override {}
+    };
+
+}  // namespace smt