Commit 94384fd3 authored by Eugen Zalinescu's avatar Eugen Zalinescu

small tets

parent 9a4a6a16
package de.tum.workflows.toz3;
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.TermFunctions._
import com.microsoft.z3._;
// import collection.mutable.HashMap
import java.util.HashMap
object Test extends App {
def toZ3(ctx: Context, t: Term) = {
t match {
case t: Var => {
ctx.mkSymbol(t.name)
}
}
}
class TestFailedException extends Exception {}
def check(ctx: Context, f: BoolExpr, sat: Status): (Model) = {
val s = ctx.mkSolver()
s.add(f)
if (s.check() != sat)
throw new TestFailedException();
if (sat == Status.SATISFIABLE)
return s.getModel();
else
return null;
}
def atest(ctx: Context) = {
val x = ctx.mkIntConst("x")
val y = ctx.mkIntConst("y")
val one = ctx.mkInt(1)
val two = ctx.mkInt(2)
val y_plus_one = ctx.mkAdd(y, one)
val c1 = ctx.mkLt(x, y_plus_one)
val c2 = ctx.mkGt(x, two)
val q = ctx.mkAnd(c1, c2)
System.out.println("model for: x < y + 1, x > 2")
val model = check(ctx, q, Status.SATISFIABLE)
System.out.println("x = " + model.evaluate(x, false) + ", y = "
+ model.evaluate(y, false))
}
def main() = {
com.microsoft.z3.Global.ToggleWarningMessages(true);
// Log.open("test.log");
System.out.print("Z3 Major Version: ");
System.out.println(Version.getMajor());
System.out.print("Z3 Full Version: ");
System.out.println(Version.getString());
System.out.print("Z3 Full Version String: ");
System.out.println(Version.getFullVersion());
val cfg = new HashMap[String,String]();
cfg.put("model", "true");
val ctx = new Context(cfg);
atest(ctx);
}
main()
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment