summaryrefslogtreecommitdiff
path: root/lib/omega/src/RelBody.cc
diff options
context:
space:
mode:
Diffstat (limited to 'lib/omega/src/RelBody.cc')
-rw-r--r--lib/omega/src/RelBody.cc906
1 files changed, 906 insertions, 0 deletions
diff --git a/lib/omega/src/RelBody.cc b/lib/omega/src/RelBody.cc
new file mode 100644
index 0000000..825b153
--- /dev/null
+++ b/lib/omega/src/RelBody.cc
@@ -0,0 +1,906 @@
+/*****************************************************************************
+ Copyright (C) 1994-2000 the Omega Project Team
+ Copyright (C) 2005-2011 Chun Chen
+ All Rights Reserved.
+
+ Purpose:
+ class Rel_Body, internal Relation representation
+
+ Notes:
+
+ History:
+ 11/26/09 Remove unecessary mandatary checking for set or relation,
+ treat them uniformly for easy coding, by Chun Chen
+*****************************************************************************/
+
+#include <basic/util.h>
+#include <omega/RelBody.h>
+#include <omega/Relation.h>
+#include <omega/pres_tree.h>
+#include <omega/pres_conj.h>
+#include <omega/omega_i.h>
+#include <assert.h>
+
+namespace omega {
+
+Rel_Body null_rel;
+bool Rel_Body::is_null() const {
+ return(this == &null_rel);
+}
+
+
+int Rel_Body::max_ufs_arity() {
+ int ma = 0, a;
+ for (Variable_ID_Iterator v(*global_decls()); v; v++) {
+ a = (*v)->get_global_var()->arity();
+ if (a > ma)
+ ma = a;
+ }
+ return ma;
+}
+
+int Rel_Body::max_ufs_arity_of_set() {
+ int ma = 0, a;
+ for (Variable_ID_Iterator v(*global_decls()); v; v++)
+ if ((*v)->function_of() == Set_Tuple) {
+ a = (*v)->get_global_var()->arity();
+ if (a > ma)
+ ma = a;
+ }
+ return ma;
+}
+
+int Rel_Body::max_ufs_arity_of_in() {
+ int ma = 0, a;
+ for (Variable_ID_Iterator v(*global_decls()); v; v++)
+ if ((*v)->function_of() == Input_Tuple) {
+ a = (*v)->get_global_var()->arity();
+ if (a > ma)
+ ma = a;
+ }
+ return ma;
+}
+
+int Rel_Body::max_ufs_arity_of_out() {
+ int ma = 0, a;
+ for (Variable_ID_Iterator v(*global_decls()); v; v++)
+ if ((*v)->function_of() == Output_Tuple) {
+ a = (*v)->get_global_var()->arity();
+ if (a > ma)
+ ma = a;
+ }
+ return ma;
+}
+
+int Rel_Body::max_shared_ufs_arity() {
+ int ma = 0, a;
+ for (Variable_ID_Iterator v(*global_decls()); v; v++)
+ for (Variable_ID_Iterator v2(*global_decls()); v2; v2++)
+ if (*v != *v2
+ && (*v)->get_global_var() == (*v2)->get_global_var()
+ && (*v)->function_of() != (*v2)->function_of()) {
+ a = (*v)->get_global_var()->arity();
+ if (a > ma)
+ ma = a;
+ }
+ return ma;
+}
+
+//
+// Input and output variables.
+//
+void Rel_Body::name_input_var(int nth, Const_String S) {
+ // assert(1 <= nth && nth <= number_input && (!is_set() || skip_set_checks > 0));
+ if (is_null())
+ throw std::invalid_argument("empty relation");
+ if (nth < 1 || nth > number_input)
+ throw std::invalid_argument("invalid input var number");
+ In_Names[nth] = S;
+}
+
+void Rel_Body::name_output_var(int nth, Const_String S) {
+ // assert(1<= nth && nth <= number_output && (!is_set() || skip_set_checks > 0));
+ if (is_null())
+ throw std::invalid_argument("empty relation");
+ if (nth < 1 || nth > number_output)
+ throw std::invalid_argument("invalid output var number");
+ Out_Names[nth] = S;
+}
+
+void Rel_Body::name_set_var(int nth, Const_String S) {
+ if (number_output != 0)
+ throw std::runtime_error("relation is not a set");
+ name_input_var(nth, S);
+}
+
+int Rel_Body::n_inp() const {
+ // assert(!is_null() && (!is_set()||skip_set_checks>0));
+ if (is_null())
+ return 0;
+ else
+ return number_input;
+}
+
+int Rel_Body::n_out() const {
+ // assert(!is_null() && (!is_set()||skip_set_checks>0));
+ if (is_null())
+ return 0;
+ else
+ return number_output;
+}
+
+int Rel_Body::n_set() const {
+ if (number_output != 0)
+ throw std::runtime_error("relation is not a set");
+ return n_inp();
+}
+
+Variable_ID Rel_Body::input_var(int nth) {
+ // assert(!is_null());
+ // assert(!is_set() || skip_set_checks>0);
+ // assert(1 <= nth && nth <= number_input);
+ if (is_null())
+ throw std::invalid_argument("empty relation");
+ if (nth < 1 || nth > number_input)
+ throw std::invalid_argument("invalid input var number");
+ input_vars[nth]->base_name = In_Names[nth];
+ return input_vars[nth];
+}
+
+Variable_ID Rel_Body::output_var(int nth) {
+ // assert(!is_null());
+ // assert(!is_set() || skip_set_checks>0);
+ // assert(1<= nth && nth <= number_output);
+ if (is_null())
+ throw std::invalid_argument("empty relation");
+ if (nth < 1 || nth > number_output)
+ throw std::invalid_argument("invalid output var number");
+ output_vars[nth]->base_name = Out_Names[nth];
+ return output_vars[nth];
+}
+
+Variable_ID Rel_Body::set_var(int nth) {
+ if (number_output != 0)
+ throw std::runtime_error("relation is not a set");
+ return input_var(nth);
+}
+
+//
+// Add the AND node to the relation.
+// Useful for adding restraints.
+//
+F_And *Rel_Body::and_with_and() {
+ assert(!is_null());
+ if (is_simplified())
+ DNF_to_formula();
+ relation()->finalized = false;
+ Formula *f = rm_formula();
+ F_And *a = add_and();
+ a->add_child(f);
+ return a;
+}
+
+//
+// Add constraint to relation at the upper level.
+//
+EQ_Handle Rel_Body::and_with_EQ() {
+ assert(!is_null());
+ if (is_simplified())
+ DNF_to_formula();
+ assert(! is_shared()); // The relation has been split.
+ relation()->finalized = false;
+ return find_available_conjunct()->add_EQ();
+}
+
+EQ_Handle Rel_Body::and_with_EQ(const Constraint_Handle &initial) {
+ assert(!is_null());
+ assert(initial.relation()->is_simplified());
+ EQ_Handle H = and_with_EQ();
+ copy_constraint(H, initial);
+ return H;
+}
+
+GEQ_Handle Rel_Body::and_with_GEQ() {
+ assert(!is_null());
+ if (is_simplified())
+ DNF_to_formula();
+ assert(! is_shared()); // The relation has been split.
+ relation()->finalized = false; // We are giving out a handle.
+ // We should evantually implement finalization
+ // of subtrees, so the existing formula cannot
+ // be modified.
+ return find_available_conjunct()->add_GEQ();
+}
+
+GEQ_Handle Rel_Body::and_with_GEQ(const Constraint_Handle &initial) {
+ assert(!is_null());
+ assert(initial.relation()->is_simplified());
+ GEQ_Handle H = and_with_GEQ();
+ copy_constraint(H, initial);
+ return H;
+}
+
+
+
+Conjunct *Rel_Body::find_available_conjunct() {
+ Conjunct *c;
+ assert(!is_null());
+
+ if (children().empty()) {
+ c = add_conjunct();
+ }
+ else {
+ assert(children().length() == 1);
+ Formula *kid = children().front(); // RelBodies have only one child
+ c = kid->find_available_conjunct();
+ if (c==NULL) {
+ remove_child(kid);
+ F_And *a = add_and();
+ a->add_child(kid);
+ c = a->add_conjunct();
+ }
+ }
+ return c;
+}
+
+void Rel_Body::finalize() {
+ assert(!is_null());
+ if (!is_finalized())
+ assert(! is_shared()); // no other pointers into here
+ finalized = true;
+ if (! children().empty())
+ children().front()->finalize(); // Can have at most one child
+}
+
+// Null Rel_Body
+// This is the only rel_body constructor that has ref_count initialized to 1;
+// That's because it's used to construct the global Rel_Body "null_rel".
+// Unfortunately because we don't know in what order global constructors will
+// be called, we could create a global relation with the default relation
+// constructor (which would set the null_rel ref count to 1), and *then*
+// call Rel_Body::Rel_Body(), which would set it back to 0, leaving a relation
+// that points to a rel_body with it's ref_count set to 0! So this is done as
+// a special case, in which the ref_count is always 1.
+Rel_Body::Rel_Body():
+ Formula(0, this),
+ ref_count(1),
+ status(under_construction),
+ number_input(0), number_output(0),
+ In_Names(0), Out_Names(0),
+ simplified_DNF(NULL),
+ r_conjs(0),
+ finalized(true),
+ _is_set(false) {
+}
+
+
+Rel_Body::Rel_Body(int n_input, int n_output):
+ Formula(0, this),
+ ref_count(0),
+ status(under_construction),
+ number_input(n_input), number_output(n_output),
+ In_Names(n_input), Out_Names(n_output),
+ simplified_DNF(NULL),
+ r_conjs(0),
+ finalized(false) {
+ if (n_output == 0)
+ _is_set = true;
+ else
+ _is_set = false;
+ if(pres_debug) {
+ fprintf(DebugFile, "+++ Create Rel_Body::Rel_Body(%d, %d) = 0x%p +++\n",
+ n_input, n_output, this);
+ }
+ int i;
+ for(i=1; i<=number_input; i++) {
+ In_Names[i] = Const_String();
+ }
+ for(i=1; i<=number_output; i++) {
+ Out_Names[i] = Const_String();
+ }
+}
+
+// Rel_Body::Rel_Body(Rel_Body *r):
+// Formula(0, this),
+// ref_count(0),
+// status(r->status),
+// number_input(r->number_input), number_output(r->number_output),
+// In_Names(r->number_input), Out_Names(r->number_output),
+// simplified_DNF(NULL),
+// r_conjs(r->r_conjs),
+// finalized(r->finalized),
+// _is_set(r->_is_set) {
+// if(pres_debug) {
+// fprintf(DebugFile, "+++ Copy Rel_Body::Rel_Body(Rel_Body * 0x%p) = 0x%p +++\n", r, this);
+// prefix_print(DebugFile);
+// }
+
+// int i;
+// for(i=1;i<=r->number_input;i++) In_Names[i] = r->In_Names[i];
+// for(i=1;i<=r->number_output;i++) Out_Names[i] = r->Out_Names[i];
+// copy_var_decls(Symbolic,r->Symbolic);
+
+// if(!r->children().empty() && r->simplified_DNF==NULL) {
+// Formula *f = r->formula()->copy(this,this);
+// f->remap();
+// children().append(f);
+// }
+// else if(r->children().empty() && r->simplified_DNF!=NULL) {
+// simplified_DNF = r->simplified_DNF->copy(this);
+// simplified_DNF->remap();
+// }
+// else { // copy NULL relation
+// }
+
+// reset_remap_field(r->Symbolic);
+// }
+
+Rel_Body *Rel_Body::clone() {
+ Rel_Body *b = new Rel_Body();
+
+ b->ref_count = 0;
+ b->status = status;
+ b->number_input = number_input;
+ b->number_output = number_output;
+ b->r_conjs = r_conjs;
+ b->finalized = finalized;
+ b->_is_set = _is_set;
+
+ b->In_Names = Tuple<Const_String>(number_input);
+ b->Out_Names = Tuple<Const_String>(number_output);
+ for(int i = 1; i <= number_input; i++)
+ b->In_Names[i] = In_Names[i];
+ for(int i = 1; i <= number_output; i++)
+ b->Out_Names[i] = Out_Names[i];
+
+ copy_var_decls(b->Symbolic, Symbolic);
+
+ if(!children().empty() && simplified_DNF==NULL) {
+ Formula *f = formula()->copy(b, b);
+ f->remap();
+ b->children().append(f);
+ }
+ else if(children().empty() && simplified_DNF!=NULL) {
+ b->simplified_DNF = simplified_DNF->copy(b);
+ b->simplified_DNF->remap();
+ }
+ else { // copy NULL relation
+ }
+
+ reset_remap_field(Symbolic);
+ return b;
+}
+
+
+Rel_Body::Rel_Body(Rel_Body *r, Conjunct *c):
+ Formula(0, this),
+ ref_count(0),
+ status(uncompressed),
+ number_input(r->number_input), number_output(r->number_output),
+ In_Names(r->number_input), Out_Names(r->number_output),
+ r_conjs(0),
+ finalized(r->finalized),
+ _is_set(r->_is_set) {
+ if(pres_debug) {
+ fprintf(DebugFile, "+++ Copy Rel_Body::Rel_Body(Rel_Body * 0x%p, Conjunct * 0x%p) = 0x%p +++\n",r,c,this);
+ }
+
+ int i;
+ for(i=1;i<=r->number_input;i++) In_Names[i] = r->In_Names[i];
+ for(i=1;i<=r->number_output;i++) Out_Names[i] = r->Out_Names[i];
+ copy_var_decls(Symbolic,r->Symbolic);
+
+ // assert that r has as many variables as c requires, or that c is from r
+ assert(r == c->relation());
+ assert(r->simplified_DNF != NULL);
+ simplified_DNF = new DNF;
+ simplified_DNF->add_conjunct(c->copy_conj_diff_relation(this,this));
+ single_conjunct()->remap();
+
+ reset_remap_field(r->Symbolic);
+}
+
+Rel_Body::~Rel_Body() {
+ if(pres_debug) {
+ fprintf(DebugFile, "+++ Destroy Rel_Body::~Rel_Body() 0x%p +++\n", this);
+ }
+ free_var_decls(Symbolic);
+ if(simplified_DNF != NULL) {
+ delete simplified_DNF;
+ }
+}
+
+//
+// Take a relation that has been simplified and convert it
+// back to formula form.
+//
+void Rel_Body::DNF_to_formula() {
+ assert(!is_null());
+ if (simplified_DNF != NULL) {
+ simplified_DNF->DNF_to_formula(this);
+ simplified_DNF = NULL;
+ status = under_construction;
+ }
+}
+
+bool Rel_Body::can_add_child() {
+ assert(this != &null_rel);
+ return n_children() < 1;
+}
+
+
+
+// ********************
+// Simplify functions
+// ********************
+
+
+extern int s_rdt_constrs;
+
+
+//
+// Simplify a given relation.
+// Store the resulting DNF in the relation, clean out the formula.
+//
+void Rel_Body::simplify(int rdt_conjs, int rdt_constrs) {
+ if(simplified_DNF == NULL) {
+ finalized = true;
+ if(children().empty()) {
+ simplified_DNF = new DNF;
+ }
+ else {
+ if(pres_debug) {
+ if(DebugFile==NULL) {
+ DebugFile = fopen("test.out", "w");
+ if(DebugFile==NULL)
+ fprintf(stderr, "Can not open file test.out\n");
+ }
+ }
+
+ assert(children().length()==1);
+ if(pres_debug) {
+ fprintf(DebugFile, "=== %p Rel_Body::simplify(%d, %d) Input tree (%d) ===\n", this,rdt_conjs,rdt_constrs,r_conjs);
+ prefix_print(DebugFile);
+ }
+ verify_tree();
+
+ beautify();
+ verify_tree();
+
+ rearrange();
+ verify_tree();
+
+ beautify();
+ verify_tree();
+
+ s_rdt_constrs = rdt_constrs;
+ if(pres_debug) {
+ fprintf(DebugFile, "\n=== In simplify, before DNFize ===\n");
+ prefix_print(DebugFile);
+ }
+ DNFize();
+ if(pres_debug) {
+ fprintf(DebugFile, "\n=== In simplify, after DNFize ===\n");
+ prefix_print(DebugFile);
+ }
+ verify_tree();
+
+
+ simplified_DNF->rm_redundant_inexact_conjs();
+ verify_tree();
+
+ if (rdt_conjs > 0 && !simplified_DNF->is_definitely_false() && simplified_DNF->length() > 1) {
+ simplified_DNF->rm_redundant_conjs(rdt_conjs-1);
+ verify_tree();
+ }
+
+ if(pres_debug) {
+ fprintf(DebugFile, "\n=== Resulting Relation ===\n");
+ prefix_print(DebugFile);
+ }
+ }
+ }
+ else {
+ /* Reprocess DNF to get rid of redundant stuff */
+
+ if (rdt_constrs < 0) return;
+ simplified_DNF->rm_redundant_inexact_conjs();
+
+ if (rdt_conjs > r_conjs) {
+ if(pres_debug)
+ fprintf(DebugFile,"=== Rel_Body::simplify() redundant CONJUNCTS ===\n");
+ simplified_DNF->rm_redundant_conjs(rdt_conjs-1);
+ }
+ if (rdt_constrs > 0 ) {
+ if(pres_debug)
+ fprintf(DebugFile,"=== Rel_Body::simplify() redundant CONSTR-S ===\n");
+ s_rdt_constrs = rdt_constrs;
+ simplified_DNF->simplify();
+ }
+ }
+
+ r_conjs = rdt_conjs;
+
+ for(DNF_Iterator D(simplified_DNF); D.live(); D.next()) {
+ D.curr()->set_relation(this);
+ D.curr()->set_parent(this);
+ }
+}
+
+
+// ******************
+// Query functions
+// ******************
+
+
+//
+// Check if relation has a single conjunct formula and return this conjunct.
+//
+Conjunct *Rel_Body::single_conjunct() {
+ simplify();
+ return simplified_DNF->single_conjunct();
+}
+
+bool Rel_Body::has_single_conjunct() {
+ simplify();
+ return simplified_DNF->has_single_conjunct();
+}
+
+//
+// Remove and return first conjunct
+//
+Conjunct *Rel_Body::rm_first_conjunct() {
+ simplify();
+ return simplified_DNF->rm_first_conjunct();
+}
+
+
+void Rel_Body::query_difference(Variable_ID v1, Variable_ID v2, coef_t &lowerBound, coef_t &upperBound, bool &guaranteed) {
+ simplify();
+
+ coef_t _lb, _ub;
+ int first = 1;
+ bool _g;
+ lowerBound = negInfinity; // default values if no DNF's
+ upperBound = posInfinity;
+ guaranteed = 0;
+
+ for (DNF_Iterator D(simplified_DNF); D.live(); D.next()) {
+ (*D)->query_difference(v1, v2, _lb, _ub, _g);
+ if (first) {
+ lowerBound = _lb;
+ upperBound = _ub;
+ guaranteed = _g;
+ first = 0;
+ }
+ else {
+ guaranteed = guaranteed && _g;
+ lowerBound = min(lowerBound, _lb);
+ upperBound = max(upperBound, _ub);
+ }
+ }
+}
+
+
+void Rel_Body::query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound) {
+ simplify();
+
+ coef_t _lb, _ub;
+ int first = 1;
+ lowerBound = negInfinity; // default values if no DNF's
+ upperBound = posInfinity;
+
+ for (DNF_Iterator D(simplified_DNF); D.live(); D.next()) {
+ (*D)->query_variable_bounds(v, _lb, _ub);
+ if (first) {
+ lowerBound = _lb;
+ upperBound = _ub;
+ first = 0;
+ }
+ else {
+ lowerBound = min(lowerBound, _lb);
+ upperBound = max(upperBound, _ub);
+ }
+ }
+}
+
+coef_t Rel_Body::query_variable_mod(Variable_ID v, coef_t factor) {
+ simplify();
+
+ bool first = true;
+ coef_t result;
+
+ for (DNF_Iterator D(simplified_DNF); D.live(); D.next()) {
+ coef_t t = (*D)->query_variable_mod(v, factor);
+ if (t == posInfinity)
+ return posInfinity;
+
+ if (first) {
+ result = t;
+ first = false;
+ }
+ else {
+ if (result != t)
+ return posInfinity;
+ }
+ }
+
+ return result;
+}
+
+
+
+//
+// Simplify formula if needed and return the resulting DNF.
+//
+DNF* Rel_Body::query_DNF() {
+ return(query_DNF(false,false));
+}
+
+DNF* Rel_Body::query_DNF(int rdt_conjs, int rdt_constrs) {
+ simplify(rdt_conjs, rdt_constrs);
+ return(simplified_DNF);
+}
+
+//
+// Other formula queries.
+//
+
+// Interpret UNKNOWN as true, then check satisfiability
+// i.e., check if the formula simplifies to FALSE, since the library
+// will never say that if the *known* constraints are unsatisfiable by
+// themselves.
+bool Rel_Body::is_upper_bound_satisfiable() {
+ int tmp = s_rdt_constrs;
+ s_rdt_constrs = -1;
+ simplify();
+ s_rdt_constrs = tmp;
+ return(!simplified_DNF->is_definitely_false());
+}
+
+// Interpret UNKNOWN as false, then check satisfiability
+// i.e., check if there exist any exact conjuncts in the solution
+bool Rel_Body::is_lower_bound_satisfiable() {
+ int tmp = s_rdt_constrs;
+ s_rdt_constrs = -1;
+ simplify();
+ s_rdt_constrs = tmp;
+ for(DNF_Iterator d(simplified_DNF); d; d++)
+ if((*d)->is_exact()) return true;
+ return false;
+}
+
+bool Rel_Body::is_satisfiable() {
+ assert(is_lower_bound_satisfiable() == is_upper_bound_satisfiable());
+ return is_upper_bound_satisfiable();
+}
+
+// Check if we can easily determine if the formula evaluates to true.
+bool Rel_Body::is_obvious_tautology() {
+ int tmp = s_rdt_constrs;
+ s_rdt_constrs = 0;
+ simplify();
+ s_rdt_constrs = tmp;
+ return(simplified_DNF->is_definitely_true());
+}
+
+// Expensive check to determine if the formula evaluates to true.
+bool Rel_Body::is_definite_tautology() {
+ if(is_obvious_tautology()) return true;
+ Relation l = Lower_Bound(Relation(*this,1));
+ return !(Complement(l).is_upper_bound_satisfiable());
+}
+
+bool Rel_Body::is_unknown() {
+ simplify();
+ return(has_single_conjunct() && single_conjunct()->is_unknown());
+}
+
+//
+// Get accuracy status of the relation
+//
+
+Rel_Unknown_Uses Rel_Body::unknown_uses() {
+ if (!is_simplified())
+ simplify();
+
+ Rel_Unknown_Uses local_status=0;
+ int n_conj=0;
+
+ for (DNF_Iterator c(simplified_DNF); c; c++) {
+ n_conj++;
+ if ((*c)->is_exact())
+ local_status |= no_u;
+ else if ((*c)->is_unknown())
+ local_status |= or_u;
+ else
+ local_status |= and_u;
+ }
+
+ if (n_conj == 0) {
+ assert(local_status == 0);
+ local_status = no_u;
+ }
+ assert(local_status);
+#if ! defined NDEBUG
+ Rel_Unknown_Uses impossible = (and_u | or_u);
+ assert( (local_status & impossible) != impossible);
+#endif
+
+ return local_status;
+}
+
+void Rel_Body::interpret_unknown_as_false() {
+ simplify();
+ simplified_DNF->remove_inexact_conj();
+}
+
+void Rel_Body::interpret_unknown_as_true() {
+ simplify();
+ for(DNF_Iterator d(simplified_DNF); d; d++)
+ (*d)->interpret_unknown_as_true();
+}
+
+
+void Rel_Body::reverse_leading_dir_info() {
+ if (is_simplified()) {
+ for (DNF_Iterator c(simplified_DNF); c; c++)
+ (*c)->reverse_leading_dir_info();
+ }
+ else {
+ assert(!simplified_DNF);
+ assert(children().size() == 1);
+ children().front()->reverse_leading_dir_info();
+ }
+}
+
+//
+// Rel_Body::DNFize just DNF-izes its child node and calls verify
+//
+
+DNF* Rel_Body::DNFize() {
+#if defined(INCLUDE_COMPRESSION)
+ assert(!this->is_compressed());
+#endif
+ if (! simplified_DNF) {
+ simplified_DNF = children().remove_front()->DNFize();
+
+ int mua = max_shared_ufs_arity();
+ if (mua > 0) {
+ if (pres_debug) {
+ fprintf(DebugFile, "\n=== In DNFize, before LCDNF ===\n");
+ prefix_print(DebugFile);
+ }
+
+ simplified_DNF->make_level_carried_to(mua);
+ }
+
+ if(pres_debug) {
+ fprintf(DebugFile, "\n=== In DNFize, before verify ===\n");
+ prefix_print(DebugFile);
+ }
+
+ simplified_DNF->simplify();
+ }
+
+ assert(children().length() == 0);
+
+ return simplified_DNF;
+}
+
+void Rel_Body::make_level_carried_to(int level) {
+ if (!simplified_DNF) {
+ DNFize();
+ }
+
+ assert(simplified_DNF && children().empty());
+
+ simplified_DNF->make_level_carried_to(level);
+}
+
+//
+// if direction==0, move all conjuncts with >= level leading 0's to return
+// else move all conjuncts with level-1 0's followed by
+// the appropriate signed difference to returned Relation
+//
+
+Relation Rel_Body::extract_dnf_by_carried_level(int level, int direction) {
+ if (!simplified_DNF) {
+ DNFize();
+ }
+
+ assert(simplified_DNF && children().empty());
+
+ simplified_DNF->make_level_carried_to(level);
+
+ Relation extracted(n_inp(), n_out());
+ extracted.copy_names(*this);
+ assert(extracted.rel_body->children().empty());
+ assert(extracted.rel_body->simplified_DNF == NULL);
+ extracted.rel_body->simplified_DNF = new DNF;
+ extracted.rel_body->Symbolic = Symbolic;
+
+ DNF *remaining = new DNF;
+ Conjunct *curr;
+
+ for (curr = simplified_DNF->rm_first_conjunct();
+ curr;
+ curr = simplified_DNF->rm_first_conjunct()) {
+ assert(curr->guaranteed_leading_0s >= level || curr->guaranteed_leading_0s == curr->possible_leading_0s);
+ assert(curr->possible_leading_0s >= 0);
+
+ curr->assert_leading_info();
+
+ if ((direction == 0 && curr->guaranteed_leading_0s >= level) ||
+ (curr->guaranteed_leading_0s == level-1 &&
+ curr->leading_dir_valid_and_known() &&
+ curr->leading_dir * direction > 0)) {
+ extracted.rel_body->simplified_DNF->add_conjunct(curr);
+ }
+ else {
+ remaining->add_conjunct(curr);
+ }
+ }
+ delete simplified_DNF;
+ simplified_DNF = remaining;
+
+#if ! defined NDEBUG
+ for (DNF_Iterator rc(simplified_DNF); rc; rc++)
+ (*rc)->assert_leading_info();
+
+ for (DNF_Iterator ec(extracted.rel_body->simplified_DNF); ec; ec++)
+ (*ec)->assert_leading_info();
+#endif
+
+ finalize();
+ extracted.finalize();
+ return extracted;
+}
+
+//Compress/uncompress functions
+
+bool Rel_Body::is_compressed() {
+#if defined(INCLUDE_COMPRESSION)
+ if(is_simplified()) {
+ for(DNF_Iterator p(simplified_DNF); p.live(); p.next()) {
+ if(p.curr()->is_compressed())
+ return true;
+ }
+ }
+ return false;
+#else
+ return true; // This allows is_compressed assertions to work
+#endif
+}
+
+void Rel_Body::compress() {
+#if !defined(INCLUDE_COMPRESSION)
+ return;
+#else
+ if (status == compressed)
+ return;
+ if (pres_debug)
+ fprintf(DebugFile,">>> Compressing relation %p\n",this);
+ simplify();
+ for(DNF_Iterator p(simplified_DNF); p.live(); p.next()) {
+ p.curr()->compress();
+ status = compressed;
+ }
+#endif
+}
+
+void Rel_Body::uncompress() {
+#if !defined(INCLUDE_COMPRESSION)
+ return;
+#else
+ if (pres_debug)
+ fprintf(DebugFile,"<<< Uncompressing relation %p\n",this);
+ assert(is_simplified());
+ for(DNF_Iterator p(simplified_DNF); p.live(); p.next()) {
+ p.curr()->uncompress();
+ status = uncompressed;
+ }
+#endif
+}
+
+}
generated by cgit v1.2.3-70-g09d2 (git 2.47.1) at 2025-02-02 00:37:57 +0000