CaDiCaL::External Struct Reference

#include <external.hpp>

Collaboration diagram for CaDiCaL::External:

Public Member Functions
void	export_learned_empty_clause ()
void	export_learned_unit_clause (int ilit)
void	export_learned_large_clause (const vector< int > &)
void	add_observed_var (int elit)
void	remove_observed_var (int elit)
void	reset_observed_vars ()
bool	observed (int elit)
bool	is_witness (int elit)
bool	is_decision (int elit)
void	force_backtrack (size_t new_level)
int	vidx (int elit) const
int	vlit (int elit) const
bool	is_valid_input (int elit)
void	push_zero_on_extension_stack ()
void	push_clause_literal_on_extension_stack (int ilit)
void	push_witness_literal_on_extension_stack (int ilit)
void	push_clause_on_extension_stack (Clause *)
void	push_clause_on_extension_stack (Clause *, int witness)
void	push_binary_clause_on_extension_stack (int64_t id, int witness, int other)
void	extend ()
void	conclude_sat ()
unsigned	elit2ulit (int elit) const
bool	marked (const vector< bool > &map, int elit) const
void	mark (vector< bool > &map, int elit)
void	unmark (vector< bool > &map, int elit)
void	push_external_clause_and_witness_on_extension_stack (const vector< int > &clause, const vector< int > &witness, int64_t id)
void	push_id_on_extension_stack (int64_t id)
void	restore_clause (const vector< int >::const_iterator &begin, const vector< int >::const_iterator &end, const int64_t id)
void	restore_clauses ()
void	freeze (int elit)
void	melt (int elit)
bool	frozen (int elit)
	External (Internal *)
	~External ()
void	enlarge (int new_max_var)
void	init (int new_max_var, bool extension=false)
int	internalize (int, bool extension=false)
void	reset_assumptions ()
void	reset_concluded ()
void	reset_extended ()
void	reset_limits ()
void	add (int elit)
void	assume (int elit)
int	solve (bool preprocess_only)
int	ival (int elit) const
bool	flip (int elit)
bool	flippable (int elit)
bool	failed (int elit)
void	terminate ()
void	constrain (int elit)
bool	failed_constraint ()
void	reset_constraint ()
int	propagate_assumptions ()
void	implied (std::vector< int > &entrailed)
void	conclude_unknown ()
int	lookahead ()
CaDiCaL::CubesWithStatus	generate_cubes (int, int)
int	fixed (int elit) const
void	phase (int elit)
void	unphase (int elit)
bool	traverse_all_frozen_units_as_clauses (ClauseIterator &)
bool	traverse_all_non_frozen_units_as_witnesses (WitnessIterator &)
bool	traverse_witnesses_backward (WitnessIterator &)
bool	traverse_witnesses_forward (WitnessIterator &)
void	copy_flags (External &other) const
void	check_assumptions_satisfied ()
void	check_constraint_satisfied ()
void	check_failing ()
void	check_solution_on_learned_clause ()
void	check_solution_on_shrunken_clause (Clause *)
void	check_solution_on_learned_unit_clause (int unit)
void	check_no_solution_after_learning_empty_clause ()
void	check_learned_empty_clause ()
void	check_learned_unit_clause (int unit)
void	check_learned_clause ()
void	check_shrunken_clause (Clause *c)
void	check_assignment (int(External::*assignment)(int) const)
void	check_satisfiable ()
void	check_unsatisfiable ()
void	check_solve_result (int res)
void	update_molten_literals ()
int	sol (int elit) const

Public Attributes
Internal *	internal
int	max_var
size_t	vsize
vector< bool >	vals
vector< int >	e2i
vector< int >	assumptions
vector< int >	constraint
vector< int64_t >	ext_units
vector< bool >	ext_flags
vector< int >	eclause
bool	extended
bool	concluded
vector< int >	extension
vector< bool >	witness
vector< bool >	tainted
vector< bool >	ervars
vector< unsigned >	frozentab
Terminator *	terminator
Learner *	learner
FixedAssignmentListener *	fixed_listener
ExternalPropagator *	propagator
vector< bool >	is_observed
unordered_map< uint64_t, vector< int > >	forgettable_original
signed char *	solution
int	solution_size
vector< int >	original
vector< bool >	moltentab
const Range	vars

Detailed Description

Definition at line 57 of file external.hpp.

Constructor & Destructor Documentation

External()

CaDiCaL::External::External

(

Internal *

i

)

Definition at line 10 of file cadical_external.cpp.

    : internal (i), max_var (0), vsize (0), extended (false),
      concluded (false), terminator (0), learner (0), fixed_listener (0),
      propagator (0), solution (0), vars (max_var) {
  CADICAL_assert (internal);
  CADICAL_assert (!internal->external);
  internal->external = this;
}

Here is the caller graph for this function:

~External()

CaDiCaL::External::~External

(

)

Definition at line 19 of file cadical_external.cpp.

                     {
  if (solution)
    delete[] solution;
}

Member Function Documentation

add()

void CaDiCaL::External::add

(

int

elit

)

Definition at line 171 of file cadical_external.cpp.

                            {
  CADICAL_assert (elit != INT_MIN);
  reset_extended ();
 
  bool forgettable = false;
 
  if (internal->opts.check &&
      (internal->opts.checkwitness || internal->opts.checkfailed)) {
 
    forgettable =
        internal->from_propagator && internal->ext_clause_forgettable;
 
    // Forgettable clauses (coming from the external propagator) are not
    // saved into the external 'original' stack. They are stored separately
    // in external 'forgettable_original', from where they are deleted when
    // the corresponding clause is deleted (actually deleted, not just
    // marked as garbage).
    if (!forgettable)
      original.push_back (elit);
  }
 
  const int ilit = internalize (elit);
  CADICAL_assert (!elit == !ilit);
 
  // The external literals of the new clause must be saved for later
  // when the proof is printed during add_original_lit (0)
  if (elit && (internal->proof || forgettable)) {
    eclause.push_back (elit);
    if (internal->lrat) {
      // actually find unit of -elit (flips elit < 0)
      unsigned eidx = (elit > 0) + 2u * (unsigned) abs (elit);
      CADICAL_assert ((size_t) eidx < ext_units.size ());
      const int64_t id = ext_units[eidx];
      bool added = ext_flags[abs (elit)];
      if (id && !added) {
        ext_flags[abs (elit)] = true;
        internal->lrat_chain.push_back (id);
      }
    }
  }
 
  if (!elit && internal->proof && internal->lrat) {
    for (const auto &elit : eclause) {
      ext_flags[abs (elit)] = false;
    }
  }
 
  if (elit)
    LOG ("adding external %d as internal %d", elit, ilit);
  internal->add_original_lit (ilit);
 
  // Clean-up saved external literals once proof line is printed
  if (!elit && (internal->proof || forgettable))
    eclause.clear ();
}

Here is the call graph for this function:

add_observed_var()

void CaDiCaL::External::add_observed_var

(

int

elit

)

Definition at line 341 of file cadical_external.cpp.

                                         {
  if (!propagator) {
    LOG ("No connected propagator that could observe the variable, "
         "observed flag is not set.");
    return;
  }
 
  CADICAL_assert (elit);
  CADICAL_assert (elit != INT_MIN);
  reset_extended (); // tainting!
 
  int eidx = abs (elit);
  if (eidx <= max_var &&
      (marked (witness, elit) || marked (witness, -elit))) {
    LOG ("Error, only clean variables are allowed to become observed.");
    CADICAL_assert (false);
 
    // TODO: here needs to come the taint and restore of the newly
    // observed variable. Restore_clauses must be called before continue.
    // LOG ("marking tainted %d", elit);
    // mark (tainted, elit);
    // mark (tainted, -elit);
    // restore_clauses ...
  }
 
  if (eidx >= (int64_t) is_observed.size ())
    is_observed.resize (1 + (size_t) eidx, false);
 
  if (is_observed[eidx])
    return;
 
  LOG ("marking %d as externally watched", eidx);
 
  // Will do the necessary internalization
  freeze (elit);
  is_observed[eidx] = true;
 
  int ilit = internalize (elit);
  // internal add-observed-var backtracks to a lower decision level to
  // unassign the variable in case it was already assigned previously (but
  // not on the current level)
  internal->add_observed_var (ilit);
 
  if (propagator->is_lazy)
    return;
 
  // In case this variable was already assigned (e.g. via unit clause) and
  // got compacted to map to another (not observed) variable, it can not be
  // unnasigned so it must be notified explicitly now. (-> Can lead to
  // repeated fixed assignment notifications, in case it was unobserved and
  // observed again. But a repeated notification is less error-prone than
  // never notifying an assignment.)
  const int tmp = fixed (elit);
  if (!tmp)
    return;
  int unit = tmp < 0 ? -elit : elit;
 
  LOG ("notify propagator about fixed assignment upon observe for %d",
       unit);
 
  // internal add-observed-var had to backtrack to root-level already
  CADICAL_assert (!internal->level);
 
  std::vector<int> assigned = {unit};
  propagator->notify_assignment (assigned);
}

Here is the call graph for this function:

assume()

void CaDiCaL::External::assume

(

int

elit

)

Definition at line 227 of file cadical_external.cpp.

                               {
  CADICAL_assert (elit);
  reset_extended ();
  if (internal->proof)
    internal->proof->add_assumption (elit);
  assumptions.push_back (elit);
  const int ilit = internalize (elit);
  CADICAL_assert (ilit);
  LOG ("assuming external %d as internal %d", elit, ilit);
  internal->assume (ilit);
}

Here is the call graph for this function:

check_assignment()

void CaDiCaL::External::check_assignment

(

int(External::*

assignment )(int) const

)

Definition at line 697 of file cadical_external.cpp.

                                                             {
 
  // First check all assigned and consistent.
  //
  for (auto idx : vars) {
    if (!(this->*a) (idx))
      FATAL ("unassigned variable: %d", idx);
    int value_idx = (this->*a) (idx);
    int value_neg_idx = (this->*a) (-idx);
    if (value_idx == idx)
      CADICAL_assert (value_neg_idx == idx);
    else {
      CADICAL_assert (value_idx == -idx);
      CADICAL_assert (value_neg_idx == -idx);
    }
    if (value_idx != value_neg_idx)
      FATAL ("inconsistently assigned literals %d and %d", idx, -idx);
  }
 
  // Then check that all (saved) original clauses are satisfied.
  //
  bool satisfied = false;
  const auto end = original.end ();
  auto start = original.begin (), i = start;
#ifndef CADICAL_QUIET
  int64_t count = 0;
#endif
  for (; i != end; i++) {
    int lit = *i;
    if (!lit) {
      if (!satisfied) {
        fatal_message_start ();
        fputs ("unsatisfied clause:\n", stderr);
        for (auto j = start; j != i; j++)
          fprintf (stderr, "%d ", *j);
        fputc ('0', stderr);
        fatal_message_end ();
      }
      satisfied = false;
      start = i + 1;
#ifndef CADICAL_QUIET
      count++;
#endif
    } else if (!satisfied && (this->*a) (lit) == lit)
      satisfied = true;
  }
 
  bool presence_flag;
  // Check those forgettable external clauses that are still present, but
  // only if the external propagator is still connected (otherwise solution
  // reconstruction is allowed to touch the previously observed variables so
  // there is no guarantee that the final model will satisfy these clauses.)
  for (const auto &forgettables : forgettable_original) {
    if (!propagator)
      break;
    presence_flag = true;
    satisfied = false;
#ifndef CADICAL_QUIET
    count++;
#endif
    std::vector<int> literals;
    for (const auto lit : forgettables.second) {
      if (presence_flag) {
        // First integer is a Boolean flag, not a literal
        if (!lit) {
          // Deleted clauses can be ignored, they count as satisfied
          satisfied = true;
          break;
        }
        presence_flag = false;
        continue;
      }
 
      if ((this->*a) (lit) == lit) {
        satisfied = true;
        break;
      }
    }
 
    if (!satisfied) {
      fatal_message_start ();
      fputs ("unsatisfied external forgettable clause:\n", stderr);
      for (size_t j = 1; j < forgettables.second.size (); j++)
        fprintf (stderr, "%d ", forgettables.second[j]);
      fputc ('0', stderr);
      fatal_message_end ();
    }
  }
#ifndef CADICAL_QUIET
  VERBOSE (1, "satisfying assignment checked on %" PRId64 " clauses",
           count);
#endif
}

Here is the call graph for this function:

Here is the caller graph for this function:

check_assumptions_satisfied()

void CaDiCaL::External::check_assumptions_satisfied

(

)

Definition at line 793 of file cadical_external.cpp.

                                            {
  for (const auto &lit : assumptions) {
    // Not 'signed char' !!!!
    const int tmp = ival (lit);
    if (tmp != lit)
      FATAL ("assumption %d falsified", lit);
    if (!tmp)
      FATAL ("assumption %d unassigned", lit);
  }
  VERBOSE (1, "checked that %zd assumptions are satisfied",
           assumptions.size ());
}

Here is the call graph for this function:

Here is the caller graph for this function:

check_constraint_satisfied()

void CaDiCaL::External::check_constraint_satisfied

(

)

Definition at line 806 of file cadical_external.cpp.

                                           {
  for (const auto lit : constraint) {
    if (ival (lit) == lit) {
      VERBOSE (1, "checked that constraint is satisfied");
      return;
    }
  }
  FATAL ("constraint not satisfied");
}

Here is the call graph for this function:

Here is the caller graph for this function:

check_failing()

void CaDiCaL::External::check_failing

(

)

Definition at line 816 of file cadical_external.cpp.

                              {
  Solver *checker = new Solver ();
  DeferDeletePtr<Solver> delete_checker (checker);
  checker->prefix ("checker ");
#ifdef LOGGING
  if (internal->opts.log)
    checker->set ("log", true);
#endif
 
  for (const auto lit : assumptions) {
    if (!failed (lit))
      continue;
    LOG ("checking failed literal %d in core", lit);
    checker->add (lit);
    checker->add (0);
  }
  if (failed_constraint ()) {
    LOG (constraint, "checking failed constraint");
    for (const auto lit : constraint)
      checker->add (lit);
  } else if (constraint.size ())
    LOG (constraint, "constraint satisfied and ignored");
 
  // Add original clauses as last step, failing () and failed_constraint ()
  // might add more external clauses (due to lazy explanation)
  for (const auto lit : original)
    checker->add (lit);
 
  // Add every forgettable external clauses
  for (const auto &forgettables : forgettable_original) {
    bool presence_flag = true;
    for (const auto lit : forgettables.second) {
      if (presence_flag) {
        // First integer is a Boolean flag, not a literal, ignore it here
        presence_flag = false;
        continue;
      }
      checker->add (lit);
    }
    checker->add (0);
  }
 
  int res = checker->solve ();
  if (res != 20)
    FATAL ("failed assumptions do not form a core");
  delete_checker.free ();
  VERBOSE (1, "checked that %zd failing assumptions form a core",
           assumptions.size ());
}

Here is the call graph for this function:

Here is the caller graph for this function:

check_learned_clause()

void CaDiCaL::External::check_learned_clause ( )

inline

Definition at line 417 of file external.hpp.

                               {
    if (solution)
      check_solution_on_learned_clause ();
  }

Here is the call graph for this function:

check_learned_empty_clause()

void CaDiCaL::External::check_learned_empty_clause ( )

inline

Definition at line 407 of file external.hpp.

                                     {
    if (solution)
      check_no_solution_after_learning_empty_clause ();
  }

Here is the call graph for this function:

check_learned_unit_clause()

void CaDiCaL::External::check_learned_unit_clause ( int unit )

inline

Definition at line 412 of file external.hpp.

                                            {
    if (solution)
      check_solution_on_learned_unit_clause (unit);
  }

Here is the call graph for this function:

check_no_solution_after_learning_empty_clause()

void CaDiCaL::External::check_no_solution_after_learning_empty_clause

(

)

Definition at line 42 of file cadical_solution.cpp.

                                                              {
  CADICAL_assert (solution);
  FATAL ("learned empty clause but got solution");
}

Here is the caller graph for this function:

check_satisfiable()

void CaDiCaL::External::check_satisfiable

(

)

Definition at line 544 of file cadical_external.cpp.

                                  {
  LOG ("checking satisfiable");
  if (!extended)
    extend ();
  if (internal->opts.checkwitness)
    check_assignment (&External::ival);
  if (internal->opts.checkassumptions && !assumptions.empty ())
    check_assumptions_satisfied ();
  if (internal->opts.checkconstraint && !constraint.empty ())
    check_constraint_satisfied ();
}

Here is the call graph for this function:

Here is the caller graph for this function:

check_shrunken_clause()

void CaDiCaL::External::check_shrunken_clause ( Clause * c )

inline

Definition at line 422 of file external.hpp.

                                         {
    if (solution)
      check_solution_on_shrunken_clause (c);
  }

Here is the call graph for this function:

check_solution_on_learned_clause()

void CaDiCaL::External::check_solution_on_learned_clause

(

)

Definition at line 17 of file cadical_solution.cpp.

                                                 {
  CADICAL_assert (solution);
  for (const auto &lit : internal->clause)
    if (sol (internal->externalize (lit)) == lit)
      return;
  fatal_message_start ();
  fputs ("learned clause unsatisfied by solution:\n", stderr);
  for (const auto &lit : internal->clause)
    fprintf (stderr, "%d ", lit);
  fputc ('0', stderr);
  fatal_message_end ();
}

Here is the call graph for this function:

Here is the caller graph for this function:

check_solution_on_learned_unit_clause()

void CaDiCaL::External::check_solution_on_learned_unit_clause

(

int

unit

)

Definition at line 47 of file cadical_solution.cpp.

                                                              {
  CADICAL_assert (solution);
  if (sol (internal->externalize (unit)) == unit)
    return;
  FATAL ("learned unit %d contradicts solution", unit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

check_solution_on_shrunken_clause()

void CaDiCaL::External::check_solution_on_shrunken_clause

(

Clause *

c

)

Definition at line 30 of file cadical_solution.cpp.

                                                           {
  CADICAL_assert (solution);
  for (const auto &lit : *c)
    if (sol (internal->externalize (lit)) == lit)
      return;
  fatal_message_start ();
  for (const auto &lit : *c)
    fprintf (stderr, "%d ", lit);
  fputc ('0', stderr);
  fatal_message_end ();
}

Here is the call graph for this function:

Here is the caller graph for this function:

check_solve_result()

void CaDiCaL::External::check_solve_result

(

int

res

)

Definition at line 568 of file cadical_external.cpp.

                                          {
  if (!internal->opts.check)
    return;
  if (res == 10)
    check_satisfiable ();
  if (res == 20)
    check_unsatisfiable ();
}

Here is the call graph for this function:

Here is the caller graph for this function:

check_unsatisfiable()

void CaDiCaL::External::check_unsatisfiable

(

)

Definition at line 558 of file cadical_external.cpp.

                                    {
  LOG ("checking unsatisfiable");
  if (!internal->opts.checkfailed)
    return;
  if (!assumptions.empty () || !constraint.empty ())
    check_failing ();
}

Here is the call graph for this function:

Here is the caller graph for this function:

conclude_sat()

void CaDiCaL::External::conclude_sat

(

)

Definition at line 269 of file cadical_extend.cpp.

                             {
  if (!internal->proof || concluded)
    return;
  concluded = true;
  if (!extended)
    extend ();
  vector<int> model;
  for (int idx = 1; idx <= max_var; idx++) {
    if (ervars[idx])
      continue;
    const int lit = ival (idx);
    model.push_back (lit);
  }
  internal->proof->conclude_sat (model);
}

Here is the call graph for this function:

conclude_unknown()

void CaDiCaL::External::conclude_unknown

(

)

Definition at line 530 of file cadical_external.cpp.

                                 {
  if (!internal->proof || concluded)
    return;
  concluded = true;
 
  vector<int> trail;
  implied (trail);
  internal->proof->conclude_unknown (trail);
}

Here is the call graph for this function:

constrain()

void CaDiCaL::External::constrain

(

int

elit

)

Definition at line 288 of file cadical_external.cpp.

                                  {
  if (constraint.size () && !constraint.back ()) {
    LOG (constraint, "replacing previous constraint");
    reset_constraint ();
  }
  CADICAL_assert (elit != INT_MIN);
  reset_extended ();
  const int ilit = internalize (elit);
  CADICAL_assert (!elit == !ilit);
  if (elit)
    LOG ("adding external %d as internal %d to constraint", elit, ilit);
  else if (!elit && internal->proof) {
    internal->proof->add_constraint (constraint);
  }
  constraint.push_back (elit);
  internal->constrain (ilit);
}

Here is the call graph for this function:

copy_flags()

void CaDiCaL::External::copy_flags

(

External &

other

)

const

Definition at line 964 of file cadical_external.cpp.

                                                {
  const vector<Flags> &this_ftab = internal->ftab;
  vector<Flags> &other_ftab = other.internal->ftab;
  const unsigned limit = min (max_var, other.max_var);
  for (unsigned eidx = 1; eidx <= limit; eidx++) {
    const int this_ilit = e2i[eidx];
    if (!this_ilit)
      continue;
    const int other_ilit = other.e2i[eidx];
    if (!other_ilit)
      continue;
    if (!internal->active (this_ilit))
      continue;
    if (!other.internal->active (other_ilit))
      continue;
    CADICAL_assert (this_ilit != INT_MIN);
    CADICAL_assert (other_ilit != INT_MIN);
    const Flags &this_flags = this_ftab[abs (this_ilit)];
    Flags &other_flags = other_ftab[abs (other_ilit)];
    this_flags.copy (other_flags);
  }
}

Here is the call graph for this function:

elit2ulit()

unsigned CaDiCaL::External::elit2ulit ( int elit ) const

inline

Definition at line 208 of file external.hpp.

                                      {
    CADICAL_assert (elit);
    CADICAL_assert (elit != INT_MIN);
    const int idx = abs (elit) - 1;
    CADICAL_assert (idx <= max_var);
    return 2u * idx + (elit < 0);
  }

Here is the caller graph for this function:

enlarge()

void CaDiCaL::External::enlarge

(

int

new_max_var

)

Definition at line 24 of file cadical_external.cpp.

                                       {
 
  CADICAL_assert (!extended);
 
  size_t new_vsize = vsize ? 2 * vsize : 1 + (size_t) new_max_var;
  while (new_vsize <= (size_t) new_max_var)
    new_vsize *= 2;
  LOG ("enlarge external size from %zd to new size %zd", vsize, new_vsize);
  vsize = new_vsize;
}

Here is the caller graph for this function:

export_learned_empty_clause()

void CaDiCaL::External::export_learned_empty_clause

(

)

Definition at line 989 of file cadical_external.cpp.

                                            {
  CADICAL_assert (learner);
  if (learner->learning (0)) {
    LOG ("exporting learned empty clause");
    learner->learn (0);
  } else
    LOG ("not exporting learned empty clause");
}

export_learned_large_clause()

void CaDiCaL::External::export_learned_large_clause

(

const vector< int > &

clause

)

Definition at line 1010 of file cadical_external.cpp.

                                                                     {
  CADICAL_assert (learner);
  size_t size = clause.size ();
  CADICAL_assert (size <= (unsigned) INT_MAX);
  if (learner->learning ((int) size)) {
    LOG ("exporting learned clause of size %zu", size);
    for (auto ilit : clause) {
      const int elit = internal->externalize (ilit);
      CADICAL_assert (elit);
      learner->learn (elit);
    }
    learner->learn (0);
  } else
    LOG ("not exporting learned clause of size %zu", size);
}

export_learned_unit_clause()

void CaDiCaL::External::export_learned_unit_clause

(

int

ilit

)

Definition at line 998 of file cadical_external.cpp.

                                                   {
  CADICAL_assert (learner);
  if (learner->learning (1)) {
    LOG ("exporting learned unit clause");
    const int elit = internal->externalize (ilit);
    CADICAL_assert (elit);
    learner->learn (elit);
    learner->learn (0);
  } else
    LOG ("not exporting learned unit clause");
}

extend()

void CaDiCaL::External::extend

(

)

Definition at line 117 of file cadical_extend.cpp.

                       {
 
  CADICAL_assert (!extended);
  START (extend);
  internal->stats.extensions++;
 
  PHASE ("extend", internal->stats.extensions,
         "mapping internal %d assignments to %d assignments",
         internal->max_var, max_var);
 
#ifndef CADICAL_QUIET
  int64_t updated = 0;
#endif
  for (unsigned i = 1; i <= (unsigned) max_var; i++) {
    const int ilit = e2i[i];
    if (!ilit)
      continue;
    if (i >= vals.size ())
      vals.resize (i + 1, false);
    vals[i] = (internal->val (ilit) > 0);
#ifndef CADICAL_QUIET
    updated++;
#endif
  }
  PHASE ("extend", internal->stats.extensions,
         "updated %" PRId64 " external assignments", updated);
  PHASE ("extend", internal->stats.extensions,
         "extending through extension stack of size %zd",
         extension.size ());
  const auto begin = extension.begin ();
  auto i = extension.end ();
#ifndef CADICAL_QUIET
  int64_t flipped = 0;
#endif
  while (i != begin) {
    bool satisfied = false;
    int lit;
    CADICAL_assert (i != begin);
    while ((lit = *--i)) {
      if (satisfied)
        continue;
      if (ival (lit) == lit)
        satisfied = true;
      CADICAL_assert (i != begin);
    }
    CADICAL_assert (i != begin);
    LOG ("id=%" PRId64, ((int64_t) *i << 32) + *(i - 1));
    CADICAL_assert (*i || *(i - 1));
    --i;
    CADICAL_assert (i != begin);
    --i;
    CADICAL_assert (i != begin);
    CADICAL_assert (!*i);
    --i;
    CADICAL_assert (i != begin);
    if (satisfied)
      while (*--i)
        CADICAL_assert (i != begin);
    else {
      while ((lit = *--i)) {
        const int tmp = ival (lit); // not 'signed char'!!!
        if (tmp != lit) {
          LOG ("flipping blocking literal %d", lit);
          CADICAL_assert (lit);
          CADICAL_assert (lit != INT_MIN);
          size_t idx = abs (lit);
          if (idx >= vals.size ())
            vals.resize (idx + 1, false);
          vals[idx] = !vals[idx];
          internal->stats.extended++;
#ifndef CADICAL_QUIET
          flipped++;
#endif
        }
        CADICAL_assert (i != begin);
      }
    }
  }
  PHASE ("extend", internal->stats.extensions,
         "flipped %" PRId64 " literals during extension", flipped);
  extended = true;
  LOG ("extended");
  STOP (extend);
}

Here is the call graph for this function:

Here is the caller graph for this function:

failed()

bool CaDiCaL::External::failed

(

int

elit

)

Definition at line 274 of file cadical_external.cpp.

                               {
  CADICAL_assert (elit);
  CADICAL_assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var)
    return 0;
  int ilit = e2i[eidx];
  if (!ilit)
    return 0;
  if (elit < 0)
    ilit = -ilit;
  return internal->failed (ilit);
}

Here is the caller graph for this function:

failed_constraint()

bool CaDiCaL::External::failed_constraint

(

)

Definition at line 306 of file cadical_external.cpp.

                                  {
  return internal->failed_constraint ();
}

Here is the caller graph for this function:

fixed()

int CaDiCaL::External::fixed ( int elit ) const

inline

Definition at line 1768 of file internal.hpp.

                                          {
  CADICAL_assert (elit);
  CADICAL_assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var)
    return 0;
  int ilit = e2i[eidx];
  if (!ilit)
    return 0;
  if (elit < 0)
    ilit = -ilit;
  return internal->fixed (ilit);
}

Here is the caller graph for this function:

flip()

bool CaDiCaL::External::flip

(

int

elit

)

Definition at line 239 of file cadical_external.cpp.

                             {
  CADICAL_assert (elit);
  CADICAL_assert (elit != INT_MIN);
  CADICAL_assert (!propagator);
 
  int eidx = abs (elit);
  if (eidx > max_var)
    return false;
  if (marked (witness, elit))
    return false;
  int ilit = e2i[eidx];
  if (!ilit)
    return false;
  bool res = internal->flip (ilit);
  if (res && extended)
    reset_extended ();
  return res;
}

Here is the call graph for this function:

flippable()

bool CaDiCaL::External::flippable

(

int

elit

)

Definition at line 258 of file cadical_external.cpp.

                                  {
  CADICAL_assert (elit);
  CADICAL_assert (elit != INT_MIN);
  CADICAL_assert (!propagator);
 
  int eidx = abs (elit);
  if (eidx > max_var)
    return false;
  if (marked (witness, elit))
    return false;
  int ilit = e2i[eidx];
  if (!ilit)
    return false;
  return internal->flippable (ilit);
}

Here is the call graph for this function:

force_backtrack()

void CaDiCaL::External::force_backtrack

(

size_t

new_level

)

Definition at line 488 of file cadical_external.cpp.

                                                {
  if (!propagator) {
    LOG ("No connected propagator that could force backtracking");
    return;
  }
  LOG ("force backtrack to level %zd", new_level);
  internal->force_backtrack (new_level);
}

freeze()

void CaDiCaL::External::freeze

(

int

elit

)

Definition at line 654 of file cadical_external.cpp.

                               {
  reset_extended ();
  int ilit = internalize (elit);
  unsigned eidx = vidx (elit);
  if (eidx >= frozentab.size ())
    frozentab.resize (eidx + 1, 0);
  unsigned &ref = frozentab[eidx];
  if (ref < UINT_MAX) {
    ref++;
    LOG ("external variable %d frozen once and now frozen %u times", eidx,
         ref);
  } else
    LOG ("external variable %d frozen but remains frozen forever", eidx);
  internal->freeze (ilit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

frozen()

bool CaDiCaL::External::frozen ( int elit )

inline

Definition at line 257 of file external.hpp.

                         {
    CADICAL_assert (elit);
    CADICAL_assert (elit != INT_MIN);
    int eidx = abs (elit);
    if (eidx > max_var)
      return false;
    if (eidx >= (int) frozentab.size ())
      return false;
    return frozentab[eidx] > 0;
  }

Here is the caller graph for this function:

generate_cubes()

CaDiCaL::CubesWithStatus CaDiCaL::External::generate_cubes	(	int	depth,
		int	min_depth = 0 )

Definition at line 631 of file cadical_external.cpp.

                                                                      {
  reset_extended ();
  update_molten_literals ();
  reset_limits ();
  auto cubes = internal->generate_cubes (depth, min_depth);
  auto externalize = [this] (int ilit) {
    const int elit = ilit ? internal->externalize (ilit) : 0;
    MSG ("lookahead internal %d external %d", ilit, elit);
    return elit;
  };
  auto externalize_map = [this, externalize] (std::vector<int> cube) {
    (void) this;
    MSG ("Cube : ");
    std::for_each (begin (cube), end (cube), externalize);
  };
  std::for_each (begin (cubes.cubes), end (cubes.cubes), externalize_map);
 
  return cubes;
}

Here is the call graph for this function:

implied()

void CaDiCaL::External::implied

(

std::vector< int > &

entrailed

)

Definition at line 508 of file cadical_external.cpp.

                                               {
  std::vector<int> ilit_implicants;
  internal->implied (ilit_implicants);
 
  // Those implied literals must be filtered out that are witnesses
  // on the reconstruction stack -> no inplace externalize is possible.
  // (Internal does not see these marks, so no earlier filter is
  // possible.)
 
  trailed.clear();
 
  for (const auto &ilit : ilit_implicants) {
    CADICAL_assert (ilit);
    const int elit = internal->externalize (ilit);
    const int eidx = abs (elit);
    const bool is_extension_var = ervars[eidx];
    if (!marked (tainted, elit) && !is_extension_var) {
      trailed.push_back (elit);
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

init()

void CaDiCaL::External::init	(	int	new_max_var,
		bool	extension = false )

Definition at line 35 of file cadical_external.cpp.

                                                    {
  CADICAL_assert (!extended);
  if (new_max_var <= max_var)
    return;
  int new_vars = new_max_var - max_var;
  int old_internal_max_var = internal->max_var;
  int new_internal_max_var = old_internal_max_var + new_vars;
  internal->init_vars (new_internal_max_var);
  if ((size_t) new_max_var >= vsize)
    enlarge (new_max_var);
  LOG ("initialized %d external variables", new_vars);
  if (!max_var) {
    CADICAL_assert (e2i.empty ());
    e2i.push_back (0);
    ext_units.push_back (0);
    ext_units.push_back (0);
    ext_flags.push_back (0);
    ervars.push_back (0);
    CADICAL_assert (internal->i2e.empty ());
    internal->i2e.push_back (0);
  } else {
    CADICAL_assert (e2i.size () == (size_t) max_var + 1);
    CADICAL_assert (internal->i2e.size () == (size_t) old_internal_max_var + 1);
  }
  unsigned iidx = old_internal_max_var + 1, eidx;
  for (eidx = max_var + 1u; eidx <= (unsigned) new_max_var;
       eidx++, iidx++) {
    LOG ("mapping external %u to internal %u", eidx, iidx);
    CADICAL_assert (e2i.size () == eidx);
    e2i.push_back (iidx);
    ext_units.push_back (0);
    ext_units.push_back (0);
    ext_flags.push_back (0);
    ervars.push_back (0);
    internal->i2e.push_back (eidx);
    CADICAL_assert (internal->i2e[iidx] == (int) eidx);
    CADICAL_assert (e2i[eidx] == (int) iidx);
  }
  if (extension)
    internal->stats.variables_extension += new_vars;
  else
    internal->stats.variables_original += new_vars;
  if (new_max_var >= (int64_t) is_observed.size ())
    is_observed.resize (1 + (size_t) new_max_var, false);
  if (internal->opts.checkfrozen)
    if (new_max_var >= (int64_t) moltentab.size ())
      moltentab.resize (1 + (size_t) new_max_var, false);
  CADICAL_assert (iidx == (size_t) new_internal_max_var + 1);
  CADICAL_assert (eidx == (size_t) new_max_var + 1);
  CADICAL_assert (ext_units.size () == (size_t) new_max_var * 2 + 2);
  max_var = new_max_var;
}

Here is the call graph for this function:

Here is the caller graph for this function:

internalize()

int CaDiCaL::External::internalize	(	int	elit,
		bool	extension = false )

Definition at line 120 of file cadical_external.cpp.

                                                   {
  int ilit;
  if (elit) {
    CADICAL_assert (elit != INT_MIN);
    const int eidx = abs (elit);
    if (extension && eidx <= max_var)
      FATAL ("can not add a definition for an already used variable %d",
             eidx);
    if (eidx > max_var) {
      init (eidx, extension);
    }
    if (extension) {
      CADICAL_assert (ervars.size () > (size_t) eidx);
      ervars[eidx] = true;
    }
    ilit = e2i[eidx];
    if (elit < 0)
      ilit = -ilit;
    if (!ilit) {
      CADICAL_assert (internal->max_var < INT_MAX);
      ilit = internal->max_var + 1u;
      internal->init_vars (ilit);
      e2i[eidx] = ilit;
      LOG ("mapping external %d to internal %d", eidx, ilit);
      e2i[eidx] = ilit;
      internal->i2e.push_back (eidx);
      CADICAL_assert (internal->i2e[ilit] == eidx);
      CADICAL_assert (e2i[eidx] == ilit);
      if (elit < 0)
        ilit = -ilit;
    }
    if (internal->opts.checkfrozen) {
      CADICAL_assert (eidx < (int64_t) moltentab.size ());
      if (moltentab[eidx])
        FATAL ("can not reuse molten literal %d", eidx);
    }
    Flags &f = internal->flags (ilit);
    if (f.status == Flags::UNUSED)
      internal->mark_active (ilit);
    else if (f.status != Flags::ACTIVE && f.status != Flags::FIXED)
      internal->reactivate (ilit);
    if (!marked (tainted, elit) && marked (witness, -elit)) {
      CADICAL_assert (!internal->opts.checkfrozen);
      LOG ("marking tainted %d", elit);
      mark (tainted, elit);
    }
  } else
    ilit = 0;
  return ilit;
}

Here is the call graph for this function:

Here is the caller graph for this function:

is_decision()

bool CaDiCaL::External::is_decision

(

int

elit

)

Definition at line 477 of file cadical_external.cpp.

                                    {
  CADICAL_assert (elit);
  CADICAL_assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var)
    return false;
 
  int ilit = internalize (elit);
  return internal->is_decision (ilit);
}

Here is the call graph for this function:

is_valid_input()

bool CaDiCaL::External::is_valid_input ( int elit )

inline

Definition at line 170 of file external.hpp.

                                        {
    CADICAL_assert (elit);
    CADICAL_assert (elit != INT_MIN);
    int eidx = abs (elit);
    return eidx > max_var || !ervars[eidx];
  }

is_witness()

bool CaDiCaL::External::is_witness

(

int

elit

)

Definition at line 468 of file cadical_external.cpp.

                                   {
  CADICAL_assert (elit);
  CADICAL_assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var)
    return false;
  return (marked (witness, elit) || marked (witness, -elit));
}

Here is the call graph for this function:

ival()

int CaDiCaL::External::ival ( int elit ) const

inline

Definition at line 325 of file external.hpp.

                                   {
    CADICAL_assert (elit != INT_MIN);
    int eidx = abs (elit);
    bool val = false;
    if (eidx <= max_var && (size_t) eidx < vals.size ())
      val = vals[eidx];
    if (elit < 0)
      val = !val;
    return val ? elit : -elit;
  }

Here is the caller graph for this function:

lookahead()

int CaDiCaL::External::lookahead

(

)

Definition at line 621 of file cadical_external.cpp.

                         {
  reset_extended ();
  update_molten_literals ();
  int ilit = internal->lookahead ();
  const int elit =
      (ilit && ilit != INT_MIN) ? internal->externalize (ilit) : 0;
  LOG ("lookahead internal %d external %d", ilit, elit);
  return elit;
}

Here is the call graph for this function:

mark()

void CaDiCaL::External::mark ( vector< bool > & map, int elit )

inline

Definition at line 221 of file external.hpp.

                                          {
    const unsigned ulit = elit2ulit (elit);
    if (ulit >= map.size ())
      map.resize (ulit + 1, false);
    map[ulit] = true;
  }

Here is the call graph for this function:

marked()

bool CaDiCaL::External::marked ( const vector< bool > & map, int elit ) const

inline

Definition at line 216 of file external.hpp.

                                                        {
    const unsigned ulit = elit2ulit (elit);
    return ulit < map.size () ? map[ulit] : false;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

melt()

void CaDiCaL::External::melt

(

int

elit

)

Definition at line 670 of file cadical_external.cpp.

                             {
  reset_extended ();
  int ilit = internalize (elit);
  unsigned eidx = vidx (elit);
  CADICAL_assert (eidx < frozentab.size ());
  unsigned &ref = frozentab[eidx];
  CADICAL_assert (ref > 0);
  if (ref < UINT_MAX) {
    if (!--ref) {
      if (observed (elit)) {
        ref++;
        LOG ("external variable %d is observed, can not be completely "
             "molten",
             eidx);
      } else
        LOG ("external variable %d melted once and now completely melted",
             eidx);
    } else
      LOG ("external variable %d melted once but remains frozen %u times",
           eidx, ref);
  } else
    LOG ("external variable %d melted but remains frozen forever", eidx);
  internal->melt (ilit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

observed()

bool CaDiCaL::External::observed

(

int

elit

)

Definition at line 456 of file cadical_external.cpp.

                                 {
  CADICAL_assert (elit);
  CADICAL_assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var)
    return false;
  if (eidx >= (int) is_observed.size ())
    return false;
 
  return is_observed[eidx];
}

Here is the caller graph for this function:

phase()

void CaDiCaL::External::phase

(

int

elit

)

Definition at line 310 of file cadical_external.cpp.

                              {
  CADICAL_assert (elit);
  CADICAL_assert (elit != INT_MIN);
  const int ilit = internalize (elit);
  internal->phase (ilit);
}

Here is the call graph for this function:

propagate_assumptions()

int CaDiCaL::External::propagate_assumptions

(

)

Definition at line 499 of file cadical_external.cpp.

                                     {
  int res = internal->propagate_assumptions ();
  if (res == 10 && !extended)
    extend (); // Call solution reconstruction
  check_solve_result (res);
  reset_limits ();
  return res;
}

Here is the call graph for this function:

push_binary_clause_on_extension_stack()

void CaDiCaL::External::push_binary_clause_on_extension_stack	(	int64_t	id,
		int	witness,
		int	other )

Definition at line 67 of file cadical_extend.cpp.

                                                                 {
  internal->stats.weakened++;
  internal->stats.weakenedlen += 2;
  push_zero_on_extension_stack ();
  push_witness_literal_on_extension_stack (pivot);
  push_zero_on_extension_stack ();
  push_id_on_extension_stack (id);
  push_zero_on_extension_stack ();
  push_clause_literal_on_extension_stack (pivot);
  push_clause_literal_on_extension_stack (other);
}

Here is the call graph for this function:

push_clause_literal_on_extension_stack()

void CaDiCaL::External::push_clause_literal_on_extension_stack

(

int

ilit

)

Definition at line 22 of file cadical_extend.cpp.

                                                               {
  CADICAL_assert (ilit);
  const int elit = internal->externalize (ilit);
  CADICAL_assert (elit);
  extension.push_back (elit);
  LOG ("pushing clause literal %d on extension stack (internal %d)", elit,
       ilit);
}

Here is the caller graph for this function:

push_clause_on_extension_stack() [1/2]

void CaDiCaL::External::push_clause_on_extension_stack

(

Clause *

c

)

Definition at line 51 of file cadical_extend.cpp.

                                                        {
  internal->stats.weakened++;
  internal->stats.weakenedlen += c->size;
  push_zero_on_extension_stack ();
  push_id_on_extension_stack (c->id);
  push_zero_on_extension_stack ();
  for (const auto &lit : *c)
    push_clause_literal_on_extension_stack (lit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

push_clause_on_extension_stack() [2/2]

void CaDiCaL::External::push_clause_on_extension_stack	(	Clause *	c,
		int	witness )

Definition at line 61 of file cadical_extend.cpp.

                                                                   {
  push_zero_on_extension_stack ();
  push_witness_literal_on_extension_stack (pivot);
  push_clause_on_extension_stack (c);
}

Here is the call graph for this function:

push_external_clause_and_witness_on_extension_stack()

void CaDiCaL::External::push_external_clause_and_witness_on_extension_stack	(	const vector< int > &	clause,
		const vector< int > &	witness,
		int64_t	id )

Definition at line 82 of file cadical_extend.cpp.

                                                            {
  CADICAL_assert (id);
  extension.push_back (0);
  for (const auto &elit : w) {
    CADICAL_assert (elit != INT_MIN);
    init (abs (elit));
    extension.push_back (elit);
    mark (witness, elit);
  }
  extension.push_back (0);
  const uint32_t higher_bits = static_cast<int> (id << 32);
  const uint32_t lower_bits = (id & (((int64_t) 1 << 32) - 1));
  extension.push_back (higher_bits);
  extension.push_back (lower_bits);
  extension.push_back (0);
  for (const auto &elit : c) {
    CADICAL_assert (elit != INT_MIN);
    init (abs (elit));
    extension.push_back (elit);
  }
}

Here is the call graph for this function:

push_id_on_extension_stack()

void CaDiCaL::External::push_id_on_extension_stack

(

int64_t

id

)

Definition at line 14 of file cadical_extend.cpp.

                                                     {
  const uint32_t higher_bits = static_cast<int> (id << 32);
  const uint32_t lower_bits = (id & (((int64_t) 1 << 32) - 1));
  extension.push_back (higher_bits);
  extension.push_back (lower_bits);
  LOG ("pushing id %" PRIu64 " = %d + %d", id, higher_bits, lower_bits);
}

Here is the caller graph for this function:

push_witness_literal_on_extension_stack()

void CaDiCaL::External::push_witness_literal_on_extension_stack

(

int

ilit

)

Definition at line 31 of file cadical_extend.cpp.

                                                                {
  CADICAL_assert (ilit);
  const int elit = internal->externalize (ilit);
  CADICAL_assert (elit);
  extension.push_back (elit);
  LOG ("pushing witness literal %d on extension stack (internal %d)", elit,
       ilit);
  if (marked (witness, elit))
    return;
  LOG ("marking witness %d", elit);
  mark (witness, elit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

push_zero_on_extension_stack()

void CaDiCaL::External::push_zero_on_extension_stack

(

)

Definition at line 9 of file cadical_extend.cpp.

                                             {
  extension.push_back (0);
  LOG ("pushing 0 on extension stack");
}

Here is the caller graph for this function:

remove_observed_var()

void CaDiCaL::External::remove_observed_var

(

int

elit

)

Definition at line 408 of file cadical_external.cpp.

                                            {
  if (!propagator) {
    LOG ("No connected propagator that could have watched the variable");
    return;
  }
  int eidx = abs (elit);
 
  if (eidx > max_var)
    return;
 
  if (is_observed[eidx]) {
    // Follow opposite order of add_observed_var, first remove internal
    // is_observed
    int ilit = e2i[eidx]; // internalize (elit);
    internal->remove_observed_var (ilit);
 
    is_observed[eidx] = false;
    melt (elit);
    LOG ("unmarking %d as externally watched", eidx);
  }
}

Here is the call graph for this function:

reset_assumptions()

void CaDiCaL::External::reset_assumptions

(

)

Definition at line 90 of file cadical_external.cpp.

                                  {
  assumptions.clear ();
  internal->reset_assumptions ();
}

reset_concluded()

void CaDiCaL::External::reset_concluded

(

)

Definition at line 95 of file cadical_external.cpp.

                                {
  concluded = false;
  internal->reset_concluded ();
}

reset_constraint()

void CaDiCaL::External::reset_constraint

(

)

Definition at line 100 of file cadical_external.cpp.

                                 {
  constraint.clear ();
  internal->reset_constraint ();
}

Here is the caller graph for this function:

reset_extended()

void CaDiCaL::External::reset_extended

(

)

Definition at line 105 of file cadical_external.cpp.

                               {
  if (!extended)
    return;
  LOG ("reset extended");
  extended = false;
}

Here is the caller graph for this function:

reset_limits()

void CaDiCaL::External::reset_limits

(

)

Definition at line 112 of file cadical_external.cpp.

{ internal->reset_limits (); }

Here is the caller graph for this function:

reset_observed_vars()

void CaDiCaL::External::reset_observed_vars

(

)

Definition at line 430 of file cadical_external.cpp.

                                    {
  // Shouldn't be called if there is no connected propagator
  CADICAL_assert (propagator);
  reset_extended ();
 
  internal->notified = 0;
  LOG ("reset notified counter to 0");
 
  if (!is_observed.size ())
    return;
 
  CADICAL_assert (!max_var || (size_t) max_var + 1 == is_observed.size ());
 
  for (auto elit : vars) {
    int eidx = abs (elit);
    CADICAL_assert (eidx <= max_var);
    if (is_observed[eidx]) {
      int ilit = internalize (elit);
      internal->remove_observed_var (ilit);
      LOG ("unmarking %d as externally watched", eidx);
      is_observed[eidx] = false;
      melt (elit);
    }
  }
}

Here is the call graph for this function:

restore_clause()

void CaDiCaL::External::restore_clause	(	const vector< int >::const_iterator &	begin,
		const vector< int >::const_iterator &	end,
		const int64_t	id )

Definition at line 54 of file cadical_restore.cpp.

                                                 {
  LOG (begin, end, "restoring external clause[%" PRId64 "]", id);
  CADICAL_assert (eclause.empty ());
  CADICAL_assert (id);
  for (auto p = begin; p != end; p++) {
    eclause.push_back (*p);
    if (internal->proof && internal->lrat) {
      const auto &elit = *p;
      unsigned eidx = (elit > 0) + 2u * (unsigned) abs (elit);
      CADICAL_assert ((size_t) eidx < ext_units.size ());
      const int64_t id = ext_units[eidx];
      bool added = ext_flags[abs (elit)];
      if (id && !added) {
        ext_flags[abs (elit)] = true;
        internal->lrat_chain.push_back (id);
      }
    }
    int ilit = internalize (*p);
    internal->add_original_lit (ilit), internal->stats.restoredlits++;
  }
  if (internal->proof && internal->lrat) {
    for (const auto &elit : eclause) {
      ext_flags[abs (elit)] = false;
    }
  }
  internal->finish_added_clause_with_id (id, true);
  eclause.clear ();
  internal->stats.restored++;
}

Here is the call graph for this function:

Here is the caller graph for this function:

restore_clauses()

void CaDiCaL::External::restore_clauses

(

)

Definition at line 88 of file cadical_restore.cpp.

                                {
 
  CADICAL_assert (internal->opts.restoreall == 2 || !tainted.empty ());
 
  START (restore);
  internal->stats.restorations++;
 
  struct {
    int64_t weakened, satisfied, restored, removed;
  } clauses;
  memset (&clauses, 0, sizeof clauses);
 
  if (internal->opts.restoreall && tainted.empty ())
    PHASE ("restore", internal->stats.restorations,
           "forced to restore all clauses");
 
#ifndef CADICAL_QUIET
  {
    unsigned numtainted = 0;
    for (const auto b : tainted)
      if (b)
        numtainted++;
 
    PHASE ("restore", internal->stats.restorations,
           "starting with %u tainted literals %.0f%%", numtainted,
           percent (numtainted, 2u * max_var));
  }
#endif
 
  auto end_of_extension = extension.end ();
  auto p = extension.begin (), q = p;
 
  // Go over all witness labelled clauses on the extension stack, restore
  // those necessary, remove restored and flush satisfied clauses.
  //
  while (p != end_of_extension) {
 
    clauses.weakened++;
 
    CADICAL_assert (!*p);
    const auto saved = q; // Save old start.
    *q++ = *p++;          // Copy zero '0'.
 
    // Copy witness part and try to find a tainted witness literal in it.
    //
    int tlit = 0; // Negation tainted.
    int elit;
    //
    CADICAL_assert (p != end_of_extension);
    //
    while ((elit = *q++ = *p++)) {
 
      if (marked (tainted, -elit)) {
        tlit = elit;
        LOG ("negation of witness literal %d tainted", tlit);
      }
 
      CADICAL_assert (p != end_of_extension);
    }
 
    // now copy the id of the clause
    const int64_t id = ((int64_t) (*p) << 32) + (int64_t) * (p + 1);
    LOG ("id is %" PRId64, id);
    *q++ = *p++;
    *q++ = *p++;
    CADICAL_assert (id);
    CADICAL_assert (!*p);
    *q++ = *p++;
 
    // Now find 'end_of_clause' (clause starts at 'p') and at the same time
    // figure out whether the clause is actually root level satisfied.
    //
    int satisfied = 0;
    auto end_of_clause = p;
    while (end_of_clause != end_of_extension && (elit = *end_of_clause)) {
      if (!satisfied && fixed (elit) > 0)
        satisfied = elit;
      end_of_clause++;
    }
    CADICAL_assert (id);
 
    // Do not apply our 'FLUSH' rule to remove satisfied (implied) clauses
    // if the corresponding option is set simply by resetting 'satisfied'.
    //
    if (satisfied && !internal->opts.restoreflush) {
      LOG (p, end_of_clause, "forced to not remove %d satisfied",
           satisfied);
      satisfied = 0;
    }
 
    if (satisfied || tlit || internal->opts.restoreall) {
 
      if (satisfied) {
        LOG (p, end_of_clause,
             "flushing implied clause satisfied by %d from extension stack",
             satisfied);
        clauses.satisfied++;
      } else {
        restore_clause (p, end_of_clause, id); // Might taint literals.
        clauses.restored++;
      }
 
      clauses.removed++;
      p = end_of_clause;
      q = saved;
 
    } else {
 
      LOG (p, end_of_clause, "keeping clause on extension stack");
 
      while (p != end_of_clause) // Copy clause too.
        *q++ = *p++;
    }
  }
 
  extension.resize (q - extension.begin ());
  shrink_vector (extension);
 
#ifndef CADICAL_QUIET
  if (clauses.satisfied)
    PHASE ("restore", internal->stats.restorations,
           "removed %" PRId64 " satisfied %.0f%% of %" PRId64
           " weakened clauses",
           clauses.satisfied, percent (clauses.satisfied, clauses.weakened),
           clauses.weakened);
  else
    PHASE ("restore", internal->stats.restorations,
           "no satisfied clause removed out of %" PRId64
           " weakened clauses",
           clauses.weakened);
 
  if (clauses.restored)
    PHASE ("restore", internal->stats.restorations,
           "restored %" PRId64 " clauses %.0f%% out of %" PRId64
           " weakened clauses",
           clauses.restored, percent (clauses.restored, clauses.weakened),
           clauses.weakened);
  else
    PHASE ("restore", internal->stats.restorations,
           "no clause restored out of %" PRId64 " weakened clauses",
           clauses.weakened);
  {
    unsigned numtainted = 0;
    for (const auto &b : tainted)
      if (b)
        numtainted++;
 
    PHASE ("restore", internal->stats.restorations,
           "finishing with %u tainted literals %.0f%%", numtainted,
           percent (numtainted, 2u * max_var));
  }
 
#endif
  LOG ("extension stack clean");
  tainted.clear ();
 
  // Finally recompute the witness bits.
  //
  witness.clear ();
  const auto begin_of_extension = extension.begin ();
  p = extension.end ();
  while (p != begin_of_extension) {
    while (*--p)
      CADICAL_assert (p != begin_of_extension);
    int elit;
    CADICAL_assert (p != begin_of_extension);
    --p;
    CADICAL_assert (p != begin_of_extension);
    CADICAL_assert (*p || *(p - 1));
    --p;
    CADICAL_assert (p != begin_of_extension);
    CADICAL_assert (!*p);
    --p;
    CADICAL_assert (p != begin_of_extension);
    while ((elit = *--p)) {
      mark (witness, elit);
      CADICAL_assert (p != begin_of_extension);
    }
  }
 
  STOP (restore);
}

Here is the call graph for this function:

sol()

int CaDiCaL::External::sol ( int elit ) const

inline

Definition at line 446 of file external.hpp.

                                  {
    CADICAL_assert (solution);
    CADICAL_assert (elit != INT_MIN);
    int eidx = abs (elit);
    if (eidx > max_var)
      return 0;
    else if (eidx > solution_size)
      return elit;
    signed char value = solution[eidx];
    if (!value)
      return 0;
    if (elit < 0)
      value = -value;
    return value > 0 ? elit : -elit;
  }

Here is the caller graph for this function:

solve()

int CaDiCaL::External::solve

(

bool

preprocess_only

)

Definition at line 610 of file cadical_external.cpp.

                                         {
  reset_extended ();
  update_molten_literals ();
  int res = internal->solve (preprocess_only);
  check_solve_result (res);
  reset_limits ();
  return res;
}

Here is the call graph for this function:

terminate()

void CaDiCaL::External::terminate

(

)

Definition at line 619 of file cadical_external.cpp.

{ internal->terminate (); }

traverse_all_frozen_units_as_clauses()

bool CaDiCaL::External::traverse_all_frozen_units_as_clauses

(

ClauseIterator &

it

)

Definition at line 914 of file cadical_external.cpp.

                                                                       {
  if (internal->unsat)
    return true;
 
  vector<int> clause;
 
  for (auto idx : vars) {
    if (!frozen (idx))
      continue;
    const int tmp = fixed (idx);
    if (!tmp)
      continue;
    int unit = tmp < 0 ? -idx : idx;
    clause.push_back (unit);
    if (!it.clause (clause))
      return false;
    clause.clear ();
  }
 
  return true;
}

Here is the call graph for this function:

traverse_all_non_frozen_units_as_witnesses()

bool CaDiCaL::External::traverse_all_non_frozen_units_as_witnesses

(

WitnessIterator &

it

)

Definition at line 936 of file cadical_external.cpp.

                         {
  if (internal->unsat)
    return true;
 
  vector<int> clause_and_witness;
  for (auto idx : vars) {
    if (frozen (idx))
      continue;
    const int tmp = fixed (idx);
    if (!tmp)
      continue;
    int unit = tmp < 0 ? -idx : idx;
    const int ilit = e2i[idx] * (tmp < 0 ? -1 : 1);
    // heurstically add + max_var to the id to avoid reusing ids
    const int64_t id = internal->lrat ? internal->unit_id (ilit) : 1;
    CADICAL_assert (id);
    clause_and_witness.push_back (unit);
    if (!it.witness (clause_and_witness, clause_and_witness, id + max_var))
      return false;
    clause_and_witness.clear ();
  }
 
  return true;
}

Here is the call graph for this function:

traverse_witnesses_backward()

bool CaDiCaL::External::traverse_witnesses_backward

(

WitnessIterator &

it

)

Definition at line 204 of file cadical_extend.cpp.

                                                               {
  if (internal->unsat)
    return true;
  vector<int> clause, witness;
  const auto begin = extension.begin ();
  auto i = extension.end ();
  while (i != begin) {
    int lit;
    while ((lit = *--i))
      clause.push_back (lit);
    CADICAL_assert (!lit);
    --i;
    const int64_t id =
        ((int64_t) * (i - 1) << 32) + static_cast<int64_t> (*i);
    CADICAL_assert (id);
    i -= 2;
    CADICAL_assert (!*i);
    CADICAL_assert (i != begin);
    while ((lit = *--i))
      witness.push_back (lit);
    reverse (clause.begin (), clause.end ());
    reverse (witness.begin (), witness.end ());
    LOG (clause, "traversing clause");
    if (!it.witness (clause, witness, id))
      return false;
    clause.clear ();
    witness.clear ();
  }
  return true;
}

Here is the call graph for this function:

traverse_witnesses_forward()

bool CaDiCaL::External::traverse_witnesses_forward

(

WitnessIterator &

it

)

Definition at line 235 of file cadical_extend.cpp.

                                                              {
  if (internal->unsat)
    return true;
  vector<int> clause, witness;
  const auto end = extension.end ();
  auto i = extension.begin ();
  if (i != end) {
    int lit = *i++;
    do {
      CADICAL_assert (!lit), (void) lit;
      while ((lit = *i++))
        witness.push_back (lit);
      CADICAL_assert (!lit);
      CADICAL_assert (i != end);
      CADICAL_assert (!*i);
      const int64_t id =
          ((int64_t) *i << 32) + static_cast<int64_t> (*(i + 1));
      CADICAL_assert (id > 0);
      i += 3;
      CADICAL_assert (*i);
      CADICAL_assert (i != end);
      while (i != end && (lit = *i++))
        clause.push_back (lit);
      if (!it.witness (clause, witness, id))
        return false;
      clause.clear ();
      witness.clear ();
    } while (i != end);
  }
  return true;
}

Here is the call graph for this function:

unmark()

void CaDiCaL::External::unmark ( vector< bool > & map, int elit )

inline

Definition at line 228 of file external.hpp.

                                            {
    const unsigned ulit = elit2ulit (elit);
    if (ulit < map.size ())
      map[ulit] = false;
  }

Here is the call graph for this function:

unphase()

void CaDiCaL::External::unphase

(

int

elit

)

Definition at line 317 of file cadical_external.cpp.

                                {
  CADICAL_assert (elit);
  CADICAL_assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var) {
  UNUSED:
    LOG ("resetting forced phase of unused external %d ignored", elit);
    return;
  }
  int ilit = e2i[eidx];
  if (!ilit)
    goto UNUSED;
  if (elit < 0)
    ilit = -ilit;
  internal->unphase (ilit);
}

update_molten_literals()

void CaDiCaL::External::update_molten_literals

(

)

Definition at line 582 of file cadical_external.cpp.

                                       {
  if (!internal->opts.checkfrozen)
    return;
  CADICAL_assert ((size_t) max_var + 1 == moltentab.size ());
#ifdef LOGGING
  int registered = 0, molten = 0;
#endif
  for (auto lit : vars) {
    if (moltentab[lit]) {
      LOG ("skipping already molten literal %d", lit);
#ifdef LOGGING
      molten++;
#endif
    } else if (frozen (lit))
      LOG ("skipping currently frozen literal %d", lit);
    else {
      LOG ("new molten literal %d", lit);
      moltentab[lit] = true;
#ifdef LOGGING
      registered++;
      molten++;
#endif
    }
  }
  LOG ("registered %d new molten literals", registered);
  LOG ("reached in total %d molten literals", molten);
}

Here is the call graph for this function:

Here is the caller graph for this function:

vidx()

int CaDiCaL::External::vidx ( int elit ) const

inline

Definition at line 155 of file external.hpp.

                                   {
    CADICAL_assert (elit);
    CADICAL_assert (elit != INT_MIN);
    int res = abs (elit);
    CADICAL_assert (res <= max_var);
    return res;
  }

Here is the caller graph for this function:

vlit()

int CaDiCaL::External::vlit ( int elit ) const

inline

Definition at line 163 of file external.hpp.

                                   {
    CADICAL_assert (elit);
    CADICAL_assert (elit != INT_MIN);
    CADICAL_assert (abs (elit) <= max_var);
    return elit;
  }

Member Data Documentation

assumptions

vector<int> CaDiCaL::External::assumptions

Definition at line 69 of file external.hpp.

concluded

bool CaDiCaL::External::concluded

Definition at line 84 of file external.hpp.

constraint

vector<int> CaDiCaL::External::constraint

Definition at line 70 of file external.hpp.

e2i

vector<int> CaDiCaL::External::e2i

Definition at line 67 of file external.hpp.

eclause

vector<int> CaDiCaL::External::eclause

Definition at line 75 of file external.hpp.

ervars

vector<bool> CaDiCaL::External::ervars

Definition at line 90 of file external.hpp.

ext_flags

vector<bool> CaDiCaL::External::ext_flags

Definition at line 74 of file external.hpp.

ext_units

vector<int64_t> CaDiCaL::External::ext_units

Definition at line 73 of file external.hpp.

extended

bool CaDiCaL::External::extended

Definition at line 83 of file external.hpp.

extension

vector<int> CaDiCaL::External::extension

Definition at line 85 of file external.hpp.

fixed_listener

FixedAssignmentListener* CaDiCaL::External::fixed_listener

Definition at line 109 of file external.hpp.

forgettable_original

unordered_map<uint64_t, vector<int> > CaDiCaL::External::forgettable_original

Definition at line 121 of file external.hpp.

frozentab

vector<unsigned> CaDiCaL::External::frozentab

Definition at line 92 of file external.hpp.

internal

Internal* CaDiCaL::External::internal

Definition at line 61 of file external.hpp.

is_observed

vector<bool> CaDiCaL::External::is_observed

Definition at line 115 of file external.hpp.

learner

Learner* CaDiCaL::External::learner

Definition at line 101 of file external.hpp.

max_var

int CaDiCaL::External::max_var

Definition at line 63 of file external.hpp.

moltentab

vector<bool> CaDiCaL::External::moltentab

Definition at line 145 of file external.hpp.

original

vector<int> CaDiCaL::External::original

Definition at line 137 of file external.hpp.

propagator

ExternalPropagator* CaDiCaL::External::propagator

Definition at line 113 of file external.hpp.

solution

signed char* CaDiCaL::External::solution

Definition at line 135 of file external.hpp.

solution_size

int CaDiCaL::External::solution_size

Definition at line 136 of file external.hpp.

tainted

vector<bool> CaDiCaL::External::tainted

Definition at line 88 of file external.hpp.

terminator

Terminator* CaDiCaL::External::terminator

Definition at line 97 of file external.hpp.

vals

vector<bool> CaDiCaL::External::vals

Definition at line 66 of file external.hpp.

vars

const Range CaDiCaL::External::vars

Definition at line 149 of file external.hpp.

vsize

size_t CaDiCaL::External::vsize

Definition at line 64 of file external.hpp.

witness

vector<bool> CaDiCaL::External::witness

Definition at line 87 of file external.hpp.

---

The documentation for this struct was generated from the following files:

• src/sat/cadical/external.hpp
• src/sat/cadical/cadical_extend.cpp
• src/sat/cadical/cadical_external.cpp
• src/sat/cadical/cadical_restore.cpp
• src/sat/cadical/cadical_solution.cpp
• src/sat/cadical/internal.hpp