Version 1.1.0

[nmacedo]

Major changes:

• proper past semantics through loop unrolling
• proper temporal instance iteration
• instances assumed to always be infinite
• evaluator for instances from unbounded engined
• skolems not considered part of temporal instances
• properly terminates electrod processes

Full description:

• two alternative encodings for the unrolling of formulas with past operators, one with explicit unrolls and another implicit (close Review past BMC semantics #24)
• unified relation hierarchy with that of Alloy5, easier to identify relations as atoms, skolems and variable
• atom relations are ignored during symmetry breaking
• unified representation for temporal instances from bounded/unbounded engines
• the previous enables the evaluator on instances from the unbounded engine (close Allow temporal evaluator over sequence traces #27)
• formulas and int expressions can also be evaluated at particular instants
• the evaluation of temporal instances relies on the original universe of the bounds (close Evaluating temporal instances returns with expanded universe #36)
• assumed temporal instances always loop, simplified translation and bounds accordingly (close Simplify translation for looping traces #26)
• two alternative encodings for temporal iteration, one reifies atoms the other uses the some-disj pattern (close#25)
• in the reification process atom relations are ignored during symmetry breaking
• in the formulation of instances, relations not mentioned in the formula are ignored (close Inconsistent iteration when relation non-referred #31)
• an optimised iteration procedure for the bounded engine that acts directly on SAT
• fixed the translation of symbolic bounds to invert bounds for "difference" expressions (close Symbolic bound resolution with difference #22)
• termination of electrod processes properly terminates children smv processes
• skolem variables are not translated back into temporal instances, nor considered during iteration (but are still used for performance purposes) (close Skolems on temporal expansion  #32 Skolemized rels not added to temporal instance #33)
• fixed a bug when expanding constants where state atoms would become part of the universe (close Univ not correctly expanded in bounded #28)
• fixed a bug when slicing formulas with extra relations (eg, created during trivial iteration)
• fixed a bug when slicing single conjunct formulas
• added support for skolems at electrod (protected symbol $)
• added missing neq method to integer expressions
• fixed bug on running non-decomposed with decomposed bounds
• iteration for trivial solutions simplified
• fetched no overflow fixes from Alloy5
• solving engines now register whether unbounded
• pmaxsat yices disabled due to unpredictable results
• fixed a bug on symbolic bounds for static relations depending on variable ones (close Bug on resolution of static relations with variable symbolic bounds #35)
• rename identifiers that are protected keywords in electrod (close Electrod protected keywords #30)