From 894a42ff7e8bf220c8795c867ae561b2a6b43ab8 Mon Sep 17 00:00:00 2001
From: Yann Thierry-Mieg <Yann.Thierry-Mieg@lip6.fr>
Date: Wed, 5 Jun 2024 13:51:02 +0200
Subject: [PATCH] bootstrap a problem from a file of constraints

---
 .../lip6/move/gal/structural/smt/Problem.java | 31 +++++++++++++++++--
 1 file changed, 29 insertions(+), 2 deletions(-)

diff --git a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/Problem.java b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/Problem.java
index 091e11456..5411346ee 100644
--- a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/Problem.java
+++ b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/Problem.java
@@ -1,5 +1,7 @@
 package fr.lip6.move.gal.structural.smt;
 
+import java.io.File;
+import java.io.IOException;
 import java.util.Arrays;
 import java.util.Collections;
 
@@ -26,6 +28,7 @@ public class Problem {
 	
 	private CandidateSolution solution = new CandidateSolution();
 	private boolean isEF;
+	private String smtFile;
 
 	public Problem(String name, boolean isEF, Expression pred) {
 		this.name = name;
@@ -45,6 +48,17 @@ public Problem(String name, boolean isEF, Expression pred) {
 		definition = declareBoolFunc(symbol, smt);
 	}
 
+	public Problem(String name, String smtFile, ISymbol symbol, VarSet support) {
+		this.name = name;
+		this.symbol = symbol;
+		this.predicate = null;
+		this.support = support;
+		this.definition = null;
+		this.refinedSymbol = null;
+		this.isEF = true;
+		this.smtFile = smtFile;
+	}
+
 	public static ICommand declareBoolFunc(ISymbol name, IExpr body) {
 		IFactory ef = SMT.instance.smtConfig.exprFactory;
 		org.smtlib.ISort.IApplication bools = SMT.instance.smtConfig.sortFactory.createSortExpression(ef.symbol("Bool"));		
@@ -69,8 +83,21 @@ public void refineDefinition(IExpr additionalConstraint, SolverState solver) {
 	
 	public boolean declareProblem(SolverState solver) {
 		solver.declareVars(support);
-		IResponse response = definition.execute(solver.getSolver());
-		return response.isOK();
+		if (definition == null) {
+			if (smtFile != null) {
+				try {
+					return solver.getSolver().readFile(new File(smtFile)).isOK();
+				} catch (IOException e) {
+					e.printStackTrace();
+				}
+			} else {
+				throw new IllegalStateException("No definition for problem " + name);
+			}
+		} else {
+			IResponse response = definition.execute(solver.getSolver());
+			return response.isOK();
+		}
+		return false;
 	}