Skip to content

UltimateEliminator

Jump to bottom
Max barth edited this page Nov 7, 2019 · 11 revisions

The Idea of this project ist to combine the quantifier elimination of Ultimate with the SMTInterpol.

Links:

Files:

  • UltimateEliminator
  • QuantifierOverapproximatingSolver
  • SmtParser
  • UltimateEliminatorSmtcomp2019

Acitivate Ultimate Eliminator:

Change "boolean inUltimateEliminatorMode = false;" in SmtParser to "true". TODO: Use the Preference Page of the SmtParser Plugin.

Benchmark Tests:

Run UltimateEliminatorSmtcomp2019 as "JUnit Plug-in Test". This will run UltiamteEliminator on SMT-Comp 2019 Benchmarks. The Benchmarks used in UltimateEliminatorSmtcomp2019 need to be in the Folder "examples/local/2019smtcomp/". The result is written in a new File in this Folder: "ultimate/surefirereports/de.uni_freiburg.informatik.ultimate.ultimatetest.suites.traceabstraction.UltimateEliminatorSmtcomp2019/"

Ultimate Eliminator Problem:

The quantifierelimination itself could use SMT-Solver. We have to make sure the quantifierelimination can only assert quantifier free Terms.

Solution 1:

Ignore the assertion if the term is quantified.

Solution 2:

If the formula is not quantifier free, we overaproximate the asserted Term. This means we try to find a formula F' for a formula F so that the implikation F ==> F' applies. F and F' are not equivalent, therefor if check-sat returns "sat" we have to return "unknown" instead.

Overapproximation

  1. Quantifier Pusher, replace qunatified subterms with "true".
  2. Simple Skolemization: If the first quantifier block is exist quantified, we replace the quantified variables with constants.

Optimizations:

  • Try SMT-Solver before quantifier elimination.
  • assert all quantifier free formulas first.

Improvements for linear integer arithmetic (LIA)

  • Throughout this section a,b,c are non-zero constants, d is some constant and x,y,z are variables.
  • The term a*x=b*y+c*z+d can be represented by the AffineRelation class.
  • In order to simplify our notation we will sometimes use / for integer division and % for integer modulo, although the SMT-LIB notation is div and mod and in SMT-LIB / is the division for reals.

1. Ideas that are already implemented

  1. If our terms have sort Real then a*x=b*y+c*z+d is equivalent to x=(b/a)*y+(c/a)*z+(d/a).

  2. The same holds for versions of this relation where the relation symbol is not = but <, <=, >, =>, or !=.

  3. If our terms have sort Int then a*x=b*y+c*z+d is in gerneral not equivalent to x=(b/a)*y+(c/a)*z+(d/a). (make yourself an example?)

  4. If our terms have sort Int then a*x=b*y+c*z+d is equivalent to x=(b/a)*y+(c/a)*z+(d/a) if b,c,d are divisible by a (i.e., b mod a = 0, c mod a = 0 and d mod a = 0.

  5. For terms t1,t2, the formula ∃x. t1<=x /\ x<=t2 is equivalent to t1<=t2. A general version of this is called transitive inequality resolution TIR and implemented in the class XnfTir. (The general version supports several conjuncts, strict inequalities, disequalities and there is a dual version for universal quantification.)

2. Ideas that were implemented after SMT-Comp 2019

Integer Division:

  1. If our terms have sort Int then a*x=b*y+c*z+d is equivalent to (x=(b*y+c*z+d) div a) /\ ((b*y+c*z+d) mod a = 0).
  2. If our terms have sort Int then a*x<=b*y+c*z+d is equivalent to x<=(b*y+c*z+d) div a (without any additional modulo constraint!).
  3. The same holds the strict inequality relation <.
  4. If our terms have sort Int then a*x>=b*y+c*z+d is equivalent to x>=(b*y+c*z+d) div a /\ (b*y+c*z+d) mod a = 0 \/ x>=((b*y+c*z+d) div a) + 1
  5. The same holds the strict inequality relation >.

Using Integer Division in XnfTir Quantifier Elimination

Solve Mod Subterms of form y = (x mod d) for x(Subject)

3. Ideas that need to be implemented

  1. Solve Div Subterms of form y = (x div d) for x(Subject)
  2. Solve Nestings of Mod and/or Div Subterms
  3. Use solve Mod/Div Subterms for a subject in the quantifier Elimination (DER) if the subject is a quantified variable
Clone this wiki locally