Синтаксическое выражение, содержащее атом из строки

Question

Метод CompUtil.parseOneExpression_fromString дает следующее сообщение об ошибке: Названия «Atom $ 0» не может быть найдено, когда строка разобрана содержит выражение, содержащее метку атома непосредственно.

Это может быть понятно, поскольку отдельные атомы не определены непосредственно на уровне модуля, а «сгенерированы» во время процесса поиска экземпляра.

НО! Можно оценивать выражения, содержащие атомы, непосредственно с помощью консольного оценщика, идущего вместе с визуализатором сплавов.

Каков тогда метод в API, используемый для оценки в решении, выражения, содержащие атомы.

образца

Кода, который приводит к ранее упомянутой ошибке:

Expr e=CompUtil.parseOneExpression_fromString(module, "Atom$0.field"); 
solution.eval(e); 

Answer 1

parseOneExpression_fromString вызова в вашем примере не удается, потому что вы не можете ожидать, чтобы быть в состоянии найти имя атома в module объекте (который представляет только ваша модель и ничего не знает о каких-либо решениях этой модели). После того как вы получите решение, вы можете добавить все атомы и имена skolem в объект модуля, а затем вы сможете анализировать выражения, содержащие имена атомов.

module = CompUtil.parseEverything_fromFile(...); 
solution = A4SolutionReader.read(module.getAllReachableSigs(), ...); 
for(ExprVar a:solution.getAllAtoms()) { module.addGlobal(a.label, a); } 
for(ExprVar a:solution.getAllSkolems()) { module.addGlobal(a.label, a); }