## ~trn/reduce-algebra

14ea731d477b4075bd3d025b2cba565b29a68aa4 — Jeffrey H. Johnson 11 days ago
Merge branch 'svn/trunk'

4 files changed, 114 insertions(+), 36 deletions(-)

M packages/redlog/cl/clqe.red
M packages/redlog/cl/clqenew.red
M packages/redlog/cl/clsimpl.red
M packages/redlog/rlsupport/rlservice.red

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 {"    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 {"    #SuccessNodes:          ", length getv(db, QEDB_SUCCESSNODES)};
+      ioto_tprin2t {"    #FailureNodes:          ", length getv(db, QEDB_FAILURENODES)};
+      ioto_tprin2t {"    #CurentTheory:          ", length getv(db, QEDB_CURRENTTHEORY)};
+      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);

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_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;
+   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_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))
+               cl_unsplit(ql, varll, ce_f(node) . point)
+            >>
>> else
qedb_setF(db, f);

@@ 206,7 278,7 @@ asserted procedure cl_qe1!-iterate_new(db: Vector): Vector;
qedb_setVars(db, varl);
+         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
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;