Propositional Logic: Proposition Evaluator

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 . Public domain.

#include
#include
#include
#include
#include
#include
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& truth_assignment) const;

// A.evaluate_all(S): Given a set S of variables,
// will return t

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;

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;
    pointer value;

    template
    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(name, sz);
}
…
Proposition Proposition::operator||(const Proposition& disjunct) const
{
    return make_shared(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& truth_assignment)> evaluator;

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

Proposition operator"" _var (const char* name, size_t sz)
{
    return [=](const set& 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& truth_assignment) {
        return self.evaluate(truth_assignment) || disjunct.evaluate(truth_assignment);
    };
}

bool Proposition::evaluate(const std::set& 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 to store truth assignments.

StackExchange Code Review Q#11154, answer score: 3