Merge pull request #339 from kszi2/ic3-base

Added IC3

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ic3/Frame.java

@@ -0,0 +1,74 @@
+package hu.bme.mit.theta.analysis.algorithm.ic3;
+
+import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr;
+import hu.bme.mit.theta.core.model.MutableValuation;
+import hu.bme.mit.theta.core.model.Valuation;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.utils.PathUtils;
+import hu.bme.mit.theta.solver.SolverStatus;
+import hu.bme.mit.theta.solver.utils.WithPushPop;
+
+import java.util.*;
+
+import hu.bme.mit.theta.solver.UCSolver;
+
+import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.*;
+import static hu.bme.mit.theta.core.utils.ExprUtils.getConjuncts;
+
+
+public class Frame {
+    private final Frame parent;
+    private final Set<Expr<BoolType>> exprs;
+
+    private final UCSolver solver;
+    private final MonolithicExpr monolithicExpr;
+
+    Frame(final Frame parent, UCSolver solver, MonolithicExpr monolithicExpr) {
+        this.parent = parent;
+        this.solver = solver;
+        this.monolithicExpr=monolithicExpr;
+        exprs = new HashSet<>();
+    }
+
+    public void refine(Expr<BoolType> expression) {
+        Collection<Expr<BoolType>> col = getConjuncts(expression);
+        for (Expr<BoolType> e : col) {
+            exprs.add(e);
+        }
+    }
+
+    public Set<Expr<BoolType>> getExprs() {
+        return exprs;
+    }
+
+    public Collection<Expr<BoolType>> check(Expr<BoolType> target) {
+        try (var wpp = new WithPushPop(solver)) {
+            solver.track(PathUtils.unfold(target, 0));
+            for (Expr<BoolType> ex : exprs) {
+                solver.track(PathUtils.unfold(ex, 0));
+            }
+            SolverStatus status = solver.check();
+
+            if (status.isSat()) {
+                final Valuation model = solver.getModel();
+                final MutableValuation filteredModel = new MutableValuation();
+                monolithicExpr.getVars().stream().map(varDecl -> varDecl.getConstDecl(0)).filter(model.toMap()::containsKey).forEach(decl -> filteredModel.put(decl, model.eval(decl).get()));
+                return getConjuncts(PathUtils.foldin(filteredModel.toExpr(), 0));
+            } else {
+                return null;
+            }
+        }
+    }
+
+    public boolean equalsParent() {
+        if (this.parent.parent == null) {
+            return false;
+        }
+        try (var wpp = new WithPushPop(solver)) {
+            solver.track(PathUtils.unfold(Not(And(parent.getExprs())), 0));
+            solver.track(PathUtils.unfold(And(exprs), 0));
+            return solver.check().isUnsat();
+        }
+    }
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ic3/Ic3Checker.java

@@ -0,0 +1,287 @@
+package hu.bme.mit.theta.analysis.algorithm.ic3;
+
+import hu.bme.mit.theta.analysis.Trace;
+import hu.bme.mit.theta.analysis.algorithm.EmptyProof;
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr;
+import hu.bme.mit.theta.analysis.expr.ExprAction;
+import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.analysis.unit.UnitPrec;
+import hu.bme.mit.theta.core.model.MutableValuation;
+import hu.bme.mit.theta.core.model.Valuation;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.LitExpr;
+import hu.bme.mit.theta.core.type.anytype.RefExpr;
+import hu.bme.mit.theta.core.type.booltype.BoolLitExpr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.utils.PathUtils;
+import hu.bme.mit.theta.solver.SolverFactory;
+import hu.bme.mit.theta.solver.UCSolver;
+import hu.bme.mit.theta.solver.utils.WithPushPop;
+
+import java.util.*;
+import java.util.function.BiFunction;
+import java.util.function.Function;
+
+import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.*;
+import static hu.bme.mit.theta.core.utils.ExprUtils.getConjuncts;
+
+
+public class Ic3Checker<S extends ExprState, A extends ExprAction> implements SafetyChecker<EmptyProof, Trace<S, A>, UnitPrec> {
+    private final MonolithicExpr monolithicExpr;
+    private final List<Frame> frames;
+    private final UCSolver solver;
+    private final Function<Valuation, S> valToState;
+    private final BiFunction<Valuation, Valuation, A> biValToAction;
+    private final boolean formerFramesOpt;
+    private final boolean unSatOpt;
+    private final boolean notBOpt;
+    private final boolean propagateOpt;
+    private final boolean filterOpt;
+    private int currentFrameNumber;
+    private final boolean forwardTrace;
+    private final boolean propertyOpt;
+
+    public Ic3Checker(MonolithicExpr monolithicExpr, boolean forwardTrace, SolverFactory solverFactory, Function<Valuation, S> valToState, BiFunction<Valuation, Valuation, A> biValToAction) {
+        this(monolithicExpr, forwardTrace, solverFactory, valToState, biValToAction, true, true, true, true, true, false);
+    }
+
+    public Ic3Checker(MonolithicExpr monolithicExpr, boolean forwardTrace, SolverFactory solverFactory, Function<Valuation, S> valToState, BiFunction<Valuation, Valuation, A> biValToAction, boolean formerFramesOpt, boolean unSatOpt, boolean notBOpt, boolean propagateOpt, boolean filterOpt, boolean propertyOpt) {
+        this.monolithicExpr = monolithicExpr;
+        this.valToState = valToState;
+        this.biValToAction = biValToAction;
+        this.formerFramesOpt = formerFramesOpt;
+        this.unSatOpt = unSatOpt;
+        this.notBOpt = notBOpt;
+        this.propagateOpt = propagateOpt;
+        this.filterOpt = filterOpt;
+        this.forwardTrace = forwardTrace;
+        this.propertyOpt = propertyOpt;
+        frames = new ArrayList<>();
+        solver = solverFactory.createUCSolver();
+        frames.add(new Frame(null, solver, monolithicExpr));
+        frames.get(0).refine(monolithicExpr.getInitExpr());
+        currentFrameNumber = 0;
+    }
+
+
+    @Override
+    public SafetyResult<EmptyProof, Trace<S, A>> check(UnitPrec prec) {
+        //check if init violates prop
+        var firstTrace = checkFirst();
+        if (firstTrace != null) {
+            return SafetyResult.unsafe(firstTrace, EmptyProof.getInstance());
+        }
+        while (true) {
+            final Collection<Expr<BoolType>> counterExample = checkCurrentFrame(Not(monolithicExpr.getPropExpr()));
+            if (counterExample != null) {
+                var proofObligationsList = tryBlock(new ProofObligation(new HashSet<>(counterExample), currentFrameNumber));
+                if (proofObligationsList != null) {
+                    var trace = traceMaker(proofObligationsList);
+                    return SafetyResult.unsafe(trace, EmptyProof.getInstance());
+                }
+            } else {
+                if (propagate()) {
+                    return SafetyResult.safe(EmptyProof.getInstance());
+                }
+            }
+        }
+    }
+
+    LinkedList<ProofObligation> tryBlock(ProofObligation mainProofObligation) {
+        final LinkedList<ProofObligation> proofObligationsQueue = new LinkedList<ProofObligation>();
+        proofObligationsQueue.add(mainProofObligation);
+        while (!proofObligationsQueue.isEmpty()) {
+            final ProofObligation proofObligation = proofObligationsQueue.getLast();
+
+            if (proofObligation.getTime() == 0) {
+                return proofObligationsQueue;
+            }
+
+            final Collection<Expr<BoolType>> b;
+            final Collection<Expr<BoolType>> unSatCore;
+            try (var wpp = new WithPushPop(solver)) {
+
+                frames.get(proofObligation.getTime() - 1).getExprs().forEach(ex -> solver.track(PathUtils.unfold(ex, 0)));
+                if (notBOpt) {
+                    solver.track(PathUtils.unfold(Not(And(proofObligation.getExpressions())), 0));
+                }
+                if (proofObligation.getTime() > 2 && formerFramesOpt) { //lehet, hogy 1, vagy 2??
+                    solver.track(PathUtils.unfold(Not(And(frames.get(proofObligation.getTime() - 2).getExprs())), monolithicExpr.getTransOffsetIndex())); //2 vel korábbi frame-ban levő dolgok
+                }
+
+                getConjuncts(monolithicExpr.getTransExpr()).forEach(ex -> solver.track(PathUtils.unfold(ex, 0)));
+                proofObligation.getExpressions().forEach(ex -> solver.track(PathUtils.unfold(ex, monolithicExpr.getTransOffsetIndex())));
+
+                if (solver.check().isSat()) {
+                    final Valuation model = solver.getModel();
+
+                    final MutableValuation filteredModel = new MutableValuation();
+                    monolithicExpr.getVars().stream().map(varDecl -> varDecl.getConstDecl(0)).filter(model.toMap()::containsKey).forEach(decl -> filteredModel.put(decl, model.eval(decl).get()));
+                    if (filterOpt) {
+                        var vars = new HashSet<>(filteredModel.toMap().keySet());
+                        for (var var : vars) {
+                            if (!(var.getType() instanceof BoolType)) {
+                                continue;
+                            }
+                            var origValue = model.eval(var).get();
+                            var negatedValue = BoolLitExpr.of(!((BoolLitExpr) origValue).getValue());
+                            filteredModel.put(var, negatedValue);
+                            try (var wpp2 = new WithPushPop(solver)) {
+                                solver.track(PathUtils.unfold(filteredModel.toExpr(), 0));
+                                if (solver.check().isSat()) {
+                                    filteredModel.remove(var);
+                                } else {
+                                    filteredModel.put(var, origValue);
+                                }
+                            }
+                        }
+                    }
+                    b = getConjuncts(PathUtils.foldin(PathUtils.extractValuation(filteredModel, 0).toExpr(), 0));
+                    unSatCore = null;
+                } else {
+                    b = null;
+                    unSatCore = solver.getUnsatCore();
+                }
+            }
+            if (b == null) {
+
+                final Collection<Expr<BoolType>> newCore = new ArrayList<Expr<BoolType>>();
+                newCore.addAll(proofObligation.getExpressions());
+                if (unSatOpt) {
+                    for (Expr<BoolType> i : proofObligation.getExpressions()) {
+                        if (!unSatCore.contains(PathUtils.unfold(i, monolithicExpr.getTransOffsetIndex()))) {
+                            newCore.remove(i);
+                            final boolean isSat;
+                            try (var wpp = new WithPushPop(solver)) {
+                                for (Expr<BoolType> solverex : newCore) {
+                                    solver.track(PathUtils.unfold(solverex, 0));
+                                }
+                                solver.track(PathUtils.unfold(monolithicExpr.getInitExpr(), 0));
+                                isSat = solver.check().isSat();
+                            }
+                            if (isSat) {
+                                newCore.add(i);
+                            }
+                        }
+                    }
+                }
+                for (int i = 1; i <= proofObligation.getTime(); ++i) {
+                    frames.get(i).refine(Not(And(newCore))); 
+                }
+                proofObligationsQueue.removeLast();
+            } else {
+                proofObligationsQueue.add(new ProofObligation(new HashSet<>(b), proofObligation.getTime() - 1));
+            }
+        }
+        return null;
+
+    }
+
+    public Trace<S, A> checkFirst() {
+        try (var wpp = new WithPushPop(solver)) {
+            solver.track(PathUtils.unfold(monolithicExpr.getInitExpr(), 0));
+            solver.track(PathUtils.unfold(Not(monolithicExpr.getPropExpr()), 0));
+            if (solver.check().isSat()) {
+                return Trace.of(List.of(valToState.apply(solver.getModel())), List.of());
+            }
+        }
+        if (propertyOpt) {
+            try (var wpp = new WithPushPop(solver)) {
+                solver.track(PathUtils.unfold(monolithicExpr.getInitExpr(), 0));
+                solver.track(PathUtils.unfold(monolithicExpr.getTransExpr(), 0));
+                solver.track(PathUtils.unfold(Not(monolithicExpr.getPropExpr()), monolithicExpr.getTransOffsetIndex()));
+                if (solver.check().isSat()) {
+                    return Trace.of(List.of(valToState.apply(solver.getModel())), List.of());
+                } else {
+                    return null;
+                }
+            }
+        } else {
+            return null;
+        }
+
+    }
+
+    public Collection<Expr<BoolType>> checkCurrentFrame(Expr<BoolType> target) {
+        if (propertyOpt) {
+            try (var wpp = new WithPushPop(solver)) {
+                frames.get(currentFrameNumber).getExprs().forEach(ex -> solver.track(PathUtils.unfold(ex, 0)));
+                getConjuncts(monolithicExpr.getTransExpr()).forEach(ex -> solver.track(PathUtils.unfold(ex, 0)));
+                solver.track(PathUtils.unfold(target, monolithicExpr.getTransOffsetIndex()));
+                if (solver.check().isSat()) {
+                    final Valuation model = solver.getModel();
+                    final MutableValuation filteredModel = new MutableValuation();
+                    monolithicExpr.getVars().stream().map(varDecl -> varDecl.getConstDecl(0)).filter(model.toMap()::containsKey).forEach(decl -> filteredModel.put(decl, model.eval(decl).get()));
+                    return getConjuncts(PathUtils.foldin(filteredModel.toExpr(), 0));
+                } else {
+                    return null;
+                }
+            }
+        } else {
+            return frames.get(currentFrameNumber).check(target);
+        }
+
+    }
+
+    public boolean propagate() {
+        frames.add(new Frame(frames.get(currentFrameNumber), solver, monolithicExpr));
+        currentFrameNumber++;
+        if (propertyOpt) {
+            for (int j = 1; j <= currentFrameNumber; j++) {
+                frames.get(j).refine(monolithicExpr.getPropExpr());
+            }
+        }
+
+        if (propagateOpt) {
+            for (int j = 1; j < currentFrameNumber; j++) {
+                for (var c : frames.get(j).getExprs()) {
+                    try (var wpp = new WithPushPop(solver)) {
+                        frames.get(j).getExprs().forEach(ex -> solver.track(PathUtils.unfold(ex, 0)));
+                        getConjuncts(monolithicExpr.getTransExpr()).forEach(ex -> solver.track(PathUtils.unfold(ex, 0)));
+                        solver.track(PathUtils.unfold(Not(c), monolithicExpr.getTransOffsetIndex()));
+                        if (solver.check().isUnsat()) {
+                            frames.get(j + 1).refine(c);
+                        }
+                    }
+                }
+                if (frames.get(j + 1).equalsParent()) {
+                    return true;
+                }
+            }
+        } else if (currentFrameNumber > 1 && frames.get(currentFrameNumber - 1).equalsParent()) {
+            return true;
+        }
+        return false;
+    }
+
+    public Trace<S, A> traceMaker(LinkedList<ProofObligation> forwardProofObligations) {
+        var stateList = new ArrayList<S>();
+        var actionList = new ArrayList<A>();
+        Valuation lastValuation = null;
+        while (!forwardProofObligations.isEmpty()) {
+            final ProofObligation currentProofObligation;
+            if (forwardTrace) {
+                currentProofObligation = forwardProofObligations.getLast();
+                forwardProofObligations.removeLast();
+            } else {
+                currentProofObligation = forwardProofObligations.getFirst();
+                forwardProofObligations.removeFirst();
+            }
+            MutableValuation mutableValuation = new MutableValuation();
+            for (Expr<BoolType> ex : currentProofObligation.getExpressions()) {
+                RefExpr<BoolType> refExpr = (RefExpr<BoolType>) ex.getOps().get(0);
+                LitExpr<BoolType> litExpr = (LitExpr<BoolType>) ex.getOps().get(1);
+                mutableValuation.put(refExpr.getDecl(), litExpr);
+
+            }
+            stateList.add(valToState.apply(mutableValuation));
+            if (lastValuation != null) {
+                actionList.add(biValToAction.apply(lastValuation, mutableValuation));
+            }
+            lastValuation = mutableValuation;
+        }
+        return Trace.of(stateList, actionList);
+    }
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ic3/ProofObligation.java

@@ -0,0 +1,23 @@
+package hu.bme.mit.theta.analysis.algorithm.ic3;
+
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+
+import java.util.Set;
+
+public class ProofObligation {
+    private Set<Expr<BoolType>> expressions;
+    private int time;
+    ProofObligation(Set<Expr<BoolType>> expressions, int time){
+        this.expressions = expressions;
+        this.time = time;
+    }
+
+    public int getTime() {
+        return time;
+    }
+
+    public Set<Expr<BoolType>> getExpressions() {
+        return expressions;
+    }
+}