Propositional Logic: Proposition Evaluator

Question

We implement a C++ class Proposition that represents a (possibly compound) propositional logic statement made up of named atomic variables combined with the operators AND, OR, NOT, IMPLIES and IFF.

We then use it to find all the truth assignments of the following proposition:

((A and not B) implies C) and ((not A) iff (B and C))

Once everything is defined, the snippet of C++ code that evaluates this proposition is:

auto proposition = ("A"_var && !"B"_var).implies("C"_var) &&
                   (!"A"_var).iff("B"_var && "C"_var);

auto truth_assignments = proposition.evaluate_all({"A", "B", "C"});

Language features used include polymorphism, implicit sharing, recursive data types, operator overloading and (new in C++ 2011 and gcc 4.7) user-defined literals.

// (C) 2012, Andrew Tomazos <andrew@tomazos.com>.  Public domain.

#include <cassert>
#include <memory>
#include <set>
#include <vector>
#include <string>
#include <iostream>
using namespace std;

struct Proposition;

// The expression...
//
//     "foo"_var
//
// ...creates an atomic proposition variable with the name 'foo'
Proposition operator"" _var (const char*, size_t);

// Represents a compound proposition
struct Proposition
{
    // A.implies(B): means that A (antecendant) implies ==> B (consequent)
    Proposition implies(const Proposition& consequent) const;

    // A.iff(B): implies that A and B form an equivalence. A <==> B
    Proposition iff(const Proposition& equivalent) const;

    // !A: the negation of target A
    Proposition operator!() const;

    // A && B: the conjunction of A and B
    Proposition operator&&(const Proposition& conjunct) const;

    // A || B: the disjunction of A and B
    Proposition operator||(const Proposition& disjunct) const;

    // A.evaluate(T): Given a set T of variable names that are true (a truth assignment),
    //     will return the truth {true, false} of the proposition
    bool evaluate(const set<string>& truth_assignment) const;

    // A.evaluate_all(S): Given a set S of variables,
    //     will return the set of truth assignments that make this proposition true
    set<set<string>> evaluate_all(const set<string>& variables) const;

private:

    struct Base { virtual bool evaluate(const set<string>& truth_assignment) const = 0; };

    typedef shared_ptr<Base> pointer;

    pointer value;
    Proposition(const pointer& value_) : value(value_) {}

    struct Variable : Base
    {
        string name;
        virtual bool evaluate(const set<string>& truth_assignment) const
        {
            return truth_assignment.count(name);
        }
    };

    struct Negation : Base
    {
        pointer target;
        bool evaluate(const set<string>& truth_assignment) const
        {
            return !target->evaluate(truth_assignment);
        }
    };

    struct Conjunction : Base
    {
        pointer first_conjunct, second_conjunct;

        bool evaluate(const set<string>& truth_assignment) const
        {
            return first_conjunct->evaluate(truth_assignment)
                && second_conjunct->evaluate(truth_assignment);
        }
    };

    struct Disjunction : Base
    {
        pointer first_disjunct, second_disjunct;

        bool evaluate(const set<string>& truth_assignment) const
        {
            return first_disjunct->evaluate(truth_assignment)
                || second_disjunct->evaluate(truth_assignment);
        }
    };

    friend Proposition operator"" _var (const char* name, size_t sz);
};

Proposition operator"" _var (const char* name, size_t sz)
{
    auto variable = make_shared<Proposition::Variable>();
    variable->name = string(name, sz);
    return { variable };
}

Proposition Proposition::implies(const Proposition& consequent) const
{
    return  (!*this) || consequent;
};

Proposition Proposition::iff(const Proposition& equivalent) const
{
    return this->implies(equivalent) && equivalent.implies(*this);
}

Proposition Proposition::operator!() const
{
    auto negation = make_shared<Negation>();
    negation->target = value;
    return { negation };
}

Proposition Proposition::operator&&(const Proposition& conjunct) const
{
    auto conjunction = make_shared<Conjunction>();
    conjunction->first_conjunct = value;
    conjunction->second_conjunct = conjunct.value;
    return { conjunction };
}

Proposition Proposition::operator||(const Proposition& disjunct) const
{
    auto disjunction = make_shared<Disjunction>();
    disjunction->first_disjunct = value;
    disjunction->second_disjunct = disjunct.value;
    return { disjunction };
}

bool Proposition::evaluate(const set<string>& truth_assignment) const
{
    return value->evaluate(truth_assignment);
}

set<set<string>> Proposition::evaluate_all(const set<string>& variables) const
{
    set<set<string>> truth_assignments;

    vector<string> V(variables.begin(), variables.end());

    size_t N = V.size();

    for (size_t i = 0; i < (size_t(1) << N); ++i)
    {
        set<string> truth_assignment;

        for (size_t j = 0; j < N; ++j)
            if (i & (1 << j))
                truth_assignment.insert(V[j]);

        if (evaluate(truth_assignment))
            truth_assignments.insert(truth_assignment);
    }

    return truth_assignments;
}

int main()
{
    assert(  ("foo"_var) .evaluate({"foo"})); // trivially true
    assert(  ("foo"_var) .evaluate_all({"foo"})
             == set<set<string>> {{"foo"}} );

    assert(  (!"foo"_var) .evaluate({})); // basic negation
    assert(! (!"foo"_var) .evaluate({"foo"})); // basic negation
    assert(  (!"foo"_var) .evaluate_all({"foo"})
             == set<set<string>> {{}} );

    assert(  (!!"foo"_var) .evaluate({"foo"})); // double negation
    assert(  (!!"foo"_var) .evaluate_all({"foo"})
             == set<set<string>> {{"foo"}} );

    assert(  ("foo"_var && "bar"_var) .evaluate({"foo", "bar"})); // conjunction
    assert(! ("foo"_var && "bar"_var) .evaluate({"bar"})); // conjunction
    assert(! ("foo"_var && "bar"_var) .evaluate({"foo"})); // conjunction
    assert(! ("foo"_var && "bar"_var) .evaluate({})); // conjunction
    assert(  ("foo"_var && "bar"_var) .evaluate_all({"foo", "bar"})
             == set<set<string>>({{"foo", "bar"}}));

    assert(  ("foo"_var || "bar"_var) .evaluate({"foo", "bar"})); // disjunction
    assert(  ("foo"_var || "bar"_var) .evaluate({"bar"})); // disjunction
    assert(  ("foo"_var || "bar"_var) .evaluate({"foo"})); // disjunction
    assert(! ("foo"_var || "bar"_var) .evaluate({})); // disjunction
    assert(  ("foo"_var || "bar"_var) .evaluate_all({"foo", "bar"})
             == set<set<string>>({{"foo", "bar"}, {"foo"}, {"bar"}}));

    assert(  ("foo"_var.implies("bar"_var)) .evaluate({"foo", "bar"})); // implication
    assert(  ("foo"_var.implies("bar"_var)) .evaluate({"bar"})); // implication
    assert(! ("foo"_var.implies("bar"_var)) .evaluate({"foo"})); // implication
    assert(  ("foo"_var.implies("bar"_var)) .evaluate({})); // implication
    assert(  ("foo"_var.implies("bar"_var)) .evaluate_all({"foo", "bar"})
             == set<set<string>>({{"foo", "bar"}, {"bar"}, {}}));

    assert(  ("foo"_var.iff("bar"_var)) .evaluate({"foo", "bar"})); // equivalence
    assert(! ("foo"_var.iff("bar"_var)) .evaluate({"bar"})); // equivalence
    assert(! ("foo"_var.iff("bar"_var)) .evaluate({"foo"})); //equivalence
    assert(  ("foo"_var.iff("bar"_var)) .evaluate({})); // equivalence
    assert(  ("foo"_var.iff("bar"_var)) .evaluate_all({"foo", "bar"})
             == set<set<string>>({{"foo", "bar"}, {}}));

    cout << "((A and not B) implies C) and ((not A) iff (B and C)):" << endl << endl;

    auto proposition = ("A"_var && !"B"_var).implies("C"_var) && (!"A"_var).iff("B"_var && "C"_var);

    auto truth_assignments = proposition.evaluate_all({"A", "B", "C"});

    cout << "A    B    C" << endl;
    cout << "-----------" << endl;

    for (auto truth_assignment : truth_assignments)
    {
        for (auto variable : {"A", "B", "C"})
            cout << (truth_assignment.count(variable) ? "1" : "0") << "    ";
        cout << endl;
    }
}

The output is as follows:

((A and not B) implies C) and ((not A) iff (B and C)):

A    B    C
-----------
1    1    0    
1    0    1    
0    1    1    

Answer 1

Avoid using namespace std

The problem with using namespace std is that you are pulling in ALL of std, including things you did not think would be there. It's therefore recommend you avoid doing this, and either just add std:: where necessary, or be more specific pulling things in from the std namespace, for example by doing:

using std::cout;
using std::endl;
using std::make_shared;
using std::set;
using std::shared_ptr;
using std::string;
using std::vector;

Note that you should never do this in a header file; a source file including it might not realize you pulled things into the global namespace.

No need for forward-declarations

There is no need to forward-declare struct Proposition and operator"" _var. Avoid forward-declarations when possible; apart from avoiding repeating yourself, you also have less risk of making mistakes that way: a typo in a forward-declaration can easily go unnoticed.

Add more const

You can make most member variables const, since they can never be changed anyway. In fact, you can make pointer a const shared pointer to a const base class:

using pointer = const std::shared_ptr<const Base>;

This has the benefit of deleting the implicit assignment operator, which prevents compiling the following code:

auto proposition1 = "A"_var;
auto proposition2 = !proposition1;
proposition1 = "B"_var; // what is proposition2 supposed to be now?

Simplify the proposition operators

You can simplify the functions that operate on propositions by adding constructors to the classes derived from Base, so that you can pass arguments to make_shared<>(). Also, by making the constructor of Proposition a template, you can pass a shared pointer of a derived type:

struct Proposition {
    …
private:
    using pointer = const std::shared_ptr<const Base>;
    pointer value;

    template<typename T>
    Proposition(T value_) : value(value_) {}

    struct Variable : Base
    {
        const std::string name;
        Variable(const char* cstr, std::size_t size): name(cstr, size) {}
        …
    };
    …
    struct Disjunction : Base
    {
        …
        Disjunction(pointer lhs_, pointer rhs_): first_disjunct(lhs_), second_disjunct(rhs_) {}
        …
    }
};

Proposition operator"" _var (const char* name, size_t sz)
{
    return make_shared<Proposition::Variable>(name, sz);
}
…
Proposition Proposition::operator||(const Proposition& disjunct) const
{
    return make_shared<Disjunction>(value, disjunct.value);
}

About the use of std::shared_ptr

I see why you used std::shared_ptr. However, it's a heavyweight smart pointer, and ideally you'd only need a std::unique_ptr, since a proposition is just a tree of sub-propositions, and each parent can own its children. However, to do the same with std::unique_ptrs would require passing ownership around, which means passing by r-value reference and using std::move() a lot.

But consider this: Base just has a single virtual member function. The derived classes implement that function and have some extra member variables. That's basically a closure, and we have those in C++! We can create lambda expressions, and store them in std::function objects. For example:

struct Proposition {
    …
private:
    std::function<bool(const std::set<std::string>& truth_assignment)> evaluator;

    template<typename T>
    Proposition(T evaluator_): evaluator(evaluator_) {}
    …
};

Proposition operator"" _var (const char* name, size_t sz)
{
    return [=](const set<string>& truth_assignment) {
        return truth_assignment.count(string(name, sz));
    };
}
…
Proposition Proposition::operator||(const Proposition& disjunct) const
{
    auto self = *this; // ensures we copy this by value in C++11
    return [=](const set<string>& truth_assignment) {
        return self.evaluate(truth_assignment) || disjunct.evaluate(truth_assignment);
    };
}

bool Proposition::evaluate(const std::set<std::string>& truth_assignment) const
{
    return evaluator(truth_assignment);
}

Optimizing for speed

While using std::sets of std::strings is a simple and clean way to get the desired functionality, it's not very efficient, neither memory usage or CPU efficiency-wise.

Consider mapping variables to numbers. For example, operator"" _var() could maintain a list of variable names, and if you create a new one, you add it to the list and use the position in the list as its number.

Once you have this mapping, and if you set a hard limit the number of variables, then you can use a std::bitset to represent truth assignments. This type has operators for AND, OR, and for checking whether any, all or none of the bits are set. If you limit the size to say, 64, then the compiler can optimize it to single CPU instructions for each logic operation, resulting in very fast code.

If you want to support an arbitrary number of variables, then you could consider std::vector<bool> to store truth assignments.