Question: Relation between quantified expressions and bounded Variables

[jfh1911]

Hey,

i have another question:

I am traversing a quantified expression with JavaSMT and Z3 as solver, like:

(declare-fun $main_inv1 (Int Int Int) Bool)
(assert   
    (forall ((n1 Int) (x2 Int) (y3 Int) ($uint4 Int))
    (and (= y3 0) (= x2 n1) (= n1 $uint4) (<= 0 $uint4) ($main_inv1 n1 x2 y3))
     )
)

Within the method visitQuantifier(BooleanFormula f, Quantifier q, List<Formula> boundVariables, BooleanFormula body) the variables n1 x2 y3 $uint4 are replaced by "fresh" bounded variables :var 0 to :var 3 in the formula body. (which makes sense)

Is it possible to get the body of a quantified expression as it is (so without the replacements)?

I tried this using the fmgr.substitute, but got stuck at another problem:

Is there any way to get a mapping between n1 and :var 0 ?

I tried tu use the deBruijnIdx when traversing a bounded variable, but this does not work, as (as far as i guess) the ordering in which the variables are replaced is not always from left to right. If I remove $uint4 and all assignments, the deBruijn Index changes.

A minimal example showing both cases is attached below:

String smt = "(declare-fun $main_inv1 (Int Int Int) Bool)"
        + "(assert   (forall ((n1 Int) (x2 Int) (y3 Int) ($uint4 Int))"
        + "  (and (= y3 0) (= x2 n1) (= n1 $uint4) (<= 0 $uint4) ($main_inv1 n1 x2 y3))))";

String smt2 = "(declare-fun $main_inv1 (Int Int Int) Bool)" + "(assert   (forall ((n1 Int) (x2 Int) (y3 Int) )"
        + "  (and (= y3 0) (= x2 n1) ($main_inv1 n1 x2 y3))))";

SolverContext context = SolverContextFactory.createSolverContext(Configuration.defaultConfiguration(),
        LogManager.createTestLogManager(), ShutdownNotifier.createDummy(), Solvers.Z3);
FormulaManager fmgr = context.getFormulaManager();

Formula f = fmgr.parse(smt);
Formula f2 = fmgr.parse(smt2);

FormulaVisitor<Formula> visitor = new DefaultFormulaVisitor<>() {

    @Override
    public Formula visitQuantifier(BooleanFormula f, Quantifier q, List<Formula> boundVariables,
            BooleanFormula body) {
        System.out.println(body);
        return body;
    }

    @Override
    protected Formula visitDefault(Formula pF) {
        return null;
    }

};
fmgr.visit(f, visitor);
fmgr.visit(f2, visitor);

(Additional remark: I also created the formulae using the manager, got the same result:

final IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();
IntegerFormula n1 = imgr.makeVariable("n1");
IntegerFormula x2 = imgr.makeVariable("x2");
IntegerFormula y3 = imgr.makeVariable("y3");

BooleanFormula and = fmgr.getBooleanFormulaManager().and(imgr.equal(y3, imgr.makeNumber(0)), imgr.equal(x2, n1),
        fmgr.getUFManager().declareAndCallUF("$main_inv1", FormulaType.BooleanType, n1, x2, y3));
BooleanFormula f3 = fmgr.getQuantifiedFormulaManager().forall(Lists.newArrayList(n1, x2, y3), and);

IntegerFormula u4 = imgr.makeVariable("$uint4");
BooleanFormula and2 = fmgr.getBooleanFormulaManager().and(imgr.equal(y3, imgr.makeNumber(0)),
        imgr.equal(x2, n1), imgr.equal(n1, u4), imgr.lessOrEquals(imgr.makeNumber(0), u4),
        fmgr.getUFManager().declareAndCallUF("$main_inv1", FormulaType.BooleanType, n1, x2, y3));
BooleanFormula f4 = fmgr.getQuantifiedFormulaManager().forall(Lists.newArrayList(n1, x2, y3, u4), and2);
fmgr.visit(f3, visitor);
fmgr.visit(f4, visitor);

[kfriedberger]

We can currently not influence the solver-specific (internal) renaming of symbols in quantified expressions. Thus, having a mapping or reverting the renaming is currently not possible and not supported.

Overall, quantifier support is not available in all solvers, and thus, we try to avoid it in user applications, for example by using SSA-indices (not part of JavaSMT, but in the user application).

For the given case from above, I can not see a direct reason for using quantifiers. Instead of using assert(forall(symbols, query)) you might also use assert(not(query)), i.e. without further quantification. Thinking about it: the negation should also negate the result... Please check this again!

[jfh1911]

Thanks for the answer :-)