GSoC 2016 Application Bill N. Acha: Port Sympy's new assumptions module to Cpp

Jason K. Moore edited this page Mar 22, 2016 · 1 revision
Clone this wiki locally

#Personal Information
Name: Bill Ngoh Acha
University: University of Buea, Cameroon
GitHub: achabill
Blog: TimeZone: UTC + 1

#Personal background I am 3rd undergraduate student of the faculty of Engineering and Technology pursuing my B.Eng in Computer Engineering.
I love to code and play around mathematics. Aside from science, I love reading.

#Programmer background ##Programming environment I code on Linux and Windows. For windows, I use Visual Studio 15 running on Windows 10. In Linux, I use Sublime Text 3 for it's simplicity and friendliness. I currently run Ubuntu 15.04 64 bit and have been using Ubuntu since 2012. ##Programming experience I have more than 3 years experience programming C/C++. A little more than 2 years working with C# and Java. I am relatively new to Python and have not used it for more than 4 months.
I created a multimedia player in QT about a year ago. I have also worked on other symbolic algebra libraries like Linbox where I applied to do GSoC last year.
I have not explored sympy much by I have gone to the depths of the assumptions module which I am interested in. This module to so exciting and definitely needs to be in SymEngine.

from sympy.assumptions import Q,ask  
from import x,y  
proposition = ask(Q.even(x*y))  
f1 = Q.integer(x)  
f2 = Q.even(y)  
assumptions = f1 & f2  
result = ask(proposition,assumptions)  
print result

I joined GitHub in 2014 and have been using Git since.

#Project ##Achievement Working on this project I'll meet programmers around the world whom I'll learn from.
Also, I'll like to be part of the contributors to open source and to SymEngine.
Making contribution by taking up this project will be a large force in kick starting a long term relationship with SymEngine. Being part of SymEngine's active development will greatly improve my communication and programming skills. ##Qualification For this project, I'll be working on assumptions, boolean algebra and satisfiability.
I've taken relevant courses including Calculus, Linear algebra, algorithms, data structures and satisfiability.
I've gone through Sympys's assumptions module through code and documentation. Also, I've gone through SymEngine's code base and am comfortable with the code. ##Current implementation Sympy has a new assumptions module. On the other hand, SymEngine doesn't have any. Looking at Sympy's assumptions module, it relies heavily on their logic module which also, SymEngine does not have. So the assumptions is completely new to SymEngine. ##Time availability My summer starts in June 2nd and classes resume in early October. Even though I'll be in school from April 22nd to June 1st, I'll compensate for the 40h week during the weekends as my school program allows me to handle it. I'll be completely available during the summer.
##Project details SymEngine does not have an assumptions module. From inspecting Sympy's assumtions, I realize that a logic module is needed.
I do not aim to completely port Sympys assumptions to SymEngine but to lay a framework for future work. As such, the design of this module will remain flexible and follow Sympys design as much as possible. ###Plan The project will be divided in 2 major phases

  1. Logic Module
  2. Assumptions Module

####Logic Module The logic module here is a premature module that only implements classes that are relevant to assumptions. It's design will greatly follow that of Sympy's logic.boolalg

Required classes include:

  • Boolean - Base class for all boolean types
  • BooleanFunction - Function that lives in Boolean space. Used as base class for And, Or, Not, etc.
  • And - Logical And
  • Or - Logical Or
  • Nor - Logical Nor
  • Not - Logical Not
  • Implies - Logical implication
  • Equivalent - Equivalence relation

Required methods include:

  • to_cnf(BooleanFunction expr) - Convert a propositional logical expr to CNF
  • satisfialbe(BooleanFunction expr) - Check satisfiability of a propositional sentence.
  • conjucts(BooleanFunction expr) - Return a list of the conjuncts in the expr

####Assumptions Module Classes:

  • AssumptionKeys
    • real
    • imaginary
    • complex
    • integer
    • rational
    • positive
    • negative
    • zero
    • even
    • odd
    • prime
    • is_true
  • AssumptionsContext - Set representing assumptions
  • AppliedPredicate - The class of expressions resulting from applying a Predicate.
  • Predicate - A predicate is a function that returns a boolean value.
  • ask(AppliedPredicate proposition, BooleanFunction assumptions, AssumptionsContext context = global_assumptions )
  • refine(Expression expr, BooleanFunction assumptins) - Simplify an expression using assumptions.
  • AskHandlers
    • AskPrimeHandler
    • AskEvenHandler
    • AskOddHandler
    • AskNegativeHandler
    • AskPositiveHandler
    • AskIntegerHandler
    • AskRationalHandler
    • AskRealHandler
    • AskImaginaryHandler
    • AskComplexHandler
  • satask(AppliedPredicate proposition, BooleanFunction assumptions, AssumptionsContext context = global_assumptions) - use satsolver. pycosat

###API //symbols RCP x = symbol("x") RCP y = symbol("y")

//basic logic
RCP<const And> and = And(x,y)
RCP<const Or> or = Or(x,y)
RCP<cost Not> not = Not(true)
std::cout << *not << std:end; // false  
RCP<const Equivalent> eq  = Equivalent(x, And(x,true))
std::cout << *eq << std::endl; // x

RCP<const Number> n = integer(4)
std::cout << ask(Q.even(n)) << std::endl;
RCP<const Number> rat = Rational::from_two_ints(*integer(2), *integer(4));
std::cout << *ask(Q.rational(rat)) << std::endl; 

RCP<const AppliedPredicate> proposition = Q.even(mul(x,y));
RCP<const AppliedPredicate> f1 = Q.integer(x);
RCP<const AppliedPredicate> f2 = Q.even(y);
RCP<const And> assumptions = And(f1,f2);
RCP<const Basic> result = ask(proposition, assumptions);
std::cout << *result << std::endl;

RCP<const Mul> arg = proposition.arg(); // Mul(x,y)
RCP<const Predicate> pred = proposition.func(); //Q.even

###TimeLine ####Pre GSoC

  • Develope bonding with the community
  • Develop procedures in converting the proposition and assumptions to an SAT problem that can be solved by SAT solvers like pycosat and SMT solver (like Z3).
  • Work on patch

####Community bonding period

  • Familiarize with mentors and the community
  • Continue inspecting sympys implementation of assumptions module
  • Continue working on procedures to convert assumptions and proposition to an SAT problem.

####Coding #####week 1 : May 23 - May 30

  • Boolean
  • BooleanFunction
  • And
  • Or
  • Not

#####week 2 : June 1 - June 7

  • Implies
  • Equivalent

#####week 3 : June 8 - June 20

  • to_cnf
  • conjucts

#####Mid-term evaluation: June 20 - June 27

#####week 4,5 : July 1 - July 15

  • satisfiable

#####week 6 : July 16 - July 23

  • AppliedPredicate
  • Predicate
  • AssumptionKeys

#####week 7 : July 24 - July 29

  • AskHandlers
  • refine

#####week 8 : August 1 - August 7

  • ask
  • satask

#####week 9 : August 8 - August 15

  • Testing

#####week 10 : Submit code and Final evaluation

####Blog During GSoC, I'll maintain a blog at where I'll record all work progress.