### Polshing

parent e1cf28a7
 ... ... @@ -760,13 +760,13 @@ its model $M$ and another call to the \QFBV solver is made to determine whether $M$ is also a~model of $\forall x_1, x_2, \dots, x_n \, (\psi)$. This is achieved by asking the solver whether the formula $\neg \widehat{\psi}$ is satisfiable, where $\widehat{\psi}$ is the formula $\psi$ after substituting values of all variables except for $x_1 \ldots x_n$ and uninterpreted functions replaced by their values in $M$. If $\neg \widehat{\psi}$ is not satisfiable, then the structure $M$ is indeed a model of the formula $\forall x_1, x_2, \dots, x_n\,(\psi)$, therefore the entire formula is satisfiable and $M$ is its model. If $\neg \widehat{\psi}$ is satisfiable, we get values $v_1, \dots, v_n$ such that where $\widehat{\psi}$ is the formula $\psi$ after replacing all uninterpreted functions and all variables except for $x_1 \ldots x_n$ and by their values in $M$. If $\neg \widehat{\psi}$ is not satisfiable, then the structure $M$ is indeed a model of the formula $\forall x_1, x_2, \dots, x_n\,(\psi)$, therefore the entire formula is satisfiable and $M$ is its model. If $\neg \widehat{\psi}$ is satisfiable, we get values $v_1, \dots, v_n$ such that $\neg\widehat{\psi}[v_1, \dots, v_n]$ holds. To rule out $M$ as a model of the input formula, the instance $\psi[v_1, \dots, v_n]$ of the quantified formula is added to the quantifier-free part, i.e.~the ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!