Skip to content

[DRAFT] Non-incremental solving #974

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
ThomasHaas wants to merge 1 commit into from
Closed

[DRAFT] Non-incremental solving #974

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,9 @@ public class OptionNames {
public static final String GRAPHVIZ_DEBUG_FILES = "refinement.generateGraphvizDebugFiles";
public static final String SYMMETRIC_LEARNING = "refinement.symmetricLearning";

// Eager SMT Options
public static final String INCREMENTAL_SOLVING = "eager.incremental";

// SMT solver Options
public static final String PHANTOM_REFERENCES = "solver.z3.usePhantomReferences";

Expand Down
117 changes: 86 additions & 31 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,31 +1,41 @@
package com.dat3m.dartagnan.verification.solving;


import com.dat3m.dartagnan.configuration.OptionNames;
import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.encoding.*;
import com.dat3m.dartagnan.smt.ProverWithTracker;
import com.dat3m.dartagnan.utils.Result;
import com.dat3m.dartagnan.verification.Context;
import com.dat3m.dartagnan.verification.VerificationTask;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.configuration.Option;
import org.sosy_lab.common.configuration.Options;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.BooleanFormulaManager;
import org.sosy_lab.java_smt.api.SolverContext;
import org.sosy_lab.java_smt.api.SolverException;

import static com.dat3m.dartagnan.utils.Result.FAIL;
import static com.dat3m.dartagnan.utils.Result.PASS;
import static com.dat3m.dartagnan.utils.Result.*;
import static java.util.Collections.singletonList;

@Options
public class AssumeSolver extends ModelChecker {


private static final Logger logger = LoggerFactory.getLogger(AssumeSolver.class);

@Option(name = OptionNames.INCREMENTAL_SOLVING,
description = "If true (default), the solver will run in incremental mode.",
secure = true
)
private boolean incremental = true;

private AssumeSolver(VerificationTask task) throws InvalidConfigurationException {
super(task);
task.getConfig().inject(this);
}

public static AssumeSolver create(VerificationTask task) throws InvalidConfigurationException {
Expand All @@ -50,52 +60,97 @@ protected void runInternal() throws InterruptedException, SolverException, Inval

initSMTSolver(task.getConfig());
final SolverContext solverContext = this.solverContext;
final ProverWithTracker prover = this.prover;

context = EncodingContext.of(task, analysisContext, solverContext.getFormulaManager());
ProgramEncoder programEncoder = ProgramEncoder.withContext(context);
PropertyEncoder propertyEncoder = PropertyEncoder.withContext(context);
WmmEncoder wmmEncoder = WmmEncoder.withContext(context);
SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context);
final ProgramEncoder programEncoder = ProgramEncoder.withContext(context);
final PropertyEncoder propertyEncoder = PropertyEncoder.withContext(context);
final WmmEncoder wmmEncoder = WmmEncoder.withContext(context);
final SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context);

logger.info("Starting encoding using {}", solverContext.getVersion());
final BooleanFormula progEnc = programEncoder.encodeFullProgram();
final BooleanFormula wmmEnc = wmmEncoder.encodeFullMemoryModel();
final BooleanFormula witnessEnc = task.getWitness().encode(context);
final BooleanFormula symEnc = symmetryEncoder.encodeFullSymmetryBreaking();
final BooleanFormula propertyEnc = propertyEncoder.encodeProperties(task.getProperty());

final ProverWithTracker prover = this.prover;
prover.writeComment("Program encoding");
prover.addConstraint(programEncoder.encodeFullProgram());
prover.addConstraint(progEnc);
prover.writeComment("Memory model encoding");
prover.addConstraint(wmmEncoder.encodeFullMemoryModel());
prover.addConstraint(wmmEnc);
// For validation this contains information.
// For verification graph.encode() just returns ctx.mkTrue()
prover.writeComment("Witness encoding");
prover.addConstraint(task.getWitness().encode(context));
prover.addConstraint(witnessEnc);
prover.writeComment("Symmetry breaking encoding");
prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking());

BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
BooleanFormula assumptionLiteral = bmgr.makeVariable("DAT3M_spec_assumption");
BooleanFormula propertyEncoding = propertyEncoder.encodeProperties(task.getProperty());
BooleanFormula assumedSpec = bmgr.implication(assumptionLiteral, propertyEncoding);
prover.writeComment("Property encoding");
prover.addConstraint(assumedSpec);
prover.addConstraint(symEnc);

checkForInterrupts();

logger.info("Starting first solver.check()");
if (prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) {
checkForInterrupts();
prover.writeComment("Bound encoding");
prover.addConstraint(propertyEncoder.encodeBoundEventExec());
logger.info("Starting second solver.check()");
res = prover.isUnsat() ? PASS : Result.UNKNOWN;
if (incremental) {
final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
final BooleanFormula assumptionLiteral = bmgr.makeVariable("DAT3M_spec_assumption");
final BooleanFormula assumedSpec = bmgr.implication(assumptionLiteral, propertyEnc);
prover.writeComment("Property encoding");
prover.addConstraint(assumedSpec);

logger.info("Starting first solver.check()");
if (prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) {
checkForInterrupts();
prover.writeComment("Bound encoding");
prover.addConstraint(propertyEncoder.encodeBoundEventExec());
logger.info("Starting second solver.check()");
res = prover.isUnsat() ? PASS : UNKNOWN;
} else {
res = FAIL;
}

if (logger.isDebugEnabled()) {
logProverStatistics(logger, prover);
}
} else {
res = FAIL;
}

if (logger.isDebugEnabled()) {
logProverStatistics(logger, prover);
prover.writeComment("Property encoding");
prover.addConstraint(propertyEnc);

logger.info("Starting first solver.check()");
res = prover.isUnsat() ? UNKNOWN : FAIL;

if (logger.isDebugEnabled()) {
logger.info("First SMT query statistics:");
logProverStatistics(logger, prover);
}

if (res == UNKNOWN) {
// TODO: This second prover does not dump its content into
// an smt file: Shall we create a second dump file for this case?
final ProverWithTracker prover2 = closeOldAndGetNewProver();
prover2.addConstraint(progEnc);
prover2.addConstraint(wmmEnc);
prover2.addConstraint(witnessEnc);
prover2.addConstraint(symEnc);
prover2.addConstraint(propertyEncoder.encodeBoundEventExec());
logger.info("Starting second solver.check()");
res = prover2.isUnsat() ? PASS : UNKNOWN;

if (logger.isDebugEnabled()) {
logger.info("Second SMT query statistics:");
logProverStatistics(logger, prover);
}
}
}

// For Safety specs, we have SAT=FAIL, but for reachability specs, we have SAT=PASS
res = Property.getCombinedType(task.getProperty(), task) == Property.Type.SAFETY ? res : res.invert();
logger.info("Verification finished with result {}", res);
}

private ProverWithTracker closeOldAndGetNewProver() {
if (this.prover != null) {
prover.close();
}
this.prover = new ProverWithTracker(solverContext, "", SolverContext.ProverOptions.GENERATE_MODELS);
return this.prover;
}

}