#include <solver/algebra.h>
// for show
#include <stdio.h>
#include <tabula.h>
#include <assert.h>
#include <alias/memory.h>
#include <alias/cpp.h>
#include "algebra-encoding.inc"
void solver_Algebra_init(struct solver_Algebra *a) {
alias_Vector_init(&a->values);
}
void solver_Algebra_free(struct solver_Algebra *a) {
alias_Vector_free(&a->values, NULL);
}
uint64_t solver_Algebra_undefined(struct solver_Algebra *a) {
return pack_undefined();
}
uint64_t solver_Algebra_variable(struct solver_Algebra *a, const char * name) {
return pack_variable(name);
}
static int qsort_term_compare(const void *lhs_, const void *rhs_, void *ud);
static uint32_t embed_values(struct solver_Algebra *a, uint32_t count, const uint64_t *values) {
uint32_t index = a->values.length;
alias_Vector_space_for(&a->values, NULL, count);
alias_memory_copy(a->values.data + index, sizeof(*a->values.data) * (a->values.capacity - index), values, sizeof(*values) * count);
a->values.length += count;
return index;
}
static uint64_t get_car(const struct solver_Algebra *a, uint64_t expr) {
return a->values.data[get_pair_index(expr) + 0];
}
static uint64_t get_cdr(const struct solver_Algebra *a, uint64_t expr) {
return a->values.data[get_pair_index(expr) + 1];
}
static uint64_t get_index(const struct solver_Algebra *a, uint64_t expr, uint32_t index) {
assert(index < get_list_count(expr));
return a->values.data[get_list_index(expr) + index];
}
#include "algebra-boolean.inc"
#include "algebra-integer.inc"
#include "algebra-fraction.inc"
#include "algebra-number.inc"
#include "algebra-sum.inc"
#include "algebra-product.inc"
#include "algebra-power.inc"
#include "algebra-compare.inc"
// map : (item ⇒ item) ⇒ tree ⇒ tree
#define MAP_IMPL(NAME) \
static uint64_t NAME(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)); \
static inline uint64_t NAME##__real(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __REAL) \
} \
static inline uint64_t NAME##__variable(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __VARIABLE) \
} \
static inline uint64_t NAME##__boolean(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __BOOLEAN) \
} \
static inline uint64_t NAME##__undefined(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __UNDEFINED) \
} \
static inline uint64_t NAME##__smallint(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __SMALLINT) \
} \
static inline uint64_t NAME##__largeint(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __LARGEINT) \
} \
static inline uint64_t NAME##__fraction(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t in_numerator = get_car(a, expr); \
uint64_t in_denominator = get_cdr(a, expr); \
uint64_t numerator = NAME(a, in_numerator ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
uint64_t denominator = NAME(a, in_denominator ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
bool changed = in_numerator != numerator || in_denominator != denominator; \
ALIAS_CPP_CAT(NAME, __FRACTION) \
} \
static inline uint64_t NAME##__power(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t in_base = get_car(a, expr); \
uint64_t in_exponent = get_cdr(a, expr); \
uint64_t base = NAME(a, in_base ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
uint64_t exponent = NAME(a, in_exponent ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
bool changed = in_base != base || in_exponent != exponent; \
ALIAS_CPP_CAT(NAME, __POWER) \
} \
static inline uint64_t NAME##__sum(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint32_t count = get_list_count(expr); \
const uint64_t *in_values = a->values.data + get_list_index(expr); \
uint64_t *values = a->values.data + get_list_index(expr); \
uint64_t mapped_value = 0; \
uint32_t i__ = 0; \
for(;i__ < count; i__++) { \
mapped_value = NAME(a, in_values[i__] ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
if(mapped_value != in_values[i__]) { \
break; \
} \
} \
bool changed = i__ != count; \
if(changed) { \
values = alias_stack_allocation(sizeof(*values) * count, alignof(*values)); \
alias_memory_copy(values, sizeof(*values) * i__, in_values, sizeof(*values) * i__); \
values[i__++] = mapped_value; \
for(;i__ < count; i__++) { \
values[i__] = NAME(a, in_values[i__] ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
} \
} \
ALIAS_CPP_CAT(NAME, __SUM) \
} \
static inline uint64_t NAME##__product(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint32_t count = get_list_count(expr); \
const uint64_t *in_values = a->values.data + get_list_index(expr); \
uint64_t *values = a->values.data + get_list_index(expr); \
uint64_t mapped_value = 0; \
uint32_t i__ = 0; \
for(;i__ < count; i__++) { \
mapped_value = NAME(a, in_values[i__] ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
if(mapped_value != in_values[i__]) { \
break; \
} \
} \
bool changed = i__ != count; \
if(changed) { \
values = alias_stack_allocation(sizeof(*values) * count, alignof(*values)); \
alias_memory_copy(values, sizeof(*values) * i__, in_values, sizeof(*values) * i__); \
values[i__++] = mapped_value; \
for(;i__ < count; i__++) { \
values[i__] = NAME(a, in_values[i__] ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
} \
} \
ALIAS_CPP_CAT(NAME, __PRODUCT) \
} \
static inline uint64_t NAME##__equals(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t in_lhs = get_car(a, expr); \
uint64_t in_rhs = get_cdr(a, expr); \
uint64_t lhs = NAME(a, in_lhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
uint64_t rhs = NAME(a, in_rhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
bool changed = in_lhs != lhs || in_rhs != rhs; \
ALIAS_CPP_CAT(NAME, __EQUALS) \
} \
static inline uint64_t NAME##__not_equals(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t in_lhs = get_car(a, expr); \
uint64_t in_rhs = get_cdr(a, expr); \
uint64_t lhs = NAME(a, in_lhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
uint64_t rhs = NAME(a, in_rhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
bool changed = in_lhs != lhs || in_rhs != rhs; \
ALIAS_CPP_CAT(NAME, __NOT_EQUALS) \
} \
static inline uint64_t NAME##__less_than(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t in_lhs = get_car(a, expr); \
uint64_t in_rhs = get_cdr(a, expr); \
uint64_t lhs = NAME(a, in_lhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
uint64_t rhs = NAME(a, in_rhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
bool changed = in_lhs != lhs || in_rhs != rhs; \
ALIAS_CPP_CAT(NAME, __LESS_THAN) \
} \
static inline uint64_t NAME##__greater_than(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t in_lhs = get_car(a, expr); \
uint64_t in_rhs = get_cdr(a, expr); \
uint64_t lhs = NAME(a, in_lhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
uint64_t rhs = NAME(a, in_rhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
bool changed = in_lhs != lhs || in_rhs != rhs; \
ALIAS_CPP_CAT(NAME, __GREATER_THAN) \
} \
static inline uint64_t NAME##__invalid(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __INVALID) \
} \
static uint64_t NAME(struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __FIRST_STATEMENT); \
switch(get_tag(expr)) { \
case Tag_Real: \
return NAME##__real(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Variable: \
return NAME##__variable(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Boolean: \
return NAME##__boolean(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Undefined: \
return NAME##__undefined(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_SmallInt: \
return NAME##__smallint(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_LargeInt: \
return NAME##__largeint(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Fraction: \
return NAME##__fraction(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Power: \
return NAME##__power(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Sum: \
return NAME##__sum(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Product: \
return NAME##__product(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Equals: \
return NAME##__equals(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_NotEquals: \
return NAME##__not_equals(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_LessThan: \
return NAME##__less_than(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_GreaterThan: \
return NAME##__greater_than(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
default: \
return NAME##__invalid(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
} \
}
#define MAP(NAME) ALIAS_CPP_EVAL_3(MAP_IMPL(NAME))
// any : (item ⇒ bool) ⇒ tree ⇒ bool
#define ANY_IMPL(NAME) \
static bool NAME(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)); \
static inline bool NAME##__real(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __REAL) \
return false; \
} \
static inline bool NAME##__variable(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __VARIABLE) \
return false; \
} \
static inline bool NAME##__boolean(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __BOOLEAN) \
return false; \
} \
static inline bool NAME##__undefined(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __UNDEFINED) \
return false; \
} \
static inline bool NAME##__smallint(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __SMALLINT) \
return false; \
} \
static inline bool NAME##__largeint(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __LARGEINT) \
return false; \
} \
static inline bool NAME##__fraction(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t numerator = get_car(a, expr); \
uint64_t denominator = get_cdr(a, expr); \
ALIAS_CPP_CAT(NAME, __FRACTION) \
if(NAME(a, numerator ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
if(NAME(a, denominator ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
return false; \
} \
static inline bool NAME##__power(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t base = get_car(a, expr); \
uint64_t exponent = get_cdr(a, expr); \
ALIAS_CPP_CAT(NAME, __POWER) \
if(NAME(a, base ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
if(NAME(a, exponent ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
return false; \
} \
static inline bool NAME##__sum(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint32_t count = get_list_count(expr); \
const uint64_t *values = a->values.data + get_list_index(expr); \
ALIAS_CPP_CAT(NAME, __SUM) \
for(uint32_t i = 0; i < count; i++) { \
if(NAME(a, values[i] ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
} \
return false; \
} \
static inline bool NAME##__product(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint32_t count = get_list_count(expr); \
const uint64_t *values = a->values.data + get_list_index(expr); \
ALIAS_CPP_CAT(NAME, __PRODUCT) \
for(uint32_t i = 0; i < count; i++) { \
if(NAME(a, values[i] ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
} \
return false; \
} \
static inline bool NAME##__equals(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t lhs = get_car(a, expr); \
uint64_t rhs = get_cdr(a, expr); \
ALIAS_CPP_CAT(NAME, __EQUALS) \
if(NAME(a, lhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
if(NAME(a, rhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
return false; \
} \
static inline bool NAME##__not_equals(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t lhs = get_car(a, expr); \
uint64_t rhs = get_cdr(a, expr); \
ALIAS_CPP_CAT(NAME, __NOT_EQUALS) \
if(NAME(a, lhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
if(NAME(a, rhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
return false; \
} \
static inline bool NAME##__less_than(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t lhs = get_car(a, expr); \
uint64_t rhs = get_cdr(a, expr); \
ALIAS_CPP_CAT(NAME, __LESS_THAN) \
if(NAME(a, lhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
if(NAME(a, rhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
return false; \
} \
static inline bool NAME##__greater_than(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
uint64_t lhs = get_car(a, expr); \
uint64_t rhs = get_cdr(a, expr); \
ALIAS_CPP_CAT(NAME, __GREATER_THAN) \
if(NAME(a, lhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
if(NAME(a, rhs ALIAS_CPP_CAT(NAME, __EXTRA_PASS))) { \
return true; \
} \
return false; \
} \
static inline bool NAME##__invalid(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __INVALID) \
return false; \
} \
static bool NAME(const struct solver_Algebra *a, uint64_t expr ALIAS_CPP_CAT(NAME, __EXTRA_PARAMS)) { \
ALIAS_CPP_CAT(NAME, __FIRST_STATEMENT); \
switch(get_tag(expr)) { \
case Tag_Real: \
return NAME##__real(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Variable: \
return NAME##__variable(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Boolean: \
return NAME##__boolean(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Undefined: \
return NAME##__undefined(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_SmallInt: \
return NAME##__smallint(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_LargeInt: \
return NAME##__largeint(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Fraction: \
return NAME##__fraction(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Power: \
return NAME##__power(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Sum: \
return NAME##__sum(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Product: \
return NAME##__product(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_Equals: \
return NAME##__equals(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_NotEquals: \
return NAME##__not_equals(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_LessThan: \
return NAME##__less_than(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
case Tag_GreaterThan: \
return NAME##__greater_than(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
default: \
return NAME##__invalid(a, expr ALIAS_CPP_CAT(NAME, __EXTRA_PASS)); \
} \
}
#define ANY(NAME) ALIAS_CPP_EVAL_3(ANY_IMPL(NAME))
// all : (item ⇒ bool) ⇒ tree ⇒ bool
// all_pair : (item ⇒ item ⇒ bool) ⇒ tree ⇒ tree ⇒ bool
// each : (item ⇒ void) ⇒ tree ⇒ void
#include "algebra-show.inc"
#include "algebra-to_boolean.inc"
#include "algebra-simplify.inc"
#include "algebra-substitute.inc"
#include "algebra-has.inc"
#undef MAP
#undef MAP_IMPL
#undef ANY
#undef ANY_IMPL
static int qsort_term_compare(const void *lhs_, const void *rhs_, void *ud) {
return term_compare((struct solver_Algebra *)ud, *(uint64_t *)lhs_, *(uint64_t *)rhs_);
}