INTERFACE JunoCompileNF;

IMPORT JunoAST, JunoScope, JunoCompileErr, StackTbl;

PROCEDURE Normalize(p: JunoAST.Formula; tbl: StackTbl.T): JunoAST.NormalForm;

Returns a formula equivalent to p that has been ``normalized''. A constraint is in ``normal form'' if it is an (optional) E quantification (all of whose variables are unhinted) over (optional) conjunctions of ``normal simple formulas''. A normal simple formula takes one of the following forms:

         1) x ~= y,
         2) P(v_1,...,v_n)
         3) x ~= F(v_1,...,v_n)
         4) CF(nsf_1,...,nsf_n)

where ~= denotes ~ (near) or = (equality), x, y, and v_1 through v_n denote either literals or variables, nsf_1 through nsf_n denote normal simple formulas, P is a predicate, F is a function, and CF is a compound formula other than AND (i.e., NOT or OR). Moreover, compound formulas (4) are guaranteed to be original top-level conjuncts of the input formula p. Note that a normal simple formula does not contain any grouped (parenthesized) expressions.

This is a purely syntactic transformation. The tbl is used to annotate new variables as they are introduced in E quantifications. New variables are not added to tbl. The variables in the result are all unhinted, and they all have their evar bits set.

Requires that all existentially quantified variables are distinct, and that every use of any of the existentially quantified variables occurs within the scope of its quantification.

PROCEDURE ToCmd(
    nf: JunoAST.NormalForm;
    scp: JunoScope.T;
    stack_tbl: StackTbl.T;
    xtra_vars: JunoAST.NearVarList := NIL):
  JunoAST.Cmd RAISES {JunoCompileErr.Error};

Return a command that solves the unknown variables in nf.var \union xtra_vars for the conjunction nf.conj if there is a solution, and fails otherwise. The resulting command contains only simple equality queries, assignments, and queries to be passed to the Juno solver (i.e., JunoAST.ConjQuery's). The queries passed to the Juno solver must be a conjunction of normal simple formulas that contain only primitive predicates (REAL, TEXT, PAIR) and functions (+, *, CONS, SIN, COS, ATAN, EXP, LN).

Requires all evar fields of the variables in nf.var to be true, all evar fields of the variables in xtra_vars to be false, and all variables in nf.var \union xtra_vars to be unhinted. The frozen bits in nf.var must all be reset, and those of xtra_vars are set iff the corresponding variable's value has been initialized.

END JunoCompileNF.