~trn/reduce-algebra

14ea731d477b4075bd3d025b2cba565b29a68aa4 — Jeffrey H. Johnson 11 days ago b471c93 + 6e68937
Merge branch 'svn/trunk'
M packages/redlog/cl/clqe.red => packages/redlog/cl/clqe.red +6 -2
@@ 298,6 298,8 @@ asserted procedure cl_gqe(f: Formula, theo: Theory, xbvl: KernelL): TheoryFormul
   % \longleftrightarrow \phi$. $\phi$ is obtained from [f] by eliminating as
   % many quantifiers as possible. Accesses the switch [rlqepnf]; if [rlqepnf]
   % is on, then [f] must be prenex.
   if !*clqenew then cl_gqe_new(f, theo, xbvl) else

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


@@ 342,9 344,9 @@ asserted procedure cl_qe(f: Formula, theo: Theory): Formula;
   % [f] \longleftrightarrow \phi$. $\phi$ is obtained from [f] by eliminating
   % as many quantifiers as possible. Accesses the switch [rlqepnf]; if
   % [rlqepnf] is on, then [f] has to be prenex.
   begin scalar er, !*rlsipw, !*rlsipo;
      if !*clqenew then return cl_qe_new(f, theo);
   if !*clqenew then cl_qe_new(f, theo) else

   begin scalar er, !*rlsipw, !*rlsipo;
      !*rlsipw := !*rlsipo := t;
      er := cl_qe1(f, theo, nil);
      if rl_exceptionp er then


@@ 364,6 366,8 @@ asserted procedure cl_qea(f: Formula, theo: Theory): ExtendedQeResult;
   %  of the parameters, [f] holds, and $A_i$ describes a satisfying sample
   %  point. Accesses the switch [rlqepnf]; if [rlqepnf] is on, then [f] has
   %  to be prenex.
   if !*clqenew then cl_qea_new(f, theo) else

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

M packages/redlog/cl/clqenew.red => packages/redlog/cl/clqenew.red +83 -9
@@ 98,6 98,29 @@ procedure qedb_print(db: Vector): Vector;
      return db
   end;

procedure qedb_verbosePrint(db: Vector): Vector;
   begin scalar !*nat;
      ioto_tprin2t {"{"};
      ioto_tprin2t {"    TypeTag:                ", getv(db, QEDB_TAG)};
      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 {"    #LastBlockInputFormula: ", rl_atnum getv(db, QEDB_LASTBLOCKINPUTFORMULA)};
      ioto_tprin2t {"    Vars:                   ", getv(db, QEDB_VARS)};
      ioto_tprin2t {"    #Formula:               ", rl_atnum getv(db, QEDB_FORMULA)};
      ioto_tprin2t {"    Answer:                 ", getv(db, QEDB_ANSWER)};
      ioto_tprin2t {"    #SuccessNodes:          ", length getv(db, QEDB_SUCCESSNODES)};
      ioto_tprin2t {"    #FailureNodes:          ", length getv(db, QEDB_FAILURENODES)};
      ioto_tprin2t {"    #CurentTheory:          ", length getv(db, QEDB_CURRENTTHEORY)};
      ioto_tprin2t {"    ProduceAnswer:          ", getv(db, QEDB_PRODUCEANSWER)};
      ioto_tprin2t {"}"};
      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);


@@ 137,25 160,71 @@ procedure qedb_setProduceAnswer(db, ans);        putv(db, QEDB_PRODUCEANSWER, an
asserted procedure cl_qe_new(f: Formula, theo: Theory): Formula;
   % Quantifier elimination. Eliminate as many quantifiers as possible from f,
   % yielding a formula g such that theo |= f <=> g.
   begin scalar db, !*rlsipw, !*rlsipo;
      !*rlsipw := !*rlsipo := t;
   begin scalar db, !*rlsipo, !*rlsipw;
      !*rlsipo := t;
      !*rlsipw := t;
      db := qedb_new();
      qedb_setInputFormula(db, f);
      qedb_setInputTheory(db, theo);
      qedb_setNoAssumeVars(db, nil);
      qedb_setAnswerMode(db, nil);
      qedb_setAssumeMode(db, nil);
      cl_qe1_new(db);
      db := cl_qe1_new(db);
      if rl_excp(db) then
         return db;
      return qedb_getF(db)
   end;

asserted procedure cl_qea_new(f: Formula, theo: Theory): List;
   % Extended quantifier elimination.
   begin scalar db, !*rlqeans, !*rlsipo, !*rlsipw;
      !*rlqeans := t;
      !*rlsipo := t;
      !*rlsipw := t;
      db := qedb_new();
      qedb_setInputFormula(db, f);
      qedb_setInputTheory(db, theo);
      qedb_setNoAssumeVars(db, nil);
      % 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);
      db := cl_qe1_new(db);
      if rl_excp(db) then
         return db;
      return qedb_getAnswer(db)
   end;

asserted procedure cl_gqe_new(f: Formula, theo: Theory, xNoAssumeVars: KernelL): DottedPair;
   % Generic quantifier elimination. Eliminate as many quantifiers as possible
   % from f, yielding a formula g such that theo |= f <=> g. The procedure is
   % allowed to assume inequations on parameters that are not in
   % xNoAssumeVars. Those assumptions are added to theo.
   begin scalar db, !*rlqegen, !*rlsipo, !*rlsipw;
      !*rlqegen := t;
      !*rlsipo := t;
      !*rlsipw := t;
      db := qedb_new();
      qedb_setInputFormula(db, f);
      qedb_setInputTheory(db, theo);
      qedb_setNoAssumeVars(db, xNoAssumeVars);
      qedb_setAnswerMode(db, nil);
      qedb_setAssumeMode(db, if !*rlqegenct then 'full else 'monomial);
      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)
   end;

asserted procedure cl_qe1_new(db: Vector): Vector;
   begin scalar f, theo, answer, ql, varll, bvl;
   begin scalar f, theo, answer, ql, varll, bvl, point;
      f := qedb_getInputFormula(db);
      theo := qedb_getInputTheory(db);
      f := rl_simpl(rl_pnf f, theo, -1);
      if f eq 'inctheo then
         return rl_exception 'inctheo;
      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;


@@ 175,8 244,11 @@ asserted procedure cl_qe1_new(db: Vector): Vector;
         % At present, we always requantify; no fallback QE with answers.
         if null ql or null cdr ql then <<
            % We have finished or at least reached the outmost block.
            answer := for each node in append(qedb_getSuccessNodes(db), qedb_getFailureNodes(db)) collect
               cl_unsplit(ql, varll, ce_f(node) . rl_qemkans(ce_ans(node), qedb_getLastBlockInputFormula(db)))
            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)
            >>
         >> else
            answer := {f . nil};
         qedb_setF(db, f);


@@ 206,7 278,7 @@ asserted procedure cl_qe1!-iterate_new(db: Vector): Vector;
         qedb_setVars(db, varl);
         produceAnswer := not null qedb_getAnswerMode(db) and null ql;
         qedb_setProduceAnswer(db, produceAnswer);
         if produceAnswer then
         if produceAnswer then  % rubbish!
            qedb_setLastBlockInputFormula(db, f);
         svrlqeprecise := !*rlqeprecise;
         svrlqeaprecise := !*rlqeaprecise;


@@ 220,7 292,9 @@ asserted procedure cl_qe1!-iterate_new(db: Vector): Vector;
         qedb_setSuccessNodes(db, nil);
         qedb_setFailureNodes(db, nil);
         qedb_setCurrentTheory(db, theo);
         if !*rlverbose then << qedb_verbosePrint(db) >>;
         cl_qeblock4_new(db);
         if !*rlverbose then << qedb_verbosePrint(db) >>;
         if q eq 'all then <<
            w := qedb_getSuccessNodes(db);
            w := for each x in w collect

M packages/redlog/cl/clsimpl.red => packages/redlog/cl/clsimpl.red +5 -5
@@ 46,15 46,15 @@ asserted procedure cl_simpl(f: Formula, atl: List, n: Integer): Formula;
   % at level [n].
   begin scalar w;
      atl := cl_simplifyTheory atl;
      if atl eq 'inctheo then
         return rl_exc 'inctheo;
      if rl_excp atl then
         return atl;
      w := rl_smupdknowl('and, atl, nil, n+1);
      if w eq 'false then
         return 'inctheo;
         return rl_exc("inconsistent theory");
      return cl_simpl1(f, w, n, nil)
   end;

asserted procedure cl_simplifyTheory(atl: List);
asserted procedure cl_simplifyTheory(atl: List): List;
   % Common logic simplify theory. [atl] is a THEORY. Returns either a
   % list $l$ of atomic formulas, or the identifier [inctheo]. In the
   % first case the conjunction over $l$ is equivalent to the


@@ 72,7 72,7 @@ asserted procedure cl_simplifyTheory(atl: List);
            natl := w . natl
      >>;
      if atf eq 'inctheo then
         return 'inctheo;
         return rl_exc("inconsistent theory");
      return natl
   end;


M packages/redlog/rlsupport/rlservice.red => packages/redlog/rlsupport/rlservice.red +20 -20
@@ 517,16 517,14 @@ asserted procedure rl_servicewrapper(rl_!*b: Applicable, u: List, names: List, t
      for each arg in u do <<
         pos := pos + 1;
         % For named parameters we admit both '=>' (replaceby) and '=' equal.
         % However, '=' can lead to ambiguities, when the "equations" occurs at
         % a position where it would make sense as a positional parameter (e.g.
         % a formula). In such cases we decide in favor of the positional
         % argument. We expect such situations to be rare. Users would use
         % variables names in single equations that do not clash with parameter
         % names, or just use '=>' in such cases. Relevant types are explicitly
         % flagged [equational].
         if eqcar(arg, 'replaceby) or
            eqcar(arg, 'equal) and not flagp(nth(types, pos), 'equational)
         then
         % However, '=' can lead to ambiguities, when the "equation" occurs
         % at a position where it would make sense as a positional parameter
         % (e.g. a formula). In such cases we decide in favor of the
         % positional argument. We expect such situations to be rare. Users
         % would use variables names in single equations that do not clash
         % with parameter names, or just use '=>' in such cases. Relevant
         % types are explicitly flagged [equational].
         if eqcar(arg, 'replaceby) or eqcar(arg, 'equal) and not rl_typeEquationalP(nth(types, pos)) then
            push(cadr arg . caddr arg, nargs)
         else
            nth(rargs, pos) := arg


@@ 640,22 638,24 @@ asserted procedure rl_knownImplementations(x: Id): List;
asserted procedure rl_exc(x: Any): DottedPair;
   % Create an "exception" as a return value in case of unexpected situations,
   % e.g. inconsistent theories. Exceptions are recognized by
   % [rl_servicewrapper] in the AM/SM interface, where rl_excErr is called with
   % ['!*rl_exc!* . x]. SM Redlog code might explicitly checked for exceptions
   % using [rl_excP] and not necessarily throw an error, since some exceptions
   % can be managed.
   % rl_servicewrapper() in the AM/SM interface, where rl_excErr() is called
   % with('!*rl_exc!* . x). SM Redlog code can explicitly check for
   % exceptions using rl_excP(). It need  not necessarily throw an error,
   % since some exceptions can be managed.
   '!*rl_exc!* . x;

% Return values constructed with [rl_exc] should be ignored by the assert
% module. For Redlog it is recommended to specifiy, e.g., "Formula" as a return
% type of a function, which might use [rl_exc].
% Return values constructed with rl_exc() should be ignored by the assert
% module:
flag('(!*rl_exc!*), 'assert_ignore);

asserted procedure rl_excP(x: Any): Boolean;
   % Check is return value is an exception.
asserted procedure rl_excp(x: Any): Boolean;
   % Check is return value is an exception. Since eqcar() checks pairp, this
   % function can be safely applied to any Lisp data type. eqcar() is not
   % mentioned in the Standard Lisp Report. It is documented in the PSL
   % manual and implemented and used throughout CSL and Reduce.
   eqcar(x, '!*rl_exc!*);

asserted procedure rl_excErr(exc: DottedPair);
asserted procedure rl_excerr(exc: DottedPair);
   % Throw an error in case of exception.
   rederr cdr exc;