psycopaths / jconstraints-z3 Goto Github PK

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?

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,

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,
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