add documentation to initial selection of tactics

doc/mk_tactic_doc.py

@@ -0,0 +1,47 @@
+# Copyright (c) Microsoft Corporation 2015
+"""
+Tactic documentation generator script
+"""
+
+import os
+import re
+
+SCRIPT_DIR = os.path.abspath(os.path.dirname(__file__))
+OUTPUT_DIRECTORY = os.path.join(os.getcwd(), 'api')
+
+def doc_path(path):
+    return os.path.join(SCRIPT_DIR, path)
+
+is_doc = re.compile("Tactic Documentation")
+is_doc_end = re.compile("\-\-\*\/")
+
+def generate_tactic_doc(ous, f, ins):
+    for line in ins:
+        if is_doc_end.search(line):
+            break
+        ous.write(line)
+
+def extract_tactic_doc(ous, f):
+    with open(f) as ins:
+        for line in ins:
+            if is_doc.search(line):
+                generate_tactic_doc(ous, f, ins)
+
+def help(ous):
+    ous.write("---\n")
+    ous.write("title: Tactics Summary\n")
+    ous.write("sidebar_position: 5\n")
+    ous.write("---\n")
+    for root, dirs, files in os.walk(doc_path("../src")):
+        for f in files:
+            if f.endswith("tactic.h"):
+                extract_tactic_doc(ous, os.path.join(root, f))
+
+def mk_dir(d):
+    if not os.path.exists(d):
+        os.makedirs(d)
+
+mk_dir(os.path.join(OUTPUT_DIRECTORY, 'md'))
+
+with open(OUTPUT_DIRECTORY + "/md/tactics-summary.md",'w') as ous:
+    help(ous)

src/ast/simplifiers/solve_context_eqs.cpp

@@ -279,7 +279,7 @@ namespace euf {
             }
             else if (m.is_not(f, f))
                 todo.push_back({ !s, depth, f });
-            else if (!s && 1 == depth % 2) {
+            else if (!s && 1 <= depth) {
                 for (extract_eq* ex : m_solve_eqs.m_extract_plugins) {
                     ex->set_allow_booleans(false);
                     ex->get_eqs(dependent_expr(m, f, df.dep()), eqs);

src/tactic/core/demodulator_tactic.h

@@ -13,44 +13,47 @@ Module Name:
 
     Nikolaj Bjorner (nbjorner) 2022-10-30
 
-Documentation Notes:
+Tactic Documentation:
 
-Name: demodulator
+## Tactic demodulator
 
-Short Description: 
-  extracts equalities from quantifiers and applies them for simplification
+### Short Description:
 
-Long Description:
-  In first-order theorem proving (FOTP), a demodulator is a universally quantified formula of the form:
+Extracts equalities from quantifiers and applies them for simplification
 
-  Forall X1, ..., Xn.  L[X1, ..., Xn] = R[X1, ..., Xn] 
-  Where L[X1, ..., Xn] contains all variables in R[X1, ..., Xn], and 
-  L[X1, ..., Xn] is "bigger" than R[X1, ...,Xn].
+### Long Description
 
-  The idea is to replace something big L[X1, ..., Xn] with something smaller R[X1, ..., Xn].
+In first-order theorem proving (FOTP), a demodulator is a universally quantified formula of the form:
 
-  After selecting the demodulators, we traverse the rest of the formula looking for instances of L[X1, ..., Xn].
-  Whenever we find an instance, we replace it with the associated instance of R[X1, ..., Xn].
+`Forall X1, ..., Xn.  L[X1, ..., Xn] = R[X1, ..., Xn]`
+Where `L[X1, ..., Xn]` contains all variables in `R[X1, ..., Xn]`, and 
+`L[X1, ..., Xn]` is "bigger" than `R[X1, ...,Xn]`.
 
-  For example, suppose we have
+The idea is to replace something big `L[X1, ..., Xn]` with something smaller `R[X1, ..., Xn]`.
 
-  ```
-  Forall x, y.  f(x+y, y) = y
-  and
-  f(g(b) + h(c), h(c)) <= 0
-  ```
+After selecting the demodulators, we traverse the rest of the formula looking for instances of `L[X1, ..., Xn]`.
+Whenever we find an instance, we replace it with the associated instance of `R[X1, ..., Xn]`.
 
-  The term `f(g(b) + h(c), h(c))` is an instance of `f(x+y, y)` if we replace `x <- g(b)` and `y <- h(c)`.
-  So, we can replace it with `y` which is bound to `h(c)` in this example. So, the result of the transformation is:
+For example, suppose we have
 
-  ```
-  Forall x, y.  f(x+y, y) = y
-  and
-  h(c) <= 0
-  ```
+```
+Forall x, y.  f(x+y, y) = y
+and
+f(g(b) + h(c), h(c)) <= 0
+```
 
+The term `f(g(b) + h(c), h(c))` is an instance of `f(x+y, y)` if we replace `x <- g(b)` and `y <- h(c)`.
+So, we can replace it with `y` which is bound to `h(c)` in this example. So, the result of the transformation is:
 
-Usage: 
+```
+Forall x, y.  f(x+y, y) = y
+and
+h(c) <= 0
+```
+
+### Example
+ 
+```
   (declare-sort S 0)
   (declare-sort S1 0)
   (declare-sort S2 0)
@@ -64,17 +67,23 @@ Long Description:
   (assert (forall ((q S) (v S)) (or (= q v) (= f1 (f2 (f3 f5 q) v)) (= (f2 (f3 f5 v) q) f1))))
   (assert (forall ((q S) (x S)) (not (= (f2 (f3 f5 q) x) f1))))
   (apply demodulator)
-   
+```
+
+It generates
+
+```
   (goals
   (goal
     (forall ((q S) (v S)) (= q v))
     (forall ((q S) (x S)) (not (= (f2 (f3 f5 q) x) f1)))
     :precision precise :depth 1)
   )
+```
 
-Supports: unsat cores
+### Notes
 
-Does not support: proofs
+* supports unsat cores
+* does not support fine-grained proofs
 
 --*/
 #pragma once

src/tactic/core/elim_uncnstr2_tactic.h

@@ -13,6 +13,96 @@ Module Name:
 
     Nikolaj Bjorner (nbjorner) 2022-10-30
 
+Tactic Documentation:
+
+## Tactic elim-uncnstr
+
+### Short Description
+
+Eliminate Unconstrained uninterpreted constants
+
+### Long Description
+
+The tactic eliminates uninterpreted constants that occur only once in a goal and such that the immediate context
+where they occur can be replaced by a fresh constant. We call these occurrences invertible.
+It relies on a series of theory specific invertibility transformations.
+In the following assume `x` and `x'` occur in a unique subterm and `y` is a fresh uninterpreted constant.
+
+#### Boolean Connectives
+
+| Original Context | New Term | Updated solution        |
+|------------------|----------|------------------------ |
+`(if c x x')`      | `y`      | `x = x' = y`            |
+`(if x x' e)`      |  `y`     | `x = true, x' = y`      |
+`(if x t x')`      | `y`      | `x = false, x' = y`     |
+`(not x)`          | `y`      | `x = (not y)`           |
+`(and x x')`       | `y`      | `x = y, x' = true`      |
+`(or  x x')`       | `y`      | `x = y, x' = false`     |
+`(= x t)`          | `y`      | `x = (if y t (diff t))` |
+
+where diff is a diagnonalization function available in domains of size `>` 1.
+
+#### Arithmetic
+
+| Original Context | New Term | Updated solution        |
+|------------------|----------|------------------------ |
+`(+ x t)`          | `y`      | `x = y - t`             |
+`(* x x')`         | `y`      | `x = y, x' = 1`         |
+`(* -1 x)`         | `y`      | `x = -y`                | 
+`(<= x t)`         | `y`      | `x = (if y t (+ t 1))`  |
+`(<= t x)`         | `y`      | `x = (if y t (- t 1))`  |
+
+#### Bit-vectors
+
+| Original Context | New Term | Updated solution         |
+|------------------|----------|--------------------------|
+`(bvadd x t)`      | `y`      | `x = y - t`              |
+`(bvmul x x')`     | `y`      | `x = y, x' = 1`          |
+`(bvmul odd x)`    | `y`      | `x = inv(odd)*y`         | 
+`((extract sz-1 0) x)` | `y`  | `x = y`                  |
+`((extract hi lo) x)`  | `y`  | `x = (concat y1 y y2)`   |
+`(udiv x x')`      | `y`      | `x = y, x' = 1`          |
+`(concat x x')`    | `y`      | `x = (extract hi1 lo1 y)` |
+`(bvule x t)`      | `(or y (= t MAX))` | `x = (if y t (bvadd t 1))` |
+`(bvule t x)`      | `(or y (= t MIN))` | `x = (if y t (bvsub t 1))` | 
+`(bvnot x)`        | `y`                | `x = (bvnot y)`            |
+`(bvand x x')`     | `y`                | `x = y, x' = MAX`          |
+
+In addition there are conversions for shift and bit-wise or and signed comparison.
+
+#### Arrays
+
+| Original Context | New Term | Updated solution         |
+|------------------|----------|--------------------------|
+`(select x t)`     | `y`      | `x = (const y)`          |
+`(store x x1 x2)`  | `y`      | `x2 = (select x x1), x = y, x1 = arb` | 
+
+#### Algebraic Datatypes
+
+| Original Context | New Term | Updated solution         |
+|------------------|----------|--------------------------|
+`(head x)`         | `y`      | `x = (cons y arb)`       |
+
+
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-fun p (Int) Bool)    
+(assert (>= (+ y (+ x y)) y))
+(assert (p y))
+(apply elim-uncnstr)
+(assert (p (+ x y)))
+(apply elim-uncnstr)
+```
+
+### Notes
+
+* supports unsat cores
+* does not support fine-grained proofs
+
 --*/
 #pragma once
 

src/tactic/core/solve_eqs_tactic.h

@@ -13,9 +13,60 @@ Module Name:
 
     Nikolaj Bjorner (nbjorner) 2022-10-30
 
+Tactic Documentation:
+
+## Tactic solve-eqs
+
+### Short Description
+
+Solve for variables
+
+### Long Description
+
+The tactic eliminates variables that can be brought into solved form.
+For example, the assertion `x = f(y + z)` can be solved for `x`, replacing `x`
+everywhere by `f(x + y)`. It depends on a set of theory specific equality solvers
+
+* Basic equations
+  * equations between uninterpreted constants and terms. 
+  * equations written as `(if p (= x t) (= x s))` are solved as `(= x (if p t s))`.
+  * asserting `p` or `(not p)` where `p` is uninterpreted, causes `p` to be replaced by `true` (or `false`).
+
+* Arithmetic equations
+  * It solves `x mod k = s` to `x = k * m' + s`, where m'` is a fresh constant. 
+  * It finds variables with unit coefficients in integer linear equations.
+  * It solves for `x * Y = Z$ under the side-condition `Y != 0` as `x = Z/Y`.
+ 
+It also allows solving for uninterpreted constants that only appear in a single disjuction. For example, 
+`(or (= x (+ 5 y)) (= y (+ u z)))` allows solving for `x`. 
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(declare-const u Int)
+(assert (or (and (= x (+ 5 y)) (> u z)) (= y (+ u z))))
+(apply solve-eqs)
+```
+
+It produces the goal
+```
+(goal
+  (or (not (<= u z)) (= y (+ u z)))
+  :precision precise :depth 1)
+```
+where `x` was solved as `(+ 5 y)`.
+
+### Notes
+
+* supports unsat cores
+* does not support fine-grained proofs
+
 --*/
-#pragma once
 
+#pragma once
 #include "util/params.h"
 #include "tactic/tactic.h"
 #include "tactic/dependent_expr_state_tactic.h"