Skip to content
GitLab
Commit b5ed266c authored by point's avatar point
Browse files

. add local context to quantified formulas

parent bb172319
Hide whitespace changes
Inline Side-by-side
src/algorithms/ar-flat-semantics.c
View file @ b5ed266c
/* $Id: ar-flat-semantics.c,v 1.3 2006/02/08 08:13:22 point Exp $ */
/* $Id: ar-flat-semantics.c,v 1.4 2006/02/08 11:21:59 point Exp $ */
#include <ccl-assert.h>
#include <ccl-hash.h>
#include "model/ar-model.h"
......@@ -62,32 +62,42 @@ s_intersect_slot_lists(ccl_list l1, ccl_list l2)
/* --------------- */
static ar_expr *
s_quantify_constraints(int index, int nb_constraints, ar_expr **constraints,
s_quantify_constraints(ar_context *ctx,
int index, int nb_constraints, ar_expr **constraints,
ccl_list *varlists, int *ordering, ccl_list qvars)
{
ccl_pair p;
ar_expr *result;
int c = ordering[index];
ccl_list vars = NULL;
ar_context *qctx = NULL;
if( ccl_list_get_size(varlists[c]) == 0 )
{
if( index == nb_constraints-1 )
return ar_expr_crt_true();
else
return s_quantify_constraints(index+1,nb_constraints,constraints,
return s_quantify_constraints(ctx,index+1,nb_constraints,constraints,
varlists,ordering,qvars);
}
if( ccl_list_get_size(qvars) > 0 )
{
vars = ccl_list_create();
qctx = ar_context_create(ctx);
for(p = FIRST(varlists[c]); p; p = CDR(p))
{
ar_context_slot *sl = (ar_context_slot *)CAR(p);
if( ccl_list_has(qvars,sl) )
ccl_list_add(vars,sl);
{
ar_identifier *id = ar_context_slot_get_name(sl);
ar_context_add_slot(qctx,id,sl);
ar_identifier_del_reference(id);
ccl_list_add(vars,sl);
}
}
for(p = FIRST(vars); p; p = CDR(p))
......@@ -98,14 +108,18 @@ s_quantify_constraints(int index, int nb_constraints, ar_expr **constraints,
ar_context_slot_del_reference(sl);
}
}
else
{
qctx = ar_context_add_reference(ctx);
}
if( index == nb_constraints-1 )
result = ar_expr_add_reference(constraints[c]);
else
{
ar_expr *tmp =
s_quantify_constraints(index+1,nb_constraints,constraints,varlists,
ordering,qvars);
s_quantify_constraints(qctx,index+1,nb_constraints,constraints,
varlists,ordering,qvars);
result = ar_expr_crt_binary(AR_EXPR_AND,constraints[c],tmp);
ar_expr_del_reference(tmp);
}
......@@ -114,12 +128,14 @@ s_quantify_constraints(int index, int nb_constraints, ar_expr **constraints,
{
if( ! ccl_list_is_empty(vars) )
{
ar_expr *tmp = ar_expr_crt_quantifier(AR_EXPR_EXIST,vars,result);
ar_expr *tmp =
ar_expr_crt_quantifier(AR_EXPR_EXIST,qctx,vars,result);
ar_expr_del_reference(result);
result = tmp;
}
ccl_list_clear_and_delete(vars,(ccl_delete_proc)ar_expr_del_reference);
}
ar_context_del_reference(qctx);
return result;
}
......@@ -211,7 +227,8 @@ s_compute_enabling_condition(ar_context *ctx, ar_trans *t, ccl_list assertions,
{
ccl_list qvars = ccl_list_deep_dup(qfvars,(ccl_duplicate_func)
ar_context_slot_add_reference);
ar_expr *qf = s_quantify_constraints(0,nb_constraints,constraints,varlists,
ar_expr *qf = s_quantify_constraints(ctx,
0,nb_constraints,constraints,varlists,
ordering,qvars);
ar_expr *tmp = ar_expr_crt_binary(AR_EXPR_AND,result,qf);
ar_expr_del_reference(qf);
......@@ -634,7 +651,6 @@ s_add_node(ar_node *result, ar_identifier *subname, ar_node *submodel,
for(p = FIRST(slots); p; p = CDR(p))
{
ar_expr *esl;
ar_identifier *sid = (ar_identifier *)CAR(p);
ar_context_slot *sl = ar_context_get_slot(subctx,sid);
ar_identifier *nid = ar_identifier_add_prefix(sid,subname);
......@@ -643,21 +659,25 @@ s_add_node(ar_node *result, ar_identifier *subname, ar_node *submodel,
ar_identifier_del_reference(sid);
ar_identifier_del_reference(nid);
ccl_assert( nsl != NULL );
if( (ar_context_slot_get_flags(nsl) & AR_SLOT_FLAG_PARAMETER) != 0 )
esl = ar_expr_crt_parameter(nsl);
else
esl = ar_expr_crt_variable(nsl);
ccl_hash_find(sl2expr,ar_context_slot_add_reference(sl));
ccl_hash_insert(sl2expr,ar_expr_add_reference(esl));
ccl_hash_find(sl2sl,ar_context_slot_add_reference(sl));
ccl_hash_insert(sl2sl,ar_context_slot_add_reference(nsl));
if( nsl != NULL )
{
ar_expr *esl;
if( (ar_context_slot_get_flags(nsl) & AR_SLOT_FLAG_PARAMETER) )
esl = ar_expr_crt_parameter(nsl);
else
esl = ar_expr_crt_variable(nsl);
ccl_hash_find(sl2expr,ar_context_slot_add_reference(sl));
ccl_hash_insert(sl2expr,ar_expr_add_reference(esl));
ccl_hash_find(sl2sl,ar_context_slot_add_reference(sl));
ccl_hash_insert(sl2sl,ar_context_slot_add_reference(nsl));
ar_context_slot_del_reference(nsl);
ar_expr_del_reference(esl);
}
ar_context_slot_del_reference(sl);
ar_context_slot_del_reference(nsl);
ar_expr_del_reference(esl);
}
ar_context_del_reference(subctx);
......
src/formulae/ar-expr.c
View file @ b5ed266c
......@@ -9,6 +9,7 @@ struct ar_expr_st {
ar_type *type;
int arity;
ar_expr **args;
ar_context *qctx;
union {
ar_identifier *field;
......@@ -18,7 +19,6 @@ struct ar_expr_st {
ccl_list qvars;
ar_identifier **fnames;
} u;
};
struct op_property {
......@@ -356,10 +356,12 @@ ar_expr_crt_ternary(ar_expr_op op, ar_expr *e0, ar_expr *e1,
/* --------------- */
ar_expr *
ar_expr_crt_quantifier(ar_expr_op op, ccl_list qvars, ar_expr *F)
ar_expr_crt_quantifier(ar_expr_op op, ar_context *ctx, ccl_list qvars,
ar_expr *F)
{
ar_expr *result = s_crt_nary(op,1,&F);
result->qctx = ar_context_add_reference(ctx);
result->u.qvars =
ccl_list_deep_dup(qvars,(ccl_duplicate_func)ar_expr_add_reference);
......@@ -836,7 +838,7 @@ ar_expr_log_gen(ccl_log_type log, ar_expr *e,
/* --------------- */
int
ar_expr_true(ar_expr *e)
ar_expr_is_true(ar_expr *e)
{
ccl_pre( e != NULL && e->type == AR_BOOLEANS );
......@@ -1594,7 +1596,7 @@ ar_expr_replace(ar_expr *e, ar_context_slot *to_replace, ar_expr *newvalue)
break;
case AR_EXPR_EXIST : case AR_EXPR_FORALL :
result = ar_expr_crt_quantifier(e->op,e->u.qvars,ops[0]);
result = ar_expr_crt_quantifier(e->op,e->qctx,e->u.qvars,ops[0]);
break;
case AR_EXPR_CALL:
......@@ -1677,7 +1679,7 @@ ar_expr_replace_with_tables(ar_expr *e, ccl_hash *subst, int nb_tables)
break;
case AR_EXPR_EXIST : case AR_EXPR_FORALL :
result = ar_expr_crt_quantifier(e->op,e->u.qvars,ops[0]);
result = ar_expr_crt_quantifier(e->op,e->qctx,e->u.qvars,ops[0]);
break;
case AR_EXPR_CALL:
......@@ -1760,7 +1762,7 @@ ar_expr_replace_with_context(ar_expr *e, ar_context *ctx)
break;
case AR_EXPR_EXIST : case AR_EXPR_FORALL :
result = ar_expr_crt_quantifier(e->op,e->u.qvars,ops[0]);
result = ar_expr_crt_quantifier(e->op,e->qctx,e->u.qvars,ops[0]);
break;
case AR_EXPR_CALL:
......@@ -1936,23 +1938,32 @@ ar_expr_expand_composite_types(ar_expr *e, ar_context *ctx)
case AR_EXPR_EXIST: case AR_EXPR_FORALL:
{
ccl_pair p;
ar_expr *qf = ar_expr_remove_composite_slots(e->args[0],ctx);
ar_expr *qf = ar_expr_remove_composite_slots(e->args[0],e->qctx);
ar_context *pqctx = ar_context_get_parent(e->qctx);
ar_context *qctx = ar_context_create(pqctx);
ccl_list qvars = ccl_list_create();
ar_context_del_reference(pqctx);
for(p = FIRST(e->u.qvars); p; p = CDR(p))
{
ar_expr *var = (ar_expr *)CAR(p);
(void)ar_context_expand_composite_slot(ctx,var->u.slot,qvars);
}
for(p = FIRST(qvars); p; p = CDR(p))
{
ar_context_slot *sl = (ar_context_slot *)CAR(p);
ar_identifier *id = ar_context_slot_get_name(sl);
ar_context_add_slot(qctx,id,sl);
CAR(p) = ar_expr_crt_variable(sl);
ar_context_slot_del_reference(sl);
ar_identifier_del_reference(id);
}
ccl_list_add(result,ar_expr_crt_quantifier(e->op,qvars,qf));
ccl_list_add(result,ar_expr_crt_quantifier(e->op,qctx,qvars,qf));
ar_expr_del_reference(qf);
ccl_list_clear_and_delete(qvars,(ccl_delete_proc)ar_expr_del_reference);
ar_context_del_reference(qctx);
}
break;
......@@ -2069,6 +2080,8 @@ s_new_expr(ar_expr_op op, int arity)
result->op = op;
result->type = NULL;
result->args = NULL;
result->qctx = NULL;
if( (result->arity = arity) )
result->args = ccl_new_array(ar_expr *,arity);
......@@ -2110,6 +2123,8 @@ s_delete_expr(ar_expr *e)
else if( e->op == AR_EXPR_VAR || e->op == AR_EXPR_PARAM )
ar_context_slot_del_reference(e->u.slot);
ccl_zdelete(ar_context_del_reference,e->qctx);
ccl_delete(e);
}
......
src/formulae/ar-expr.h
View file @ b5ed266c
/* $Id: ar-expr.h,v 1.12 2006/02/08 08:11:54 point Exp $ */
/* $Id: ar-expr.h,v 1.13 2006/02/08 11:21:59 point Exp $ */
#ifndef __AR_EXPR_H__
# define __AR_EXPR_H__
......@@ -59,7 +59,8 @@ ar_expr_crt_binary(ar_expr_op op, ar_expr *e1, ar_expr *e2);
CCL_EXTERN ar_expr *
ar_expr_crt_ternary(ar_expr_op op, ar_expr *e1, ar_expr *e2, ar_expr *e3);
CCL_EXTERN ar_expr *
ar_expr_crt_quantifier(ar_expr_op op, ccl_list qvars, ar_expr *F);
ar_expr_crt_quantifier(ar_expr_op op, ar_context *ctx,
ccl_list qvars, ar_expr *F);
CCL_EXTERN ar_expr *
ar_expr_crt_function_call(ar_signature *sig, ar_expr **args);
CCL_EXTERN ar_expr *
......
src/model/ar-node.c
View file @ b5ed266c
/* $Id: ar-node.c,v 1.13 2006/02/08 08:11:34 point Exp $ */
/* $Id: ar-node.c,v 1.14 2006/02/08 11:22:00 point Exp $ */
#include <ccl-types.h>
#include <ccl-assert.h>
#include <ccl-memory.h>
......@@ -1694,10 +1694,19 @@ ar_node_remove_composite_types(ar_node *node)
for(p = FIRST(slots); p; p = CDR(p))
{
ar_context_slot *slot;
ar_type *type;
ar_identifier *sid = (ar_identifier *)CAR(p);
ar_context_slot *slot = ar_context_get_slot(node->ctx,sid);
ar_type *type = ar_context_slot_get_type(slot);
if( ar_context_has_slot(ctx,sid) )
{
ar_identifier_del_reference(sid);
continue;
}
slot = ar_context_get_slot(node->ctx,sid);
type = ar_context_slot_get_type(slot);
if( ar_type_is_scalar(type) )
{
uint32_t flags = ar_context_slot_get_flags(slot);
......
src/model/ar-ptree-interp-expr.c
View file @ b5ed266c
......@@ -434,7 +434,7 @@ s_interp_quantified_formula(altarica_tree t, ar_context *ctx)
ccl_try(altarica_interpretation_exception)
{
F = ar_interp_boolean_expression(t->child->next,newctx);
R = ar_expr_crt_quantifier(op,qvars,F);
R = ar_expr_crt_quantifier(op,newctx,qvars,F);
}
ccl_no_catch;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment