Exercise 8 - CcSolver.java

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;
	}
	
}