psycopaths / jconstraints-z3 Goto Github PK
View Code? Open in Web Editor NEWjConstraints abstraction layer for Z3
License: Apache License 2.0
jConstraints abstraction layer for Z3
License: Apache License 2.0
Hello,
When trying to build jconstraints-z3, using the latestZ3 version I get an error: cannot find symbol: com.microsoft.z3.IDisposable.
I checked and I found out that this class no longer exists in Z3 src so I downloaded Z3 4.4.1 and the issue is solved however I get a new error: java.lang.UnsupportedClassVersionError: com/microsoft/z3/Z3Exception : Unsupported major.minor version 52.0.
Update: it works with Z3 version 4.4.0
Update2:
Now I get a new error: JPF configuration error: error instantiating class gov.nasa.jpf.jdart.JDart for entry "shell":
exception in gov.nasa.jpf.jdart.JDart(gov.nasa.jpf.Config):
java.lang.NoClassDefFoundError: com/microsoft/z3/Z3Exception
I have followed all the installation descriptions on jConstraints and Z3 but when I type "mvn install" under jconstraints-z3 directory, I get these errors:
[MVNVM] Using maven: 3.3.9
[INFO] Scanning for projects...
[INFO]
[INFO] ------------------------------------------------------------------------
[INFO] Building jConstraints-z3 1.0-SNAPSHOT
[INFO] ------------------------------------------------------------------------
[INFO]
[INFO] --- maven-resources-plugin:2.6:resources (default-resources) @ jConstraints-z3 ---
[INFO] Using 'UTF-8' encoding to copy filtered resources.
[INFO] Copying 1 resource
[INFO]
[INFO] --- maven-compiler-plugin:3.1:compile (default-compile) @ jConstraints-z3 ---
[INFO] Nothing to compile - all classes are up to date
[INFO]
[INFO] --- maven-resources-plugin:2.6:testResources (default-testResources) @ jConstraints-z3 ---
[INFO] Using 'UTF-8' encoding to copy filtered resources.
[INFO] skip non existing resourceDirectory /Users/Chaofeng/jpf/jconstraints-z3/src/test/resources
[INFO]
[INFO] --- maven-compiler-plugin:3.1:testCompile (default-testCompile) @ jConstraints-z3 ---
[INFO] Nothing to compile - all classes are up to date
[INFO]
[INFO] --- maven-surefire-plugin:2.12.4:test (default-test) @ jConstraints-z3 ---
[INFO] Surefire report directory: /Users/Chaofeng/jpf/jconstraints-z3/target/surefire-reports
T E S T S
Running TestSuite
Configuring TestNG with: org.apache.maven.surefire.testng.conf.TestNG652Configurator@c2e1f26
Jun 03, 2016 7:07:44 PM gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory registerProvider
WARNING: Overwriting constraint solver provider with name {0}
Jun 03, 2016 7:07:44 PM gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy createSolver
WARNING: Using deprecated solver name 'NativeZ3' might fail in future releases
((127 & 63) == 'i1')
Jun 03, 2016 7:07:44 PM gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy createSolver
WARNING: Using deprecated solver name 'NativeZ3' might fail in future releases
c1:5.2E-8
c2:1.01E-7
((('i1' + 5.2E-8) * 'i2') > 1.01E-7)
Names: i1 i2
((('int_0' + 5.2E-8) * 'int_1') > 1.01E-7)
(('i1' + 5.2E-8) > 1.01E-7)
Jun 03, 2016 7:07:44 PM gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy createSolver
WARNING: Using deprecated solver name 'NativeZ3' might fail in future releases
Tests run: 8, Failures: 8, Errors: 0, Skipped: 0, Time elapsed: 0.365 sec <<< FAILURE!
testToString(gov.nasa.jpf.constraints.expressions.ContextTest) Time elapsed: 0.041 sec <<< FAILURE!
java.lang.UnsatisfiedLinkError: no libz3java in java.library.path
at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1867)
at java.lang.Runtime.loadLibrary0(Runtime.java:870)
at java.lang.System.loadLibrary(System.java:1122)
at com.microsoft.z3.Native.(Native.java:14)
at com.microsoft.z3.Global.setParameter(Global.java:47)
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver.(NativeZ3Solver.java:46)
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy.createSolver(NativeZ3SolverProviderLegacy.java:36)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.ContextTest.testToString(ContextTest.java:37)
expressionTest(gov.nasa.jpf.constraints.expressions.ExpressionZ3BVTest) Time elapsed: 0.013 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy.createSolver(NativeZ3SolverProviderLegacy.java:36)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.ExpressionZ3BVTest.expressionTest(ExpressionZ3BVTest.java:69)
expressionTest(gov.nasa.jpf.constraints.expressions.ExpressionZ3Test) Time elapsed: 0.003 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy.createSolver(NativeZ3SolverProviderLegacy.java:36)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.ExpressionZ3Test.expressionTest(ExpressionZ3Test.java:101)
testIntegerFunction(gov.nasa.jpf.constraints.expressions.IntegerTest) Time elapsed: 0.001 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.IntegerTest.testIntegerFunction(IntegerTest.java:47)
testAtan2(gov.nasa.jpf.constraints.expressions.TrigonometricTest) Time elapsed: 0.001 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.createContext(TrigonometricTest.java:45)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.testAtan2(TrigonometricTest.java:54)
testCoral1(gov.nasa.jpf.constraints.expressions.TrigonometricTest) Time elapsed: 0.001 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.createContext(TrigonometricTest.java:45)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.testCoral1(TrigonometricTest.java:132)
testCoral2(gov.nasa.jpf.constraints.expressions.TrigonometricTest) Time elapsed: 0.001 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.createContext(TrigonometricTest.java:45)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.testCoral2(TrigonometricTest.java:174)
testTrigonometrics(gov.nasa.jpf.constraints.expressions.TrigonometricTest) Time elapsed: 0.001 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.createContext(TrigonometricTest.java:45)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.testTrigonometrics(TrigonometricTest.java:83)
Results :
Failed tests: testToString(gov.nasa.jpf.constraints.expressions.ContextTest): no libz3java in java.library.path
expressionTest(gov.nasa.jpf.constraints.expressions.ExpressionZ3BVTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
expressionTest(gov.nasa.jpf.constraints.expressions.ExpressionZ3Test): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
testIntegerFunction(gov.nasa.jpf.constraints.expressions.IntegerTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
testAtan2(gov.nasa.jpf.constraints.expressions.TrigonometricTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
testCoral1(gov.nasa.jpf.constraints.expressions.TrigonometricTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
testCoral2(gov.nasa.jpf.constraints.expressions.TrigonometricTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
testTrigonometrics(gov.nasa.jpf.constraints.expressions.TrigonometricTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
Tests run: 8, Failures: 8, Errors: 0, Skipped: 0
[INFO] ------------------------------------------------------------------------
[INFO] BUILD FAILURE
[INFO] ------------------------------------------------------------------------
[INFO] Total time: 1.860 s
[INFO] Finished at: 2016-06-03T19:07:44-06:00
[INFO] Final Memory: 10M/220M
[INFO] ------------------------------------------------------------------------
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-surefire-plugin:2.12.4:test (default-test) on project jConstraints-z3: There are test failures.
[ERROR]
[ERROR] Please refer to /Users/Chaofeng/jpf/jconstraints-z3/target/surefire-reports for the individual test results.
[ERROR] -> [Help 1]
[ERROR]
[ERROR] To see the full stack trace of the errors, re-run Maven with the -e switch.
[ERROR] Re-run Maven using the -X switch to enable full debug logging.
[ERROR]
[ERROR] For more information about the errors and possible solutions, please read the following articles:
[ERROR] [Help 1] http://cwiki.apache.org/confluence/display/MAVEN/MojoFailureException
I have followed everything on the manual. After I did some research, I have found someone mentioned a ~/.jconstraints folder which the application hasn't created so far. So, is this issue related to that folder?
For no apparent reason, reals do not work after I updated z3. Here is some code to check reproducibility:
public class DoubleTest {
@Test
public void expressionTest() throws RecognitionException {
Properties conf = new Properties();
conf.setProperty("symbolic.dp", "NativeZ3");
Variable<Double> s1 = Variable.create(BuiltinTypes.DOUBLE, "s1");
Variable<Double> s2 = Variable.create(BuiltinTypes.DOUBLE, "s2");
Variable<Double> r1 = Variable.create(BuiltinTypes.DOUBLE, "r1");
Constant<Double> c0 = Constant.create(BuiltinTypes.DOUBLE, 0.0);
Constant<Double> c1 = Constant.create(BuiltinTypes.DOUBLE, 1.0);
ConstraintSolverFactory factory = new ConstraintSolverFactory(conf);
ConstraintSolver solver = factory.createSolver();
//(assert (< s2 r1))
//(assert (> s2 s1))
//(assert (= 1.0 r1))
//(assert (= 0.0 s1))
//(assert (not (= 0.0 s2)))
//(assert (not (= 1.0 s2)))
Expression<Boolean> expr = ExpressionUtil.and(
new NumericBooleanExpression(s2, NumericComparator.LT, r1),
new NumericBooleanExpression(s2, NumericComparator.GT, s1),
new NumericBooleanExpression(r1, NumericComparator.EQ, c1),
new NumericBooleanExpression(s1, NumericComparator.EQ, c0),
new NumericBooleanExpression(s2, NumericComparator.NE, c0),
new NumericBooleanExpression(s2, NumericComparator.NE, c1)
);
System.out.println(expr.toString(3));
Valuation val = new Valuation();
ConstraintSolver.Result result = solver.solve(expr, val);
System.out.println(result);
System.out.println(val);
Assert.assertEquals(result, Result.SAT);
}
}
s2 is supposed to be between 0.0 and 1.0 (both bounds exclusive).
With my setup, z3 returns unsat.
I added some debug spam. It seems that all variables are created of sort Real in z3.
Hello,
I want to know what can cause this kind of error:
Exception in thread "main" java.lang.NoSuchMethodError: com.microsoft.z3.Solver.getUnsatCore()[Lcom/microsoft/z3/Expr;
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverContext.solve(NativeZ3SolverContext.java:102)
at gov.nasa.jpf.jdart.constraints.InternalConstraintsTree.findNext(InternalConstraintsTree.java:466)
at gov.nasa.jpf.jdart.ConcolicMethodExplorer.hasMoreChoices(ConcolicMethodExplorer.java:206)
at gov.nasa.jpf.jdart.ConcolicExplorer.hasMoreChoices(ConcolicExplorer.java:206)
at gov.nasa.jpf.jdart.JDartChoiceGenerator.hasMoreChoices(JDartChoiceGenerator.java:64)
at gov.nasa.jpf.vm.SystemState.advanceCurCg(SystemState.java:883)
at gov.nasa.jpf.vm.SystemState.initializeNextTransition(SystemState.java:745)
at gov.nasa.jpf.vm.VM.forward(VM.java:1709)
at gov.nasa.jpf.search.Search.forward(Search.java:579)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
at gov.nasa.jpf.JPF.run(JPF.java:613)
at gov.nasa.jpf.jdart.JDart.run(JDart.java:207)
at gov.nasa.jpf.jdart.JDart.start(JDart.java:131)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:108)
I think that this occurs when a path cannot be resolved logically (no concrete solution), I'm not really sure about that, if that turns out to be true, I need to know what else can cause this exception.
Best regards,
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.