User:Franc

Franc Ivankovic is (Dec-Jan 2010) working on adding support for the ABsolver solver to ASCEND.

• absolver:solvers/absolver
• absolver:ascend/compiler/logrel_cnf.c
• absolver:ascend/compiler/logrel_cnf.h

Goals

1. write C code to convert arbitrary logical relations to CNF form.
2. make the above code such that it re-uses ascend/compiler/logical_relation.h data structures.
3. write a simple ASCEND solver the reads WHEN lists and creates logical relation data structures to represent the conditional modelling problem encoded therein.
4. make output from the above solver which can be sent as a text file for processing by ABSolver
5. parse the output of ABSolver in response to the above input file, and poke the resulting solution values back into ASCEND for review by the user.
6. test the resulting code with sample models from Andreas Bauer, translated into ASCEND. If time permits, test the new solver with models from Vicente Rico-Ramirez (CMSlv) as well.

Notes from John about parse WHEN lists

The 'relation_term' data structures: ascend/compiler/relation_type.h

Sample code that manipulates same: ascend/compiler/exprsym.h

How to get access to the list of whens

Note we looked at CMSlv and we found that instead of accessing the list of WHENs directly, the solver was instead parsing the 'dvars' or discrete variables and identifying which WHEN each of those variables occurred it. For reasons that benefited the algorithm that they wanted to implement.

We have a different need, which is to export the whole model to another solver.

In ascend/system/slv_client.h, see slv_get_solvers_when_list(...) - returns a NULL-terminated list.

In ascend/system/conditional.h,

 extern struct gl_list_t *when_dvars_list( struct w_when *when);
 /**< Retrieves the list of dis variables of the given when. */

 extern struct gl_list_t *when_cases_list( struct w_when *when);
 /**< Retrieves the list of cases of the given when. */

Note that the above functions return 'gl_list_t' objects, for which you need to use the routines in ascend/general/list.h like gl_fetch and gl_length, for example, in looping. Note that gl_lists start at 1 and not 0 like most C arrays. Stoopid.

The when_dvars_list is a list containing dis_discrete objects, see ascend/system/discrete.h for details.

Also see

 extern int32 *when_case_values_list( struct when_case *wc);
 /**< Retrieves the list of values of the given case. */

which will tell us the values of the dvars in the present 'when_case'.

 extern struct gl_list_t *when_case_rels_list( struct when_case *wc);
 /**< Retrieves the list of rels of the given case. */

will tell us the relations that are switched on by this case.

but note that WHENs can also be used to switch on...

logical relations

 extern struct gl_list_t *when_case_logrels_list( struct when_case *wc);
 /**< Retrieves the list of logrels of the given case. */

nested WHENs

 extern struct gl_list_t *when_case_whens_list( struct when_case *wc);
 /**<  Retrieves the list of whens nested in the given case. */

That looks like all you need to know... I hope. You might have to double-check the types of the objects being returned in the above.

Note that 'var_variable' and 'rel_relation' have names that are generated by the compiler, and with a bit of fiddling, they are accessible to the solver. You might find some code to help with that tucked away in some of the other solvers.

Note var_make_name can be used to create names of variables, if you have the pointer to the var_variable that you need.

Names can include dots, etc., e.g.:

mymodel.submodel.var1

To build up the tree, you will need to have some tree-data-structure functions. The ones in exprsym.c are good examples, but not all that you need.

static Term *MakeAdd(Term *left, Term *right)

for example does the job of creating a "plus" node that is linked to left and right operands.

The advantage of using these built-in data structures is that you can probably test your to-CNF routines without having to write all the MakeAnd etc etc, by using ASCEND to parse a model containing some logical relations, and then run your routine on those relations directly.

static void test_instantiate_file(void){

from ascend/compiler/test/test_basics.c shows you how to write a show C-language test routine that will load your file and then allow you to access the data structures.

Notes from John about CUnit tests

I have committed some test code that you can use to access relation structures for use in testing your converted-to-ASCEND C code.

To use this code, you first need to install CUnit. Although CUnit is available from Ubuntu repsitories, that package is outdated and contains a bug. Hence, you should install CUnit from its svn repository; there are some quick instructions for that here:

http://ascendwiki.cheme.cmu.edu/Developer%27s_Manual#CUnit_test_suites

The test that I wrote to help you is here:

test/test compiler_expr.boolrel

The code for that test is in ascend/compiler/test/test_expr.c, around line 100. You can modify that file to make calls to your CNF code, which I suggest you add as a file logrel_cnf.c in ascend/compiler directory. That file should be added to the filename list in ascend/compiler/SConscript in order for it to be compiled as part of libascend.

I will add you as a user to our Subversion repository, and create a branch for you, so that you can safely store your code in ASCEND's server.

IMPORTANT: while building the above test, I noticed the the relation structure data types are indeed different for logical relations, as compared to real-valued relations. The file in which the data structures are defined is in ascend/compiler/logical_relation.h. The code in the various files ascend/compiler/log*.h will help you with different routines that you can use with those data structures. The structures are very similar to the relation.h structures, but a bit simpler because of their narrower scope.

The next thing I will do to help you will be to build a skeleton solver into which you will be able to place some looping code to create your relation structures using the WHEN/CASE lists. I'll try to do something towards that this evening.

Running the test suite

export LD_LIBRARY_PATH=~/ascend:/usr/local/lib
ldd test/test # should show ~/ascend/libascend.so.1 being successfully found, make sure not linking to /usr/lib
export ASCENDLIBRARY=~/ascend/models:~/ascend/solvers/absolver

Discrete variables

Initially let's worry about boolean WHEN statements only, so we need to check the discrete variable type, see the ascend/system/discrete.h header for the appropriate structures and ways to handle that.

Numbering issues

When creating the boolean expression, we need unique numbers for all the boolean variables in our SAT expression.

For dvars, we can use dis_sindex(dv) to return a suitable number.

For relations (from USE) we can use rel_sindex(rel) (from ascend/system/rel.h) to return a suitable number.

Both of these are (I believe) starting at zero, so to compile a master list, we should add ndvars to the rel_sindex, maybe plus 1?