Merge pull request #381 from potassco/feature/backend-theory

add theory functionality to backend

CHANGES.md

@@ -2,6 +2,7 @@
 
 ## clingo 5.6.0
 
+  * add theory related functions to backend (#381)
   * add support for comparisons with more than one relation (#368)
   * extend safety by computing intervals from comparisons (#375)
   * add and ground base part by default in Python API (#378)

libclingo/clingo.h

@@ -1481,6 +1481,15 @@ typedef struct clingo_propagator {
 //! @addtogroup ProgramBuilder
 //! @{
 
+//! Enumeration of theory sequence types.
+enum clingo_theory_sequence_type_e {
+    clingo_theory_sequence_type_tuple, //!< Theory tuples "(t1,...,tn)".
+    clingo_theory_sequence_type_list,  //!< Theory lists "[t1,...,tn]".
+    clingo_theory_sequence_type_set    //!< Theory sets "{t1,...,tn}".
+};
+//! Corresponding type to ::clingo_theory_sequence_type_e.
+typedef int clingo_theory_sequence_type_t;
+
 //! Enumeration of different heuristic modifiers.
 //! @ingroup ProgramInspection
 enum clingo_heuristic_type_e {
@@ -1610,6 +1619,83 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_backend_acyc_edge(clingo_backend_t *backen
 //! @param[out] atom the resulting atom
 //! @return whether the call was successful
 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_add_atom(clingo_backend_t *backend, clingo_symbol_t *symbol, clingo_atom_t *atom);
+//! Add a numeric theory term.
+//!
+//! @param[in] backend the target backend
+//! @param[in] number the value of the term
+//! @param[out] term_id the resulting term id
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_backend_theory_term_number(clingo_backend_t *backend, int number, clingo_id_t *term_id);
+//! Add a theory term representing a string.
+//!
+//! @param[in] backend the target backend
+//! @param[in] string the value of the term
+//! @param[out] term_id the resulting term id
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_backend_theory_term_string(clingo_backend_t *backend, char const *string, clingo_id_t *term_id);
+//! Add a theory term representing a sequence of theory terms.
+//!
+//! @param[in] backend the target backend
+//! @param[in] type the type of the sequence
+//! @param[in] arguments the term ids of the terms in the sequence
+//! @param[in] size the number of elements of the sequence
+//! @param[out] term_id the resulting term id
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_backend_theory_term_sequence(clingo_backend_t *backend, clingo_theory_sequence_type_t type, clingo_id_t const *arguments, size_t size, clingo_id_t *term_id);
+//! Add a theory term representing a function.
+//!
+//! @param[in] backend the target backend
+//! @param[in] name the name of the function
+//! @param[in] arguments an array of term ids for the theory terms in the arguments
+//! @param[in] size the number of arguments
+//! @param[out] term_id the resulting term id
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_backend_theory_term_function(clingo_backend_t *backend, char const *name, clingo_id_t const *arguments, size_t size, clingo_id_t *term_id);
+//! Convert the given symbol into a theory term.
+//!
+//! @param[in] backend the target backend
+//! @param[in] symbol the symbol to convert
+//! @param[out] term_id the resulting term id
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_backend_theory_term_symbol(clingo_backend_t *backend, clingo_symbol_t symbol, clingo_id_t *term_id);
+//! Add a theory atom element.
+//!
+//! @param[in] backend the target backend
+//! @param[in] tuple the array of term ids represeting the tuple
+//! @param[in] tuple_size the size of the tuple
+//! @param[in] condition an array of program literals represeting the condition
+//! @param[in] condition_size the size of the condition
+//! @param[out] element_id the resulting element id
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_backend_theory_element(clingo_backend_t *backend, clingo_id_t const *tuple, size_t tuple_size, clingo_literal_t const *condition, size_t condition_size, clingo_id_t *element_id);
+//! Add a theory atom without a guard.
+//!
+//! @param[in] backend the target backend
+//! @param[in] atom_id_or_zero a program atom or zero for theory directives
+//! @param[in] term_id the term id of the term associated with the theory atom
+//! @param[in] elements an array of element ids for the theory atoms's elements
+//! @param[in] size the number of elements
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_backend_theory_atom(clingo_backend_t *backend, clingo_atom_t atom_id_or_zero, clingo_id_t term_id, clingo_id_t const *elements, size_t size);
+//! Add a theory atom with a guard.
+//!
+//! @param[in] backend the target backend
+//! @param[in] atom_id_or_zero a program atom or zero for theory directives
+//! @param[in] term_id the term id of the term associated with the theory atom
+//! @param[in] elements an array of element ids for the theory atoms's elements
+//! @param[in] size the number of elements
+//! @param[in] operator_name the string representation of a theory operator
+//! @param[in] right_hand_side_id the term id of the right hand side term
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_backend_theory_atom_with_guard(clingo_backend_t *backend, clingo_atom_t atom_id_or_zero, clingo_id_t term_id, clingo_id_t const *elements, size_t size, char const *operator_name, clingo_id_t right_hand_side_id);
 
 //! @}
 
@@ -2330,10 +2416,12 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_close(clingo_solve_handle_t *
 //! @{
 
 //! Enumeration of theory sequence types.
+//!
+//! Same as clingo_theory_sequence_type_e but kept for backward compatibility.
 enum clingo_ast_theory_sequence_type_e {
-    clingo_ast_theory_sequence_type_tuple, //!< Theory tuples "(t1,...,tn)".
-    clingo_ast_theory_sequence_type_list,  //!< Theory lists "[t1,...,tn]".
-    clingo_ast_theory_sequence_type_set    //!< Theory sets "{t1,...,tn}".
+    clingo_ast_theory_sequence_type_tuple = clingo_theory_sequence_type_tuple, //!< Theory tuples "(t1,...,tn)".
+    clingo_ast_theory_sequence_type_list = clingo_theory_sequence_type_list,   //!< Theory lists "[t1,...,tn]".
+    clingo_ast_theory_sequence_type_set = clingo_theory_sequence_type_set      //!< Theory sets "{t1,...,tn}".
 };
 //! Corresponding type to ::clingo_ast_theory_sequence_type_e.
 typedef int clingo_ast_theory_sequence_type_t;

libclingo/clingo.hh

@@ -460,13 +460,24 @@ public:
     ReferenceType operator[](size_t offset) const { return *(begin() + offset); }
     ReferenceType front() const { return *begin(); }
     ReferenceType back() const { return *I::operator()(end_-1); }
+    T const *data() const { return begin_; }
     size_t size() const { return end_ - begin_; }
     bool empty() const { return begin_ == end_; }
 private:
     T const *begin_;
     T const *end_;
 };
 
+template <class T, class I>
+inline typename Span<T, I>::IteratorType begin(Span<T, I> const &span) {
+    return span.begin();
+}
+
+template <class T, class I>
+inline typename Span<T, I>::IteratorType end(Span<T, I> const& span) {
+    return span.end();
+}
+
 template <class T, class I = ToIterator<T>>
 inline Span<T, I> make_span(T const *begin, size_t size, I to_it = I()) {
     return {begin, size, std::move(to_it)};
@@ -478,13 +489,11 @@ bool equal_range(T const &a, U const &b) {
     return a.size() == b.size() && std::equal(begin(a), end(a), begin(b));
 }
 
-template <class T, class I, class V>
-bool operator==(Span<T, I> span, V const &v) { return equal_range(span, v); }
-template <class T, class I, class V>
-bool operator==(V const &v, Span<T, I> span) { return equal_range(span, v); }
+template <class T, class I>
+bool operator==(Span<T, I> const &a, Span<T, I> const &b) { return equal_range(a, b); }
 
 template <class T, class I>
-std::ostream &operator<<(std::ostream &out, Span<T, I> span) {
+std::ostream &operator<<(std::ostream &out, Span<T, I> const &span) {
     out << "{";
     bool comma = false;
     for (auto &x : span) {
@@ -1442,6 +1451,12 @@ inline std::ostream &operator<<(std::ostream &out, Location loc) {
 
 // {{{1 backend
 
+enum class TheorySequenceType {
+    Tuple = clingo_theory_sequence_type_tuple,
+    List = clingo_theory_sequence_type_list,
+    Set = clingo_theory_sequence_type_set,
+};
+
 class Backend {
 public:
     explicit Backend(clingo_backend_t *backend);
@@ -1461,6 +1476,14 @@ public:
     void acyc_edge(int node_u, int node_v, LiteralSpan condition);
     atom_t add_atom();
     atom_t add_atom(Symbol symbol);
+    id_t add_theory_term_number(int number);
+    id_t add_theory_term_string(char const *string);
+    id_t add_theory_term_sequence(TheorySequenceType type, IdSpan elements);
+    id_t add_theory_term_function(char const *name, IdSpan elements);
+    id_t add_theory_term_symbol(Symbol symbol);
+    id_t add_theory_element(IdSpan tuple, LiteralSpan condition);
+    void theory_atom(id_t atom_id_or_zero, id_t term_id, IdSpan elements);
+    void theory_atom(id_t atom_id_or_zero, id_t term_id, IdSpan elements, char const *operator_name, id_t right_hand_side_id);
     clingo_backend_t *to_c() const { return backend_; }
 private:
     clingo_backend_t *backend_;
@@ -1807,11 +1830,7 @@ private:
 
 namespace AST {
 
-enum class TheorySequenceType {
-    Tuple = clingo_ast_theory_sequence_type_tuple,
-    List = clingo_ast_theory_sequence_type_list,
-    Set = clingo_ast_theory_sequence_type_set,
-};
+using Clingo::TheorySequenceType;
 
 enum class ComparisonOperator {
     GreaterThan = clingo_ast_comparison_operator_greater_than,
@@ -3105,6 +3124,50 @@ inline atom_t Backend::add_atom(Symbol symbol) {
     return ret;
 }
 
+inline id_t Backend::add_theory_term_number(int number) {
+    clingo_id_t ret = 0;
+    Detail::handle_error(clingo_backend_theory_term_number(backend_, number, &ret));
+    return ret;
+}
+
+inline id_t Backend::add_theory_term_string(char const *string) {
+    clingo_id_t ret = 0;
+    Detail::handle_error(clingo_backend_theory_term_string(backend_, string, &ret));
+    return ret;
+}
+
+inline id_t Backend::add_theory_term_sequence(TheorySequenceType type, IdSpan elements) {
+    clingo_id_t ret = 0;
+    Detail::handle_error(clingo_backend_theory_term_sequence(backend_, static_cast<clingo_theory_sequence_type_e>(type), elements.data(), elements.size(), &ret));
+    return ret;
+}
+
+inline id_t Backend::add_theory_term_function(char const *name, IdSpan elements) {
+    clingo_id_t ret = 0;
+    Detail::handle_error(clingo_backend_theory_term_function(backend_, name, elements.data(), elements.size(), &ret));
+    return ret;
+}
+
+inline id_t Backend::add_theory_term_symbol(Symbol symbol) {
+    clingo_id_t ret = 0;
+    Detail::handle_error(clingo_backend_theory_term_symbol(backend_, symbol.to_c(), &ret));
+    return ret;
+}
+
+inline id_t Backend::add_theory_element(IdSpan tuple, LiteralSpan condition) {
+    clingo_id_t ret = 0;
+    Detail::handle_error(clingo_backend_theory_element(backend_, tuple.data(), tuple.size(), condition.begin(), condition.size(), &ret));
+    return ret;
+}
+
+inline void Backend::theory_atom(id_t atom_id_or_zero, id_t term_id, IdSpan elements) {
+    Detail::handle_error(clingo_backend_theory_atom(backend_, atom_id_or_zero, term_id, elements.begin(), elements.size()));
+}
+
+inline void Backend::theory_atom(id_t atom_id_or_zero, id_t term_id, IdSpan elements, char const *operator_name, id_t right_hand_side_id) {
+    Detail::handle_error(clingo_backend_theory_atom_with_guard(backend_, atom_id_or_zero, term_id, elements.begin(), elements.size(), operator_name, right_hand_side_id));
+}
+
 // {{{2 statistics
 
 template <bool constant>

libclingo/clingo/clingocontrol.hh

@@ -335,6 +335,9 @@ public:
     void interrupt() override;
     void *claspFacade() override;
     bool beginAddBackend() override;
+    Gringo::Output::TheoryData &theoryData() override {
+        return out_->data.theory();
+    }
     Id_t addAtom(Symbol sym) override;
     void addFact(Potassco::Atom_t uid) override;
     Backend *getBackend() override {

libclingo/clingo/control.hh

@@ -30,7 +30,7 @@
 #include <gringo/locatable.hh>
 #include <gringo/backend.hh>
 #include <gringo/logger.hh>
-#include <gringo/output/literal.hh>
+#include <gringo/output/literals.hh>
 #include <potassco/clingo.h>
 #include <clingo.h>
 
@@ -253,6 +253,7 @@ struct clingo_control {
     virtual void registerObserver(Gringo::UBackend program, bool replace) = 0;
     virtual Potassco::Atom_t addProgramAtom() = 0;
     virtual bool beginAddBackend() = 0;
+    virtual Gringo::Output::TheoryData &theoryData() = 0;
     virtual Gringo::Id_t addAtom(Gringo::Symbol sym) = 0;
     virtual void addFact(Potassco::Atom_t uid) = 0;
     virtual Gringo::Backend *getBackend() = 0;

libclingo/src/control.cc

@@ -22,6 +22,7 @@
 
 // }}}
 
+#include "potassco/basic_types.h"
 #if defined(__GNUC__) && !defined(__clang__)
 #pragma GCC diagnostic push
 #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
@@ -1111,6 +1112,64 @@ extern "C" bool clingo_backend_acyc_edge(clingo_backend_t *backend, int node_u,
     GRINGO_CLINGO_CATCH;
 }
 
+extern "C" bool clingo_backend_theory_term_number(clingo_backend_t *backend, int number, clingo_id_t *term_id) {
+    GRINGO_CLINGO_TRY { *term_id = backend->theoryData().addTerm(number); }
+    GRINGO_CLINGO_CATCH;
+}
+
+extern "C" bool clingo_backend_theory_term_string(clingo_backend_t *backend, char const *string, clingo_id_t *term_id) {
+    GRINGO_CLINGO_TRY { *term_id = backend->theoryData().addTerm(string); }
+    GRINGO_CLINGO_CATCH;
+}
+
+extern "C" bool clingo_backend_theory_term_function(clingo_backend_t *backend, char const *name, clingo_id_t const *arguments, size_t size, clingo_id_t *term_id) {
+    GRINGO_CLINGO_TRY {
+        auto &theory = backend->theoryData();
+        auto name_id  = theory.addTerm(name);
+        *term_id = theory.addTermFun(name_id, Potassco::IdSpan{arguments, size});
+    }
+    GRINGO_CLINGO_CATCH;
+}
+
+extern "C" bool clingo_backend_theory_term_symbol(clingo_backend_t *backend, clingo_symbol_t symbol, clingo_id_t *term_id) {
+    GRINGO_CLINGO_TRY {
+        *term_id  = backend->theoryData().addTerm(Gringo::Symbol{symbol});
+    }
+    GRINGO_CLINGO_CATCH;
+}
+
+extern "C" bool clingo_backend_theory_term_sequence(clingo_backend_t *backend, clingo_theory_sequence_type_t type, clingo_id_t const *arguments, size_t size, clingo_id_t *term_id) {
+    GRINGO_CLINGO_TRY {
+        *term_id  = backend->theoryData().addTermTup(Potassco::Tuple_t{-static_cast<int>(type)}, Potassco::IdSpan{arguments, size});
+    }
+    GRINGO_CLINGO_CATCH;
+}
+
+extern "C" bool clingo_backend_theory_element(clingo_backend_t *backend, clingo_id_t const *tuple, size_t tuple_size, clingo_literal_t const *condition, size_t condition_size, clingo_id_t *element_id) {
+    GRINGO_CLINGO_TRY {
+        *element_id = backend->theoryData().addElem(Potassco::IdSpan{tuple, tuple_size}, Potassco::LitSpan{condition, condition_size});
+    }
+    GRINGO_CLINGO_CATCH;
+}
+
+extern "C" bool clingo_backend_theory_atom(clingo_backend_t *backend, clingo_atom_t atom_id_or_zero, clingo_id_t term_id, clingo_id_t const *elements, size_t size) {
+    GRINGO_CLINGO_TRY {
+        auto newAtom = [atom_id_or_zero]() -> Atom_t { return atom_id_or_zero; };
+        backend->theoryData().addAtom(newAtom, term_id, Potassco::IdSpan{elements, size});
+    }
+    GRINGO_CLINGO_CATCH;
+}
+
+extern "C" bool clingo_backend_theory_atom_with_guard(clingo_backend_t *backend, clingo_atom_t atom_id_or_zero, clingo_id_t term_id, clingo_id_t const *elements, size_t size, char const *operator_name, clingo_id_t right_hand_side_id) {
+    GRINGO_CLINGO_TRY {
+        auto &theory = backend->theoryData();
+        auto op_id = theory.addTerm(operator_name);
+        auto newAtom = [atom_id_or_zero]() -> Atom_t { return atom_id_or_zero; };
+        theory.addAtom(newAtom, term_id, Potassco::IdSpan{elements, size}, op_id, right_hand_side_id);
+    }
+    GRINGO_CLINGO_CATCH;
+}
+
 extern "C" bool clingo_backend_add_atom(clingo_backend_t *backend, clingo_symbol_t *symbol, clingo_atom_t *ret) {
     GRINGO_CLINGO_TRY {
         if (symbol) {

libclingo/src/gringo_app.cc

@@ -233,6 +233,9 @@ struct IncrementalControl : Control {
         if (!backend_) { throw std::runtime_error("backend not available"); }
         return backend_;
     }
+    Output::TheoryData &theoryData() override {
+        return out.data.theory();
+    }
     Id_t addAtom(Symbol sym) override {
         bool added = false;
         auto atom  = out.addAtom(sym, &added);