Theory RCLogic
theory RCLogic
imports Wellformed
begin
hide_const Syntax.dom
chapter ‹Refinement Constraint Logic›
text ‹ Semantics for the logic we use in the refinement constraints. It is a multi-sorted, quantifier free
logic with polymorphic datatypes and linear arithmetic. We could have modelled by using one of the
encodings to FOL however we wanted to explore using a more direct model. ›
section ‹Evaluation and Satisfiability›
subsection ‹Valuation›
text ‹ Refinement constraint logic values. SUt is a value for the uninterpreted
sort that corresponds to basic type variables. For now we only need one of these universes.
We wrap an smt\_val inside it during a process we call 'boxing'
which is introduced in the RCLogicL theory ›