From 2aab43f95d3c905eeb6def32da6e304f2fa68a14 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 29 Jan 2018 23:37:50 -0600 Subject: [PATCH] comments and doc --- src/smt/DESIGN.md | 11 +++++++++++ src/smt/Equiv_class.mli | 19 +++++++++++++++++++ 2 files changed, 30 insertions(+) diff --git a/src/smt/DESIGN.md b/src/smt/DESIGN.md index 766005a4..0754001e 100644 --- a/src/smt/DESIGN.md +++ b/src/smt/DESIGN.md @@ -135,3 +135,14 @@ It's very important that, in a long chain of reduction `t1 → t2 → … → tn only `tn` is active and the other terms are only there to provide explanations but do not cost any complexity during CC. +## Theories + +- have `x+2y+z` be arith terms +- shostak like canonizer (turns equations into `x := …`) +- use same evaluation mechanism as for evaluation of terms, + for dynamic simplifications (rewriting). + * no preprocessing, everything done dynamically + * theory terms subscribe to their arguments (subterms) to potentially + rewrite themselves if their arguments change + e.g. `x+y+1` subscribes to {x,y} so as to reduce to `y+z+3` when + x:=z+2 happens diff --git a/src/smt/Equiv_class.mli b/src/smt/Equiv_class.mli index cfae55cc..6ec193ad 100644 --- a/src/smt/Equiv_class.mli +++ b/src/smt/Equiv_class.mli @@ -1,6 +1,25 @@ open Solver_types +(** {1 Equivalence Classes} *) + +(** An equivalence class is a set of terms that are currently equal + in the partial model built by the solver. + The class is represented by a collection of nodes, one of which is + distinguished and is called the "representative". + + All information pertaining to the whole equivalence class is stored + in this representative's node. + + When two classes become equal (are "merged"), one of the two + representatives is picked as the representative of the new class. + The new class contains the union of the two old classes' nodes. + + We also allow theories to store additional information in the + representative. This information can be used when two classes are + merged, to detect conflicts and solve equations à la Shostak. +*) + type t = cc_node type repr = private t type payload = cc_node_payload