diff --git a/.classpath b/.classpath index 5c45723..7c6ac24 100644 --- a/.classpath +++ b/.classpath @@ -4,8 +4,9 @@ - + + diff --git a/src/backend/z3smt/Z3SmtFormatTranslator.java b/src/backend/z3smt/Z3SmtFormatTranslator.java deleted file mode 100644 index eee0eee..0000000 --- a/src/backend/z3smt/Z3SmtFormatTranslator.java +++ /dev/null @@ -1,88 +0,0 @@ -package backend.z3smt; - -import checkers.inference.model.CombVariableSlot; -import checkers.inference.model.ConstantSlot; -import checkers.inference.model.ExistentialVariableSlot; -import checkers.inference.model.LubVariableSlot; -import checkers.inference.model.RefinementVariableSlot; -import checkers.inference.model.Slot; -import checkers.inference.model.VariableSlot; -import checkers.inference.solver.backend.AbstractFormatTranslator; -import checkers.inference.solver.frontend.Lattice; -import com.microsoft.z3.BoolExpr; -import com.microsoft.z3.Context; -import java.util.Collection; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import javax.annotation.processing.ProcessingEnvironment; -import javax.lang.model.element.AnnotationMirror; - -// AbstractFormatTranslator -public abstract class Z3SmtFormatTranslator - extends AbstractFormatTranslator { - - protected Context ctx; - - /** Cache of all serialized slots, keyed on slot ID. */ - protected final Map serializedSlots; - - public Z3SmtFormatTranslator(Lattice lattice) { - super(lattice); - serializedSlots = new HashMap<>(); - } - - public final void init(Context ctx) { - this.ctx = ctx; - finishInitializingEncoders(); - } - - protected abstract SlotEncodingT serializeVarSlot(VariableSlot slot); - - protected abstract SlotEncodingT serializeConstantSlot(ConstantSlot slot); - - @Override - public SlotEncodingT serialize(VariableSlot slot) { - return serializeVarSlot(slot); - } - - @Override - public SlotEncodingT serialize(ConstantSlot slot) { - return serializeConstantSlot(slot); - } - - @Override - public SlotEncodingT serialize(ExistentialVariableSlot slot) { - return serializeVarSlot(slot); - } - - @Override - public SlotEncodingT serialize(RefinementVariableSlot slot) { - return serializeVarSlot(slot); - } - - @Override - public SlotEncodingT serialize(CombVariableSlot slot) { - return serializeVarSlot(slot); - } - - @Override - public SlotEncodingT serialize(LubVariableSlot slot) { - return serializeVarSlot(slot); - } - - /** - * Subclasses can override this method to perform pre-analysis of slots for encoding - * optimization - */ - public void preAnalyzeSlots(Collection slots) {} - - public abstract String generateZ3SlotDeclaration(VariableSlot slot); - - public abstract BoolExpr encodeSlotWellformnessConstraint(VariableSlot slot); - - public abstract BoolExpr encodeSlotPreferenceConstraint(VariableSlot slot); - - public abstract Map decodeSolution( - List model, ProcessingEnvironment processingEnv); -} diff --git a/src/backend/z3smt/Z3SmtSolver.java b/src/backend/z3smt/Z3SmtSolver.java deleted file mode 100644 index 6484bd1..0000000 --- a/src/backend/z3smt/Z3SmtSolver.java +++ /dev/null @@ -1,635 +0,0 @@ -package backend.z3smt; - -import checkers.inference.InferenceMain; -import checkers.inference.model.ArithmeticConstraint; -import checkers.inference.model.ArithmeticConstraint.ArithmeticOperationKind; -import checkers.inference.model.ComparableConstraint; -import checkers.inference.model.Constraint; -import checkers.inference.model.Slot; -import checkers.inference.model.SubtypeConstraint; -import checkers.inference.model.VariableSlot; -import checkers.inference.model.serialization.ToStringSerializer; -import checkers.inference.solver.backend.Solver; -import checkers.inference.solver.frontend.Lattice; -import checkers.inference.solver.util.ExternalSolverUtils; -import checkers.inference.solver.util.FileUtils; -import checkers.inference.solver.util.SolverArg; -import checkers.inference.solver.util.SolverEnvironment; -import checkers.inference.solver.util.Statistics; -import com.microsoft.z3.BoolExpr; -import com.microsoft.z3.Context; -import com.microsoft.z3.Expr; -import java.io.BufferedReader; -import java.io.File; -import java.io.IOException; -import java.util.ArrayList; -import java.util.Collection; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import javax.lang.model.element.AnnotationMirror; -import org.checkerframework.javacutil.BugInCF; - -// TODO: make this an abstract class with common features -public class Z3SmtSolver - extends Solver> { - - public enum Z3SolverEngineArg implements SolverArg { - /** option to use optimizing mode or not */ - optimizingMode - } - - protected final Context ctx; - protected com.microsoft.z3.Optimize solver; - protected StringBuffer smtFileContents; - - protected static final String z3Program = "z3"; - protected boolean optimizingMode; - protected boolean getUnsatCore; - - // used in non-optimizing mode to find unsat constraints - protected final Map serializedConstraints = new HashMap<>(); - protected final List unsatConstraintIDs = new ArrayList<>(); - - // file is written at projectRootFolder/constraints.smt - protected static final String pathToProject = - new File(new File("").getAbsolutePath()).toString(); - protected static final String constraintsFile = pathToProject + "/z3Constraints.smt"; - protected static final String constraintsUnsatCoreFile = - pathToProject + "/z3ConstraintsUnsatCore.smt"; - protected static final String constraintsStatsFile = pathToProject + "/z3ConstraintsGlob.smt"; - - // timing statistics variables - protected long serializationStart; - protected long serializationEnd; - protected long solvingStart; - protected long solvingEnd; - - public Z3SmtSolver( - SolverEnvironment solverEnvironment, - Collection slots, - Collection constraints, - Z3SmtFormatTranslator z3SmtFormatTranslator, - Lattice lattice) { - super(solverEnvironment, slots, constraints, z3SmtFormatTranslator, lattice); - - // creating solver with timeout - // Map z3Args = new HashMap<>(); - // int timeout = 2 * 60 * 1000; // timeout of 2 mins - // z3Args.put("timeout", Integer.toString(timeout)); - // ctx = new Context(z3Args); - - // creating solver without timeout - ctx = new Context(); - - z3SmtFormatTranslator.init(ctx); - } - - // Main entry point - @Override - public Map solve() { - Map result; - - // serialize based on user choice of running in optimizing or non-optimizing mode - optimizingMode = solverEnvironment.getBoolArg(Z3SolverEngineArg.optimizingMode); - getUnsatCore = false; - - if (optimizingMode) { - System.err.println("Encoding for optimizing mode"); - } else { - System.err.println("Encoding for non-optimizing mode"); - } - - serializeSMTFileContents(); - - solvingStart = System.currentTimeMillis(); - // in Units, if the status is SAT then there must be output in the model - List results = runZ3Solver(); - solvingEnd = System.currentTimeMillis(); - - Statistics.addOrIncrementEntry( - "smt_serialization_time(millisec)", serializationEnd - serializationStart); - Statistics.addOrIncrementEntry("smt_solving_time(millisec)", solvingEnd - solvingStart); - - // Debug use, finds out number of calls to each instrumented method - // TODO: use updated stats package to print out the counters - System.err.println("=== Arithmetic Constraints Printout ==="); - Map arithmeticConstraintCounters = new HashMap<>(); - for (ArithmeticOperationKind kind : ArithmeticOperationKind.values()) { - arithmeticConstraintCounters.put(kind, 0); - } - for (Constraint constraint : constraints) { - if (constraint instanceof ArithmeticConstraint) { - ArithmeticConstraint arithmeticConstraint = (ArithmeticConstraint) constraint; - ArithmeticOperationKind kind = arithmeticConstraint.getOperation(); - arithmeticConstraintCounters.put(kind, arithmeticConstraintCounters.get(kind) + 1); - } - } - for (ArithmeticOperationKind kind : ArithmeticOperationKind.values()) { - System.err.println( - " Made arithmetic " - + kind.getSymbol() - + " constraint: " - + arithmeticConstraintCounters.get(kind)); - } - - // TODO: update parse scripts to interpret output of - // "comparableconstraint" - // System.err.println("=== Comparison Constraints Printout ==="); - // int comparableConstraints = 0; - // for (Constraint constraint : constraints) { - // if (constraint instanceof ComparableConstraint) { - // comparableConstraints++; - // } - // } - // System.err.println(" Made comparison constraint: " + - // comparableConstraints); - - if (results != null) { - result = - formatTranslator.decodeSolution( - results, solverEnvironment.processingEnvironment); - } else { - System.err.println("\n\n!!! The set of constraints is unsatisfiable! !!!"); - result = null; - } - - return result; - } - - @Override - public Collection explainUnsatisfiable() { - optimizingMode = false; - getUnsatCore = true; - - System.err.println("Now encoding for unsat core dump."); - serializeSMTFileContents(); - - solvingStart = System.currentTimeMillis(); - runZ3Solver(); - solvingEnd = System.currentTimeMillis(); - - Statistics.addOrIncrementEntry( - "smt_unsat_serialization_time(millisec)", serializationEnd - serializationStart); - Statistics.addOrIncrementEntry( - "smt_unsat_solving_time(millisec)", solvingEnd - solvingStart); - - // System.err.println(); - // System.err.println("Unsatisfiable constraints: " + String.join(" ", - // unsatConstraintIDs)); - // System.err.println(); - - List unsatConstraints = new ArrayList<>(); - - for (String constraintID : unsatConstraintIDs) { - Constraint c = serializedConstraints.get(constraintID); - // System.err.println(constraintID + " :"); - // System.err.println(c); - // System.err.println(c.getLocation()); - // System.err.println(); - unsatConstraints.add(c); - } - - return unsatConstraints; - } - - private void serializeSMTFileContents() { - // make a fresh solver to contain encodings of the slots - solver = ctx.mkOptimize(); - // make a new buffer to store the serialized smt file contents - smtFileContents = new StringBuffer(); - - // only enable in non-optimizing mode - if (!optimizingMode && getUnsatCore) { - smtFileContents.append("(set-option :produce-unsat-cores true)\n"); - } - - serializationStart = System.currentTimeMillis(); - encodeAllSlots(); - encodeAllConstraints(); - serializationEnd = System.currentTimeMillis(); - - System.err.println("Encoding constraints done!"); - - smtFileContents.append("(check-sat)\n"); - if (!optimizingMode && getUnsatCore) { - smtFileContents.append("(get-unsat-core)\n"); - } else { - smtFileContents.append("(get-model)\n"); - } - - System.err.println("Writing constraints to file: " + constraintsFile); - - writeConstraintsToSMTFile(); - } - - private void writeConstraintsToSMTFile() { - String fileContents = smtFileContents.toString(); - - if (!getUnsatCore) { - // write the constraints to the file for external solver use - FileUtils.writeFile(new File(constraintsFile), fileContents); - } else { - // write the constraints to the file for external solver use - FileUtils.writeFile(new File(constraintsUnsatCoreFile), fileContents); - } - // write a copy in append mode to stats file for later bulk analysis - FileUtils.appendFile(new File(constraintsStatsFile), fileContents); - } - // - // private String generateZ3Constraint(BoolExpr serializedConstraint, String - // constraintSource) { - // Expr simplifiedConstraint = serializedConstraint.simplify(); - // - // if (simplifiedConstraint.isTrue()) { - // // This only works if the BoolExpr is directly the value Z3True. - // // Still a good - // // filter, but doesn't filter enough. - // // EG: (and (= false false) (= false false) (= 0 0) (= 0 0) (= 0 - // // 0)) - // // Skip tautology. - // // System.err.println(" simplified to tautology."); - // return ""; - // } - // - // if (simplifiedConstraint.isFalse()) { - // throw new BugInCF("impossible constraint: " + constraintSource); - // } - // - // // TODO: properly support adding wellformedness constraint as a debug output option - // for unsat dump - // - // return generateZ3Constraint(simplifiedConstraint.toString()); - // } - // - // private String generateZ3Constraint(String clause) { - // return "(assert " + clause + ")" + System.lineSeparator(); - // } - // - // private String generateZ3UnsatCoreConstraint(String clause, String constraintName) { - // return "(assert (! " + clause + " :named " + constraintName + "))" + - // System.lineSeparator(); - // } - // - // private void addConstraint(BoolExpr serializedConstraint, Constraint constraint) { - // Expr simplifiedConstraint = serializedConstraint.simplify(); - // - // if (simplifiedConstraint.isTrue()) { - // // This only works if the BoolExpr is directly the value Z3True. - // // Still a good - // // filter, but doesn't filter enough. - // // EG: (and (= false false) (= false false) (= 0 0) (= 0 0) (= 0 - // // 0)) - // // Skip tautology. - // // System.err.println(" simplified to tautology."); - // return; - // } - // - // if (simplifiedConstraint.isFalse()) { - // final ToStringSerializer toStringSerializer = new ToStringSerializer(false); - // throw new BugInCF( - // "impossible constraint: " - // + constraint.serialize(toStringSerializer) - // + "\nSerialized:\n" - // + serializedConstraint); - // } - // - // solver.Assert(serializedConstraint); - // } - // - // private void addSoftConstraint(Constraint constraint, BoolExpr serializedConstraint) { - // Expr simplifiedConstraint = serializedConstraint.simplify(); - // - // if (simplifiedConstraint.isTrue()) { - // // This only works if the BoolExpr is directly the value Z3True. - // // Still a good - // // filter, but doesn't filter enough. - // // EG: (and (= false false) (= false false) (= 0 0) (= 0 0) (= 0 - // // 0)) - // // Skip tautology. - // // System.err.println(" simplified to tautology."); - // return; - // } - // - // if (simplifiedConstraint.isFalse()) { - // final ToStringSerializer toStringSerializer = new ToStringSerializer(false); - // throw new BugInCF( - // "impossible constraint: " - // + constraint.serialize(toStringSerializer) - // + "\nSerialized:\n" - // + serializedConstraint); - // } - // - // solver.AssertSoft(serializedConstraint); - // } - - protected void encodeAllSlots() { - // preprocess slots - formatTranslator.preAnalyzeSlots(slots); - - // StringBuilder z3SlotDefinitions = new StringBuilder(); - // - // // generate slot definitions - // for (Slot slot : slots) { - // if (slot.isVariable()) { - // String slotDefinition = - // formatTranslator.generateZ3SlotDeclaration((VariableSlot) slot); - // System.err.println(slotDefinition); - // z3SlotDefinitions.append(slotDefinition); - // } - // } - - // generate slot constraints - for (Slot slot : slots) { - if (slot.isVariable()) { - VariableSlot varSlot = (VariableSlot) slot; - - BoolExpr wfConstraint = formatTranslator.encodeSlotWellformnessConstraint(varSlot); - - if (!wfConstraint.simplify().isTrue()) { - solver.Assert(wfConstraint); - } - if (optimizingMode) { - // empty string means no optimization group - solver.AssertSoft( - formatTranslator.encodeSlotPreferenceConstraint(varSlot), 1, ""); - } - } - } - - // solver.toString() also includes "(check-sat)" as the last line, - // remove it - String slotDefinitionsAndConstraints = solver.toString(); - int truncateIndex = slotDefinitionsAndConstraints.lastIndexOf("(check-sat)"); - assert truncateIndex != -1; - - // append slot definitions to overall smt file - smtFileContents.append(slotDefinitionsAndConstraints.substring(0, truncateIndex)); - - // debug use: - // Write Slots to file - FileUtils.appendFile(new File(pathToProject + "/slots.smt"), solver.toString()); - } - - @Override - protected void encodeAllConstraints() { - int current = 1; - - StringBuffer constraintSmtFileContents = new StringBuffer(); - - for (Constraint constraint : constraints) { - // System.err.println("Getting next item."); - - // System.err.println( - // " Serializing Constraint " + current + " / " + total + " : " + - // constraint); - - // if (current % 100 == 0) { - // System.err.println("=== Running GC ==="); - // Runtime.getRuntime().gc(); // trigger garbage collector - // } - - BoolExpr serializedConstraint = constraint.serialize(formatTranslator); - - // System.err.println(" Constraint serialized. "); - - if (serializedConstraint == null) { - // TODO: Should error abort if unsupported constraint detected. - // Currently warning is a workaround for making ontology - // working, as in some cases existential constraints generated. - // Should investigate on this, and change this to ErrorAbort - // when eliminated unsupported constraints. - System.err.println( - "Unsupported constraint detected! Constraint type: " - + constraint.getClass().getSimpleName()); - // current++; - continue; - } - - // System.err.println(" Constraint \n" + serializedConstraint - // + "\n simplified :\n " + serializedConstraint.simplify()); - - Expr simplifiedConstraint = serializedConstraint.simplify(); - - if (simplifiedConstraint.isTrue()) { - // This only works if the BoolExpr is directly the value Z3True. - // Still a good - // filter, but doesn't filter enough. - // EG: (and (= false false) (= false false) (= 0 0) (= 0 0) (= 0 - // 0)) - // Skip tautology. - // System.err.println(" simplified to tautology."); - current++; - continue; - } - - if (simplifiedConstraint.isFalse()) { - final ToStringSerializer toStringSerializer = new ToStringSerializer(false); - throw new BugInCF( - "impossible constraint: " - + constraint.serialize(toStringSerializer) - + "\nSerialized:\n" - + serializedConstraint); - } - - String clause = simplifiedConstraint.toString(); - - if (!optimizingMode && getUnsatCore) { - // add assertions with names, for unsat core dump - String constraintName = constraint.getClass().getSimpleName() + current; - - constraintSmtFileContents.append("(assert (! "); - constraintSmtFileContents.append(clause); - constraintSmtFileContents.append(" :named " + constraintName + "))\n"); - - // add constraint to serialized constraints map, so that we can - // retrieve later using - // the constraint name when outputting the unsat core - serializedConstraints.put(constraintName, constraint); - } else { - constraintSmtFileContents.append("(assert "); - constraintSmtFileContents.append(clause); - constraintSmtFileContents.append(")\n"); - } - - // generate a soft constraint that we prefer equality for subtype - // TODO: perhaps prefer not bottom and prefer not top will suffice? - if (optimizingMode && constraint instanceof SubtypeConstraint) { - SubtypeConstraint stc = (SubtypeConstraint) constraint; - - Constraint eqc = - InferenceMain.getInstance() - .getConstraintManager() - .createEqualityConstraint(stc.getSubtype(), stc.getSupertype()); - - Expr simplifiedEQC = eqc.serialize(formatTranslator).simplify(); - - if (!simplifiedEQC.isTrue()) { - constraintSmtFileContents.append("(assert-soft "); - constraintSmtFileContents.append(simplifiedEQC); - constraintSmtFileContents.append(" :weight 1)\n"); - } - } - - // generate soft constraint for comparisons that their args are - // equal - if (optimizingMode && constraint instanceof ComparableConstraint) { - ComparableConstraint cc = (ComparableConstraint) constraint; - - Constraint eqc = - InferenceMain.getInstance() - .getConstraintManager() - .createEqualityConstraint(cc.getFirst(), cc.getSecond()); - - Expr simplifiedEQC = eqc.serialize(formatTranslator).simplify(); - - if (!simplifiedEQC.isTrue()) { - constraintSmtFileContents.append("(assert-soft "); - constraintSmtFileContents.append(simplifiedEQC); - constraintSmtFileContents.append(" :weight 1)\n"); - } - } - - current++; - // System.err.println(" Added constraint. HasNext? " + - // iter.hasNext()); - } - - String constraintSmt = constraintSmtFileContents.toString(); - - smtFileContents.append(constraintSmt); - - // debug use - // Write Constraints to file - FileUtils.appendFile(new File(pathToProject + "/constraints.smt"), constraintSmt); - } - - private List runZ3Solver() { - // TODO: add z3 stats? - String[] command; - if (!getUnsatCore) { - command = new String[] {z3Program, constraintsFile}; - } else { - command = new String[] {z3Program, constraintsUnsatCoreFile}; - } - - // TODO: build Typecheckunits here? - // Map solutionSlots = new HashMap<>(); - - // stores results from z3 program output - final List results = new ArrayList<>(); - - // Run command - // TODO: check that stdErr has no errors - int exitStatus = - ExternalSolverUtils.runExternalSolver( - command, - stdOut -> parseStdOut(stdOut, results), - stdErr -> ExternalSolverUtils.printStdStream(System.err, stdErr)); - // if exit status from z3 is not 0, then it is unsat - return exitStatus == 0 ? results : null; - } - - // Sample satisfying output format: - /* @formatter:off // this is for eclipse formatter */ - /* - sat - (model - (define-fun |338-BOT| () Bool - false) - (define-fun |509-TOP| () Bool - false) - (define-fun |750-m| () Int - (- 9)) - (define-fun |355-s| () Int - 0) - (define-fun |790-PREFIX| () Int - 0) - ) - */ - /* @formatter:on // this is for eclipse formatter */ - - // Sample unsat output format: - /* @formatter:off // this is for eclipse formatter */ - /* - unsat - (SubtypeConstraint58 ArithmeticConstraint73 EqualityConstraint188 SubtypeConstraint553) - */ - /* @formatter:on // this is for eclipse formatter */ - - // parses the STD output from the z3 process and handles SAT and UNSAT - // outputs - private void parseStdOut(BufferedReader stdOut, List results) { - String line = ""; - - boolean declarationLine = true; - // each result line is "varName value" - String resultsLine = ""; - - boolean unsat = false; - - try { - while ((line = stdOut.readLine()) != null) { - line = line.trim(); - - if (getUnsatCore) { - // UNSAT Cases ==================== - if (line.contentEquals("unsat")) { - unsat = true; - continue; - } - if (unsat) { - if (line.startsWith("(")) { - line = line.substring(1); // remove open bracket - } - if (line.endsWith(")")) { - line = line.substring(0, line.length() - 1); - } - - for (String constraintID : line.split(" ")) { - unsatConstraintIDs.add(constraintID); - } - continue; - } - } else { - // SAT Cases ======================= - // processing define-fun lines - if (declarationLine && line.startsWith("(define-fun")) { - declarationLine = false; - - int firstBar = line.indexOf('|'); - int lastBar = line.lastIndexOf('|'); - - assert firstBar != -1; - assert lastBar != -1; - assert firstBar < lastBar; - assert line.contains("Bool") || line.contains("Int"); - - // copy z3 variable name into results line - resultsLine += line.substring(firstBar + 1, lastBar); - continue; - } - // processing lines immediately following define-fun lines - if (!declarationLine) { - declarationLine = true; - String value = line.substring(0, line.lastIndexOf(')')); - - if (value.contains("-")) { // negative number - // remove brackets surrounding negative numbers - value = value.substring(1, value.length() - 1); - // remove space between - and the number itself - value = String.join("", value.split(" ")); - } - - resultsLine += " " + value; - results.add(resultsLine); - resultsLine = ""; - continue; - } - } - } - } catch (IOException e) { - e.printStackTrace(); - } - } -} diff --git a/src/backend/z3smt/Z3SmtSolverFactory.java b/src/backend/z3smt/Z3SmtSolverFactory.java deleted file mode 100644 index f280f5b..0000000 --- a/src/backend/z3smt/Z3SmtSolverFactory.java +++ /dev/null @@ -1,25 +0,0 @@ -package backend.z3smt; - -import checkers.inference.model.Constraint; -import checkers.inference.model.Slot; -import checkers.inference.solver.backend.AbstractSolverFactory; -import checkers.inference.solver.backend.Solver; -import checkers.inference.solver.frontend.Lattice; -import checkers.inference.solver.util.SolverEnvironment; -import java.util.Collection; - -public abstract class Z3SmtSolverFactory - extends AbstractSolverFactory> { - - @Override - public Solver createSolver( - SolverEnvironment solverEnvironment, - Collection slots, - Collection constraints, - Lattice lattice) { - Z3SmtFormatTranslator formatTranslator = - createFormatTranslator(lattice); - return new Z3SmtSolver( - solverEnvironment, slots, constraints, formatTranslator, lattice); - } -} diff --git a/src/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java b/src/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java deleted file mode 100644 index badc64b..0000000 --- a/src/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java +++ /dev/null @@ -1,25 +0,0 @@ -package backend.z3smt.encoder; - -import backend.z3smt.Z3SmtFormatTranslator; -import checkers.inference.solver.backend.encoder.AbstractConstraintEncoder; -import checkers.inference.solver.frontend.Lattice; -import com.microsoft.z3.BoolExpr; -import com.microsoft.z3.Context; - -/** Abstract base class for every Z3Int constraint encoders. */ -public class Z3SmtAbstractConstraintEncoder - extends AbstractConstraintEncoder { - - protected final Context ctx; - protected final Z3SmtFormatTranslator z3SmtFormatTranslator; - - public Z3SmtAbstractConstraintEncoder( - Lattice lattice, - Context ctx, - Z3SmtFormatTranslator z3SmtFormatTranslator) { - // empty value is z3True, contradictory value is z3False - super(lattice, ctx.mkTrue(), ctx.mkFalse()); - this.ctx = ctx; - this.z3SmtFormatTranslator = z3SmtFormatTranslator; - } -} diff --git a/src/backend/z3smt/encoder/Z3SmtConstraintEncoderFactory.java b/src/backend/z3smt/encoder/Z3SmtConstraintEncoderFactory.java deleted file mode 100644 index 6e79ba6..0000000 --- a/src/backend/z3smt/encoder/Z3SmtConstraintEncoderFactory.java +++ /dev/null @@ -1,28 +0,0 @@ -package backend.z3smt.encoder; - -import backend.z3smt.Z3SmtFormatTranslator; -import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; -import checkers.inference.solver.frontend.Lattice; -import com.microsoft.z3.BoolExpr; -import com.microsoft.z3.Context; - -/** - * Abstract Z3 implementation of {@link - * checkers.inference.solver.backend.encoder.ConstraintEncoderFactory} for integer theory. - * Subclasses must specify the exact encoders used. - * - * @see checkers.inference.solver.backend.encoder.ConstraintEncoderFactory - */ -public abstract class Z3SmtConstraintEncoderFactory - extends AbstractConstraintEncoderFactory< - BoolExpr, Z3SmtFormatTranslator> { - protected final Context ctx; - - public Z3SmtConstraintEncoderFactory( - Lattice lattice, - Context ctx, - Z3SmtFormatTranslator z3SmtFormatTranslator) { - super(lattice, z3SmtFormatTranslator); - this.ctx = ctx; - } -} diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index f94f770..6ddfc74 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -1,6 +1,7 @@ package units; import com.sun.source.tree.BinaryTree; +import com.sun.source.tree.LiteralTree; import com.sun.source.tree.Tree.Kind; import java.lang.annotation.Annotation; import java.util.HashSet; @@ -13,6 +14,7 @@ import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.qual.LiteralKind; import org.checkerframework.framework.qual.TypeUseLocation; +import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeFormatter; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotationClassLoader; @@ -21,6 +23,9 @@ import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; +import org.checkerframework.framework.type.typeannotator.DefaultForTypeAnnotator; +import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator; +import org.checkerframework.framework.type.typeannotator.TypeAnnotator; import org.checkerframework.framework.util.AnnotationFormatter; import org.checkerframework.framework.util.GraphQualifierHierarchy; import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; @@ -43,11 +48,6 @@ public UnitsAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker, true); unitsRepUtils = UnitsRepresentationUtils.getInstance(processingEnv, elements); postInit(); - - // add implicits for exceptions - addTypeNameImplicit(java.lang.Exception.class, unitsRepUtils.DIMENSIONLESS); - addTypeNameImplicit(java.lang.Throwable.class, unitsRepUtils.DIMENSIONLESS); - addTypeNameImplicit(java.lang.Void.class, unitsRepUtils.BOTTOM); } @Override @@ -350,12 +350,13 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { @Override public TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( - new UnitsTypecheckImplicitsTreeAnnotator(), new UnitsPropagationTreeAnnotator()); + new UnitsTypecheckLiteralTreeAnnotator(), + new UnitsPropagationTreeAnnotator()); } - protected final class UnitsTypecheckImplicitsTreeAnnotator extends UnitsImplicitsTreeAnnotator { + protected final class UnitsTypecheckLiteralTreeAnnotator extends UnitsLiteralTreeAnnotator { // Programmatically set the qualifier implicits - public UnitsTypecheckImplicitsTreeAnnotator() { + public UnitsTypecheckLiteralTreeAnnotator() { super(UnitsAnnotatedTypeFactory.this); // in type checking mode, we also set dimensionless for the number literals addLiteralKind(LiteralKind.INT, unitsRepUtils.DIMENSIONLESS); @@ -369,6 +370,12 @@ private final class UnitsPropagationTreeAnnotator extends PropagationTreeAnnotat public UnitsPropagationTreeAnnotator() { super(UnitsAnnotatedTypeFactory.this); } + + @Override + public Void visitLiteral(LiteralTree tree, AnnotatedTypeMirror type) { + + return super.visitLiteral(tree, type); + } @Override public Void visitBinary(BinaryTree binaryTree, AnnotatedTypeMirror type) { @@ -433,6 +440,24 @@ public Void visitBinary(BinaryTree binaryTree, AnnotatedTypeMirror type) { return null; } } + + @Override + protected TypeAnnotator createTypeAnnotator() { + return new ListTypeAnnotator( + new UnitsDefaultForTypeAnnotator(this), super.createTypeAnnotator()); + } + + protected class UnitsDefaultForTypeAnnotator extends DefaultForTypeAnnotator { + // Programmatically set the qualifier + public UnitsDefaultForTypeAnnotator(AnnotatedTypeFactory atf) { + super(atf); + + // add defaults for exceptions + addTypes(java.lang.Exception.class, unitsRepUtils.DIMENSIONLESS); + addTypes(java.lang.Throwable.class, unitsRepUtils.DIMENSIONLESS); + addTypes(java.lang.Void.class, unitsRepUtils.BOTTOM); + } + } // for use in AnnotatedTypeMirror.toString() @Override diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index b652d17..3c942b3 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -300,14 +300,14 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { @Override public TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( - new UnitsInferenceImplicitsTreeAnnotator(), + new UnitsInferenceLiteralTreeAnnotator(), new UnitsInferenceTreeAnnotator( this, realChecker, realTypeFactory, variableAnnotator, slotManager)); } - protected final class UnitsInferenceImplicitsTreeAnnotator extends UnitsImplicitsTreeAnnotator { + protected final class UnitsInferenceLiteralTreeAnnotator extends UnitsLiteralTreeAnnotator { // Programmatically set the qualifier implicits - public UnitsInferenceImplicitsTreeAnnotator() { + public UnitsInferenceLiteralTreeAnnotator() { super(UnitsInferenceAnnotatedTypeFactory.this); // in inference mode, we do not implicitly set dimensionless for the number // literals as we want to treat them as polymorphic. A "cast" is inferred for @@ -391,7 +391,7 @@ private void generateVarSlotForStaticFinalConstants( // Generate a fresh variable for inference AnnotationLocation loc = VariableAnnotator.treeToLocation(atypeFactory, tree); - VariableSlot varSlot = slotManager.createVariableSlot(loc); + VariableSlot varSlot = slotManager.createVariableSlot(loc, atm.getUnderlyingType()); atm.replaceAnnotation(slotManager.getAnnotation(varSlot)); } } diff --git a/src/units/UnitsImplicitsTreeAnnotator.java b/src/units/UnitsLiteralTreeAnnotator.java similarity index 56% rename from src/units/UnitsImplicitsTreeAnnotator.java rename to src/units/UnitsLiteralTreeAnnotator.java index c09524c..ef4cbec 100644 --- a/src/units/UnitsImplicitsTreeAnnotator.java +++ b/src/units/UnitsLiteralTreeAnnotator.java @@ -2,25 +2,25 @@ import org.checkerframework.framework.qual.LiteralKind; import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.type.treeannotator.ImplicitsTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; import units.representation.UnitsRepresentationUtils; -/** Common base class for ImplicitsTreeAnnotator. */ -public abstract class UnitsImplicitsTreeAnnotator extends ImplicitsTreeAnnotator { +/** Common base class for LiteralTreeAnnotator. */ +public abstract class UnitsLiteralTreeAnnotator extends LiteralTreeAnnotator { UnitsRepresentationUtils unitsRepUtils = UnitsRepresentationUtils.getInstance(); - // Programmatically set the qualifier implicits - public UnitsImplicitsTreeAnnotator(AnnotatedTypeFactory atf) { + // Programmatically set the qualifier for literals + public UnitsLiteralTreeAnnotator(AnnotatedTypeFactory atf) { super(atf); - // set BOTTOM as the implicit qualifier for null literals + // set BOTTOM as the literal qualifier for null literals addLiteralKind(LiteralKind.NULL, unitsRepUtils.BOTTOM); addLiteralKind(LiteralKind.STRING, unitsRepUtils.DIMENSIONLESS); addLiteralKind(LiteralKind.CHAR, unitsRepUtils.DIMENSIONLESS); addLiteralKind(LiteralKind.BOOLEAN, unitsRepUtils.DIMENSIONLESS); - // TODO: set BOTTOM as the implicit qualifier for lower bounds? Its nice to + // TODO: set BOTTOM as the literal qualifier for lower bounds? Its nice to // infer a bound which is the current mode. } } diff --git a/src/units/solvers/backend/gje/encoder/UnitsGJEComparableConstraintEncoder.java b/src/units/solvers/backend/gje/encoder/UnitsGJEComparableConstraintEncoder.java index 2705b76..4b6318a 100644 --- a/src/units/solvers/backend/gje/encoder/UnitsGJEComparableConstraintEncoder.java +++ b/src/units/solvers/backend/gje/encoder/UnitsGJEComparableConstraintEncoder.java @@ -1,5 +1,6 @@ package units.solvers.backend.gje.encoder; +import checkers.inference.model.ComparableConstraint.ComparableOperationKind; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; @@ -38,4 +39,28 @@ public GJEEquationSet encodeVariable_Constant(VariableSlot fst, ConstantSlot snd public GJEEquationSet encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { return encode(fst, snd); } + + @Override + public GJEEquationSet encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, + VariableSlot snd) { + return encode(fst, snd); + } + + @Override + public GJEEquationSet encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, + ConstantSlot snd) { + return encode(fst, snd); + } + + @Override + public GJEEquationSet encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, + VariableSlot snd) { + return encode(fst, snd); + } + + @Override + public GJEEquationSet encodeConstant_Constant(ComparableOperationKind operation, ConstantSlot fst, + ConstantSlot snd) { + return encode(fst, snd); + } } diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java index d0c3245..36ce57f 100644 --- a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java +++ b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java @@ -1,14 +1,12 @@ package units.solvers.backend.z3smt; -import backend.z3smt.Z3SmtFormatTranslator; +import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.ConstraintEncoderFactory; import checkers.inference.solver.frontend.Lattice; import com.microsoft.z3.BoolExpr; -import com.microsoft.z3.IntExpr; -import java.util.ArrayList; import java.util.Collection; import java.util.HashMap; import java.util.HashSet; @@ -52,43 +50,6 @@ protected ConstraintEncoderFactory createConstraintEncoderFactory() { return new UnitsZ3SmtConstraintEncoderFactory(lattice, ctx, this); } - @Override - public String generateZ3SlotDeclaration(VariableSlot slot) { - Z3InferenceUnit encodedSlot = serializeVarSlot(slot); - - List slotDeclaration = new ArrayList<>(); - - slotDeclaration.add(addZ3BoolDefinition(encodedSlot.getUnknownUnits())); - slotDeclaration.add(addZ3BoolDefinition(encodedSlot.getUnitsBottom())); - - if (unitsRepUtils.serializePrefix()) { - slotDeclaration.add(addZ3IntDefinition(encodedSlot.getPrefixExponent())); - } - for (String baseUnit : unitsRepUtils.serializableBaseUnits()) { - slotDeclaration.add(addZ3IntDefinition(encodedSlot.getExponent(baseUnit))); - } - - return String.join(System.lineSeparator(), slotDeclaration); - } - - private String addZ3BoolDefinition(BoolExpr z3BoolVariable) { - // gives the assigned variable name generated by - // Z3InferenceUnit.makeVariableSlot(), eg |5-m| - // System.err.println(z3BoolVariable.toString()); - - // (declare-fun |5-TOP| () Bool) - return "(declare-fun " + z3BoolVariable.toString() + " () Bool)"; - } - - private String addZ3IntDefinition(IntExpr z3IntVariable) { - // gives the assigned variable name generated by - // Z3InferenceUnit.makeVariableSlot(), eg |5-m| - // System.err.println(z3IntVariable.toString()); - - // (declare-fun |5-m| () Int) - return "(declare-fun " + z3IntVariable.toString() + " () Int)"; - } - @Override protected Z3InferenceUnit serializeVarSlot(VariableSlot slot) { int slotID = slot.getId(); diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtSolver.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtSolver.java new file mode 100644 index 0000000..0c3f73d --- /dev/null +++ b/src/units/solvers/backend/z3smt/UnitsZ3SmtSolver.java @@ -0,0 +1,58 @@ +package units.solvers.backend.z3smt; + +import java.util.Collection; + +import com.microsoft.z3.Expr; + +import checkers.inference.InferenceMain; +import checkers.inference.model.ComparableConstraint; +import checkers.inference.model.Constraint; +import checkers.inference.model.Slot; +import checkers.inference.model.SubtypeConstraint; +import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; +import checkers.inference.solver.backend.z3smt.Z3SmtSolver; +import checkers.inference.solver.frontend.Lattice; +import checkers.inference.solver.util.SolverEnvironment; +import units.representation.TypecheckUnit; +import units.solvers.backend.z3smt.representation.Z3InferenceUnit; + +public class UnitsZ3SmtSolver extends Z3SmtSolver { + + public UnitsZ3SmtSolver( + SolverEnvironment solverEnvironment, + Collection slots, + Collection constraints, + Z3SmtFormatTranslator z3SmtFormatTranslator, + Lattice lattice) { + super(solverEnvironment, slots, constraints, z3SmtFormatTranslator, lattice); + } + + @Override + protected void encodeSoftSubtypeConstraint(SubtypeConstraint stc) { + Constraint eqc = + InferenceMain.getInstance() + .getConstraintManager() + .createEqualityConstraint(stc.getSubtype(), stc.getSupertype()); + + Expr simplifiedEQC = eqc.serialize(formatTranslator).simplify(); + + if (!simplifiedEQC.isTrue()) { + addSoftConstraint(simplifiedEQC, 1); + } + } + + @Override + protected void encodeSoftComparableConstraint(ComparableConstraint cc) { + Constraint eqc = + InferenceMain.getInstance() + .getConstraintManager() + .createEqualityConstraint(cc.getFirst(), cc.getSecond()); + + Expr simplifiedEQC = eqc.serialize(formatTranslator).simplify(); + + if (!simplifiedEQC.isTrue()) { + addSoftConstraint(simplifiedEQC, 1); + } + } + +} diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtSolverFactory.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtSolverFactory.java index 6da9a60..c2c86e9 100644 --- a/src/units/solvers/backend/z3smt/UnitsZ3SmtSolverFactory.java +++ b/src/units/solvers/backend/z3smt/UnitsZ3SmtSolverFactory.java @@ -1,8 +1,14 @@ package units.solvers.backend.z3smt; -import backend.z3smt.Z3SmtFormatTranslator; -import backend.z3smt.Z3SmtSolverFactory; +import java.util.Collection; + +import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; +import checkers.inference.solver.backend.z3smt.Z3SmtSolverFactory; +import checkers.inference.model.Constraint; +import checkers.inference.model.Slot; +import checkers.inference.solver.backend.Solver; import checkers.inference.solver.frontend.Lattice; +import checkers.inference.solver.util.SolverEnvironment; import units.representation.TypecheckUnit; import units.solvers.backend.z3smt.representation.Z3InferenceUnit; @@ -13,4 +19,15 @@ protected Z3SmtFormatTranslator createFormatTran Lattice lattice) { return new UnitsZ3SmtFormatTranslator(lattice); } + + @Override + public Solver createSolver( + SolverEnvironment solverEnvironment, + Collection slots, + Collection constraints, + Lattice lattice) { + Z3SmtFormatTranslator formatTranslator = + createFormatTranslator(lattice); + return new UnitsZ3SmtSolver(solverEnvironment, slots, constraints, formatTranslator, lattice); + } } diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtArithmeticConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtArithmeticConstraintEncoder.java index d18e681..bc4f9d9 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtArithmeticConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtArithmeticConstraintEncoder.java @@ -1,7 +1,7 @@ package units.solvers.backend.z3smt.encoder; -import backend.z3smt.Z3SmtFormatTranslator; -import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; +import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; +import checkers.inference.solver.backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; import checkers.inference.model.ArithmeticConstraint.ArithmeticOperationKind; import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.ConstantSlot; diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtComparableConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtComparableConstraintEncoder.java index 541dcbb..f6e84c2 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtComparableConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtComparableConstraintEncoder.java @@ -1,7 +1,8 @@ package units.solvers.backend.z3smt.encoder; -import backend.z3smt.Z3SmtFormatTranslator; -import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; +import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; +import checkers.inference.solver.backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; +import checkers.inference.model.ComparableConstraint.ComparableOperationKind; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; @@ -47,4 +48,24 @@ public BoolExpr encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { public BoolExpr encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { return encode(fst, snd); } + + @Override + public BoolExpr encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd) { + return encode(fst, snd); + } + + @Override + public BoolExpr encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd) { + return encode(fst, snd); + } + + @Override + public BoolExpr encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, VariableSlot snd) { + return encode(fst, snd); + } + + @Override + public BoolExpr encodeConstant_Constant(ComparableOperationKind operation, ConstantSlot fst, ConstantSlot snd) { + return encode(fst, snd); + } } diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java index 83b8acc..0c6b8ff 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java @@ -1,7 +1,6 @@ package units.solvers.backend.z3smt.encoder; -import backend.z3smt.Z3SmtFormatTranslator; -import backend.z3smt.encoder.Z3SmtConstraintEncoderFactory; +import checkers.inference.solver.backend.z3smt.encoder.Z3SmtConstraintEncoderFactory; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; @@ -14,6 +13,7 @@ import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; import units.representation.TypecheckUnit; +import units.solvers.backend.z3smt.UnitsZ3SmtFormatTranslator; import units.solvers.backend.z3smt.representation.Z3InferenceUnit; /** @@ -27,7 +27,7 @@ public class UnitsZ3SmtConstraintEncoderFactory public UnitsZ3SmtConstraintEncoderFactory( Lattice lattice, Context ctx, - Z3SmtFormatTranslator z3SmtFormatTranslator) { + UnitsZ3SmtFormatTranslator z3SmtFormatTranslator) { super(lattice, ctx, z3SmtFormatTranslator); } diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEqualityConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEqualityConstraintEncoder.java index 8d1be07..716d6ab 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEqualityConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEqualityConstraintEncoder.java @@ -1,7 +1,7 @@ package units.solvers.backend.z3smt.encoder; -import backend.z3smt.Z3SmtFormatTranslator; -import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; +import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; +import checkers.inference.solver.backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtSubtypeConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtSubtypeConstraintEncoder.java index a4ba018..bfc57bf 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtSubtypeConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtSubtypeConstraintEncoder.java @@ -1,7 +1,7 @@ package units.solvers.backend.z3smt.encoder; -import backend.z3smt.Z3SmtFormatTranslator; -import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; +import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; +import checkers.inference.solver.backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot;