Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Hi Francisco,

There is nothing published on the conditional equation/membership/rule 
mechanism. It's implemented in a very general way, and new condition fragment 
types can be plugged in to a standard interface, the abstract base class 
ConditionFragment. Each type of condition fragment can derive a new class to 
hold its runtime execution state from abstract base class ConditionState.

The top level execution mechanism is in Core/preEquation.cc, functions 
PreEquation::checkCondition() and PreEquation::solveCondition(). They 
maintain 
an explicit state stack since we may need restart the search for solutions to 
the conjunction of condition fragments at different points in callers (say 
for 
search or model checking) and thus can't use recursion.

The solver code for each type of condition fragment is called through the 
virtual function ConditionFragment::solve(). Different types condition 
fragment 
need to do different things; all 4 currently supported types recursively call 
the rewrite engine using the normal C++ system stack.

You can find the code for each of the 4 currently supported types of 
condition 
fragment in Higher/*ConditionFragment.cc. Only classes 
AssignmentConditionFragment and RewriteConditionFragment need state that 
persists across calls and this is held in classes AssignmentConditionState 
and 
RewriteConditionState respectively.

I hope this gives you a starting point. If you need more gory details you'll 
just have to read the code.

Steven

On Monday 18 April 2011 03:30:36 am Francisco Frechina wrote:
> Hello,
> 
> I'm Francisco and I'm writing you looking for help.
> Due to my thesis work, I need to know how the conditional equation is
>  implemented in maude (same for rules), If you can send me some reference I
>  will thank you
> 
> Cordially,
> Francisco Frechina
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>