From b405634b1df293f2e6fadd728669ff63bba1adab Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 20 Jun 2017 17:37:03 +0200 Subject: [PATCH] fix typos --- src/mcsat/README.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/mcsat/README.md b/src/mcsat/README.md index 29288155..80ab1a01 100644 --- a/src/mcsat/README.md +++ b/src/mcsat/README.md @@ -6,21 +6,21 @@ McSat theories have different interfaces and requirements than classic SMT theories. The good point of these additional requirements is that it becomes easier to combine theories, since the assignments allow theories to exchange information about -the equality of terms. In a context where there are multple theories, they each have +the equality of terms. In a context where there are multiple theories, they each have to handle the following operations: -- return an assignement value for a given term -- receive a new assignemnt value for a term (the assignemnt may, or not, have been +- return an assignment value for a given term +- receive a new assignment value for a term (the assignment may, or not, have been done by another theory) -- receive a new assertion (i.e an atomic formula asseted to be true by the sat solver) +- receive a new assertion (i.e an atomic formula asserted to be true by the sat solver) With assignments, the reason for a theory returning UNSAT now becomes when -some term has no potential assignemnt value because of past assignemnts +some term has no potential assignment value because of past assignments and assertions, (or in some cases, an assignments decided by a theory A is incompatible with the possible assignments of the same term according to theory B). When returning UNSAT, the theory must, as usual return a conflict clause. -The conflcit clause must be a tautology, and such that every atomic proposition +The conflict clause must be a tautology, and such that every atomic proposition in it must evaluate to false using assignments. @@ -31,9 +31,9 @@ of known equalities (*NOT* computing congruence closure, only the reflexive-tran closure of the equalities), where each class can be tagged with an optional assignment. When receiving a new assertions by the sat, we update the union-find. When the theory is -asked for an assignemnt value for a term, we lookup its class. If it is tagged, we return +asked for an assignment value for a term, we lookup its class. If it is tagged, we return the tagged value. Else, we take an arbitrary representative $x$ of the class and return it. -When a new assignement $t \mapsto v$ is propagated by the sat solver, there are three cases: +When a new assignment $t \mapsto v$ is propagated by the sat solver, there are three cases: - the class of $t$ if not tagged, we then tag it with $t \mapsto v$ and continue - the class of $t$ is already tagged with $\_ mapsto v$, we do nothing