add some documentation on Formula-interface.
* JavaSMT is an API wrapper for a collection of SMT solvers.
* This file is part of JavaSMT.
*
- * Copyright (C) 2007-2016 Dirk Beyer
+ * Copyright (C) 2007-2018 Dirk Beyer
* All rights reserved.
*
* Licensed under the Apache License, Version 2.0 (the "License");
*/
package org.sosy_lab.java_smt.api;
+import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
+
/** An arbitrary SMT formula. */
-public interface Formula {}
+public interface Formula {
+
+ /**
+ * returns an arbitrary representation of the formula, might be human- or machine-readable.
+ *
+ * <p>We do not guarantee that the returned String is in any way related to the formula. The
+ * solver might apply escaping or even un-escaping. A user should not use the returned String for
+ * further processing. For analyzing formulas, we recommend to use a {@link FormulaVisitor}.
+ */
+ @Override
+ String toString();
+
+ /**
+ * checks whether the other object is a formula of the same structure. Does not apply an expensive
+ * SAT-check to check equisatisfiability.
+ *
+ * <p>Two formulas that are structured in the same way, are determined as "equal". Due to
+ * transformations and simplifications, two equisatisfiable formulas with different structure
+ * might not be determined as "equal".
+ */
+ @Override
+ boolean equals(Object other);
+
+ /** returns a valid hashCode satisfying the constraints given by {@link #equals}. */
+ @Override
+ int hashCode();
+}
