diff --git a/class_20_03102023/summary.txt b/class_20_03102023/summary.txt
new file mode 100644
index 0000000..efd9faf
--- /dev/null
+++ b/class_20_03102023/summary.txt
@@ -0,0 +1,16 @@
+Resolution
+Examples 
+Soundness of resolution rule.
+
+Res*(F) 
+
+Proposition 1: 
+If \emptyset \in Res*(F) then F is unsatisfiable. 
+Proof : (by contradiction and using soundness of resolution rule) 
+
+Proposition 2: 
+If  F is unsatisfiable  then  \emptyset \in Res*(F)  
+Proof : (by induction on #prop_variables appearing in F
+Base case : when F has only one variable. 
+
+
diff --git a/class_21_05102023/Z3_slides.pdf b/class_21_05102023/Z3_slides.pdf
new file mode 100644
index 0000000..8ce09c2
Binary files /dev/null and b/class_21_05102023/Z3_slides.pdf differ
diff --git a/class_21_05102023/demorgan.cpp b/class_21_05102023/demorgan.cpp
new file mode 100644
index 0000000..49cba81
--- /dev/null
+++ b/class_21_05102023/demorgan.cpp
@@ -0,0 +1,38 @@
+#include <iostream>
+#include <sstream>
+#include<vector>
+#include"z3++.h"
+
+using namespace z3;
+
+
+/**
+   De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
+*/
+ 
+ 
+int main(){
+
+context c; 
+expr  x  = c.bool_const("x"); 
+expr  y  = c.bool_const("y"); 
+expr conjecture = !(x && y) == (!x || !y); 
+
+//create a solver 
+solver s(c); 
+
+//assert the negation of conjecture 
+s.add(!conjecture); 
+
+std::cout << s << "\n";
+std::cout << s.to_smt2() << "\n"; 
+
+//check if the result if unsat
+switch (s.check()) {
+case unsat: std::cout << "demorgan is valid\n"; break;
+case sat: std::cout << "demorgan is not valid\n"; break;
+case unknown: std::cout <<"unknown\n"; break; 
+}
+} //end of function 
+
+
diff --git a/class_21_05102023/example.cpp b/class_21_05102023/example.cpp
new file mode 100644
index 0000000..6f92c00
--- /dev/null
+++ b/class_21_05102023/example.cpp
@@ -0,0 +1,1421 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+#include <iostream>
+#include <sstream>
+#include<vector>
+#include"z3++.h"
+
+using namespace z3;
+
+
+
+
+/**
+   Demonstration of how Z3 can be used to prove validity of
+   De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
+*/
+void demorgan() {
+    std::cout << "de-Morgan example\n";
+    
+    context c;
+
+    expr x = c.bool_const("x");
+    expr y = c.bool_const("y");
+    expr conjecture = (!(x && y)) == (!x || !y);
+    
+    solver s(c);
+    // adding the negation of the conjecture as a constraint.
+    s.add(!conjecture);
+    std::cout << s << "\n";
+    std::cout << s.to_smt2() << "\n";
+    switch (s.check()) {
+    case unsat:   std::cout << "de-Morgan is valid\n"; break;
+    case sat:     std::cout << "de-Morgan is not valid\n"; break;
+    case unknown: std::cout << "unknown\n"; break;
+    }
+}
+
+/**
+   \brief Find a model for <tt>x >= 1 and y < x + 3</tt>.
+*/
+void find_model_example1() {
+    std::cout << "find_model_example1\n";
+    context c;
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    solver s(c);
+
+    s.add(x >= 1);
+    s.add(y < x + 3);
+    std::cout << s.check() << "\n";
+
+    model m = s.get_model();
+    std::cout << m << "\n";
+    // traversing the model
+    for (unsigned i = 0; i < m.size(); i++) {
+        func_decl v = m[i];
+        // this problem contains only constants
+        assert(v.arity() == 0); 
+        std::cout << v.name() << " = " << m.get_const_interp(v) << "\n";
+    }
+    // we can evaluate expressions in the model.
+    std::cout << "x + y + 1 = " << m.eval(x + y + 1) << "\n";
+}
+
+
+/**
+   \brief Prove <tt>x = y implies g(x) = g(y)</tt>, and
+   disprove <tt>x = y implies g(g(x)) = g(y)</tt>.
+
+   This function demonstrates how to create uninterpreted types and
+   functions.
+*/
+void prove_example1() {
+    std::cout << "prove_example1\n";
+    
+    context c;
+    expr x      = c.int_const("x");
+    expr y      = c.int_const("y");
+    sort I      = c.int_sort();
+    func_decl g = function("g", I, I);
+    
+    solver s(c);
+    expr conjecture1 = implies(x == y, g(x) == g(y));
+    std::cout << "conjecture 1\n" << conjecture1 << "\n";
+    s.add(!conjecture1);
+    if (s.check() == unsat) 
+        std::cout << "proved" << "\n";
+    else
+        std::cout << "failed to prove" << "\n";
+
+    s.reset(); // remove all assertions from solver s
+
+    expr conjecture2 = implies(x == y, g(g(x)) == g(y));
+    std::cout << "conjecture 2\n" << conjecture2 << "\n";
+    s.add(!conjecture2);
+    if (s.check() == unsat) {
+        std::cout << "proved" << "\n";
+    }
+    else {
+        std::cout << "failed to prove" << "\n";
+        model m = s.get_model();
+        std::cout << "counterexample:\n" << m << "\n";
+        std::cout << "g(g(x)) = " << m.eval(g(g(x))) << "\n";
+        std::cout << "g(y)    = " << m.eval(g(y)) << "\n";
+    }
+}
+
+/**
+   \brief Prove <tt>not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 </tt>.
+   Then, show that <tt>z < -1</tt> is not implied.
+
+   This example demonstrates how to combine uninterpreted functions and arithmetic.
+*/
+void prove_example2() {
+    std::cout << "prove_example1\n";
+    context c;
+    expr x      = c.int_const("x");
+    expr y      = c.int_const("y");
+    expr z      = c.int_const("z");
+    sort I      = c.int_sort();
+    func_decl g = function("g", I, I);
+    
+    expr conjecture1 = implies(g(g(x) - g(y)) != g(z) && x + z <= y && y <= x,
+                               z < 0);
+
+    solver s(c);
+    s.add(!conjecture1);
+    std::cout << "conjecture 1:\n" << conjecture1 << "\n";
+    if (s.check() == unsat) 
+        std::cout << "proved" << "\n";
+    else
+        std::cout << "failed to prove" << "\n";
+
+    expr conjecture2 = implies(g(g(x) - g(y)) != g(z) && x + z <= y && y <= x,
+                               z < -1);
+    s.reset();
+    s.add(!conjecture2);
+    std::cout << "conjecture 2:\n" << conjecture2 << "\n";
+
+    if (s.check() == unsat) {
+        std::cout << "proved" << "\n";
+    }
+    else {
+        std::cout << "failed to prove" << "\n";
+        std::cout << "counterexample:\n" << s.get_model() << "\n";
+    }
+}
+
+/**
+   \brief Nonlinear arithmetic example 1
+*/
+void nonlinear_example1() {
+    std::cout << "nonlinear example 1\n";
+    config cfg;
+    cfg.set("auto_config", true);
+    context c(cfg);
+
+    expr x = c.real_const("x");
+    expr y = c.real_const("y");
+    expr z = c.real_const("z");
+                     
+    solver s(c);
+
+    s.add(x*x + y*y == 1);                     // x^2 + y^2 == 1
+    s.add(x*x*x + z*z*z < c.real_val("1/2"));  // x^3 + z^3 < 1/2
+    s.add(z != 0);
+    std::cout << s.check() << "\n";
+    model m = s.get_model();
+    std::cout << m << "\n";
+    set_param("pp.decimal", true); // set decimal notation
+    std::cout << "model in decimal notation\n";
+    std::cout << m << "\n";
+    set_param("pp.decimal-precision", 50); // increase number of decimal places to 50.
+    std::cout << "model using 50 decimal places\n";
+    std::cout << m << "\n";
+    set_param("pp.decimal", false); // disable decimal notation
+}
+
+/**
+   \brief Simple function that tries to prove the given conjecture using the following steps:
+   1- create a solver
+   2- assert the negation of the conjecture
+   3- checks if the result is unsat.
+*/
+void prove(expr conjecture) {
+    context & c = conjecture.ctx();
+    solver s(c);
+    s.add(!conjecture);
+    std::cout << "conjecture:\n" << conjecture << "\n";
+    if (s.check() == unsat) {
+        std::cout << "proved" << "\n";
+    }
+    else {
+        std::cout << "failed to prove" << "\n";
+        std::cout << "counterexample:\n" << s.get_model() << "\n";
+    }
+}
+
+/**
+   \brief Simple bit-vector example. This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers
+*/
+void bitvector_example1() {
+    std::cout << "bitvector example 1\n";
+    context c;
+    expr x = c.bv_const("x", 32);
+    
+    // using signed <=
+    prove((x - 10 <= 0) == (x <= 10));
+
+    // using unsigned <=
+    prove(ule(x - 10, 0) == ule(x, 10));
+
+    expr y = c.bv_const("y", 32);
+    prove(implies(concat(x, y) == concat(y, x), x == y));
+}
+
+/**
+   \brief Find x and y such that: x ^ y - 103 == x * y
+*/
+void bitvector_example2() {
+    std::cout << "bitvector example 2\n";
+    context c;
+    expr x = c.bv_const("x", 32);
+    expr y = c.bv_const("y", 32);
+    solver s(c);
+    // In C++, the operator == has higher precedence than ^.
+    s.add((x ^ y) - 103 == x * y);
+    std::cout << s << "\n";
+    std::cout << s.check() << "\n";
+    std::cout << s.get_model() << "\n";
+}
+
+/**
+   \brief Mixing C and C++ APIs.
+*/
+void capi_example() {
+    std::cout << "capi example\n";
+    context c;
+    expr x = c.bv_const("x", 32);
+    expr y = c.bv_const("y", 32);
+    // Invoking a C API function, and wrapping the result using an expr object.
+    expr r = to_expr(c, Z3_mk_bvsrem(c, x, y));
+    std::cout << "r: " << r << "\n";
+}
+
+/**
+   \brief Demonstrate how to evaluate expressions in a model.
+*/
+void eval_example1() {
+    std::cout << "eval example 1\n";
+    context c;
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    solver s(c);
+
+    /* assert x < y */
+    s.add(x < y);
+    /* assert x > 2 */
+    s.add(x > 2);
+    
+    std::cout << s.check() << "\n";
+    
+    model m = s.get_model();
+    std::cout << "Model:\n" << m << "\n";
+    std::cout << "x+y = " << m.eval(x+y) << "\n";
+}
+
+/**
+   \brief Several contexts can be used simultaneously.
+*/
+void two_contexts_example1() {
+    std::cout << "two contexts example 1\n";
+    context c1, c2;
+    
+    expr x = c1.int_const("x");
+    expr n = x + 1;
+    // We cannot mix expressions from different contexts, but we can copy
+    // an expression from one context to another.
+    // The following statement copies the expression n from c1 to c2.
+    expr n1 = to_expr(c2, Z3_translate(c1, n, c2));
+    std::cout << n1 << "\n";
+}
+
+/**
+   \brief Demonstrates how to catch API usage errors.
+ */
+void error_example() {
+    std::cout << "error example\n";
+
+    context c;
+    expr x = c.bool_const("x");
+
+    // Error using the C API can be detected using Z3_get_error_code.
+    // The next call fails because x is a constant.
+    //Z3_ast arg = Z3_get_app_arg(c, x, 0);
+    if (Z3_get_error_code(c) != Z3_OK) {
+        std::cout << "last call failed.\n";
+    }
+
+    // The C++ layer converts API usage errors into exceptions.
+    try {
+        // The next call fails because x is a Boolean.
+        expr n = x + 1;
+    }
+    catch (exception & ex) {
+        std::cout << "failed: " << ex << "\n";
+    }
+
+    // The functions to_expr, to_sort and to_func_decl also convert C API errors into exceptions.
+    try {
+        expr arg = to_expr(c, Z3_get_app_arg(c, x, 0));
+    }
+    catch (exception & ex) {
+        std::cout << "failed: " << ex << "\n";
+    }
+}
+
+/**
+    \brief Demonstrate different ways of creating rational numbers: decimal and fractional representations.
+*/
+void numeral_example() {
+    std::cout << "numeral example\n";
+    context c;
+    
+    expr n1 = c.real_val("1/2");
+    expr n2 = c.real_val("0.5");
+    expr n3 = c.real_val(1, 2);
+    std::cout << n1 << " " << n2 << " " << n3 << "\n";
+    prove(n1 == n2 && n1 == n3);
+    
+    n1 = c.real_val("-1/3");
+    n2 = c.real_val("-0.3333333333333333333333333333333333");
+    std::cout << n1 << " " << n2 << "\n";
+    prove(n1 != n2);
+}
+
+/**
+   \brief Test ite-term (if-then-else terms).
+*/
+void ite_example() {
+    std::cout << "if-then-else example\n";
+    context c;
+    
+    expr f    = c.bool_val(false);
+    expr one  = c.int_val(1);
+    expr zero = c.int_val(0);
+    expr ite  = to_expr(c, Z3_mk_ite(c, f, one, zero));
+
+    std::cout << "term: " << ite << "\n";
+}
+
+void ite_example2() {
+    std::cout << "if-then-else example2\n";
+    context c;
+    expr b = c.bool_const("b");
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    std::cout << (ite(b, x, y) > 0) << "\n";
+}
+
+/**
+   \brief Small example using quantifiers.
+*/
+void quantifier_example() {
+    std::cout << "quantifier example\n";
+    context c;
+    
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    sort I = c.int_sort();
+    func_decl f = function("f", I, I, I);
+    
+    solver s(c);
+    
+    // making sure model based quantifier instantiation is enabled.
+    params p(c);
+    p.set("mbqi", true);
+    s.set(p);
+
+    s.add(forall(x, y, f(x, y) >= 0));
+    expr a = c.int_const("a");
+    s.add(f(a, a) < a);
+    std::cout << s << "\n";
+    std::cout << s.check() << "\n";
+    std::cout << s.get_model() << "\n";
+    s.add(a < 0);
+    std::cout << s.check() << "\n";
+}
+
+/**
+   \brief Unsat core example
+*/
+void unsat_core_example1() {
+    std::cout << "unsat core example1\n";
+    context c;
+    // We use answer literals to track assertions.
+    // An answer literal is essentially a fresh Boolean marker
+    // that is used to track an assertion.
+    // For example, if we want to track assertion F, we 
+    // create a fresh Boolean variable p and assert (p => F)
+    // Then we provide p as an argument for the check method.
+    expr p1 = c.bool_const("p1");
+    expr p2 = c.bool_const("p2");
+    expr p3 = c.bool_const("p3");
+    expr x  = c.int_const("x");
+    expr y  = c.int_const("y");
+    solver s(c);
+    s.add(implies(p1, x > 10));
+    s.add(implies(p1, y > x));
+    s.add(implies(p2, y < 5));
+    s.add(implies(p3, y > 0));
+    expr assumptions[3] = { p1, p2, p3 };
+    std::cout << s.check(3, assumptions) << "\n";
+    expr_vector core = s.unsat_core();
+    std::cout << core << "\n";
+    std::cout << "size: " << core.size() << "\n";
+    for (unsigned i = 0; i < core.size(); i++) {
+        std::cout << core[i] << "\n";
+    }
+    // Trying again without p2
+    expr assumptions2[2] = { p1, p3 };
+    std::cout << s.check(2, assumptions2) << "\n";
+}
+
+/**
+   \brief Unsat core example 2
+*/
+void unsat_core_example2() {
+    std::cout << "unsat core example 2\n";
+    context c;
+    // The answer literal mechanism, described in the previous example,
+    // tracks assertions. An assertion can be a complicated
+    // formula containing containing the conjunction of many subformulas.
+    expr p1 = c.bool_const("p1");
+    expr x  = c.int_const("x");
+    expr y  = c.int_const("y");
+    solver s(c);
+    expr F  = x > 10 && y > x && y < 5 && y > 0;
+    s.add(implies(p1, F));
+    expr assumptions[1] = { p1 };
+    std::cout << s.check(1, assumptions) << "\n";
+    expr_vector core = s.unsat_core();
+    std::cout << core << "\n";
+    std::cout << "size: " << core.size() << "\n";
+    for (unsigned i = 0; i < core.size(); i++) {
+        std::cout << core[i] << "\n";
+    }
+    // The core is not very informative, since p1 is tracking the formula F
+    // that is a conjunction of subformulas.
+    // Now, we use the following piece of code to break this conjunction
+    // into individual subformulas. First, we flat the conjunctions by
+    // using the method simplify.
+    std::vector<expr> qs; // auxiliary vector used to store new answer literals.
+    assert(F.is_app()); // I'm assuming F is an application.
+    if (F.decl().decl_kind() == Z3_OP_AND) {
+        // F is a conjunction
+        std::cout << "F num. args (before simplify): " << F.num_args() << "\n";
+        F = F.simplify();
+        std::cout << "F num. args (after simplify):  " << F.num_args() << "\n";
+        for (unsigned i = 0; i < F.num_args(); i++) {
+            std::cout << "Creating answer literal q" << i << " for " << F.arg(i) << "\n";
+            std::stringstream qname; qname << "q" << i;
+            expr qi = c.bool_const(qname.str().c_str()); // create a new answer literal
+            s.add(implies(qi, F.arg(i)));
+            qs.push_back(qi);
+        }
+    }
+    // The solver s already contains p1 => F
+    // To disable F, we add (not p1) as an additional assumption
+    qs.push_back(!p1);
+    std::cout << s.check(static_cast<unsigned>(qs.size()), &qs[0]) << "\n";
+    expr_vector core2 = s.unsat_core();
+    std::cout << core2 << "\n";
+    std::cout << "size: " << core2.size() << "\n";
+    for (unsigned i = 0; i < core2.size(); i++) {
+        std::cout << core2[i] << "\n";
+    }
+}
+
+/**
+   \brief Unsat core example 3
+*/
+void unsat_core_example3() {
+    // Extract unsat core using tracked assertions
+    std::cout << "unsat core example 3\n";
+    context c;
+    expr x  = c.int_const("x");
+    expr y  = c.int_const("y");
+    solver s(c);
+
+    // enabling unsat core tracking
+    params p(c);
+    p.set("unsat_core", true);
+    s.set(p);
+
+    // The following assertion will not be tracked.
+    s.add(x > 0);
+
+    // The following assertion will be tracked using Boolean variable p1.
+    // The C++ wrapper will automatically create the Boolean variable.
+    s.add(y > 0, "p1");
+
+    // Asserting other tracked assertions.
+    s.add(x < 10, "p2");
+    s.add(y < 0,  "p3");
+
+    std::cout << s.check() << "\n";
+    std::cout << s.unsat_core() << "\n";
+}
+
+void tactic_example1() {
+    /*
+      Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic
+      reasoning steps are represented as functions known as tactics, and tactics are composed
+      using combinators known as tacticals. Tactics process sets of formulas called Goals.
+
+      When a tactic is applied to some goal G, four different outcomes are possible. The tactic succeeds
+      in showing G to be satisfiable (i.e., feasible); succeeds in showing G to be unsatisfiable (i.e., infeasible); 
+      produces a sequence of subgoals; or fails. When reducing a goal G to a sequence of subgoals G1, ..., Gn, 
+      we face the problem of model conversion. A model converter construct a model for G using a model for some subgoal Gi.
+
+      In this example, we create a goal g consisting of three formulas, and a tactic t composed of two built-in tactics: 
+      simplify and solve-eqs. The tactic simplify apply transformations equivalent to the ones found in the command simplify. 
+      The tactic solver-eqs eliminate variables using Gaussian elimination. Actually, solve-eqs is not restricted 
+      only to linear arithmetic. It can also eliminate arbitrary variables. 
+      Then, sequential composition combinator & applies simplify to the input goal and solve-eqs to each subgoal produced by simplify. 
+      In this example, only one subgoal is produced.
+    */
+    std::cout << "tactic example 1\n";
+    context c;
+    expr x = c.real_const("x");
+    expr y = c.real_const("y");
+    goal g(c);
+    g.add(x > 0);
+    g.add(y > 0);
+    g.add(x == y + 2);
+    std::cout << g << "\n";
+    tactic t1(c, "simplify");
+    tactic t2(c, "solve-eqs");
+    tactic t = t1 & t2;
+    apply_result r = t(g);
+    std::cout << r << "\n";
+}
+
+void tactic_example2() {
+    /*
+      In Z3, we say a clause is any constraint of the form (f_1 || ... || f_n). 
+      The tactic split-clause will select a clause in the input goal, and split it n subgoals. 
+      One for each subformula f_i.
+    */
+    std::cout << "tactic example 2\n";
+    context c;
+    expr x = c.real_const("x");
+    expr y = c.real_const("y");
+    goal g(c);
+    g.add(x < 0 || x > 0);
+    g.add(x == y + 1);
+    g.add(y < 0);
+    tactic t(c, "split-clause");
+    apply_result r = t(g);
+    for (unsigned i = 0; i < r.size(); i++) {
+        std::cout << "subgoal " << i << "\n" << r[i] << "\n";
+    }
+}
+
+void tactic_example3() {
+    /*
+      - The choice combinator t | s first applies t to the given goal, if it fails then returns the result of s applied to the given goal.      
+      - repeat(t) Keep applying the given tactic until no subgoal is modified by it.
+      - repeat(t, n) Keep applying the given tactic until no subgoal is modified by it, or the number of iterations is greater than n.
+      - try_for(t, ms) Apply tactic t to the input goal, if it does not return in ms milliseconds, it fails.
+      - with(t, params) Apply the given tactic using the given parameters.      
+    */
+    std::cout << "tactic example 3\n";
+    context c;
+    expr x = c.real_const("x");
+    expr y = c.real_const("y");
+    expr z = c.real_const("z");
+    goal g(c);
+    g.add(x == 0 || x == 1);
+    g.add(y == 0 || y == 1);
+    g.add(z == 0 || z == 1);
+    g.add(x + y + z > 2);
+    // split all clauses
+    tactic split_all = repeat(tactic(c, "split-clause") | tactic(c, "skip"));
+    std::cout << split_all(g) << "\n";
+    tactic split_at_most_2 = repeat(tactic(c, "split-clause") | tactic(c, "skip"), 1);
+    std::cout << split_at_most_2(g) << "\n";
+    // In the tactic split_solver, the tactic solve-eqs discharges all but one goal. 
+    // Note that, this tactic generates one goal: the empty goal which is trivially satisfiable (i.e., feasible)
+    tactic split_solve = split_all & tactic(c, "solve-eqs");
+    std::cout << split_solve(g) << "\n";
+}
+
+void tactic_example4() {
+    /*
+      A tactic can be converted into a solver object using the method mk_solver(). 
+      If the tactic produces the empty goal, then the associated solver returns sat. 
+      If the tactic produces a single goal containing False, then the solver returns unsat. 
+      Otherwise, it returns unknown.
+
+      In this example, the tactic t implements a basic bit-vector solver using equation solving, 
+      bit-blasting, and a propositional SAT solver. 
+      We use the combinator `with` to configure our little solver. 
+      We also include the tactic `aig` which tries to compress Boolean formulas using And-Inverted Graphs.
+    */
+    std::cout << "tactic example 4\n";
+    context c;
+    params p(c);
+    p.set("mul2concat", true);
+    tactic t = 
+        with(tactic(c, "simplify"), p) &
+        tactic(c, "solve-eqs") &
+        tactic(c, "bit-blast") &
+        tactic(c, "aig") &
+        tactic(c, "sat");
+    solver s = t.mk_solver();
+    expr x = c.bv_const("x", 16);
+    expr y = c.bv_const("y", 16);
+    s.add(x*32 + y == 13);
+    // In C++, the operator < has higher precedence than &.
+    s.add((x & y) < 10);
+    s.add(y > -100);
+    std::cout << s.check() << "\n";
+    model m = s.get_model();
+    std::cout << m << "\n";
+    std::cout << "x*32 + y = " << m.eval(x*32 + y) << "\n";
+    std::cout << "x & y    = " << m.eval(x & y) << "\n";
+}
+
+void tactic_example5() {
+    /*
+      The tactic smt wraps the main solver in Z3 as a tactic.
+    */
+    std::cout << "tactic example 5\n";
+    context c;
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    solver s = tactic(c, "smt").mk_solver();
+    s.add(x > y + 1);
+    std::cout << s.check() << "\n";
+    std::cout << s.get_model() << "\n";
+}
+
+void tactic_example6() {
+    /*
+      In this example, we show how to implement a solver for integer arithmetic using SAT. 
+      The solver is complete only for problems where every variable has a lower and upper bound.
+    */ 
+    std::cout << "tactic example 6\n";
+    context c;
+    params p(c);
+    p.set("arith_lhs", true);
+    p.set("som", true); // sum-of-monomials normal form
+    solver s = 
+        (with(tactic(c, "simplify"), p) &
+         tactic(c, "normalize-bounds") &
+         tactic(c, "lia2pb") &
+         tactic(c, "pb2bv") &
+         tactic(c, "bit-blast") &
+         tactic(c, "sat")).mk_solver();
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    expr z = c.int_const("z");
+    s.add(x > 0 && x < 10);
+    s.add(y > 0 && y < 10);
+    s.add(z > 0 && z < 10);
+    s.add(3*y + 2*x == z);
+    std::cout << s.check() << "\n";
+    std::cout << s.get_model() << "\n";
+    s.reset();
+    s.add(3*y + 2*x == z);
+    std::cout << s.check() << "\n";
+}
+
+void tactic_example7() {
+    /*
+      Tactics can be combined with solvers. 
+      For example, we can apply a tactic to a goal, produced a set of subgoals, 
+      then select one of the subgoals and solve it using a solver. 
+      This example demonstrates how to do that, and 
+      how to use model converters to convert a model for a subgoal into a model for the original goal.
+    */
+    std::cout << "tactic example 7\n";
+    context c;
+    tactic t = 
+        tactic(c, "simplify") &
+        tactic(c, "normalize-bounds") &
+        tactic(c, "solve-eqs");
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    expr z = c.int_const("z");
+    goal g(c);
+    g.add(x > 10);
+    g.add(y == x + 3);
+    g.add(z > y);
+    apply_result r = t(g);
+    // r contains only one subgoal
+    std::cout << r << "\n";
+    solver s(c);
+    goal subgoal = r[0];
+    for (unsigned i = 0; i < subgoal.size(); i++) {
+        s.add(subgoal[i]);
+    }
+    std::cout << s.check() << "\n";
+    model m = s.get_model();
+    std::cout << "model for subgoal:\n" << m << "\n";
+    std::cout << "model for original goal:\n" << subgoal.convert_model(m) << "\n";
+}
+
+void tactic_example8() {
+    /*
+      Probes (aka formula measures) are evaluated over goals. 
+      Boolean expressions over them can be built using relational operators and Boolean connectives. 
+      The tactic fail_if(cond) fails if the given goal does not satisfy the condition cond.
+      Many numeric and Boolean measures are available in Z3.
+
+      In this example, we build a simple tactic using fail_if. 
+      It also shows that a probe can be applied directly to a goal.
+    */
+    std::cout << "tactic example 8\n";
+    context c;
+
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    expr z = c.int_const("z");
+    
+    goal g(c);
+    g.add(x + y + z > 0);
+    
+    probe p(c, "num-consts");
+    std::cout << "num-consts: " << p(g) << "\n";
+    
+    tactic t = fail_if(p > 2);
+    try {
+        t(g);
+    }
+    catch (exception&) {
+        std::cout << "tactic failed...\n";
+    }
+    std::cout << "trying again...\n";
+    g.reset();
+    g.add(x + y > 0);
+    std::cout << t(g) << "\n";
+}
+
+void tactic_example9() {
+    /*
+      The combinator (tactical) cond(p, t1, t2) is a shorthand for:
+      
+      (fail_if(p) & t1) | t2
+
+      The combinator when(p, t) is a shorthand for:
+
+      cond(p, t, tactic(c, "skip"))
+      
+      The tactic skip just returns the input goal. 
+      This example demonstrates how to use the cond combinator.
+    */
+    std::cout << "tactic example 9\n";
+    context c;
+
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    expr z = c.int_const("z");
+
+    goal g(c);
+    g.add(x*x - y*y >= 0);
+
+    probe p(c, "num-consts");
+    tactic t = cond(p > 2, tactic(c, "simplify"), tactic(c, "factor"));
+    std::cout << t(g) << "\n";
+
+    g.reset();
+    g.add(x + x + y + z >= 0);
+    g.add(x*x - y*y >= 0);
+    std::cout << t(g) << "\n";
+}
+
+void tactic_qe() {
+    std::cout << "tactic example using quantifier elimination\n";
+    context c;
+    
+    // Create a solver using "qe" and "smt" tactics
+    solver s = 
+        (tactic(c, "qe") &
+         tactic(c, "smt")).mk_solver();
+    
+    expr a = c.int_const("a");
+    expr b = c.int_const("b");
+    expr x = c.int_const("x");
+    expr f = implies(x <= a, x < b);
+    
+    expr qf = forall(x, f);
+
+    std::cout << qf << "\n";
+    
+    s.add(qf);
+    std::cout << s.check() << "\n";
+    std::cout << s.get_model() << "\n";
+}
+
+void visit(std::vector<bool>& visited, expr const & e) {
+    if (visited.size() <= e.id()) {
+        visited.resize(e.id()+1, false);
+    }
+    if (visited[e.id()]) {
+        return;
+    }
+    visited[e.id()] = true;
+
+    if (e.is_app()) {
+        unsigned num = e.num_args();
+        for (unsigned i = 0; i < num; i++) {
+            visit(visited, e.arg(i));
+        }
+        // do something
+        // Example: print the visited expression
+        func_decl f = e.decl();
+        std::cout << "application of " << f.name() << ": " << e << "\n";
+    }
+    else if (e.is_quantifier()) {
+        visit(visited, e.body());
+        // do something
+    }
+    else { 
+        assert(e.is_var());
+        // do something
+    }
+}
+
+void tst_visit() {
+    std::cout << "visit example\n";
+    context c;
+
+    // only one of the occurrences of x*x is visited 
+    // because they are the same subterms
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    expr z = c.int_const("z");
+    expr f = x*x + x*x - y*y >= 0;
+    std::vector<bool> visited;
+    visit(visited, f);
+}
+
+void tst_numeral() {
+    std::cout << "numeral example\n";
+    context c;
+    expr x = c.real_val("1/3");
+    double d = 0;
+    if (!x.is_numeral(d)) {
+        std::cout << x << " is not recognized as a numeral\n";
+        return;
+    }
+    std::cout << x << " is " << d << "\n";
+}
+
+void incremental_example1() {
+    std::cout << "incremental example1\n";
+    context c;
+    expr x = c.int_const("x");
+    solver s(c);
+    s.add(x > 0);
+    std::cout << s.check() << "\n";
+    // We can add more formulas to the solver
+    s.add(x < 0);
+    // and, invoke s.check() again...
+    std::cout << s.check() << "\n";
+}
+
+void incremental_example2() {
+    // In this example, we show how push() and pop() can be used
+    // to remove formulas added to the solver.
+    std::cout << "incremental example2\n";
+    context c;
+    expr x = c.int_const("x");
+    solver s(c);
+    s.add(x > 0);
+    std::cout << s.check() << "\n";
+    // push() creates a backtracking point (aka a snapshot).
+    s.push();
+    // We can add more formulas to the solver
+    s.add(x < 0);
+    // and, invoke s.check() again...
+    std::cout << s.check() << "\n";
+    // pop() will remove all formulas added between this pop() and the matching push()
+    s.pop();
+    // The context is satisfiable again
+    std::cout << s.check() << "\n";
+    // and contains only x > 0
+    std::cout << s << "\n";
+}
+
+void incremental_example3() {
+    // In this example, we show how to use assumptions to "remove" 
+    // formulas added to a solver. Actually, we disable them.
+    std::cout << "incremental example3\n";
+    context c;
+    expr x = c.int_const("x");
+    solver s(c);
+    s.add(x > 0);
+    std::cout << s.check() << "\n";
+    // Now, suppose we want to add x < 0 to the solver, but we also want
+    // to be able to disable it later.
+    // To do that, we create an auxiliary Boolean variable
+    expr b = c.bool_const("b");
+    // and, assert (b implies x < 0)
+    s.add(implies(b, x < 0));
+    // Now, we check whether s is satisfiable under the assumption "b" is true.
+    expr_vector a1(c);
+    a1.push_back(b);
+    std::cout << s.check(a1) << "\n";
+    // To "disable" (x > 0), we may just ask with the assumption "not b" or not provide any assumption.
+    std::cout << s.check() << "\n";
+    expr_vector a2(c);
+    a2.push_back(!b);
+    std::cout << s.check(a2) << "\n";
+}
+
+void enum_sort_example() {
+    std::cout << "enumeration sort example\n";
+    context ctx;
+    const char * enum_names[] = { "a", "b", "c" };
+    func_decl_vector enum_consts(ctx);
+    func_decl_vector enum_testers(ctx);
+    sort s = ctx.enumeration_sort("enumT", 3, enum_names, enum_consts, enum_testers);
+    // enum_consts[0] is a func_decl of arity 0.
+    // we convert it to an expression using the operator()
+    expr a = enum_consts[0u]();
+    expr b = enum_consts[1u]();
+    expr x = ctx.constant("x", s);
+    expr test = (x==a) && (x==b);
+    std::cout << "1: " << test << std::endl;
+    tactic qe(ctx, "ctx-solver-simplify");
+    goal g(ctx);
+    g.add(test);
+    expr res(ctx);
+    apply_result result_of_elimination = qe.apply(g);
+    goal result_goal = result_of_elimination[0];
+    std::cout << "2: " << result_goal.as_expr() << std::endl;
+}
+
+void tuple_example() {
+    std::cout << "tuple example\n";
+    context ctx;
+    const char * names[] = { "first", "second" };
+    sort sorts[2] = { ctx.int_sort(), ctx.bool_sort() };
+    func_decl_vector projs(ctx);
+    func_decl pair = ctx.tuple_sort("pair", 2, names, sorts, projs);
+    sorts[1] = pair.range();
+    func_decl pair2 = ctx.tuple_sort("pair2", 2, names, sorts, projs);
+    
+    std::cout << pair2 << "\n";
+}
+
+void datatype_example() {
+    std::cout << "datatype example\n";
+    context ctx;
+    constructors cs(ctx);
+    symbol ilist = ctx.str_symbol("ilist");
+    symbol accs[2] = { ctx.str_symbol("hd"), ctx.str_symbol("tl") };
+    sort sorts[2] = { ctx.int_sort(), ctx.datatype_sort(ilist) };
+    cs.add(ctx.str_symbol("nil"), ctx.str_symbol("is-nil"), 0, nullptr, nullptr);
+    cs.add(ctx.str_symbol("cons"), ctx.str_symbol("is-cons"), 2, accs, sorts);
+    sort ls = ctx.datatype(ilist, cs);
+    std::cout << ls << "\n";
+    func_decl nil(ctx), is_nil(ctx);
+    func_decl_vector nil_acc(ctx);
+    cs.query(0, nil, is_nil, nil_acc);
+    func_decl cons(ctx), is_cons(ctx);
+    func_decl_vector cons_acc(ctx);
+    cs.query(1, cons, is_cons, cons_acc);
+    std::cout << nil << " " << is_nil << " " << nil_acc << "\n";
+    std::cout << cons << " " << is_cons << " " << cons_acc << "\n";
+
+    symbol tree = ctx.str_symbol("tree");
+    symbol tlist = ctx.str_symbol("tree_list");
+    symbol accs1[2] = { ctx.str_symbol("left"), ctx.str_symbol("right") };
+    symbol accs2[2] = { ctx.str_symbol("hd"), ctx.str_symbol("tail") };
+    sort sorts1[2] = { ctx.datatype_sort(tlist), ctx.datatype_sort(tlist) };
+    sort sorts2[2] = { ctx.int_sort(), ctx.datatype_sort(tree) };
+    constructors cs1(ctx), cs2(ctx);
+    cs1.add(ctx.str_symbol("tnil"), ctx.str_symbol("is-tnil"), 0, nullptr, nullptr);
+    cs1.add(ctx.str_symbol("tnode"), ctx.str_symbol("is-tnode"), 2, accs1, sorts1);
+    constructor_list cl1(cs1);
+    cs2.add(ctx.str_symbol("lnil"), ctx.str_symbol("is-lnil"), 0, nullptr, nullptr);
+    cs2.add(ctx.str_symbol("lcons"), ctx.str_symbol("is-lcons"), 2, accs2, sorts2);
+    constructor_list cl2(cs2);
+    symbol names[2] = { tree, tlist };
+    constructor_list* cl[2] = { &cl1, &cl2 };
+    sort_vector dsorts = ctx.datatypes(2, names, cl);
+    std::cout << dsorts << "\n";
+    cs1.query(0, nil, is_nil, nil_acc);
+    cs1.query(1, cons, is_cons, cons_acc);
+    std::cout << nil << " " << is_nil << " " << nil_acc << "\n";
+    std::cout << cons << " " << is_cons << " " << cons_acc << "\n";
+
+    cs2.query(0, nil, is_nil, nil_acc);
+    cs2.query(1, cons, is_cons, cons_acc);
+    std::cout << nil << " " << is_nil << " " << nil_acc << "\n";
+    std::cout << cons << " " << is_cons << " " << cons_acc << "\n";
+
+}
+
+void expr_vector_example() {
+    std::cout << "expr_vector example\n";
+    context c;
+    const unsigned N = 10;
+
+    expr_vector x(c);
+
+    for (unsigned i = 0; i < N; i++) { 
+        std::stringstream x_name; 
+        x_name << "x_" << i;
+        x.push_back(c.int_const(x_name.str().c_str()));
+    }
+    
+    solver s(c);
+    for (unsigned i = 0; i < N; i++) {
+        s.add(x[i] >= 1);
+    }
+
+    std::cout << s << "\n" << "solving...\n" << s.check() << "\n";
+    model m = s.get_model();
+    std::cout << "solution\n" << m;
+}
+
+void exists_expr_vector_example() {
+    std::cout << "exists expr_vector example\n";
+    context c;
+    const unsigned N = 10;
+
+    expr_vector xs(c);
+    expr x(c);
+    expr b(c);
+    b = c.bool_val(true); 
+
+    for (unsigned i = 0; i < N; i++) { 
+        std::stringstream x_name; 
+        x_name << "x_" << i;
+        x = c.int_const(x_name.str().c_str());
+        xs.push_back(x);
+        b = b && x >= 0;
+    }
+
+    expr ex(c);
+    ex = exists(xs, b);
+    std::cout << ex << std::endl;
+}
+
+void substitute_example() {
+    std::cout << "substitute example\n";
+    context c;
+    expr x(c);
+    x = c.int_const("x");
+    expr f(c);
+    f = (x == 2) || (x == 1);
+    std::cout << f << std::endl;
+
+    expr two(c), three(c);
+    two   = c.int_val(2);
+    three = c.int_val(3);
+    Z3_ast from[] = { two };
+    Z3_ast to[]   = { three };
+    expr new_f(c);
+    new_f = to_expr(c, Z3_substitute(c, f, 1, from, to));
+    
+    std::cout << new_f << std::endl;
+}
+
+void opt_example() {
+    context c;
+    optimize opt(c);
+    params p(c);
+    p.set("priority",c.str_symbol("pareto"));
+    opt.set(p);
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    opt.add(10 >= x && x >= 0);
+    opt.add(10 >= y && y >= 0);
+    opt.add(x + y <= 11);
+    optimize::handle h1 = opt.maximize(x);
+    optimize::handle h2 = opt.maximize(y);
+    while (true) {
+        if (sat == opt.check()) {
+            std::cout << x << ": " << opt.lower(h1) << " " << y << ": " << opt.lower(h2) << "\n";
+        }
+        else {
+            break;
+        }
+    }
+}
+
+/**
+ * translate from one optimization context to another.
+ */
+void opt_translate_example() {
+    context c1, c2;
+    optimize o1(c1);
+    expr x = c1.int_const("x");
+    expr y = c1.int_const("y");
+    o1.add(10 >= x && x >= 0);
+    o1.add(10 >= y && y >= 0);
+    o1.add(x + y <= 11);
+    optimize::handle h1 = o1.maximize(x);
+    optimize::handle h2 = o1.maximize(y);
+    (void)h1;
+    (void)h2;
+    optimize o2(c2, o1);
+    expr z = c2.int_const("z");
+    expr x2 = c2.int_const("x");
+    o2.add(x2 + z == 2);
+    o2.minimize(z);
+    std::cout << o2 << "\n";
+}
+
+void extract_example() {
+    std::cout << "extract example\n";
+    context c;
+    expr x(c);
+    x = c.constant("x", c.bv_sort(32));
+    expr y = x.extract(21, 10);
+    std::cout << y << " " << y.hi() << " " << y.lo() << "\n";
+}
+
+void sudoku_example() {
+    std::cout << "sudoku example\n";
+
+    context c;
+
+    // 9x9 matrix of integer variables 
+    expr_vector x(c);
+    for (unsigned i = 0; i < 9; ++i)
+        for (unsigned j = 0; j < 9; ++j) {
+            std::stringstream x_name;
+
+            x_name << "x_" << i << '_' << j;
+            x.push_back(c.int_const(x_name.str().c_str()));
+        }
+
+    solver s(c);
+
+    // each cell contains a value in {1, ..., 9}
+    for (unsigned i = 0; i < 9; ++i)
+        for (unsigned j = 0; j < 9; ++j) {
+            s.add(x[i * 9 + j] >= 1 && x[i * 9 + j] <= 9);
+        }
+
+    // each row contains a digit at most once
+    for (unsigned i = 0; i < 9; ++i) {
+        expr_vector t(c);
+        for (unsigned j = 0; j < 9; ++j)
+            t.push_back(x[i * 9 + j]);
+        s.add(distinct(t));
+    }
+
+    // each column contains a digit at most once
+    for (unsigned j = 0; j < 9; ++j) {
+        expr_vector t(c);
+        for (unsigned i = 0; i < 9; ++i)
+            t.push_back(x[i * 9 + j]);
+        s.add(distinct(t));
+    }
+
+    // each 3x3 square contains a digit at most once
+    for (unsigned i0 = 0; i0 < 3; i0++) {
+        for (unsigned j0 = 0; j0 < 3; j0++) {
+            expr_vector t(c);
+            for (unsigned i = 0; i < 3; i++)
+                for (unsigned j = 0; j < 3; j++)
+                    t.push_back(x[(i0 * 3 + i) * 9 + j0 * 3 + j]);
+            s.add(distinct(t));
+        }
+    }
+
+    // sudoku instance, we use '0' for empty cells
+    int instance[9][9] = {{0,0,0,0,9,4,0,3,0},
+                          {0,0,0,5,1,0,0,0,7},
+                          {0,8,9,0,0,0,0,4,0},
+                          {0,0,0,0,0,0,2,0,8},
+                          {0,6,0,2,0,1,0,5,0},
+                          {1,0,2,0,0,0,0,0,0},
+                          {0,7,0,0,0,0,5,2,0},
+                          {9,0,0,0,6,5,0,0,0},
+                          {0,4,0,9,7,0,0,0,0}};
+
+    for (unsigned i = 0; i < 9; i++)
+        for (unsigned j = 0; j < 9; j++)
+            if (instance[i][j] != 0)
+                s.add(x[i * 9 + j] == instance[i][j]);
+
+    std::cout << s.check() << std::endl;
+    std::cout << s << std::endl;
+
+    model m = s.get_model();
+    for (unsigned i = 0; i < 9; ++i) {
+        for (unsigned j = 0; j < 9; ++j)
+            std::cout << m.eval(x[i * 9 + j]);
+        std::cout << '\n';
+    }
+}
+
+void param_descrs_example() {
+    std::cout << "parameter description example\n";
+    context c;
+    param_descrs p = param_descrs::simplify_param_descrs(c);
+    std::cout << p << "\n";
+    unsigned sz = p.size();
+    for (unsigned i = 0; i < sz; ++i) {
+        symbol nm = p.name(i);
+        char const* kind = "other";
+        Z3_param_kind k = p.kind(nm);
+        if (k == Z3_PK_UINT) kind = "uint";
+        if (k == Z3_PK_BOOL) kind = "bool";
+        std::cout << nm << ": " << p.documentation(nm) << " kind: " << kind << "\n";
+    }
+}
+
+void consequence_example() {
+    std::cout << "consequence example\n";
+    context c;
+    expr A = c.bool_const("a");
+    expr B = c.bool_const("b");
+    expr C = c.bool_const("c");
+    solver s(c);
+    s.add(implies(A, B));
+    s.add(implies(B, C));
+    expr_vector assumptions(c), vars(c), consequences(c);
+    assumptions.push_back(!C);
+    vars.push_back(A);
+    vars.push_back(B);
+    vars.push_back(C);
+    std::cout << s.consequences(assumptions, vars, consequences) << "\n";
+    std::cout << consequences << "\n";
+}
+
+static void parse_example() {
+    std::cout << "parse example\n";
+    context c;
+    sort_vector sorts(c);
+    func_decl_vector decls(c);
+    sort B = c.bool_sort();
+    decls.push_back(c.function("a", 0, 0, B));
+    expr_vector a = c.parse_string("(assert a)", sorts, decls);
+    std::cout << a << "\n";
+
+    // expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))");
+}
+
+static void parse_string() {
+    std::cout << "parse string\n";
+    z3::context c;
+    z3::solver s(c);
+    s.from_string("(declare-const x Int)(assert (> x 10))");
+    std::cout << s.check() << "\n";
+}
+
+void mk_model_example() {
+    context c;
+
+    // construct empty model
+    model m(c);
+
+    // create constants "a", "b" and get their func_decl
+    expr a = c.int_const("a");
+    expr b = c.int_const("b");
+    func_decl a_decl = a.decl();
+    func_decl b_decl = b.decl();
+
+    // create numerals to be used in model
+    expr zero_numeral = c.int_val(0);
+    expr one_numeral = c.int_val(1);
+
+    // add assignment to model
+    m.add_const_interp(a_decl, zero_numeral);
+    m.add_const_interp(b_decl, one_numeral);
+
+    // evaluate a + b < 2 in the model
+    std::cout << m.eval(a + b < 2)<< std::endl;
+}
+
+void recfun_example() {
+    std::cout << "recfun example\n";
+    context c;    
+    expr x = c.int_const("x");
+    expr y = c.int_const("y");
+    expr b = c.bool_const("b");
+    sort I = c.int_sort();
+    sort B = c.bool_sort();    
+    func_decl f = recfun("f", I, B, I);
+    expr_vector args(c);
+    args.push_back(x); args.push_back(b);
+    c.recdef(f, args, ite(b, x, f(x + 1, !b)));
+    prove(f(x,c.bool_val(false)) > x);
+}
+
+static void string_values() {
+    context c;
+    std::cout << "string_values\n";
+    expr s = c.string_val("abc\n\n\0\0", 7);
+    std::cout << s << "\n";
+    std::string s1 = s.get_string();
+    std::cout << s1 << "\n";
+    std::u32string buffer = s.get_u32string();
+    for (unsigned ch : buffer)
+        std::cout << "char: " << ch << "\n";
+}
+
+expr MakeStringConstant(context* context, std::string value) {
+    return context->string_val(value.c_str());
+}
+
+expr MakeStringFunction(context* c, std::string s) {
+    sort sort = c->string_sort();
+    symbol name = c->str_symbol(s.c_str());
+    return c->constant(name, sort);
+}
+
+static void string_issue_2298() {
+    context c;
+    solver s(c);
+    s.push();
+    expr func1 = MakeStringFunction(&c, "func1");
+    expr func2 = MakeStringFunction(&c, "func2");
+    
+    expr abc = MakeStringConstant(&c, "abc");
+    expr cde = MakeStringConstant(&c, "cde");
+    
+    expr length = func1.length();
+    expr five = c.int_val(5);
+    
+    s.add(func2 == abc || func1 == cde);
+    s.add(func2 == abc || func2 == cde);
+    s.add(length <= five);
+    
+    s.check();
+    s.pop();
+}
+
+void iterate_args() {
+    std::cout << "iterate arguments\n";
+    context c;
+    expr x      = c.int_const("x");
+    expr y      = c.int_const("y");
+    sort I      = c.int_sort();
+    func_decl g = function("g", I, I, I);
+    expr e = g(x, y);
+    std::cout << "expression " << e << "\n";
+    for (expr arg : e)
+        std::cout << "arg " << arg << "\n";
+
+}
+
+int main() {
+
+    try {
+//        demorgan(); std::cout << "\n";
+        find_model_example1(); std::cout << "\n";
+/*        prove_example1(); std::cout << "\n";
+        prove_example2(); std::cout << "\n";
+        nonlinear_example1(); std::cout << "\n";
+        bitvector_example1(); std::cout << "\n";
+        bitvector_example2(); std::cout << "\n";
+        capi_example(); std::cout << "\n";
+        eval_example1(); std::cout << "\n";
+        two_contexts_example1(); std::cout << "\n";
+        error_example(); std::cout << "\n";
+        numeral_example(); std::cout << "\n";
+        ite_example(); std::cout << "\n";
+        ite_example2(); std::cout << "\n";
+        quantifier_example(); std::cout << "\n";
+        unsat_core_example1(); std::cout << "\n";
+        unsat_core_example2(); std::cout << "\n";
+        unsat_core_example3(); std::cout << "\n";
+        tactic_example1(); std::cout << "\n";
+        tactic_example2(); std::cout << "\n";
+        tactic_example3(); std::cout << "\n";
+        tactic_example4(); std::cout << "\n";
+        tactic_example5(); std::cout << "\n";
+        tactic_example6(); std::cout << "\n";
+        tactic_example7(); std::cout << "\n";
+        tactic_example8(); std::cout << "\n";
+        tactic_example9(); std::cout << "\n";
+        tactic_qe(); std::cout << "\n";
+        tst_visit(); std::cout << "\n";
+        tst_numeral(); std::cout << "\n";
+        incremental_example1(); std::cout << "\n";
+        incremental_example2(); std::cout << "\n";
+        incremental_example3(); std::cout << "\n";
+        enum_sort_example(); std::cout << "\n";
+        tuple_example(); std::cout << "\n";
+        datatype_example(); std::cout << "\n";
+        expr_vector_example(); std::cout << "\n";
+        exists_expr_vector_example(); std::cout << "\n";
+        substitute_example(); std::cout << "\n";
+        opt_example(); std::cout << "\n";
+        opt_translate_example(); std::cout << "\n";
+        extract_example(); std::cout << "\n";
+        param_descrs_example(); std::cout << "\n";
+        sudoku_example(); std::cout << "\n";
+        consequence_example(); std::cout << "\n";
+        parse_example(); std::cout << "\n";
+        parse_string(); std::cout << "\n";
+        mk_model_example(); std::cout << "\n";
+        recfun_example(); std::cout << "\n";
+        string_values(); std::cout << "\n";
+        string_issue_2298(); std::cout << "\n";
+	iterate_args(); std::cout << "\n";
+*/
+        std::cout << "done\n";
+    }
+    catch (exception & ex) {
+        std::cout << "unexpected error: " << ex << "\n";
+    }
+    Z3_finalize_memory();
+    return 0;
+}
diff --git a/class_21_05102023/expr_vector.cpp b/class_21_05102023/expr_vector.cpp
new file mode 100644
index 0000000..7a28382
--- /dev/null
+++ b/class_21_05102023/expr_vector.cpp
@@ -0,0 +1,47 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+--*/
+
+#include <iostream>
+#include <sstream>
+#include<vector>
+#include"z3++.h"
+
+using namespace z3;
+ 
+ 
+ 
+void expr_vector_example() {
+    std::cout << "expr_vector example\n";
+    context c;
+    const unsigned N = 10;
+
+    expr_vector x(c);
+
+    for (unsigned i = 0; i < N; i++) { 
+        std::stringstream x_name; 
+        x_name << "x_" << i;
+        x.push_back(c.int_const(x_name.str().c_str()));
+    }
+    
+    solver s(c);
+    for (unsigned i = 0; i < N; i++) {
+        s.add(x[i] >= 1);
+    }
+
+    std::cout << s << "\n" << "solving...\n" << s.check() << "\n";
+    model m = s.get_model();
+    std::cout << "solution\n" << m;
+}
+
+int main() {
+
+    try {
+        expr_vector_example(); std::cout << "\n";
+        std::cout << "done\n";
+    }
+    catch (exception & ex) {
+        std::cout << "unexpected error: " << ex << "\n";
+    }
+    return 0;
+}
diff --git a/class_21_05102023/getmodel.cpp b/class_21_05102023/getmodel.cpp
new file mode 100644
index 0000000..8d244de
--- /dev/null
+++ b/class_21_05102023/getmodel.cpp
@@ -0,0 +1,45 @@
+#include <iostream>
+#include <sstream>
+#include<vector>
+#include"z3++.h"
+
+using namespace z3;
+
+
+/**
+find values of expressions that satisfy the following ineaualities 
+x >= 1 
+y < x +3 
+*/
+ 
+int main(){
+context c; 
+expr  x  = c.int_const("x"); 
+expr  y  = c.int_const("y"); 
+//create a solver 
+solver s(c); 
+//adding the constraints
+s.add(x >=1); 
+s.add(y < x+3); 
+
+std::cout << s.check() << "\n\n";
+
+model m = s.get_model(); 
+std::cout << m << "\n";
+
+//traversing the model 
+std::cout << "traversing the model" << "\n";
+for (unsigned i =0; i < m.size(); i++){
+	func_decl v = m[i];
+	assert(v.arity() ==0);
+	std::cout << v.name()<<"="<<m.get_const_interp(v) << "\n";
+}
+ 
+// evaluating the expressions in the model.
+std::cout << "evaluating the expressions in the model" << "\n";
+std::cout << "x+y+1= "<< m.eval(x+y+1)<<"\n";
+
+return 0;  
+} //end of function 
+
+
diff --git a/class_22_09102923/summary.txt b/class_22_09102923/summary.txt
new file mode 100644
index 0000000..f3978c2
--- /dev/null
+++ b/class_22_09102923/summary.txt
@@ -0,0 +1,14 @@
+Introduction to FOL
+
+-- socrates example.
+   Why do we need FOL to deduct that Socrates is mortal. 
+-- Predicates are relating the objects and properties. 
+-- Signature of FOL (constants, functions, relations). 
+-- we need variables, logical symbols and non-logical symbols, 
+   also to define wffs. 
+
+
+-- Example of Number Theory and some formulas 
+-- Example of set theory and some examples
+-- Example of min FOL (with only =). 
+
diff --git a/class_23_10102923/summary.txt b/class_23_10102923/summary.txt
new file mode 100644
index 0000000..6432373
--- /dev/null
+++ b/class_23_10102923/summary.txt
@@ -0,0 +1,10 @@
+-- Syntax of FOL 
+-- step (1) terms : constant, variabls, or succussive applications to functions. 
+   -- examples of terms in number theory, set theory, min FOL 
+
+-- step (2) atomic formulas : Relations over terms, = exists unless
+specified.  
+   -- examples of atomic formulas in number theory, set theory, min FOL 
+-- step (3) wffs : atomic formulas, or formulas constructed from
+smaller formulas using negation, implication, \forall, \exists. 
+
diff --git a/class_24_12102023/summary.txt b/class_24_12102023/summary.txt
new file mode 100644
index 0000000..bc16af0
--- /dev/null
+++ b/class_24_12102023/summary.txt
@@ -0,0 +1,10 @@
+Revision of syntax of FOL. 
+Semantics of FOL
+Structure.
+Example of  structure of natural numbers
+EXamples of formulas from number theory 
+
+Assignment functions S: Variables --> \universe
+
+Extenstion of S to give meaning to terms, atomic formulas and wffs. 
+