package jkind.solvers.smtlib2;

import java.math.BigInteger;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Set;

import jkind.lustre.NamedType;
import jkind.sexp.Sexp;
import jkind.sexp.Symbol;
import jkind.solvers.Eval;
import jkind.solvers.Lambda;
import jkind.solvers.Model;
import jkind.solvers.Value;
import jkind.util.SexpUtil;

public class SmtLib2Model extends Model {
	private HashMap<String, Sexp> values;
	private HashMap<String, Lambda> functions;

	public SmtLib2Model() {
		this.values = new HashMap<>();
		this.functions = new HashMap<>();
	}

	public void addValue(String id, Sexp sexp) {
		values.put(id, sexp);
	}

	public void addFunction(String fn, Lambda lambda) {
		functions.put(fn, lambda);
	}

	@Override
	public Value getValue(Symbol sym) {
		return new Eval(this).eval(values.get(sym.toString()));
	}

	@Override
	public Value getFunctionValue(String fn, BigInteger index) {
		Lambda lambda;
		if (functions.containsKey(fn)) {
			lambda = functions.get(fn);
		} else if (definitions.containsKey(fn)) {
			lambda = definitions.get(fn).getLambda();
		} else {
			lambda = new Lambda(SexpUtil.I, getDefaultValue(fn));
			functions.put(fn, lambda);
		}
		
		return new Eval(this).eval(lambda.instantiate(new Symbol(index.toString())));
	}

	private Symbol getDefaultValue(String fn) {
		if (declarations.get(fn).getType() == NamedType.BOOL) {
			return new Symbol("true");
		} else {
			return new Symbol("0");
		}
	}

	
	public Lambda getFunction(String fn) {
		return functions.get(fn);
	}
	
	@Override
	public Set<String> getFunctionNames() {
		return new HashSet<>(functions.keySet());
	}
}

@@ -430,16 +430,34 @@
 %3E values
+ = new HashMap%3C%3E()
 ;%0A%09priva
@@ -496,107 +496,27 @@
 ions
-;%0A%0A%09public SmtLib2Model() %7B%0A%09%09this.values = new HashMap%3C%3E();%0A%09%09this.functions = new HashMap%3C%3E();%0A%09%7D
+ = new HashMap%3C%3E();
 %0A%0A%09p
@@ -1130,18 +1130,16 @@
 a);%0A%09%09%7D%0A
-%09%09
 %0A%09%09retur
@@ -1394,18 +1394,16 @@
 %09%09%7D%0A%09%7D%0A%0A
-%09%0A
 %09public 
@@ -1465,17 +1465,16 @@
 fn);%0A%09%7D%0A
-%09
 %0A%09@Overr

Clean up