How to perform constraint solving with mixed data types?

Question

I'm working on source-to-source transformer for Java 6^*1).

I need to maintain negative information as well as positive information, so I have to implement the small constraint system for the transformer. The constraint system is the restricted kind of CNF formula that can be defined as the following:

(v1 == c1 /\ v2 == c2 ... vn == cn) /\ ((w1,1 != d1,1 \/ w1,2 !== d1,2 ... w1,k != d1,k) /\ (w2,1 != d2,1 \/ ...) /\ ... (wm,1 != dm,1 \/ ... \/ wm,k != dm,k))

where vi == ci are equality constraints (substitutions, variable assignments),

wj != dj,l are disequality constraints,

vi, wj,l are variables,

ci, dj,l are constants (literals).

Constant types are Java primitive types and reference types mapped to integers. Constants are also arbitrary AST-like structures (which represent partially evaluated expressions and possibly contain (meta)-variables).

Constraint system works as the following:

When the transformer reaches a conditional (e.g. if(x == c) then b else b1) the constraint x == c is added to the constraint system of then branch and the constraint x != c, in turn, is added to the constraint system (formula) of else branch.

So, new formula of then branch is: x == c /\ formula (positive part of the formula is the conjunction of equalities);

new formula of else branch is: x != c \/ formula (negative part of the formula is the conjunction of disjunctions of disequalities).

Edit: Satisfiability of the constraint system.

For the constraint system to be satisfiable it must be possible to assign values to the variables in the system such that constraints are satisfied.

The constraint system is thus satisfied iff there exists a substituition Theta such that, for each equation v = c Thetav will be syntactically identical to Thetac, and likewise, for each disequation w != d Thetaw will be syntactically different from Thetad.

Unfortunately, I'm pretty new to constraint programming and I came across the problems.

1. It is not entirely clear for me how to map AST constants to integers in this case. Should I simply use the index of the constants' array or some hash function?

2. It is not clear how to handle long type. Rewrite int-based solver making it long-based or use floating-point solver?

3. It is also not clear how to handle combined integer and floating-point data. As I realize the straightforward solution is using floating point solver for both integer and floating point constraints. Is it true? Or I can solve floating-point and integer part of constraints separately?

Please, could someone help me? Some directions, hints ...

¹⁾ Currently, source=8 / target=8 scheme is accepted.

Psychological

Answer 1

It would be good if you would also post your final goal (what does a solved constraint actually mean).

However, it seems to me that you want to know the set of possible values for each variable at a given statement. In that case you will need an interval constraint solver

The distinction between integer and rational intervals depends on your use case and the solver you choose, but in general it is possible to handle integers as floating points (which might result in non-integer solutions of your constraint).

It is important to keep in mind that you will not be able to prove equality of arbitrary AST fragments. Hence, you either need to reduce the expressiveness of said fragments (e.g. polynomials over your variables of a given order) or approximate equality (e.g. referencing the same (i.e. same context, same syntax, no side-effects) AST fragment. However, it might be best to just translate AST fragments to unbound (or pessimistically bound) intervals.

Womanlike

Thank you for the answer! Unfortunately, I found almost nothing about unbound (or pessimistically bound) intervals..Do you have any links about that? – Psychological

There won't be much literature about that. What I meant is that an unevaluated AST fragment should yield the interval (-∞,∞), or rather (min, max) for whatever your numerical datatype is (eg. Int.MAX). – Womanlike