Skip to content

Commit 5e13202

Browse files
refactormyselfrefactormyself
committed
Add BasicSample and test run
1 parent 00e03b2 commit 5e13202

File tree

2 files changed

+278
-0
lines changed

2 files changed

+278
-0
lines changed

‎runBasicSamples.sh‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
#!/bin/bash
2+
3+
#------------------------------------------------------------------------------
4+
# check Java version
5+
#------------------------------------------------------------------------------
6+
7+
[ -z "$JAVA" ] && JAVA=java
8+
java_version="`$JAVA -XX:-UsePerfData -Xmx5m -version 2>&1`"
9+
result=$?
10+
if [ $result -eq 127 ]; then
11+
echo "Java not found, please install Java 1.8 or newer." 1>&2
12+
echo "For Ubuntu: sudo apt-get install openjdk-8-jre" 1>&2
13+
echo "If you have installed Java 8, but it is not in your PATH," 1>&2
14+
echo "let the environment variable JAVA point to the \"java\" binary." 1>&2
15+
exit 1
16+
fi
17+
if [ $result -ne 0 ]; then
18+
echo "Failed to execute Java VM, return code was $result and output was"
19+
echo "$java_version"
20+
echo "Please make sure you are able to execute Java processes by running \"$JAVA\"."
21+
exit 1
22+
fi
23+
java_version="`echo "$java_version" | grep -e "^\(java\|openjdk\) version" | cut -f2 -d\\\" | sed 's/\.//g' | cut -b1-2`"
24+
if [ -z "$java_version" ] || [ "$java_version" -lt 18 -a "$java_version" -gt 13 ] ; then
25+
echo "Your Java version is too old, please install Java 1.8 or newer." 1>&2
26+
echo "For Ubuntu: sudo apt-get install openjdk-8-jre" 1>&2
27+
echo "If you have installed Java 8, but it is not in your PATH," 1>&2
28+
echo "let the environment variable JAVA point to the \"java\" binary." 1>&2
29+
exit 1
30+
fi
31+
32+
33+
#------------------------------------------------------------------------------
34+
# build classpath for JavaSMT
35+
#------------------------------------------------------------------------------
36+
37+
platform="`uname -s`"
38+
39+
# where the project directory is, relative to the location of this script
40+
case "$platform" in
41+
Linux|CYGWIN*)
42+
SCRIPT="$(readlink -f "$0")"
43+
[ -n "$PATH_TO_JAVASMT" ] || PATH_TO_JAVASMT="$(readlink -f "$(dirname "$SCRIPT")")"
44+
;;
45+
# other platforms like Mac don't support readlink -f
46+
*)
47+
[ -n "$PATH_TO_JAVASMT" ] || PATH_TO_JAVASMT="$(dirname "$0")"
48+
;;
49+
esac
50+
51+
if [ ! -e "$PATH_TO_JAVASMT/bin/org/sosy_lab/java_smt/example/AllSatExample.class" ] ; then
52+
if [ ! -e "$PATH_TO_JAVASMT/javasmt.jar" ] ; then
53+
echo "Could not find JAVASMT binary, please check path to project directory" 1>&2
54+
exit 1
55+
fi
56+
fi
57+
58+
case "$platform" in
59+
CYGWIN*)
60+
JAVA_VM_ARGUMENTS="$JAVA_VM_ARGUMENTS -classpath `cygpath -wp $CLASSPATH`"
61+
;;
62+
esac
63+
64+
export CLASSPATH="$CLASSPATH:$PATH_TO_JAVASMT/bin:$PATH_TO_JAVASMT/JAVASMT.jar:$PATH_TO_JAVASMT/lib/*:$PATH_TO_JAVASMT/lib/java/runtime/*"
65+
66+
# Run Examples for Java-SMT.
67+
# PerfDisableSharedMem avoids hsperfdata in /tmp (disable it to connect easily with VisualConsole and Co.).
68+
69+
# for EXAMPLE in AllSatExample HoudiniApp Interpolation OptimizationFormulaWeights OptimizationIntReal; do
70+
71+
for EXAMPLE in AllSatExample BasicSample1; do
72+
echo "####################################################"
73+
echo "# executing example $EXAMPLE"
74+
echo "####################################################"
75+
"$JAVA" \
76+
-XX:+PerfDisableSharedMem \
77+
-Djava.awt.headless=true \
78+
-ea \
79+
$JAVA_VM_ARGUMENTS \
80+
org.sosy_lab.java_smt.example.$EXAMPLE
81+
done

‎src/org/sosy_lab/java_smt/example/BasicSample1.java‎

Lines changed: 197 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,197 @@
1+
/*
2+
* JavaSMT is an API wrapper for a collection of SMT solvers.
3+
* This file is part of JavaSMT.
4+
*
5+
* Copyright (C) 2007-2019 Dirk Beyer
6+
* All rights reserved.
7+
*
8+
* Licensed under the Apache License, Version 2.0 (the "License");
9+
* you may not use this file except in compliance with the License.
10+
* You may obtain a copy of the License at
11+
*
12+
* http://www.apache.org/licenses/LICENSE-2.0
13+
*
14+
* Unless required by applicable law or agreed to in writing, software
15+
* distributed under the License is distributed on an "AS IS" BASIS,
16+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
17+
* See the License for the specific language governing permissions and
18+
* limitations under the License.
19+
*/
20+
package org.sosy_lab.java_smt.example;
21+
22+
import org.sosy_lab.common.ShutdownNotifier;
23+
import org.sosy_lab.common.configuration.Configuration;
24+
import org.sosy_lab.common.configuration.InvalidConfigurationException;
25+
import org.sosy_lab.common.log.BasicLogManager;
26+
import org.sosy_lab.common.log.LogManager;
27+
import org.sosy_lab.java_smt.SolverContextFactory;
28+
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
29+
import org.sosy_lab.java_smt.api.BooleanFormula;
30+
import org.sosy_lab.java_smt.api.BooleanFormulaManager;
31+
import org.sosy_lab.java_smt.api.IntegerFormulaManager;
32+
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
33+
import org.sosy_lab.java_smt.api.ProverEnvironment;
34+
import org.sosy_lab.java_smt.api.SolverContext;
35+
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
36+
import org.sosy_lab.java_smt.api.SolverException;
37+
38+
public class BasicSample1 {
39+
private BasicSample1() {}
40+
41+
public static void main(String[] args)
42+
throws InvalidConfigurationException, SolverException, InterruptedException {
43+
44+
// Setup and Congigurations
45+
Configuration config = Configuration.fromCmdLineArguments(args);
46+
LogManager logger = BasicLogManager.create(config);
47+
48+
// deal with cleanup and shutdowns
49+
// ShutdownManager shutdown = ShutdownManager.create();
50+
ShutdownNotifier shutdownNotifier = ShutdownNotifier.createDummy();
51+
52+
// We can do this too but ...
53+
// SolverContext context = SolverContextFactory.createSolverContext(
54+
// config, logger, shutdown.getNotifier(), Solvers.SMTINTERPOL);
55+
56+
// Solvers solver = Solvers.SMTINTERPOL;
57+
//
58+
for (Solvers solver : Solvers.values()) {
59+
System.out.println("NOW TESTING WITH : " + solver + ".. \n");
60+
61+
// Instantiate JavaSMT with SMTInterpol as backend (for dependencies cf. documentation)
62+
try (SolverContext context =
63+
SolverContextFactory.createSolverContext(config, logger, shutdownNotifier, solver)) {
64+
65+
/* BOOLEAN THEORY */
66+
// create the manager
67+
BooleanFormulaManager booleFormularMgr =
68+
context.getFormulaManager().getBooleanFormulaManager();
69+
70+
// create atoms
71+
BooleanFormula xL = booleFormularMgr.makeVariable("xL");
72+
BooleanFormula xH = booleFormularMgr.makeVariable("xH");
73+
BooleanFormula yL = booleFormularMgr.makeVariable("yL");
74+
BooleanFormula yH = booleFormularMgr.makeVariable("yH");
75+
76+
// create formular
77+
BooleanFormula lowXOR = booleFormularMgr.xor(xL, yL);
78+
BooleanFormula highXOR = booleFormularMgr.xor(xH, yH);
79+
BooleanFormula twoBitAdder = booleFormularMgr.and(lowXOR, highXOR); // Formula to solve
80+
81+
/* LRA (Integer) THEORY */
82+
// create the manager
83+
IntegerFormulaManager intFormularMgr =
84+
context.getFormulaManager().getIntegerFormulaManager();
85+
86+
// create atoms
87+
IntegerFormula x = intFormularMgr.makeVariable("x");
88+
IntegerFormula y = intFormularMgr.makeVariable("y");
89+
90+
// create formula
91+
92+
IntegerFormula twoX = intFormularMgr.multiply(x, intFormularMgr.makeNumber(2));
93+
IntegerFormula threeX = intFormularMgr.multiply(x, intFormularMgr.makeNumber(3));
94+
IntegerFormula twoY = intFormularMgr.multiply(y, intFormularMgr.makeNumber(2));
95+
96+
// 3*x + y = 11
97+
BooleanFormula eqA1 =
98+
intFormularMgr.equal(intFormularMgr.add(threeX, y), intFormularMgr.makeNumber(11));
99+
// 2*x + y = 8
100+
BooleanFormula eqA2 =
101+
intFormularMgr.equal(intFormularMgr.add(twoX, y), intFormularMgr.makeNumber(8));
102+
103+
// Formula to solve (3,2)
104+
BooleanFormula intTheorySampleA = booleFormularMgr.and(eqA1, eqA2);
105+
106+
// x>2
107+
BooleanFormula eqB1 = intFormularMgr.greaterThan(x, intFormularMgr.makeNumber(2));
108+
// y<10
109+
BooleanFormula eqB2 = intFormularMgr.lessThan(y, intFormularMgr.makeNumber(10));
110+
// x+2*y == 7 (how do I differentiate)
111+
BooleanFormula eqB3 =
112+
intFormularMgr.equal(intFormularMgr.add(x, twoY), intFormularMgr.makeNumber(7));
113+
114+
// Formula to solve (0,7)
115+
BooleanFormula intTheorySampleB = booleFormularMgr.and(eqB1, eqB2, eqB3);
116+
117+
/* LRA (Rational) THEORY */
118+
// create the manager
119+
// RationalFormulaManager rationalFormularMgr =
120+
// context.getFormulaManager().getRationalFormulaManager();
121+
122+
// create atoms
123+
// RationalFormula a = rationalFormularMgr.makeVariable("a");
124+
// RationalFormula b = rationalFormularMgr.makeVariable("b");
125+
126+
// RationalFormula a1 = rationalFormularMgr.makeVariable("a1");
127+
// RationalFormula a2 = rationalFormularMgr.makeVariable("a2");
128+
// RationalFormula b1 = rationalFormularMgr.makeVariable("b1");
129+
// RationalFormula b2 = rationalFormularMgr.makeVariable("b2");
130+
131+
// create formula
132+
/*
133+
* UNSUPPORTED a^2 ==> this is linear
134+
*
135+
* RationalFormula a_square = rationalFormularMgr.multiply(a, a); RationalFormula b_square =
136+
* rationalFormularMgr.multiply(b, b); // a^2 + b^2 < 1 BooleanFormula eqR1 =
137+
* rationalFormularMgr.lessThan( rationalFormularMgr.add(a_square, b_square),
138+
* rationalFormularMgr.makeNumber(1)); // x*y > 0.1 BooleanFormula eqR2 = rationalFormularMgr
139+
* .greaterThan(rationalFormularMgr.multiply(a, b), rationalFormularMgr.makeNumber(0.1));
140+
*
141+
* BooleanFormula ratTheorySample1 = booleFormularMgr.and(eqR1, eqR2); // Formula to solve
142+
* (1/8, // 7/8)
143+
*
144+
* // x*y > 1 BooleanFormula eqR3 = rationalFormularMgr
145+
* .greaterThan(rationalFormularMgr.multiply(a, b), rationalFormularMgr.makeNumber(1));
146+
*
147+
* BooleanFormula ratTheorySample2 = booleFormularMgr.and(eqR1, eqR3); // Formula to solve //
148+
* (UNSAT)
149+
*/
150+
151+
boolean isUnsat;
152+
153+
// Solve formulae, get model, and print variable assignment
154+
try (ProverEnvironment prover =
155+
context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
156+
157+
prover.addConstraint(twoBitAdder);
158+
isUnsat = prover.isUnsat();
159+
assert !isUnsat;
160+
// try (Model model = prover.getModel()) {
161+
System.out.println("SAT : 2-bit Adder ");
162+
// }
163+
164+
prover.addConstraint(intTheorySampleA);
165+
isUnsat = prover.isUnsat();
166+
assert !isUnsat;
167+
// try (Model model = prover.getModel()) {
168+
// System.out.printf("SAT with a = %s, b = %s", model.evaluate(a), model.evaluate(b));
169+
System.out.println("SAT : 2 equations 3*x + y = 11 AND 2*x + y = 8");
170+
// }
171+
172+
prover.addConstraint(intTheorySampleB);
173+
isUnsat = prover.isUnsat();
174+
assert !isUnsat;
175+
// try (Model model = prover.getModel()) {
176+
System.out.println("SAT : 3 equations x>2 AND y<10 AND x+2*y == 7");
177+
// }
178+
179+
// prover.addConstraint(ratTheorySample1);
180+
// isUnsat = prover.isUnsat();
181+
// assert !isUnsat;
182+
// // try (Model model = prover.getModel()) {
183+
// System.out.println("SAT : 2 equations a^2 + b^2 < 1 AND x*y > 0.1 ");
184+
// // }
185+
//
186+
// prover.addConstraint(ratTheorySample2);
187+
// isUnsat = prover.isUnsat();
188+
// assert isUnsat;
189+
// // try (Model model = prover.getModel()) {
190+
// System.out.println("UNSAT : 2 equations a^2 + b^2 < 1 AND x*y > 1 ");
191+
// // }
192+
193+
}
194+
}
195+
}
196+
}
197+
}

0 commit comments

Comments
 (0)