#210, rework smtlib2 Horn clause parsing: convert to CNF first (keepi…

…ng the Boolean structure of interpreted parts intact), then generate horn clauses

trunk/source/Library-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HornClause.java

@@ -209,7 +209,7 @@ public String toString() {
 		}
 
 		// return mTransitionFormula.getFormula().toString();
-		return mFormula.toString();
+		return mFormula.toStringDirect();
 		// return String.format("(%s) ^^ (%s) ~~> (%s) || in : %s || out : %s ",
 		// cobody, mTransitionFormula, body,
 		// return String.format("(%s) ^^ (%s) ~~> (%s)", cobody,

trunk/source/SmtParser/src/de/uni_freiburg/informatik/ultimate/source/smtparser/SmtParser.java

@@ -201,8 +201,8 @@ private void processFile(final File file) throws IOException {
 			final ConstructAndInitializeBackendSmtSolver caibss =
 					new HCGBuilderHelper.ConstructAndInitializeBackendSmtSolver(mServices, mStorage,
 							"treeAutomizerSolver");
-			script = new HornClauseParserScript(file.getName(), caibss.getScript(), caibss.getLogicForExternalSolver(),
-					caibss.getSolverSettings());
+			script = new HornClauseParserScript(mServices, file.getName(), caibss.getScript(),
+					caibss.getLogicForExternalSolver(), caibss.getSolverSettings());
 		} else {
 			if (useExternalSolver) {
 				mLogger.info("Starting external SMT solver with command " + commandExternalSolver);

trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/parsing/HornClauseBody.java

@@ -67,6 +67,14 @@ public HornClauseBody(final HornClauseParserScript script) {
 		mParserScript = script;
 	}
 
+	/***
+	 * Copy constructor
+	 */
+	public HornClauseBody(final HornClauseBody original) {
+		mCobody = new HornClauseCobody(original.mCobody);
+		mParserScript = original.mParserScript;
+	}
+
 	/***
 	 * Add literal to the cobody.
 	 * @param literal

trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/parsing/HornClauseCobody.java

@@ -57,8 +57,8 @@ public class HornClauseCobody {
 
 	private boolean mFinalized = false;
 
-	private final List<HornClausePredicateSymbol> mPredicateSymbols = new ArrayList<>();
-	private final List<List<TermVariable>> mPredicateSymbolToVariables = new ArrayList<>();
+	private final List<HornClausePredicateSymbol> mPredicateSymbols;
+	private final List<List<TermVariable>> mPredicateSymbolToVariables;
 
 	private final HornClauseParserScript mParserScript;
 
@@ -68,10 +68,27 @@ public class HornClauseCobody {
 	 */
 	public HornClauseCobody(final HornClauseParserScript parserScript) {
 		mPredicates = new ArrayList<>();
+		mPredicateSymbols = new ArrayList<>();
+		mPredicateSymbolToVariables = new ArrayList<>();
 		mTransitions = new HashSet<>();
 		mParserScript = parserScript;
 	}
 
+	/**
+	 *
+	 * @param original
+	 */
+	public HornClauseCobody(final HornClauseCobody original) {
+		mPredicates = new ArrayList<>(original.mPredicates);
+		mPredicateSymbols = new ArrayList<>(original.mPredicateSymbols);
+		mPredicateSymbolToVariables = new ArrayList<>();
+		for (final List<TermVariable> l : original.mPredicateSymbolToVariables) {
+			mPredicateSymbolToVariables.add(new ArrayList<>(l));
+		}
+		mTransitions = new HashSet<>(original.mTransitions);
+		mParserScript = original.mParserScript;
+	}
+
 	/***
 	 * Add a literal predicate to the cobody.
 	 * @param literal
@@ -171,8 +188,8 @@ private void computePredicates(final HCSymbolTable symbolTable) {
 			final List<TermVariable> parameterTermVariables = Arrays.asList(pred.getParameters()).stream()
 					.map(t -> (TermVariable) t)
 					.collect(Collectors.toList());
-			assert parameterTermVariables.size() == new HashSet<>(parameterTermVariables).size() : "TODO: eliminate "
-					+ "duplicate arguments";
+//			assert parameterTermVariables.size() == new HashSet<>(parameterTermVariables).size() : "TODO: eliminate "
+//					+ "duplicate arguments";
 			final List<TermVariable> bodyVars = parameterTermVariables;
 			mPredicateSymbolToVariables.add(bodyVars);
 		}