Skip to content

Commit

Permalink
Confused !
Browse files Browse the repository at this point in the history
  • Loading branch information
@refactormyself
refactormyself committed Aug 6, 2019
1 parent 6be724b commit 7599622
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 81 deletions.
35 changes: 18 additions & 17 deletions src/org/sosy_lab/java_smt/solvers/stp/StpAbstractProver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,19 +59,18 @@ public void pop() {
StpJavaApi.vc_pop(currVC);
}

/*
* @Override public @Nullable T addConstraint(BooleanFormula pConstraint) throws
* InterruptedException { // TODO Auto-generated method stub return null; }
*
* @Override public void push() { // TODO Auto-generated method stub
*
* }
*/
@Override
public void push() {
Preconditions.checkState(!closed);
StpJavaApi.vc_push(currVC);
}

@Override
public boolean isUnsat() throws SolverException, InterruptedException {
// TODO update to use vc_query_with_timeout

// To go this route I will have to implement the Stack for the "Constraints" ?!

This comment has been minimized.

Sign in to view

Copy link
@kfriedberger

kfriedberger Aug 6, 2019

Member

Why? All asserted formulae should be on the internal stack. Thus, a simple sat-check should already check their conjunction.
// Preconditions.checkState(!closed);

This comment has been minimized.

Sign in to view

Copy link
@refactormyself

refactormyself Aug 6, 2019

Author Contributor

From our discussion on trello about implementing the UNSAT. However, please see my comment below
// int result = StpJavaApi.vc_query(curVC, queryExpr)
// if (result == 0) {
Expand All @@ -94,7 +93,8 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
}

@Override
public Model getModel() throws SolverException {
public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant)
throws InterruptedException, SolverException {
// TODO Auto-generated method stub
return null;
}
Expand All @@ -113,6 +113,14 @@ public List<BooleanFormula> getUnsatCore() {
return null;
}

@Override
public Model getModel() throws SolverException {
// TODO Auto-generated method stub

// I don't understand this model stuff.
return null;

This comment has been minimized.

Sign in to view

Copy link
@kfriedberger

kfriedberger Aug 6, 2019

Member

What exactly is the problem?
A model contains the assignments for a satisfiable set of formulae.
For example, for formula x=3+y & (y=4 | b=false) has a model {y=4,x=7,b=true}.
This can also be implemented later.

This comment has been minimized.

Sign in to view

Copy link
@refactormyself

refactormyself Aug 6, 2019

Author Contributor

I am trying to implement the StpModel class but I could not grasp the idea. I think I get it now
}

@Override
public void close() {
if (!closed) {
Expand All @@ -124,11 +132,4 @@ public void close() {
}
}

@Override
public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant)
throws InterruptedException, SolverException {
// TODO Auto-generated method stub
return null;
}

}
}
66 changes: 2 additions & 64 deletions src/org/sosy_lab/java_smt/solvers/stp/StpTheoremProver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,18 +19,12 @@
*/
package org.sosy_lab.java_smt.solvers.stp;

import com.google.common.base.Preconditions;
import java.util.Collection;
import java.util.List;
import java.util.Optional;
import java.util.Set;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.sosy_lab.common.ShutdownNotifier;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.Model;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
import org.sosy_lab.java_smt.api.SolverException;

class StpTheoremProver extends StpAbstractProver<Void> implements ProverEnvironment {

Expand All @@ -42,67 +36,11 @@ protected StpTheoremProver(
super(pContext, pOptions, pFrmcreator, pShutdownNotifier);
}

@Override
public void pop() {
// TODO Auto-generated method stub

}

@Override
public @Nullable Void addConstraint(BooleanFormula pConstraint) throws InterruptedException {

This comment has been minimized.

Sign in to view

Copy link
@refactormyself

refactormyself Aug 6, 2019

Author Contributor

@kfriedberger It seems that I will have to implement the Stack to manage the constraints. That seems to be the only way to implement UNSAT as discussed on trello. The STP C++ Interface seems to have it implemented, but I discover C++ with Swig is quite very different in C++'s way.

Please, do you think it is a right move.

This comment has been minimized.

Sign in to view

Copy link
@kfriedberger

kfriedberger Aug 6, 2019

Member

If Swig does not offer sufficient methods for existing C++-methods, then the Swig-wrapper needs to be improved or replaced by a better solution.

This comment has been minimized.

Sign in to view

Copy link
@kfriedberger

kfriedberger Aug 6, 2019

Member

What would be the benefit of our own stack? Would this stack then track all asserted formulae and check them on IS_UNSAT directly?

This comment has been minimized.

Sign in to view

Copy link
@refactormyself

refactormyself Aug 6, 2019

Author Contributor

What would be the benefit of our own stack? Would this stack then track all asserted formulae and check them on IS_UNSAT directly?

Yes that is my thinking but I think I will invest time improving the wrapper. But currently all useful functions in STP's C-interface are supported. There important ones missing not just UNSAT, getModel, and more too
// TODO Auto-generated method stub
return null;
}

@Override
public void push() {
Preconditions.checkState(!closed);
StpJavaApi.vc_push(currVC);
}
//
// @Override
// public boolean isUnsat() throws SolverException, InterruptedException {
// // TODO Auto-generated method stub
// return false;
// }

// @Override
// public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
// throws SolverException, InterruptedException {
// // TODO Auto-generated method stub
// return false;
// }

@Override
public Model getModel() throws SolverException {
// TODO Auto-generated method stub
return null;
}

@Override
public List<BooleanFormula> getUnsatCore() {
// TODO Auto-generated method stub
return null;
}

@Override
public Optional<List<BooleanFormula>>
unsatCoreOverAssumptions(Collection<BooleanFormula> pAssumptions)
throws SolverException, InterruptedException {
// TODO Auto-generated method stub
return null;
}

@Override
public void close() {
// TODO Auto-generated method stub

}

@Override
public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant)
throws InterruptedException, SolverException {
// TODO Auto-generated method stub
// It seems the only option is to implement the stack
// and hence make pop and push work with it
return null;
}

Expand Down

0 comments on commit 7599622

Please sign in to comment.