Exercise 8 - CcSolver.java
CcSolver.java — Python Source, 2 kB (2772 bytes)
File contents
import java.io.PrintWriter; import java.util.ArrayList; import java.util.HashMap; import java.util.HashSet; import java.util.Map.Entry; import org.apache.log4j.Logger; import org.apache.log4j.SimpleLayout; import org.apache.log4j.WriterAppender; import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm; import de.uni_freiburg.informatik.ultimate.logic.NoopScript; import de.uni_freiburg.informatik.ultimate.logic.SMTLIBException; import de.uni_freiburg.informatik.ultimate.logic.Term; import de.uni_freiburg.informatik.ultimate.smtinterpol.Config; //TODO: Again, you may, but need not, use the contents of this file // as a start for your solver implementation. Only asserts of single // atoms which are either a "=" or a "distinct" are parsed, right now. // This suffices for the conjunctive quantifier-free fragment, but you // may augment it with n-ary "=", "and", or whatever you wish, of course... // note, that this time you need not only implement checksat(), but you also // have to build up your data structures in assertTerm(Term t). // (which gets called for every (assert ...) in the smt file, obviously..) public class CcSolver extends NoopScript { class UfNode { public UfNode find() { return null; } public void union(UfNode other) { } public HashSet<UfNode> getCcPar() { return null; } public boolean congruent(UfNode arg) { return false; } public void merge(UfNode arg) { } } private SimpleLayout m_Layout; private Logger m_Logger; private WriterAppender m_Appender; private PrintWriter m_Err = new PrintWriter(System.err); public CcSolver(Logger logger) { m_Logger = logger; m_Layout = new SimpleLayout(); m_Appender = new WriterAppender(m_Layout, m_Err); m_Logger.addAppender(m_Appender); m_Logger.setLevel(Config.DEFAULT_LOG_LEVEL); reset(); } @Override public LBool assertTerm(Term term) throws SMTLIBException { ApplicationTerm at = (ApplicationTerm) term; assert (at.getFunction().getName() == "=" || at.getFunction().getName() == "distinct"); String functionName = at.getFunction().getName(); ApplicationTerm atom = at; assert (atom.getParameters().length == 2); ApplicationTerm t1 = (ApplicationTerm) atom.getParameters()[0]; ApplicationTerm t2 = (ApplicationTerm) atom.getParameters()[1]; //On ApplicationTerm you can call f.i.: //Term[] getParameters() //String getFunction().getName() //ApplicationTerm inherits from Term //remember that variables are ApplicationTerms with no parameters if (functionName == "=") ; else if (functionName == "distinct") ; else assert false; return super.assertTerm(term); } @Override public LBool checkSat() { return LBool.UNKNOWN; } }