Wiki » History » Revision 4
Revision 3 (Karine Even Mendoza, 13/05/2016 17:53) → Revision 4/27 (Karine Even Mendoza, 13/05/2016 18:02)
h1. Skype Meeting 03/05/2016 Why we need combination of theories, multipication of non-constants Short Code example: t1 = x*y; x' = x; y'= y; t2 = x'*y'; assert(t1 != t2); Solution: t1 = f(x, y) ===== h1. Work Plan - Meeting 9-11/05/2016 h2. Mile-Stones I. Propositional logic MC for FunFrog + OpenSMT2 Tasks (1) - (3) II. Theories MC for FunFrog + OpenSMT2/Other Tasks (1) - (3) III. Theory aware MC for FunFrog + OpenSMT2 Tasks (1) - (4) and (5.5) IV. Incremental SMT for FunFrog Tasks (1) - (4) V. Unbounded MC (loops) Tasks (1) - (4) h3. Tasks for OpenSMT2 # Library + Headers (A,L) # Interface (ALL) # Interpolation (L,S) # Incrementality - Push/Pop (M,A) # Parallelizaion and clause sharing between theories (M,A) 5.5 Quantifiers (G,A,M) =====