githwxi/ATS-Postiats — pull request #77 by wdblair (2014-05-16 19:13:30+00:00)
Title: Adjustments for External Constraint Solver

These changes were made in order to support an external constraint solver for ATS. They include the following sections and are the only changes needed to make the new solver work. A separate pull request will be made for the work-in-progress solver.

Exporting More Sort Information
======================

In order to support interpretations for functions given in external SMT2 files, I need to know the sorts for static const functions. In this patch, I export this info so I can reconstruct function signatures in my constraint solver.

Decreasing Metrics
==============

I make s2exp_metdec_reduce a function specified in pats_staexp2_util.sats, instead of local to pats_constraint3.dats. This allows me to get termination metrics as static expression which my constraint solver can readily handle. Otherwise, I would need to do the simplification myself which involves the "hnfize" functions. These, in turn, rely on the static environment which I do not have available in my constraint solver.

Prevent Normalizing Static Variables
==========================

This is a subtle issue I found last summer when using an SMT solver to do constraint solving. During type checking, we may encounter a static that has a substitution made for it in the current environment. When we call "s2exp_hnfize_flag_svar" on this svar, we will replace the svar with the expression it is equal to. This is not good for the SMT solver, because later we will check constraints involving the svar, in question and we may have left out some assertions by normalizing it. For example, if we want to assert two static variables n and p are equal, we would need the following

(assert (= n p))

but if the type checker has a substitution for both n and p, normalizing n and p gives the following

;; n -> 0
;; p -> 0
(assert (= 0 0))

Which is perfectly valid, but doesn't inform the SMT solver that n and p are actually equal. This causes later constraints about n and p to fail. For this reason, I add a flag to pats_global.sats to indicate we are exporting constraints, and then skip normalizing s2vars if so.