SARL Description and Demo

SARL: The Symbolic Algebra and Reasoning Library is a Java-based library for creating, manipulating, and reasoning about symbolic expressions. The library can be used to support various applications that require symbolic reasoning, such as symbolic execution tools for program analysis, verification, or test case generation.

Some of the features of SARL include:

Symbolic references. There is a "reference type" which includes symbolic values representing concepts such as r1="the i-th element of an array", or "the i-th field of the j-th element of an array of tuples". There is a method dereference that takes a reference value and a symbolic expression of the appropriate type and returns the subexpression specified by the reference. For example, dereference(r1, a) will return "a[i]". Reference types can be used to represent pointer values in a C program. There is also a method assign(r,x,y), which returns the symbolic expression obtained by starting with x and replacing the subexpression specified by r with y. This makes the symbolic execution of C statements like *(p.f)=e easy.

Union types. Given any sequence of types t1,...,tn, you can form the union type t1+...+tn. The domain of this type is the union of the domains of the ti. This can be used to represent a heap. For example, let t1,...,tn be all the types that are ever malloced, and define the "heap type" to be (t1[]+...+tn[])[], i.e., array of union (over i) of (array of ti). Union types can also be used for message queues, which are arrays that can hold various types of elements.

Simplifications. Given a boolean-valued expression (the "context") and another symbolic expression, the simplify method returns a simplified version of the expression under the assumption that the context holds. For example, if context is "x>1" and e is "x>0" then e is simplified to "true". If the context contains a bunch of polynomial equalities, these are treated as linear expressions in the monomials and Gaussian elimination is performed to solve for any/all of those monomials. And so on. This is useful in symbolic execution, where the context is the path condition, and you can run over the whole state simplifying it, getting the state to (as close as possible to) a canonical form. This can help you decide if you have seen the state before and greatly simplifies theorem proving queries.

Herbrand versions of the numeric types. In addition to the (ideal) integer and real types, there are Herbrand integer and Herbrand real types. A numerical operation involving a Herbrand type is treated as an uninterpreted function (and never simplified). Hence in one program you can mix and match: have some Herbrand and some ideal values. The Herbrands are useful, for example, for representing floating point values when you don't want to assume anything about the floating point operations.

Reasoning. SARL can determine the validity (or dually, the satisfiability) of first-order formulas, i.e., symbolic expressions of boolean type. It is similar to an SMT theorem prover, and in fact it uses several SMT theorem provers "under the hood". You can think of SARL as a higher-level interface to these provers. SARL has a number of optimizations designed to minimize the actual calls to the underlying provers. First, many validity queries can be resolved immediately through simplification. For those that can't, SARL uses state-of-the-art context minimization, canonicalization, and caching techniques to reduce the number and complexity of prover calls.

The following demonstrate some of SARL's capabilities. This is a small sample; see the Java API documentation for the full story.

Define some symbolic constants x, y, and z of real type. Let z1=(x+y)^100, z2=(x+y)^99. Print z1, z2, and z1/z2. Notice that the final result is simplified automatically; there is no need for an explicit simplify call: 

static PrintStream out = System.out;
SymbolicUniverse universe = SARL.newStandardUniverse();
SymbolicType realType = universe.realType();
NumericExpression zero = universe.rational(0);
NumericExpression x = (NumericExpression) universe.symbolicConstant(
	universe.stringObject("x"), realType);
NumericExpression y = (NumericExpression) universe.symbolicConstant(
	universe.stringObject("y"), realType);
NumericExpression z = (NumericExpression) universe.symbolicConstant(
	universe.stringObject("z"), realType);

NumericExpression z1 = universe.power(universe.add(x, y), 100);
NumericExpression z2 = universe.power(universe.add(x, y), 99);
out.println("(x+y)^100 = " + z1);
out.println("(x+y)^99 = " + z2);
out.println("(x+y)^100/(x+y)^99 = " + universe.divide(z1, z2));

Output:

(x+y)^100 = x^100+100*((x^99)*y)+4950*((x^98)*(y^2))+161700*((x^97)*(y^3))+3921225*((x^96)*(y^4))+75287520*((x^95)*(y^5))+1192052400*((x^94)*(y^6))+16007560800*((x^93)*(y^7))+186087894300*((x^92)*(y^8))+1902231808400*((x^91)*(y^9))+17310309456440*((x^90)*(y^10))+141629804643600*((x^89)*(y^11))+1050421051106700*((x^88)*(y^12))+7110542499799200*((x^87)*(y^13))+44186942677323600*((x^86)*(y^14))+253338471349988640*((x^85)*(y^15))+1345860629046814650*((x^84)*(y^16))+6650134872937201800*((x^83)*(y^17))+30664510802988208300*((x^82)*(y^18))+132341572939212267400*((x^81)*(y^19))+535983370403809682970*((x^80)*(y^20))+2041841411062132125600*((x^79)*(y^21))+7332066885177656269200*((x^78)*(y^22))+24865270306254660391200*((x^77)*(y^23))+79776075565900368755100*((x^76)*(y^24))+242519269720337121015504*((x^75)*(y^25))+699574816500972464467800*((x^74)*(y^26))+1917353200780443050763600*((x^73)*(y^27))+4998813702034726525205100*((x^72)*(y^28))+12410847811948286545336800*((x^71)*(y^29))+29372339821610944823963760*((x^70)*(y^30))+66324638306863423796047200*((x^69)*(y^31))+143012501349174257560226775*((x^68)*(y^32))+294692427022540894366527900*((x^67)*(y^33))+580717429720889409486981450*((x^66)*(y^34))+1095067153187962886461165020*((x^65)*(y^35))+1977204582144932989443770175*((x^64)*(y^36))+3420029547493938143902737600*((x^63)*(y^37))+5670048986634686922786117600*((x^62)*(y^38))+9013924030034630492634340800*((x^61)*(y^39))+13746234145802811501267369720*((x^60)*(y^40))+20116440213369968050635175200*((x^59)*(y^41))+28258808871162574166368460400*((x^58)*(y^42))+38116532895986727945334202400*((x^57)*(y^43))+49378235797073715747364762200*((x^56)*(y^44))+61448471214136179596720592960*((x^55)*(y^45))+73470998190814997343905056800*((x^54)*(y^46))+84413487283064039501507937600*((x^53)*(y^47))+93206558875049876949581681100*((x^52)*(y^48))+98913082887808032681188722800*((x^51)*(y^49))+100891344545564193334812497256*((x^50)*(y^50))+98913082887808032681188722800*((x^49)*(y^51))+93206558875049876949581681100*((x^48)*(y^52))+84413487283064039501507937600*((x^47)*(y^53))+73470998190814997343905056800*((x^46)*(y^54))+61448471214136179596720592960*((x^45)*(y^55))+49378235797073715747364762200*((x^44)*(y^56))+38116532895986727945334202400*((x^43)*(y^57))+28258808871162574166368460400*((x^42)*(y^58))+20116440213369968050635175200*((x^41)*(y^59))+13746234145802811501267369720*((x^40)*(y^60))+9013924030034630492634340800*((x^39)*(y^61))+5670048986634686922786117600*((x^38)*(y^62))+3420029547493938143902737600*((x^37)*(y^63))+1977204582144932989443770175*((x^36)*(y^64))+1095067153187962886461165020*((x^35)*(y^65))+580717429720889409486981450*((x^34)*(y^66))+294692427022540894366527900*((x^33)*(y^67))+143012501349174257560226775*((x^32)*(y^68))+66324638306863423796047200*((x^31)*(y^69))+29372339821610944823963760*((x^30)*(y^70))+12410847811948286545336800*((x^29)*(y^71))+4998813702034726525205100*((x^28)*(y^72))+1917353200780443050763600*((x^27)*(y^73))+699574816500972464467800*((x^26)*(y^74))+242519269720337121015504*((x^25)*(y^75))+79776075565900368755100*((x^24)*(y^76))+24865270306254660391200*((x^23)*(y^77))+7332066885177656269200*((x^22)*(y^78))+2041841411062132125600*((x^21)*(y^79))+535983370403809682970*((x^20)*(y^80))+132341572939212267400*((x^19)*(y^81))+30664510802988208300*((x^18)*(y^82))+6650134872937201800*((x^17)*(y^83))+1345860629046814650*((x^16)*(y^84))+253338471349988640*((x^15)*(y^85))+44186942677323600*((x^14)*(y^86))+7110542499799200*((x^13)*(y^87))+1050421051106700*((x^12)*(y^88))+141629804643600*((x^11)*(y^89))+17310309456440*((x^10)*(y^90))+1902231808400*((x^9)*(y^91))+186087894300*((x^8)*(y^92))+16007560800*((x^7)*(y^93))+1192052400*((x^6)*(y^94))+75287520*((x^5)*(y^95))+3921225*((x^4)*(y^96))+161700*((x^3)*(y^97))+4950*((x^2)*(y^98))+100*(x*(y^99))+y^100
(x+y)^99 = x^99+99*((x^98)*y)+4851*((x^97)*(y^2))+156849*((x^96)*(y^3))+3764376*((x^95)*(y^4))+71523144*((x^94)*(y^5))+1120529256*((x^93)*(y^6))+14887031544*((x^92)*(y^7))+171200862756*((x^91)*(y^8))+1731030945644*((x^90)*(y^9))+15579278510796*((x^89)*(y^10))+126050526132804*((x^88)*(y^11))+924370524973896*((x^87)*(y^12))+6186171974825304*((x^86)*(y^13))+38000770702498296*((x^85)*(y^14))+215337700647490344*((x^84)*(y^15))+1130522928399324306*((x^83)*(y^16))+5519611944537877494*((x^82)*(y^17))+25144898858450330806*((x^81)*(y^18))+107196674080761936594*((x^80)*(y^19))+428786696323047746376*((x^79)*(y^20))+1613054714739084379224*((x^78)*(y^21))+5719012170438571889976*((x^77)*(y^22))+19146258135816088501224*((x^76)*(y^23))+60629817430084280253876*((x^75)*(y^24))+181889452290252840761628*((x^74)*(y^25))+517685364210719623706172*((x^73)*(y^26))+1399667836569723427057428*((x^72)*(y^27))+3599145865465003098147672*((x^71)*(y^28))+8811701946483283447189128*((x^70)*(y^29))+20560637875127661376774632*((x^69)*(y^30))+45764000431735762419272568*((x^68)*(y^31))+97248500917438495140954207*((x^67)*(y^32))+197443926105102399225573693*((x^66)*(y^33))+383273503615787010261407757*((x^65)*(y^34))+711793649572175876199757263*((x^64)*(y^35))+1265410932572757113244012912*((x^63)*(y^36))+2154618614921181030658724688*((x^62)*(y^37))+3515430371713505892127392912*((x^61)*(y^38))+5498493658321124600506947888*((x^60)*(y^39))+8247740487481686900760421832*((x^59)*(y^40))+11868699725888281149874753368*((x^58)*(y^41))+16390109145274293016493707032*((x^57)*(y^42))+21726423750712434928840495368*((x^56)*(y^43))+27651812046361280818524266832*((x^55)*(y^44))+33796659167774898778196326128*((x^54)*(y^45))+39674339023040098565708730672*((x^53)*(y^46))+44739148260023940935799206928*((x^52)*(y^47))+48467410615025936013782474172*((x^51)*(y^48))+50445672272782096667406248628*((x^50)*(y^49))+50445672272782096667406248628*((x^49)*(y^50))+48467410615025936013782474172*((x^48)*(y^51))+44739148260023940935799206928*((x^47)*(y^52))+39674339023040098565708730672*((x^46)*(y^53))+33796659167774898778196326128*((x^45)*(y^54))+27651812046361280818524266832*((x^44)*(y^55))+21726423750712434928840495368*((x^43)*(y^56))+16390109145274293016493707032*((x^42)*(y^57))+11868699725888281149874753368*((x^41)*(y^58))+8247740487481686900760421832*((x^40)*(y^59))+5498493658321124600506947888*((x^39)*(y^60))+3515430371713505892127392912*((x^38)*(y^61))+2154618614921181030658724688*((x^37)*(y^62))+1265410932572757113244012912*((x^36)*(y^63))+711793649572175876199757263*((x^35)*(y^64))+383273503615787010261407757*((x^34)*(y^65))+197443926105102399225573693*((x^33)*(y^66))+97248500917438495140954207*((x^32)*(y^67))+45764000431735762419272568*((x^31)*(y^68))+20560637875127661376774632*((x^30)*(y^69))+8811701946483283447189128*((x^29)*(y^70))+3599145865465003098147672*((x^28)*(y^71))+1399667836569723427057428*((x^27)*(y^72))+517685364210719623706172*((x^26)*(y^73))+181889452290252840761628*((x^25)*(y^74))+60629817430084280253876*((x^24)*(y^75))+19146258135816088501224*((x^23)*(y^76))+5719012170438571889976*((x^22)*(y^77))+1613054714739084379224*((x^21)*(y^78))+428786696323047746376*((x^20)*(y^79))+107196674080761936594*((x^19)*(y^80))+25144898858450330806*((x^18)*(y^81))+5519611944537877494*((x^17)*(y^82))+1130522928399324306*((x^16)*(y^83))+215337700647490344*((x^15)*(y^84))+38000770702498296*((x^14)*(y^85))+6186171974825304*((x^13)*(y^86))+924370524973896*((x^12)*(y^87))+126050526132804*((x^11)*(y^88))+15579278510796*((x^10)*(y^89))+1731030945644*((x^9)*(y^90))+171200862756*((x^8)*(y^91))+14887031544*((x^7)*(y^92))+1120529256*((x^6)*(y^93))+71523144*((x^5)*(y^94))+3764376*((x^4)*(y^95))+156849*((x^3)*(y^96))+4851*((x^2)*(y^97))+99*(x*(y^98))+y^99
(x+y)^100/(x+y)^99 = x+y

A non-trivial simplification. Let a=xy, b=yz, and c=xz. Assume b+c>0, a+b=6, and a-b=2. The last two assumptions imply a=4 and b=2, so the first simplifies to 2+c>0.

Now under this assumption, ask SARL to simplify the expression a+b+c>0. This reduces to 6+c>0, i.e., c>-6. But since the assumption implies c>-2, which implies c>-6, the expression simplifies to true: 

NumericExpression a = universe.multiply(x, y), b = universe.multiply(y,z), c = universe.multiply(x, z);
BooleanExpression context =
    universe.and(
        Arrays.asList(
            universe.lessThan(zero, universe.add(b, c)),
            universe.equals(universe.add(a, b), universe.rational(6)),
            universe.equals(universe.subtract(a, b), universe.rational(2))));
out.println("context = " + context);
SymbolicExpression expr = universe.lessThan(zero, universe.add(Arrays.asList(a, b, c)));
out.println("expr = " + expr);
Reasoner reasoner = universe.reasoner(context);
out.println("reduced context = " + reasoner.getReducedContext());
out.println("simplified expr = " + reasoner.simplify(expr));

Output:

context = (0 == x*y+-1*(y*z)+-2) && (0 == x*y+y*z+-6) && (0 < x*z+y*z)
expr = 0 < x*y+x*z+y*z
reduced context = (0 == x*y+-4) && (0 == y*z+-2) && (0 < x*z+2)
simplified expr = true

References: here we create a reference to an element of a 2-dimensional array. We use it to read and to write:

SymbolicType real5 = universe.arrayType(realType, universe.integer(5));
SymbolicType real55 = universe.arrayType(real5, universe.integer(5));
SymbolicExpression a = universe.symbolicConstant(universe.stringObject("a"), real55);
out.println("a = " + a);
ReferenceExpression r23 = universe.arrayElementReference(
    universe.arrayElementReference(universe.identityReference(), universe.integer(2)),
    universe.integer(3));
out.println("r23 = " + r23);
out.println("dereference(a,r23)=" + universe.dereference(a, r23));
SymbolicExpression a_new = universe.assign(a, r23, universe.rational(7));
out.println("a_new = " + a_new);
out.println("a_new[2][3] = "+
    universe.arrayRead(universe.arrayRead(a_new, universe.integer(2)),
    universe.integer(3)));

Output:

a = a
r23 = ArrayElementRef(ArrayElementRef(Ref<1>,2),3)
dereference(a,r23)=a[2][3]
a_new = a[2:=a[2][3:=7]]
a_new[2][3] = 7

Reasoning: if xy=0, does it follow that x=0 or y=0? 

Reasoner reasoner = universe.reasoner(universe.equals(zero, universe.multiply(x, y)));
BooleanExpression assertion = universe.or(universe.equals(zero, x), universe.equals(zero, y));
out.println(reasoner.isValid(assertion));

Output:

true
VSL