Skip to content

Commit d9deaf6

Browse files
kfriedbergerkfriedberger
authored
Merge pull request #165 from sosy-lab/cvc4_integration
Cvc4 integration
2 parents 708246a + dab5110 commit d9deaf6

File tree

59 files changed

+3281
-180
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

59 files changed

+3281
-180
lines changed

‎.classpath‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818
<classpathentry kind="lib" path="lib/java/runtime/princess-smt-parser_2.12.jar"/>
1919
<classpathentry kind="lib" path="lib/java/runtime/java-cup-runtime.jar"/>
2020
<classpathentry kind="lib" path="lib/java/runtime/com.microsoft.z3.jar"/>
21+
<classpathentry kind="lib" path="lib/java/runtime/CVC4.jar"/>
2122
<classpathentry kind="lib" path="lib/java/test/truth-java8-extension.jar" sourcepath="lib/java-contrib/truth-java8-extension-sources.jar"/>
2223
<classpathentry kind="lib" path="lib/java/runtime/checker-qual.jar" sourcepath="lib/java-contrib/checker-qual-sources.jar"/>
2324
<classpathentry kind="lib" path="lib/java/test/diffutils.jar"/>

‎build/build-publish-solvers.xml‎

Lines changed: 45 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -62,46 +62,69 @@
6262
description="Copy CVC4 binaries to the root folder along with the version postfix.">
6363
<fail unless="cvc4.path">
6464
Please specify the path to CVC4 with the flag -Dcvc4.path=/path/to/cvc4.
65-
The path has to point to the root CVC4 folder.
65+
The path has to point to the root CVC4 folder, i.e.,
66+
a checkout of the official git repositoy from 'https://github.com/CVC4/CVC4.git'.
6667
Note that shell substitutions do not work and a full absolute
6768
path has to be specified.
6869
</fail>
6970
<fail unless="cvc4.customRev">
7071
Please specify a custom revision with the flag -Dcvc4.customRev=XXX.
7172
The custom revision has to be unique amongst the already known version
72-
numbers from the ivy repository.
73+
numbers from the ivy repository. The script will append the git revision.
7374
</fail>
74-
<exec executable="sed" dir="${cvc4.path}/builds" outputproperty="cvc4.version">
75-
<arg value="-n" />
76-
<arg value="-e" />
77-
<arg value="s/distdir = cvc4-/${cvc4.customRev}/p" />
78-
<arg value="Makefile" />
75+
76+
<!-- get a nive version -->
77+
<exec executable="git" dir="${cvc4.path}" outputproperty="cvc4.revision">
78+
<arg value="show"/>
79+
<arg value="-s"/>
80+
<arg value="--format=%h"/>
81+
</exec>
82+
<property name="cvc4.version" value="${cvc4.customRev}-g${cvc4.revision}"/>
83+
<echo message="Building CVC4 in version '${cvc4.version}'"/>
84+
85+
<!-- build CVC4 -->
86+
<exec executable="rm" dir="${cvc4.path}">
87+
<arg value="-rf"/>
88+
<arg value="symfpu-CVC4"/>
89+
</exec>
90+
<exec executable="./contrib/get-symfpu" dir="${cvc4.path}"/>
91+
<exec executable="./configure.sh" dir="${cvc4.path}">
92+
<arg value="--symfpu"/>
93+
<arg value="--language-bindings=java"/>
7994
</exec>
80-
<exec executable="strip" dir="${cvc4.path}/builds/x86_64-unknown-linux-gnu/production/src/bindings/java/.libs">
95+
<exec executable="make" dir="${cvc4.path}/build/">
96+
<arg value="-j4" />
97+
</exec>
98+
99+
<!-- remove unneeded symbols -->
100+
<exec executable="strip" dir="${cvc4.path}/build/src/bindings/java/">
81101
<arg value="libcvc4jni.so" />
82102
</exec>
83-
<exec executable="strip" dir="${cvc4.path}/builds/x86_64-unknown-linux-gnu/production/src/.libs">
103+
<exec executable="strip" dir="${cvc4.path}/build/src/">
84104
<arg value="libcvc4.so" />
85105
</exec>
86-
<exec executable="strip" dir="${cvc4.path}/builds/x86_64-unknown-linux-gnu/production/src/parser/.libs">
106+
<exec executable="strip" dir="${cvc4.path}/build/src/parser/">
87107
<arg value="libcvc4parser.so" />
88108
</exec>
89109

90-
<exec executable="chrpath" dir="${cvc4.path}/builds/x86_64-unknown-linux-gnu/production/src/bindings/java/.libs">
91-
<arg value="-r" />
92-
<arg value="$ORIGIN" />
93-
<arg value="libcvc4jni.so" />
110+
<!-- fix RPATH and library dependencies -->
111+
<exec executable="patchelf" dir="${cvc4.path}/build/src/parser/">
112+
<arg value="--set-rpath"/><arg value="$ORIGIN"/>
113+
<arg value="--replace-needed"/><arg value="libcvc4.so.6"/><arg value="libcvc4.so"/>
114+
<arg value="libcvc4parser.so"/>
94115
</exec>
95-
<exec executable="chrpath" dir="${cvc4.path}/builds/x86_64-unknown-linux-gnu/production/src/parser/.libs">
96-
<arg value="-r" />
97-
<arg value="$ORIGIN" />
98-
<arg value="libcvc4parser.so" />
116+
<exec executable="patchelf" dir="${cvc4.path}/build/src/bindings/java/">
117+
<arg value="--set-rpath"/><arg value="$ORIGIN"/>
118+
<arg value="--replace-needed"/><arg value="libcvc4.so.6"/><arg value="libcvc4.so"/>
119+
<arg value="--replace-needed"/><arg value="libcvc4parser.so.6"/><arg value="libcvc4parser.so"/>
120+
<arg value="libcvc4jni.so"/>
99121
</exec>
100122

101-
<copy file="${cvc4.path}/builds/x86_64-unknown-linux-gnu/production/src/bindings/java/.libs/libcvc4jni.so" tofile="libcvc4jni-${cvc4.version}.so"/>
102-
<copy file="${cvc4.path}/builds/x86_64-unknown-linux-gnu/production/src/.libs/libcvc4.so" tofile="libcvc4.so-${cvc4.version}.3"/>
103-
<copy file="${cvc4.path}/builds/x86_64-unknown-linux-gnu/production/src/parser/.libs/libcvc4parser.so" tofile="libcvc4parser.so-${cvc4.version}.3"/>
104-
<copy file="${cvc4.path}/builds/x86_64-unknown-linux-gnu/production/src/bindings/CVC4.jar" tofile="CVC4-${cvc4.version}.jar"/>
123+
<!-- copy library files into directory to be published for IVY -->
124+
<copy file="${cvc4.path}/build/src/libcvc4.so" tofile="libcvc4-${cvc4.version}.so"/>
125+
<copy file="${cvc4.path}/build/src/parser/libcvc4parser.so" tofile="libcvc4parser-${cvc4.version}.so"/>
126+
<copy file="${cvc4.path}/build/src/bindings/java/libcvc4jni.so" tofile="libcvc4jni-${cvc4.version}.so"/>
127+
<copy file="${cvc4.path}/build/src/bindings/java/CVC4.jar" tofile="CVC4-${cvc4.version}.jar"/>
105128
</target>
106129

107130
<target name="publish-cvc4" depends="package-cvc4, load-ivy"

‎lib/ivy.xml‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
<license name="The Apache Software License, Version 2.0" url="http://www.apache.org/licenses/LICENSE-2.0.txt"/>
88

99
<description homepage="https://github.com/sosy-lab/java-smt">
10-
Java wrapper for Z3, MathSAT5, SMTInterpol, Princess SMT solvers.
10+
Java wrapper for Z3, MathSAT5, SMTInterpol, Princess, CVC4 SMT solvers.
1111
</description>
1212
</info>
1313

@@ -24,9 +24,10 @@
2424
<conf name="runtime-smtinterpol" extends="core" description="only one solver included"/>
2525
<conf name="runtime-princess" extends="core" description="only one solver included"/>
2626
<conf name="runtime-z3" extends="core" description="only one solver included"/>
27+
<conf name="runtime-cvc4" extends="core" description="only one solver included"/>
2728

2829
<!-- The normal dependencies with all solvers included. -->
29-
<conf name="runtime" extends="runtime-mathsat,runtime-optimathsat,runtime-smtinterpol,runtime-princess,runtime-z3" description="all solvers included"/>
30+
<conf name="runtime" extends="runtime-mathsat,runtime-optimathsat,runtime-smtinterpol,runtime-princess,runtime-z3,runtime-cvc4" description="all solvers included"/>
3031

3132
<!-- Dependencies needed for building or running tests. -->
3233
<conf name="test" visibility="private" description="for developing and testing"/>
@@ -135,6 +136,7 @@
135136
<dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.5.4-sosy0" conf="runtime-mathsat->solver-mathsat" />
136137
<dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.7.1" conf="runtime-z3->solver-z3" />
137138
<dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.6.3" conf="runtime-optimathsat->solver-optimathsat" />
139+
<dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2019-10-05-g6972cfa" conf="runtime-cvc4->solver-cvc4" />
138140

139141
<!-- Guava has a dependency on error_prone_annotations without a revision number, need an override. -->
140142
<override org="com.google.errorprone" module="error_prone_annotations" rev="2.3.2"/>

‎lib/native/x86_64-linux/libcvc4.so‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../../java/runtime/libcvc4.so

‎lib/native/x86_64-linux/libcvc4jni.so‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../../java/runtime/libcvc4jni.so

‎lib/native/x86_64-linux/libcvc4parser.so‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../../java/runtime/libcvc4parser.so

‎solvers_ivy_conf/ivy_cvc4.xml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@
1616
</configurations>
1717

1818
<publications defaultconf="solver-cvc4">
19-
<artifact name="libcvc4jni" conf="solver-cvc4" type="shared-object" ext="so" />
20-
<artifact name="libcvc4.so" conf="solver-cvc4" type="shared-object" ext="3"/>
21-
<artifact name="libcvc4parser.so" conf="solver-cvc4" type="shared-object" ext="3"/>
19+
<artifact name="libcvc4jni" conf="solver-cvc4" type="shared-object" ext="so"/>
20+
<artifact name="libcvc4" conf="solver-cvc4" type="shared-object" ext="so"/>
21+
<artifact name="libcvc4parser" conf="solver-cvc4" type="shared-object" ext="so"/>
2222
<artifact name="CVC4" conf="solver-cvc4" />
2323
</publications>
2424

‎src/org/sosy_lab/java_smt/SolverContextFactory.java‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,7 @@
5151
import org.sosy_lab.java_smt.api.SolverContext;
5252
import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
5353
import org.sosy_lab.java_smt.logging.LoggingSolverContext;
54+
import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext;
5455
import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5SolverContext;
5556
import org.sosy_lab.java_smt.solvers.princess.PrincessSolverContext;
5657
import org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolSolverContext;
@@ -68,7 +69,8 @@ public enum Solvers {
6869
MATHSAT5,
6970
SMTINTERPOL,
7071
Z3,
71-
PRINCESS
72+
PRINCESS,
73+
CVC4
7274
}
7375

7476
@Option(secure = true, description = "Export solver queries in SmtLib format into a file.")
@@ -183,6 +185,14 @@ public SolverContext generateContext(Solvers solverToCreate)
183185
private SolverContext generateContext0(Solvers solverToCreate)
184186
throws InvalidConfigurationException {
185187
switch (solverToCreate) {
188+
case CVC4:
189+
return CVC4SolverContext.create(
190+
logger,
191+
shutdownNotifier,
192+
(int) randomSeed,
193+
nonLinearArithmetic,
194+
floatingPointRoundingMode);
195+
186196
case SMTINTERPOL:
187197
return SmtInterpolSolverContext.create(
188198
config, logger, shutdownNotifier, logfile, randomSeed, nonLinearArithmetic);

‎src/org/sosy_lab/java_smt/api/FormulaManager.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,13 @@ public interface FormulaManager {
7575
/** Returns the function for dealing with uninterpreted functions (UFs). */
7676
UFManager getUFManager();
7777

78+
/**
79+
* Returns the Seperation-Logic-Theory.
80+
*
81+
* @throws UnsupportedOperationException If the theory is not supported by the solver.
82+
*/
83+
SLFormulaManager getSLFormulaManager();
84+
7885
/**
7986
* Returns the interface for handling quantifiers.
8087
*

‎src/org/sosy_lab/java_smt/api/FormulaType.java‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,10 @@ public boolean isIntegerType() {
6969
return false;
7070
}
7171

72+
public boolean isSLType() {
73+
return false;
74+
}
75+
7276
@Override
7377
public abstract String toString();
7478

0 commit comments

Comments
 (0)