~trn/reduce-algebra

409cfd288089217cebe78111ac839f45a2c863d2 — Jeffrey H. Johnson 8 days ago cde426d + b2efd07
Merge branch 'svn/trunk'
M packages/redlog/cl/clqe.red => packages/redlog/cl/clqe.red +2 -0
@@ 323,6 323,8 @@ asserted procedure cl_gqea(f: Formula, theo: Theory, xbvl: KernelL): Elimination
   % for an interpretation of the parameters, then [f] holds, and $A_i$
   % describes a satisfying sample point. Accesses the switch [rlqepnf]; if
   % [rlqepnf] is on, then [f] must be prenex.
   if !*clqenew then cl_gqea_new(f, theo, xbvl) else

   begin scalar er, theo, eqr, !*rlqegen, !*rlsipw, !*rlsipo, !*rlqeans;
      !*rlsipw := !*rlqegen := !*rlqeans := t;
      er := cl_qe1(f, theo, xbvl);

M packages/redlog/cl/clqenew.red => packages/redlog/cl/clqenew.red +257 -160
@@ 33,12 33,11 @@ copyright('clqenew, "(c) 2021 A. Dolzmann, T. Sturm");
#define QEDB_INPUTFORMULA 1
#define QEDB_INPUTTHEORY 2
#define QEDB_NOASSUMEVARS 3
#define QEDB_ANSWERMODE 4
#define QEDB_ASSUMEMODE 5
#define QEDB_BLOCKSYMBOLS 6
#define QEDB_BLOCKVARLISTS 7
#define QEDB_ASSUMEMODE 4
#define QEDB_ANSWERMODE 5
#define QEDB_BLOCKS 6
#define QEDB_LASTBLOCKINPUTFORMULA 8
#define QEDB_VARS 9
#define QEDB_VARIABLES 9
#define QEDB_FORMULA 10
#define QEDB_ANSWER 11
#define QEDB_SUCCESSNODES 12


@@ 48,25 47,21 @@ copyright('clqenew, "(c) 2021 A. Dolzmann, T. Sturm");
#define QEDB_LAST 15

asserted procedure qedb_new(): Vector;
   % QE data for a block new.
   % QE data for a block, construct new instance.
   begin scalar db;
      db := mkvect(QEDB_LAST);
      putv(db, QEDB_TAG, 'qedb);

      % The following fields are constant, i.e., assigned exactly once after the creation of qedb:
      putv(db, QEDB_INPUTFORMULA, 'undefined);       % InputTheory
      putv(db, QEDB_INPUTTHEORY, 'undefined);        % InputTheory
      putv(db, QEDB_NOASSUMEVARS, 'undefined);       % NoAssumeVars; do not make assumptions on these variables, includes quantified variables
      putv(db, QEDB_ANSWERMODE, 'undefined);         % AnswerMode; 'raw, 'standard, or nil
      putv(db, QEDB_ASSUMEMODE, 'undefined);         % AssumeMode; 'full, 'monomial, or nil

      putv(db, QEDB_ANSWERMODE, 'undefined);         % AnswerMode; 'raw, 'standard, or nil
      % The following fields change during execution:
      putv(db, QEDB_BLOCKSYMBOLS, 'undefined);
      putv(db, QEDB_BLOCKVARLISTS, 'undefined);
      putv(db, QEDB_BLOCKS, 'undefined);
      putv(db, QEDB_LASTBLOCKINPUTFORMULA, 'undefined);

      putv(db, QEDB_VARS, 'undefined);               % Vars; list of existentially quantified variables to be eliminated
      putv(db, QEDB_FORMULA, 'undefined);            % F; matrix formula of the current block
      putv(db, QEDB_VARIABLES, 'undefined);          % list of existentially quantified variables to be eliminated
      putv(db, QEDB_FORMULA, 'undefined);            % matrix formula of the current block
      putv(db, QEDB_ANSWER, 'undefined);
      putv(db, QEDB_SUCCESSNODES, 'undefined);       % SuccessNodes; list
      putv(db, QEDB_FAILURENODES, 'undefined);       % FailureNodes; list


@@ 82,12 77,11 @@ procedure qedb_print(db: Vector): Vector;
      ioto_tprin2t {"    InputFormula:          ", getv(db, QEDB_INPUTFORMULA)};
      ioto_tprin2t {"    InputTheory:           ", getv(db, QEDB_INPUTTHEORY)};
      ioto_tprin2t {"    NoAssumeVars:          ", getv(db, QEDB_NOASSUMEVARS)};
      ioto_tprin2t {"    AnswerMode:            ", getv(db, QEDB_ANSWERMODE)};
      ioto_tprin2t {"    AssumeMode:            ", getv(db, QEDB_ASSUMEMODE)};
      ioto_tprin2t {"    BlockSymbols:          ", getv(db, QEDB_BLOCKSYMBOLS)};
      ioto_tprin2t {"    BlockVarLists:         ", getv(db, QEDB_BLOCKVARLISTS)};
      ioto_tprin2t {"    AnswerMode:            ", getv(db, QEDB_ANSWERMODE)};
      ioto_tprin2t {"    Blocks:                ", getv(db, QEDB_BLOCKS)};
      ioto_tprin2t {"    LastBlockInputFormula: ", getv(db, QEDB_LASTBLOCKINPUTFORMULA)};
      ioto_tprin2t {"    Vars:                  ", getv(db, QEDB_VARS)};
      ioto_tprin2t {"    Vars:                  ", getv(db, QEDB_VARIABLES)};
      ioto_tprin2t {"    Formula:               ", ioto_smaprin rl_prepfof getv(db, QEDB_FORMULA)};
      ioto_tprin2t {"    Answer:                ", getv(db, QEDB_ANSWER)};
      ioto_tprin2t {"    SuccessNodes:          ", getv(db, QEDB_SUCCESSNODES)};


@@ 105,12 99,11 @@ procedure qedb_verbosePrint(db: Vector): Vector;
      ioto_tprin2t {"    #InputFormula:          ", rl_atnum getv(db, QEDB_INPUTFORMULA)};
      ioto_tprin2t {"    #InputTheory:           ", length getv(db, QEDB_INPUTTHEORY)};
      ioto_tprin2t {"    NoAssumeVars:           ", getv(db, QEDB_NOASSUMEVARS)};
      ioto_tprin2t {"    AnswerMode:             ", getv(db, QEDB_ANSWERMODE)};
      ioto_tprin2t {"    AssumeMode:             ", getv(db, QEDB_ASSUMEMODE)};
      ioto_tprin2t {"    BlockSymbols:           ", getv(db, QEDB_BLOCKSYMBOLS)};
      ioto_tprin2t {"    BlockVarLists:          ", getv(db, QEDB_BLOCKVARLISTS)};
      ioto_tprin2t {"    AnswerMode:             ", getv(db, QEDB_ANSWERMODE)};
      ioto_tprin2t {"    Blocks:                 ", getv(db, QEDB_BLOCKS)};
      ioto_tprin2t {"    #LastBlockInputFormula: ", rl_atnum getv(db, QEDB_LASTBLOCKINPUTFORMULA)};
      ioto_tprin2t {"    Vars:                   ", getv(db, QEDB_VARS)};
      ioto_tprin2t {"    Vars:                   ", getv(db, QEDB_VARIABLES)};
      ioto_tprin2t {"    #Formula:               ", rl_atnum getv(db, QEDB_FORMULA)};
      ioto_tprin2t {"    Answer:                 ", getv(db, QEDB_ANSWER)};
      ioto_tprin2t {"    #SuccessNodes:          ", length getv(db, QEDB_SUCCESSNODES)};


@@ 121,41 114,148 @@ procedure qedb_verbosePrint(db: Vector): Vector;
      return db
   end;

procedure qedb_getInputFormula(db);              getv(db, QEDB_INPUTFORMULA);
procedure qedb_getInputTheory(db);               getv(db, QEDB_INPUTTHEORY);
procedure qedb_getNoAssumeVars(db);              getv(db, QEDB_NOASSUMEVARS);
procedure qedb_getAnswerMode(db);                getv(db, QEDB_ANSWERMODE);
procedure qedb_getAssumeMode(db);                getv(db, QEDB_ASSUMEMODE);

procedure qedb_getBlockSymbols(db);              getv(db, QEDB_BLOCKSYMBOLS);
procedure qedb_getBlockVarLists(db);             getv(db, QEDB_BLOCKVARLISTS);
procedure qedb_getLastBlockInputFormula(db);     getv(db, QEDB_LASTBLOCKINPUTFORMULA);

procedure qedb_getVars(db);                      getv(db, QEDB_VARS);
procedure qedb_getF(db);                         getv(db, QEDB_FORMULA);
procedure qedb_getAnswer(db);                    getv(db, QEDB_ANSWER);
procedure qedb_getSuccessNodes(db);              getv(db, QEDB_SUCCESSNODES);
procedure qedb_getFailureNodes(db);              getv(db, QEDB_FAILURENODES);
procedure qedb_getCurrentTheory(db);             getv(db, QEDB_CURRENTTHEORY);
procedure qedb_getProduceAnwer(db);              getv(db, QEDB_PRODUCEANSWER);

procedure qedb_setInputFormula(db, theory);      putv(db, QEDB_INPUTFORMULA, theory);
procedure qedb_setInputTheory(db, theory);       putv(db, QEDB_INPUTTHEORY, theory);
procedure qedb_setNoAssumeVars(db, navs);        putv(db, QEDB_NOASSUMEVARS, navs);
procedure qedb_setAnswerMode(db, mode);          putv(db, QEDB_ANSWERMODE, mode);
procedure qedb_setAssumeMode(db, mode);          putv(db, QEDB_ASSUMEMODE, mode);

procedure qedb_setBlockSymbols(db, ql);          putv(db, QEDB_BLOCKSYMBOLS, ql);
procedure qedb_setBlockVarLists(db, vll);        putv(db, QEDB_BLOCKVARLISTS, vll);
procedure qedb_setLastBlockInputFormula(db, f);  putv(db, QEDB_LASTBLOCKINPUTFORMULA, f);

procedure qedb_setVars(db, vars);                putv(db, QEDB_VARS, vars);
procedure qedb_setF(db, f);                      putv(db, QEDB_FORMULA, f);
procedure qedb_setAnswer(db, answer);            putv(db, QEDB_ANSWER, answer);
procedure qedb_setSuccessNodes(db, nodes);       putv(db, QEDB_SUCCESSNODES, nodes);
procedure qedb_setFailureNodes(db, nodes);       putv(db, QEDB_FAILURENODES, nodes);
procedure qedb_setCurrentTheory(db, theory);     putv(db, QEDB_CURRENTTHEORY, theory);
procedure qedb_setProduceAnswer(db, ans);        putv(db, QEDB_PRODUCEANSWER, ans);
asserted procedure qedb_getInputFormula(db: Vector): Formula;
   getv(db, QEDB_INPUTFORMULA);

asserted procedure qedb_setInputFormula(db: Vector, theory: Theory): Vector;
   << putv(db, QEDB_INPUTFORMULA, theory); db >>;

asserted procedure qedb_getInputTheory(db: Vector): Theory;
   getv(db, QEDB_INPUTTHEORY);

asserted procedure qedb_setInputTheory(db: Vector, theory: Theory): Vector;
   << putv(db, QEDB_INPUTTHEORY, theory); db >>;

asserted procedure qedb_getNoAssumeVars(db: Vector): List;
   getv(db, QEDB_NOASSUMEVARS);

asserted procedure qedb_setNoAssumeVars(db: Vector, vars: List): Vector;
   << putv(db, QEDB_NOASSUMEVARS, vars); db >>;

asserted procedure qedb_getAssumeMode(db: Vector): Id;
   getv(db, QEDB_ASSUMEMODE);

asserted procedure qedb_setAssumeMode(db: Vector, mode: Id): Vector;
   << putv(db, QEDB_ASSUMEMODE, mode); db >>;

asserted procedure qedb_getAnswerMode(db: Vector): Id;
   getv(db, QEDB_ANSWERMODE);

asserted procedure qedb_setAnswerMode(db: Vector, mode: Id): Vector;
   << putv(db, QEDB_ANSWERMODE, mode); db >>;

asserted procedure qedb_getBlocks(db: Vector): List;
   getv(db, QEDB_BLOCKS);

asserted procedure qedb_setBlocks(db: Vector, blocks: List): Vector;
   << putv(db, QEDB_BLOCKS, blocks); db >>;

asserted procedure qedb_getLastBlockInputFormula(db: Vector): Formula;
   getv(db, QEDB_LASTBLOCKINPUTFORMULA);

asserted procedure qedb_setLastBlockInputFormula(db: Vector, f: Formula): Vector;
   << putv(db, QEDB_LASTBLOCKINPUTFORMULA, f); db >>;

asserted procedure qedb_getVariables(db: Vector): List;
   getv(db, QEDB_VARIABLES);

asserted procedure qedb_setVariables(db: Vector, vars: List): Vector;
   << putv(db, QEDB_VARIABLES, vars); db >>;

asserted procedure qedb_getFormula(db: Vector): Formula;
   getv(db, QEDB_FORMULA);

asserted procedure qedb_setFormula(db: Vector, f: Formula): Vector;
   << putv(db, QEDB_FORMULA, f); db >>;

asserted procedure qedb_getAnswer(db: Vector): List;
   getv(db, QEDB_ANSWER);

asserted procedure qedb_setAnswer(db: Vector, answer: List): Vector;
   << putv(db, QEDB_ANSWER, answer); db >>;

asserted procedure qedb_getSuccessNodes(db: Vector): List;
   getv(db, QEDB_SUCCESSNODES);

asserted procedure qedb_setSuccessNodes(db: Vector, nodes: List): Vector;
   << putv(db, QEDB_SUCCESSNODES, nodes); db >>;

asserted procedure qedb_getFailureNodes(db: Vector): List;
   getv(db, QEDB_FAILURENODES);

asserted procedure qedb_setFailureNodes(db: Vector, nodes: List): Vector;
   << putv(db, QEDB_FAILURENODES, nodes); db >>;

asserted procedure qedb_getCurrentTheory(db: Vector): Theory;
   getv(db, QEDB_CURRENTTHEORY);

asserted procedure qedb_setCurrentTheory(db: Vector, theory: Theory): Vector;
   << putv(db, QEDB_CURRENTTHEORY, theory); db >>;

asserted procedure qedb_getProduceAnwer(db: Vector): Boolean;
   getv(db, QEDB_PRODUCEANSWER);

asserted procedure qedb_setProduceAnswer(db: Vector, ans: Boolean): Vector;
   << putv(db, QEDB_PRODUCEANSWER, ans); db >>;

asserted procedure qeco_new(traversalMode: Id): Vector;
   % QE data for a block new.
   begin scalar db;
      db := mkvect(4);
      putv(db, 0, 'qeco);
      putv(db, 1, nil);                                             % Nodes: list (stack or queue) of QE tree working nodes
      putv(db, 2, if traversalMode eq 'bfs then nil else 'unused);  % LastNode: the last node in Nodes
      putv(db, 3, traversalMode);                                   % 'bfs (breadth-first search) or 'dfs (depth-first search)
      if traversalMode eq 'dfs then
      putv(db, 4, nil)
      else <<
         ASSERT( traversalMode eq 'bfs );
      putv(db, 4, 'unused)        % hashed dynamic programming data
      >>;
      return db
   end;

asserted procedure qeco_add(co: Container, new: NodeL): Container;
   begin scalar nodes, lastNode;
      if null new then
         return co;
      nodes := getv(co, 1);
      if getv(co, 3) eq 'bfs then <<
         lastNode := getv(co ,2);
         if null lastNode then
            lastNode := nodes := {pop new};
         for each node in new do
            if not member(node, nodes) then <<
               cdr lastNode := node . nil;
               lastNode := cdr lastNode
            >>;
         putv(co, 1, nodes);
         putv(co, 2, lastNode)
      >> else <<
         ASSERT( getv(co, 3) eq 'dfs );
         for each node in new do
            if not lto_hmember(node, getv(co, 4), 'co_hfn) then <<
               lto_hinsert(node, getv(co, 4), 'co_hfn);
               nodes := node . nodes
            >>;
         putv(co, 1, nodes)
      >>;
      return co
   end;

asserted procedure qeco_fetch(co: Container): Node;
   begin scalar nodes, node;
      nodes := getv(co, 1);
      ASSERT( not null nodes );
      node := pop nodes;
      if null nodes and getv(co, 3) eq 'bfs then
         putv(co, 2, nil);
      putv(co, 1, nodes);
      return node
   end;

asserted procedure qeco_isEmpty(co: Container): Boolean;
   null getv(co, 1);

asserted procedure cl_qe_new(f: Formula, theo: Theory): Formula;
   % Quantifier elimination. Eliminate as many quantifiers as possible from f,


@@ 172,11 272,11 @@ asserted procedure cl_qe_new(f: Formula, theo: Theory): Formula;
      db := cl_qe1_new(db);
      if rl_excp(db) then
         return db;
      return qedb_getF(db)
      return qedb_getFormula(db)
   end;

asserted procedure cl_qea_new(f: Formula, theo: Theory): List;
   % Extended quantifier elimination.
   % Extended quantifier elimination (aka "with answer").
   begin scalar db, !*rlqeans, !*rlsipo, !*rlsipw;
      !*rlqeans := t;
      !*rlsipo := t;


@@ 188,8 288,8 @@ asserted procedure cl_qea_new(f: Formula, theo: Theory): List;
      % Standard answers work only for decision problems. The old procedure
      % did not check this and rederr() could happen in the ANU module. We
      % now check this here, but we should think about checking later.
      qedb_setAnswerMode(db, if !*rlqestdans and null rl_fvarl f then'standard else 'raw);
      qedb_setAssumeMode(db, nil);
      qedb_setAnswerMode(db, if !*rlqestdans and null rl_fvarl f then'standard else 'raw);
      db := cl_qe1_new(db);
      if rl_excp(db) then
         return db;


@@ 209,86 309,145 @@ asserted procedure cl_gqe_new(f: Formula, theo: Theory, xNoAssumeVars: KernelL):
      qedb_setInputFormula(db, f);
      qedb_setInputTheory(db, theo);
      qedb_setNoAssumeVars(db, xNoAssumeVars);
      qedb_setAssumeMode(db, if !*rlqegenct then 'full else 'monomial);
      qedb_setAnswerMode(db, nil);
      db := cl_qe1_new(db);
      if rl_excp(db) then
         return db;
      % The old procedure applies rl_thsimpl(). This must be checked.
      return qedb_getCurrentTheory(db) . qedb_getFormula(db)
   end;

asserted procedure cl_gqea_new(f: Formula, theo: Theory, xNoAssumeVars: KernelL): DottedPair;
   % Generic extended quantifier elimination (aka "with answer").
   begin scalar db, !*rlqeans, !*rlqegen, !*rlsipo, !*rlsipw;
      !*rlqegen := t;
      !*rlqeans := t;
      !*rlsipo := t;
      !*rlsipw := t;
      db := qedb_new();
      qedb_setInputFormula(db, f);
      qedb_setInputTheory(db, theo);
      qedb_setNoAssumeVars(db, xNoAssumeVars);
      qedb_setAssumeMode(db, if !*rlqegenct then 'full else 'monomial);
      qedb_setAnswerMode(db, if !*rlqestdans and null rl_fvarl f then'standard else 'raw);
      db := cl_qe1_new(db);
      if rl_excp(db) then
         return db;
      % The old procedure applies rl_thsimpl(). This must be checked.
      return qedb_getCurrentTheory(db) . qedb_getF(db)
      return qedb_getCurrentTheory(db) . qedb_getAnswer(db)
   end;

asserted procedure cl_qe1_new(db: Vector): Vector;
   begin scalar f, theo, answer, ql, varll, bvl, point;
   begin scalar f, theo, answer, blocks, allQuantifiedVariables, point;
      f := qedb_getInputFormula(db);
      theo := qedb_getInputTheory(db);
      % I have a memory that AD suggested to simplify only the matrix.
      f := rl_simpl(rl_pnf f, theo, -1);
      if rl_excp(f) then
         return f;
      if not rl_quap rl_op f then
         return qedb_setF(db, f);
      {ql, varll, f, bvl} := cl_split f;
      {blocks, f, allQuantifiedVariables} := cl_split_new f;
      % Remove from the theory atomic formulas containing quantified variables:
      qedb_setCurrentTheory(db, for each atf in theo join if null intersection(rl_varlat atf, bvl) then {atf});
      qedb_setCurrentTheory(db, for each atf in theo join if null intersection(rl_varlat atf, allQuantifiedVariables) then {atf});
      % Prohibit assumptions on quantified variables:
      qedb_setNoAssumeVars(db, union(bvl, qedb_getNoAssumeVars(db)));
      qedb_setBlockSymbols(db, ql);
      qedb_setBlockVarlists(db, varll);
      qedb_setF(db, f);
      qedb_setNoAssumeVars(db, union(allQuantifiedVariables, qedb_getNoAssumeVars(db)));
      qedb_setBlocks(db, blocks);
      qedb_setFormula(db, f);
      if null blocks then <<
         % TS has moved this down a bit. There are no quantifiers left after
         % initial simplification.  Note the remark before that
         % simplification! We are here at a point where the formula and the
         % theory have been set properly in the db. However, the answer is
         % still undefined. Recall that the semantics of the answer depends
         % on the quantifier type of the outmost block, which does not exist
         % here. The definition of the answer as {f . nil} chosen here
         % corresponds to the old code and is semantically correct. Still, TS
         % does not like the entire situation.
         if not null qedb_getAnswerMode(db) then
            qedb_setAnswer(db, {f . nil});
         return db
      >>;
      cl_qe1!-iterate_new(db);
      ql := qedb_getBlockSymbols(db);
      varll := qedb_getBlockVarLists(db);
      blocks := qedb_getBlocks(db);
      theo := qedb_getCurrentTheory(db);
      f := cl_simpl(cl_unsplit(ql, varll, qedb_getF(db)), theo, -1);
      f := cl_simpl(cl_unsplit_new(blocks, qedb_getFormula(db)), theo, -1);
      if not null qedb_getAnswerMode(db) then <<
         % At present, we always requantify; no fallback QE with answers.
         if null ql or null cdr ql then <<
         if null blocks or null cdr blocks then <<
            % We have finished or at least reached the outmost block.
            answer := for each node in append(qedb_getSuccessNodes(db), qedb_getFailureNodes(db)) collect <<
               point := rl_qemkans(ce_ans(node), qedb_getLastBlockInputFormula(db))
                        where !*rlqestdans=(qedb_getAnswerMode(db) eq 'standard);
               cl_unsplit(ql, varll, ce_f(node) . point)
               cl_unsplit_new(blocks, ce_f(node)) . point
            >>
         >> else
            answer := {f . nil};
         qedb_setF(db, f);
         qedb_setFormula(db, f);
         qedb_setAnswer(db, answer);
         return db
      >>;
      if !*rlqefb and rl_quap rl_op f then
         theo . f := rl_fbqe(f, theo);
      qedb_setCurrentTheory(db, theo);
      qedb_setF(db, f);
      qedb_setFormula(db, f);
      return db
   end;

asserted procedure cl_split_new(f: Formula): List3;
   % Split a prenex formula. Returns a list containing the quantifier blocks,
   % the matrix, and the quantified variables. The quantifier blocks are are
   % list of pairs conatining the quantifier symbol and a list of variables.
   begin scalar currentQuantifier, currentQuantifiedVariables, blocks, allQuantifiedVariables;
      if not rl_quap rl_op f then
         return {nil, f, nil};
      currentQuantifier := rl_op f;
      while rl_quap rl_op f do <<
         if rl_op f neq currentQuantifier then <<
            push(currentQuantifier . currentQuantifiedVariables, blocks);
            currentQuantifier := rl_op f;
            currentQuantifiedVariables := nil
         >>;
         push(rl_var f, currentQuantifiedVariables);
         push(rl_var f, allQuantifiedVariables);
         f := rl_mat f
      >>;
      push(currentQuantifier . currentQuantifiedVariables, blocks);
      return {blocks, f, allQuantifiedVariables}
   end;

asserted procedure cl_unsplit_new(blocks: List, f: Formula): Formula;
   begin scalar result;
      result := f;
      for each block in blocks do
         for each variable in cdr block do
            result := rl_mkq(car block, variable, result);
      return result
   end;

asserted procedure cl_qe1!-iterate_new(db: Vector): Vector;
   % Iteratively apply cl_qeblock to quantifier blocks.
   begin scalar ql, varll, f, produceAnswer, theo, db, svrlidentify,
                svrlqeprecise, svrlqeaprecise, q, varl,rvl, w;
   begin scalar blocks, f, produceAnswer, theo, db, svrlidentify, svrlqeprecise, svrlqeaprecise, q, varl,rvl, w;
      svrlidentify := !*rlidentify;
      ql := qedb_getBlockSymbols(db);
      varll := qedb_getBlockVarLists(db);
      f := qedb_getF(db);
      blocks := qedb_getBlocks(db);
      f := qedb_getFormula(db);
      theo := qedb_getInputTheory(db);
      ASSERT( not null ql );
      while null rvl and ql do <<
         q := pop ql;
         varl := pop varll;
         qedb_setVars(db, varl);
         produceAnswer := not null qedb_getAnswerMode(db) and null ql;
      ASSERT( not null blocks );
      while null rvl and blocks do <<
         q . varl := pop blocks;
         qedb_setVariables(db, varl);
         produceAnswer := not null qedb_getAnswerMode(db) and null blocks;
         qedb_setProduceAnswer(db, produceAnswer);
         if produceAnswer then  % rubbish!
         if produceAnswer then  % TODO: rubbish!
            qedb_setLastBlockInputFormula(db, f);
         svrlqeprecise := !*rlqeprecise;
         svrlqeaprecise := !*rlqeaprecise;
         if ql then <<  % Should better be an argument of qeblock ...
         if blocks then <<  % Should better be an argument of qeblock ...
            off1 'rlqeprecise;
            off1 'rlqeaprecise
         >>;
         if q eq 'all then
            f := rl_simpl(rl_nnfnot f, theo, -1);
         qedb_setF(db, f);
         qedb_setFormula(db, f);
         qedb_setSuccessNodes(db, nil);
         qedb_setFailureNodes(db, nil);
         qedb_setCurrentTheory(db, theo);


@@ 311,27 470,24 @@ asserted procedure cl_qe1!-iterate_new(db: Vector): Vector;
            for each node in qedb_getFailureNodes(db) do
               rvl := union(rvl, ce_vl node);
         theo := qedb_getCurrentTheory(db);
         if ql then <<
         if blocks then <<
            onoff('rlqeprecise, svrlqeprecise);
            onoff('rlqeaprecise, svrlqeaprecise)
         >>
      >>;
      onoff('rlidentify, svrlidentify);
      if not null rvl then <<
         ql := q . ql;
         varll := rvl . varll
      >>;
      qedb_setF(db, f);
      qedb_setBlockSymbols(db, ql);
      qedb_setBlockVarlists(db, varll);
      if not null rvl then
         push(q . rvl, blocks);
      qedb_setFormula(db, f);
      qedb_setBlocks(db, blocks);
      return db
   end;

asserted procedure cl_qeblock4_new(db: Vector): Vector;
   begin scalar f, varl, theo, w, co, cvl, coe, successNodes, failureNodes;
      theo := qedb_getCurrentTheory(db);
      varl := qedb_getVars(db);
      f := qedb_getF(db);
      varl := qedb_getVariables(db);
      f := qedb_getFormula(db);
      if !*rlqegsd then
         f := rl_gsn(f, theo, 'dnf);
      co := qeco_new(if !*rlqedfs then 'dfs else 'bfs);


@@ 372,65 528,6 @@ asserted procedure cl_qeblock4_new(db: Vector): Vector;
      return db
   end;

asserted procedure qeco_new(traversalMode: Id): Vector;
   % QE data for a block new.
   begin scalar db;
      db := mkvect(4);
      putv(db, 0, 'qeco);
      putv(db, 1, nil);                                             % Nodes: list (stack or queue) of QE tree working nodes
      putv(db, 2, if traversalMode eq 'bfs then nil else 'unused);  % LastNode
      putv(db, 3, traversalMode);                                   % 'bfs (breadth-first search) or 'dfs (depth-first search)
      if traversalMode eq 'dfs then
         putv(db, 4, nil)
      else <<
         ASSERT( traversalMode eq 'bfs );
         putv(db, 4, 'unused)        % hashed dynamic programming data
      >>;
      return db
   end;

asserted procedure qeco_add(co: Container, new: NodeL): Container;
   begin scalar nodes, lastNode;
      if null new then
         return co;
      nodes := getv(co, 1);
      if getv(co, 3) eq 'bfs then <<
         lastNode := getv(co ,2);
         if null lastNode then
            lastNode := nodes := {pop new};
         for each node in new do
            if not member(node, nodes) then <<
               cdr lastNode := node . nil;
               lastNode := cdr lastNode
            >>;
         putv(co, 1, nodes);
         putv(co, 2, lastNode)
      >> else <<
         ASSERT( getv(co, 3) eq 'dfs );
         for each node in new do
            if not lto_hmember(node, getv(co, 4), 'co_hfn) then <<
               lto_hinsert(node, getv(co, 4), 'co_hfn);
               nodes := node . nodes
            >>;
         putv(co, 1, nodes);
      >>;
      return co
   end;

asserted procedure qeco_fetch(co: Container): Node;
   begin scalar nodes, node;
      nodes := getv(co, 1);
      ASSERT( not null nodes );
      node := pop nodes;
      if null nodes and getv(co, 3) eq 'bfs then
         putv(co, 2, nil);
      putv(co, 1, nodes);
      return node
   end;

asserted procedure qeco_isEmpty(co: Container): Boolean;
   null getv(co, 1);

endmodule;

end;

M packages/redlog/rlsupport/rlsupport.red => packages/redlog/rlsupport/rlsupport.red +12 -0
@@ 84,6 84,18 @@ inline procedure rl_skiplcbkt(proc);
         rederr {"expecting '{' in, ", proc, "but found", cursym!*}
   >>;

asserted procedure rl_include(filename: String);
   begin scalar path;
      if ifl!* then
         path := reversip explode2 car ifl!*
      else
         lprim {"empty ifl!* in include", filename};
      while not eqcar(path, '!/) do
         path := cdr path;
      path := nconc(reversip explode2 filename, path);
      infile(list2string reversip path)
   end;

endmodule;

end;

M packages/support/entry.red => packages/support/entry.red +8 -7
@@ 737,7 737,8 @@ defautoload(revision, rlsupport, expr, 2);

defautoload(copyright, rlsupport, expr, 2);

defautoload(rl_provideService, rlsupport, expr, 2);
put('rl_provideService, 'stat, 'rl_provideServiceStat);
defautoload(rl_provideServiceStat, rlsupport, expr, 0);

put('rl_type, 'stat, 'rl_typeStat);
defautoload(rl_typeStat, rlsupport, expr, 0);


@@ 748,19 749,19 @@ defautoload(rl_builtinStat, rlsupport, expr, 0);
put('rl_service, 'stat, 'rl_serviceStat);
defautoload(rl_serviceStat, rlsupport, expr, 0);

put('rl_blackBox, 'formfn, 'rl_formBlackBox);
defautoload(rl_formBlackBox, rlsupport, expr, 3);
put('rl_blackbox, 'stat, 'rl_blackboxStat);
defautoload(rl_blackboxStat, rlsupport, expr, 0);

defautoload(rl_servicewrapper, rlsupport, expr, 8);

defautoload(rl_exception, rlsupport, expr, 1);

defautoload(rl_exceptionp, rlsupport, expr, 1);

defautoload(rl_exc, rlsupport, expr, 1);

defautoload(rl_excp, rlsupport, expr, 1);

defautoload(rl_exception, rlsupport, expr, 1);

defautoload(rl_exceptionp, rlsupport, expr, 1);

% Redlog entry points

switch rlabout;