CaDiCaL::Solver Class Reference

#include <cadical.hpp>

Classes
struct	CubesWithStatus

Public Member Functions
	Solver ()
	~Solver ()
void	add (int lit)
void	clause (int)
void	clause (int, int)
void	clause (int, int, int)
void	clause (int, int, int, int)
void	clause (int, int, int, int, int)
void	clause (const std::vector< int > &)
void	clause (const int *, size_t)
bool	inconsistent ()
void	assume (int lit)
int	solve ()
int	val (int lit)
bool	flip (int lit)
bool	flippable (int lit)
bool	failed (int lit)
void	connect_terminator (Terminator *terminator)
void	disconnect_terminator ()
void	connect_learner (Learner *learner)
void	disconnect_learner ()
void	connect_fixed_listener (FixedAssignmentListener *fixed_listener)
void	disconnect_fixed_listener ()
void	connect_external_propagator (ExternalPropagator *propagator)
void	disconnect_external_propagator ()
void	add_observed_var (int var)
void	remove_observed_var (int var)
void	reset_observed_vars ()
bool	is_decision (int lit)
void	force_backtrack (size_t new_level)
void	constrain (int lit)
bool	constraint_failed ()
int	propagate ()
void	implied (std::vector< int > &implicants)
int	lookahead (void)
CubesWithStatus	generate_cubes (int, int min_depth=0)
void	reset_assumptions ()
void	reset_constraint ()
const State &	state () const
int	status () const
void	copy (Solver &other) const
int	vars ()
void	reserve (int min_max_var)
int	reserve_difference (int number_of_vars)
int	get (const char *name)
void	prefix (const char *verbose_message_prefix)
bool	set (const char *name, int val)
bool	set_long_option (const char *arg)
bool	configure (const char *)
void	optimize (int val)
bool	limit (const char *arg, int val)
bool	is_valid_limit (const char *arg)
int	active () const
int64_t	redundant () const
int64_t	irredundant () const
int	simplify (int rounds=3)
void	terminate ()
bool	frozen (int lit) const
void	freeze (int lit)
void	melt (int lit)
int	fixed (int lit) const
void	phase (int lit)
void	unphase (int lit)
bool	trace_proof (FILE *file, const char *name)
bool	trace_proof (const char *path)
void	flush_proof_trace (bool print=false)
void	close_proof_trace (bool print=false)
void	connect_proof_tracer (Tracer *tracer, bool antecedents, bool finalize_clauses=false)
void	connect_proof_tracer (InternalTracer *tracer, bool antecedents, bool finalize_clauses=false)
void	connect_proof_tracer (StatTracer *tracer, bool antecedents, bool finalize_clauses=false)
void	connect_proof_tracer (FileTracer *tracer, bool antecedents, bool finalize_clauses=false)
void	conclude ()
bool	disconnect_proof_tracer (Tracer *tracer)
bool	disconnect_proof_tracer (StatTracer *tracer)
bool	disconnect_proof_tracer (FileTracer *tracer)
void	statistics ()
void	resources ()
void	options ()
bool	traverse_clauses (ClauseIterator &) const
bool	traverse_witnesses_backward (WitnessIterator &) const
bool	traverse_witnesses_forward (WitnessIterator &) const
const char *	read_dimacs (FILE *file, const char *name, int &vars, int strict=1)
const char *	read_dimacs (const char *path, int &vars, int strict=1)
const char *	read_dimacs (FILE *file, const char *name, int &vars, int strict, bool &incremental, std::vector< int > &cubes)
const char *	read_dimacs (const char *path, int &vars, int strict, bool &incremental, std::vector< int > &cubes)
const char *	write_dimacs (const char *path, int min_max_var=0)
const char *	write_extension (const char *path)

Static Public Member Functions
static const char *	signature ()
static const char *	version ()
static bool	is_valid_option (const char *name)
static bool	is_preprocessing_option (const char *name)
static bool	is_valid_long_option (const char *arg)
static bool	is_valid_configuration (const char *)
static void	usage ()
static void	configurations ()
static void	build (FILE *file, const char *prefix="c ")

Friends
class	Testing
class	App
class	Mobical
class	Parser
struct	DumpCall
struct	LemmaCall
struct	ObserveCall
struct	DisconnectCall
class	MockPropagator

Detailed Description

Definition at line 230 of file cadical.hpp.

Constructor & Destructor Documentation

Solver()

CaDiCaL::Solver::Solver

(

)

Definition at line 326 of file cadical_solver.cpp.

                {
 
#ifndef CADICAL_NTRACING
  const char *path = getenv ("CADICAL_API_TRACE");
  if (!path)
    path = getenv ("CADICALAPITRACE");
  if (path) {
    if (tracing_api_calls_through_environment_variable_method)
      FATAL ("can not trace API calls of two solver instances "
             "using environment variable 'CADICAL_API_TRACE'");
    if (!(trace_api_file = fopen (path, "w")))
      FATAL ("failed to open file '%s' to trace API calls "
             "using environment variable 'CADICAL_API_TRACE'",
             path);
    close_trace_api_file = true;
    tracing_api_calls_through_environment_variable_method = true;
  } else {
    tracing_api_calls_through_environment_variable_method = false;
    close_trace_api_file = false;
    trace_api_file = 0;
  }
#endif
 
  adding_clause = false;
  adding_constraint = false;
  _state = INITIALIZING;
  internal = new Internal ();
  DeferDeletePtr<Internal> delete_internal (internal);
  TRACE ("init");
  external = new External (internal);
  DeferDeletePtr<External> delete_external (external);
  STATE (CONFIGURING);
#ifndef CADICAL_NTRACING
  if (tracing_api_calls_through_environment_variable_method)
    message ("tracing API calls to '%s'", path);
#endif
 
  const char *lidrup_path = getenv ("CADICAL_LIDRUP_TRACE");
  if (!lidrup_path)
    lidrup_path = getenv ("CADICALLIDRUPTRACE");
  if (lidrup_path) {
 
    // if (tracing_nb_lidrup_env_var_method)
    // FATAL ("can not trace LIDRUP of two solver instances "
    //   "using environment variable 'CADICAL_LIDRUP_TRACE'");
    // Here we use the solver interface to setup non-binary IDRUP tracing to
    // the defined file. Options set by the user can and will overwrite
    // these settings if neeed be.
    set ("lidrup", 1);
    set ("binary", 0);
    trace_proof (lidrup_path);
    tracing_nb_lidrup_env_var_method = true;
  } else {
    tracing_nb_lidrup_env_var_method = false;
  }
 
  delete_internal.release ();
  delete_external.release ();
}

Here is the call graph for this function:

Here is the caller graph for this function:

~Solver()

CaDiCaL::Solver::~Solver

(

)

Definition at line 386 of file cadical_solver.cpp.

                 {
 
  TRACE ("reset");
  REQUIRE_VALID_OR_SOLVING_STATE ();
  STATE (DELETING);
 
  tracing_nb_lidrup_env_var_method = false;
 
#ifdef LOGGING
  //
  // After deleting 'internal' logging does not work anymore.
  //
  bool logging = internal->opts.log;
  int level = internal->level;
  string prefix = internal->prefix;
#endif
 
  delete internal;
  delete external;
 
#ifndef CADICAL_NTRACING
  if (close_trace_api_file) {
    close_trace_api_file = false;
    CADICAL_assert (trace_api_file);
    CADICAL_assert (tracing_api_calls_through_environment_variable_method);
    fclose (trace_api_file);
    tracing_api_calls_through_environment_variable_method = false;
  }
#endif
 
#ifdef LOGGING
  //
  // Need to log success of this API call manually.
  //
  if (logging) {
    printf ("%s%sLOG %s%d%s API call %s'reset ()'%s succeeded%s\n",
            prefix.c_str (), tout.log_code (), tout.emph_code (), level,
            tout.log_code (), tout.api_code (), tout.log_code (),
            tout.normal_code ());
    fflush (stdout);
  }
#endif
}

Here is the call graph for this function:

Member Function Documentation

active()

int CaDiCaL::Solver::active

(

)

const

Definition at line 1069 of file cadical_solver.cpp.

                          {
  TRACE ("active");
  REQUIRE_VALID_STATE ();
  int res = internal->active ();
  LOG_API_CALL_RETURNS ("active", res);
  return res;
}

add()

void CaDiCaL::Solver::add

(

int

lit

)

Definition at line 577 of file cadical_solver.cpp.

                         {
  TRACE ("add", lit);
  REQUIRE_VALID_STATE ();
  if (lit)
    REQUIRE_VALID_LIT (lit);
  transition_to_steady_state ();
  external->add (lit);
  adding_clause = lit;
  if (adding_clause)
    STATE (ADDING);
  else if (!adding_constraint)
    STATE (STEADY);
  LOG_API_CALL_END ("add", lit);
}

Here is the caller graph for this function:

add_observed_var()

void CaDiCaL::Solver::add_observed_var

(

int

var

)

Definition at line 1044 of file cadical_solver.cpp.

                                      {
  TRACE ("observe", idx);
  REQUIRE_VALID_OR_SOLVING_STATE ();
  REQUIRE_VALID_LIT (idx);
  external->add_observed_var (idx);
  LOG_API_CALL_END ("observe", idx);
}

assume()

void CaDiCaL::Solver::assume

(

int

lit

)

Definition at line 664 of file cadical_solver.cpp.

                            {
  TRACE ("assume", lit);
  REQUIRE_VALID_STATE ();
  REQUIRE_VALID_LIT (lit);
  transition_to_steady_state ();
  external->assume (lit);
  LOG_API_CALL_END ("assume", lit);
}

build()

void CaDiCaL::Solver::build ( FILE * file, const char * prefix = "c " )

static

Definition at line 1266 of file cadical_solver.cpp.

                                                  {
 
  CADICAL_assert (file == stdout || file == stderr);
 
  Terminal *terminal;
 
  if (file == stdout)
    terminal = &tout;
  else if (file == stderr)
    terminal = &terr;
  else
    terminal = 0;
 
  const char *v = CaDiCaL::version ();
  const char *i = identifier ();
  const char *c = compiler ();
  const char *b = date ();
  const char *f = flags ();
 
  CADICAL_assert (v);
 
  fputs (prefix, file);
  if (terminal)
    terminal->magenta ();
  fputs ("Version ", file);
  if (terminal)
    terminal->normal ();
  fputs (v, file);
  if (i) {
    if (terminal)
      terminal->magenta ();
    fputc (' ', file);
    fputs (i, file);
    if (terminal)
      terminal->normal ();
  }
  fputc ('\n', file);
 
  if (c) {
    fputs (prefix, file);
    if (terminal)
      terminal->magenta ();
    fputs (c, file);
    if (f) {
      fputc (' ', file);
      fputs (f, file);
    }
    if (terminal)
      terminal->normal ();
    fputc ('\n', file);
  }
 
  if (b) {
    fputs (prefix, file);
    if (terminal)
      terminal->magenta ();
    fputs (b, file);
    if (terminal)
      terminal->normal ();
    fputc ('\n', file);
  }
 
  fflush (file);
}

Here is the call graph for this function:

clause() [1/7]

void CaDiCaL::Solver::clause	(	const int *	lits,
		size_t	size )

Definition at line 627 of file cadical_solver.cpp.

                                                 {
  REQUIRE (!size || lits,
           "first argument 'lits' zero while second argument 'size' not");
  const int *end = lits + size;
  for (const int *p = lits; p != end; p++) {
    const int lit = *p;
    REQUIRE_VALID_LIT (lit);
    add (lit);
  }
  add (0);
}

Here is the call graph for this function:

clause() [2/7]

void CaDiCaL::Solver::clause

(

const std::vector< int > &

lits

)

Definition at line 639 of file cadical_solver.cpp.

                                               {
  for (auto lit : lits) {
    REQUIRE_VALID_LIT (lit);
    add (lit);
  }
  add (0);
}

Here is the call graph for this function:

clause() [3/7]

void CaDiCaL::Solver::clause

(

int

a

)

Definition at line 592 of file cadical_solver.cpp.

                          {
  REQUIRE_VALID_LIT (a);
  add (a), add (0);
}

Here is the call graph for this function:

clause() [4/7]

void CaDiCaL::Solver::clause	(	int	a,
		int	b )

Definition at line 597 of file cadical_solver.cpp.

                                 {
  REQUIRE_VALID_LIT (a);
  REQUIRE_VALID_LIT (b);
  add (a), add (b), add (0);
}

Here is the call graph for this function:

clause() [5/7]

void CaDiCaL::Solver::clause	(	int	a,
		int	b,
		int	c )

Definition at line 603 of file cadical_solver.cpp.

                                        {
  REQUIRE_VALID_LIT (a);
  REQUIRE_VALID_LIT (b);
  REQUIRE_VALID_LIT (c);
  add (a), add (b), add (c), add (0);
}

Here is the call graph for this function:

clause() [6/7]

void CaDiCaL::Solver::clause	(	int	a,
		int	b,
		int	c,
		int	d )

Definition at line 610 of file cadical_solver.cpp.

                                               {
  REQUIRE_VALID_LIT (a);
  REQUIRE_VALID_LIT (b);
  REQUIRE_VALID_LIT (c);
  REQUIRE_VALID_LIT (d);
  add (a), add (b), add (c), add (d), add (0);
}

Here is the call graph for this function:

clause() [7/7]

void CaDiCaL::Solver::clause	(	int	a,
		int	b,
		int	c,
		int	d,
		int	e )

Definition at line 618 of file cadical_solver.cpp.

                                                      {
  REQUIRE_VALID_LIT (a);
  REQUIRE_VALID_LIT (b);
  REQUIRE_VALID_LIT (c);
  REQUIRE_VALID_LIT (d);
  REQUIRE_VALID_LIT (e);
  add (a), add (b), add (c), add (d), add (e), add (0);
}

Here is the call graph for this function:

close_proof_trace()

void CaDiCaL::Solver::close_proof_trace

(

bool

print = false

)

Definition at line 1162 of file cadical_solver.cpp.

                                                                  {
  TRACE ("close_proof_trace");
  REQUIRE_VALID_STATE ();
  REQUIRE (!internal->file_tracers.empty (), "proof is not traced");
  REQUIRE (!internal->file_tracers.back ()->closed (),
           "proof trace already closed");
  internal->close_trace (print_statistics_unless_quiet);
  LOG_API_CALL_END ("close_proof_trace");
}

conclude()

void CaDiCaL::Solver::conclude

(

)

Definition at line 1247 of file cadical_solver.cpp.

                       {
  TRACE ("conclude");
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == UNSATISFIED || state () == SATISFIED ||
               state () == INCONCLUSIVE,
           "can only conclude in satisfied, unsatisfied or inconclusive state");
  if (state () == UNSATISFIED)
    internal->conclude_unsat ();
  else if (state () == SATISFIED)
    external->conclude_sat ();
  else if (state () == INCONCLUSIVE)
    external->conclude_unknown ();
  CADICAL_assert (state () == UNSATISFIED || state () == SATISFIED ||
          state () == INCONCLUSIVE);
  LOG_API_CALL_END ("conclude");
}

Here is the call graph for this function:

configurations()

void CaDiCaL::Solver::configurations ( )

static

Definition at line 1342 of file cadical_solver.cpp.

{ Config::usage (); }

Here is the call graph for this function:

configure()

bool CaDiCaL::Solver::configure

(

const char *

name

)

Definition at line 563 of file cadical_solver.cpp.

                                        {
  TRACE ("configure", name);
  LOG_API_CALL_BEGIN ("configure", name);
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == CONFIGURING,
           "can only set configuration '%s' right after initialization",
           name);
  bool res = Config::set (internal->opts, name);
  LOG_API_CALL_END ("configure", name, res);
  return res;
}

Here is the call graph for this function:

connect_external_propagator()

void CaDiCaL::Solver::connect_external_propagator

(

ExternalPropagator *

propagator

)

Definition at line 1004 of file cadical_solver.cpp.

                                                                        {
  LOG_API_CALL_BEGIN ("connect_external_propagator");
  REQUIRE_VALID_STATE ();
  REQUIRE (propagator, "can not connect zero propagator");
#ifdef LOGGING
  if (external->propagator)
    LOG ("connecting new external propagator (disconnecting previous one)");
  else
    LOG ("connecting new external propagator (no previous one)");
#endif
  if (external->propagator)
    disconnect_external_propagator ();
 
  external->propagator = propagator;
  internal->connect_propagator ();
  internal->external_prop = true;
  internal->external_prop_is_lazy = propagator->is_lazy;
  LOG_API_CALL_END ("connect_external_propagator");
}

Here is the call graph for this function:

connect_fixed_listener()

void CaDiCaL::Solver::connect_fixed_listener

(

FixedAssignmentListener *

fixed_listener

)

Definition at line 965 of file cadical_solver.cpp.

                                             {
  LOG_API_CALL_BEGIN ("connect_fixed_listener");
  REQUIRE_VALID_STATE ();
  REQUIRE (fixed_listener, "can not connect zero fixed listener");
 
#ifdef LOGGING
  if (external->fixed_listener)
    LOG ("connecting new listener of fixed assignments (disconnecting "
         "previous one)");
  else
    LOG ("connecting new listener of fixed assigments (no previous one)");
#endif
  if (external->fixed_listener)
    disconnect_fixed_listener ();
  external->fixed_listener = fixed_listener;
  // Listeners are treated as real-time listeners, thus previously found
  // fixed assignments are not sent out (would be rather expensive to
  // recover it retrospect, see external_propagate.cpp/get_fixed_literals ()
  // function).
  LOG_API_CALL_END ("connect_fixed_listener");
}

Here is the call graph for this function:

connect_learner()

void CaDiCaL::Solver::connect_learner

(

Learner *

learner

)

Definition at line 936 of file cadical_solver.cpp.

                                              {
  LOG_API_CALL_BEGIN ("connect_learner");
  REQUIRE_VALID_STATE ();
  REQUIRE (learner, "can not connect zero learner");
#ifdef LOGGING
  if (external->learner)
    LOG ("connecting new learner (disconnecting previous one)");
  else
    LOG ("connecting new learner (no previous one)");
#endif
  external->learner = learner;
  LOG_API_CALL_END ("connect_learner");
}

Here is the caller graph for this function:

connect_proof_tracer() [1/4]

void CaDiCaL::Solver::connect_proof_tracer	(	FileTracer *	tracer,
		bool	antecedents,
		bool	finalize_clauses = false )

Definition at line 1207 of file cadical_solver.cpp.

                                                          {
  LOG_API_CALL_BEGIN ("connect proof tracer with file");
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == CONFIGURING,
           "can only start proof tracing right after initialization");
  REQUIRE (tracer, "can not connect zero tracer");
  internal->connect_proof_tracer (tracer, antecedents, finalize_clauses);
  LOG_API_CALL_END ("connect proof tracer with file");
}

Here is the call graph for this function:

connect_proof_tracer() [2/4]

void CaDiCaL::Solver::connect_proof_tracer	(	InternalTracer *	tracer,
		bool	antecedents,
		bool	finalize_clauses = false )

Definition at line 1185 of file cadical_solver.cpp.

                                                          {
  LOG_API_CALL_BEGIN ("connect proof tracer");
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == CONFIGURING,
           "can only start proof tracing to right after initialization");
  REQUIRE (tracer, "can not connect zero tracer");
  internal->connect_proof_tracer (tracer, antecedents, finalize_clauses);
  LOG_API_CALL_END ("connect proof tracer");
}

Here is the call graph for this function:

connect_proof_tracer() [3/4]

void CaDiCaL::Solver::connect_proof_tracer	(	StatTracer *	tracer,
		bool	antecedents,
		bool	finalize_clauses = false )

Definition at line 1196 of file cadical_solver.cpp.

                                                          {
  LOG_API_CALL_BEGIN ("connect proof tracer with stats");
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == CONFIGURING,
           "can only start proof tracing to right after initialization");
  REQUIRE (tracer, "can not connect zero tracer");
  internal->connect_proof_tracer (tracer, antecedents, finalize_clauses);
  LOG_API_CALL_END ("connect proof tracer with stats");
}

Here is the call graph for this function:

connect_proof_tracer() [4/4]

void CaDiCaL::Solver::connect_proof_tracer	(	Tracer *	tracer,
		bool	antecedents,
		bool	finalize_clauses = false )

Definition at line 1174 of file cadical_solver.cpp.

                                                          {
  LOG_API_CALL_BEGIN ("connect proof tracer");
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == CONFIGURING,
           "can only start proof tracing to right after initialization");
  REQUIRE (tracer, "can not connect zero tracer");
  internal->connect_proof_tracer (tracer, antecedents, finalize_clauses);
  LOG_API_CALL_END ("connect proof tracer");
}

Here is the call graph for this function:

connect_terminator()

void CaDiCaL::Solver::connect_terminator

(

Terminator *

terminator

)

Definition at line 907 of file cadical_solver.cpp.

                                                       {
  LOG_API_CALL_BEGIN ("connect_terminator");
  REQUIRE_VALID_STATE ();
  REQUIRE (terminator, "can not connect zero terminator");
#ifdef LOGGING
  if (external->terminator)
    LOG ("connecting new terminator (disconnecting previous one)");
  else
    LOG ("connecting new terminator (no previous one)");
#endif
  external->terminator = terminator;
  LOG_API_CALL_END ("connect_terminator");
}

Here is the caller graph for this function:

constrain()

void CaDiCaL::Solver::constrain

(

int

lit

)

Definition at line 649 of file cadical_solver.cpp.

                               {
  TRACE ("constrain", lit);
  REQUIRE_VALID_STATE ();
  if (lit)
    REQUIRE_VALID_LIT (lit);
  transition_to_steady_state ();
  external->constrain (lit);
  adding_constraint = lit;
  if (adding_constraint)
    STATE (ADDING);
  else if (!adding_clause)
    STATE (STEADY);
  LOG_API_CALL_END ("constrain", lit);
}

constraint_failed()

bool CaDiCaL::Solver::constraint_failed

(

)

Definition at line 862 of file cadical_solver.cpp.

                                {
  TRACE ("constraint_failed");
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == UNSATISFIED,
           "can only determine if constraint failed in unsatisfied state");
  bool res = external->failed_constraint ();
  LOG_API_CALL_RETURNS ("constraint_failed", res);
  CADICAL_assert (state () == UNSATISFIED);
  return res;
}

Here is the call graph for this function:

copy()

void CaDiCaL::Solver::copy

(

Solver &

other

)

const

Definition at line 1691 of file cadical_solver.cpp.

                                      {
  REQUIRE_READY_STATE ();
  REQUIRE (other.state () & CONFIGURING, "target solver already modified");
  internal->opts.copy (other.internal->opts);
  ClauseCopier clause_copier (other);
  traverse_clauses (clause_copier);
  WitnessCopier witness_copier (other.external);
  traverse_witnesses_forward (witness_copier);
  external->copy_flags (*other.external);
}

Here is the call graph for this function:

disconnect_external_propagator()

void CaDiCaL::Solver::disconnect_external_propagator

(

)

Definition at line 1024 of file cadical_solver.cpp.

                                             {
  LOG_API_CALL_BEGIN ("disconnect_external_propagator");
  REQUIRE_VALID_STATE ();
 
#ifdef LOGGING
  if (external->propagator)
    LOG ("disconnecting previous external propagator");
  else
    LOG ("ignoring to disconnect external propagator (no previous one)");
#endif
  if (external->propagator)
    external->reset_observed_vars ();
 
  external->propagator = 0;
  internal->set_tainted_literal ();
  internal->external_prop = false;
  internal->external_prop_is_lazy = true;
  LOG_API_CALL_END ("disconnect_external_propagator");
}

Here is the caller graph for this function:

disconnect_fixed_listener()

void CaDiCaL::Solver::disconnect_fixed_listener

(

)

Definition at line 988 of file cadical_solver.cpp.

                                        {
  LOG_API_CALL_BEGIN ("disconnect_fixed_listener");
  REQUIRE_VALID_STATE ();
#ifdef LOGGING
  if (external->fixed_listener)
    LOG ("disconnecting previous listener of fixed assignments");
  else
    LOG ("ignoring to disconnect listener of fixed assignments (no "
         "previous one)");
#endif
  external->fixed_listener = 0;
  LOG_API_CALL_END ("disconnect_fixed_listener");
}

Here is the caller graph for this function:

disconnect_learner()

void CaDiCaL::Solver::disconnect_learner

(

)

Definition at line 950 of file cadical_solver.cpp.

                                 {
  LOG_API_CALL_BEGIN ("disconnect_learner");
  REQUIRE_VALID_STATE ();
#ifdef LOGGING
  if (external->learner)
    LOG ("disconnecting previous learner");
  else
    LOG ("ignoring to disconnect learner (no previous one)");
#endif
  external->learner = 0;
  LOG_API_CALL_END ("disconnect_learner");
}

Here is the caller graph for this function:

disconnect_proof_tracer() [1/3]

bool CaDiCaL::Solver::disconnect_proof_tracer

(

FileTracer *

tracer

)

Definition at line 1236 of file cadical_solver.cpp.

                                                        {
  LOG_API_CALL_BEGIN ("disconnect proof tracer");
  REQUIRE_VALID_STATE ();
  REQUIRE (tracer, "can not disconnect zero tracer");
  bool res = internal->disconnect_proof_tracer (tracer);
  LOG_API_CALL_RETURNS ("disconnect proof tracer", res);
  return res;
}

disconnect_proof_tracer() [2/3]

bool CaDiCaL::Solver::disconnect_proof_tracer

(

StatTracer *

tracer

)

Definition at line 1227 of file cadical_solver.cpp.

                                                        {
  LOG_API_CALL_BEGIN ("disconnect proof tracer");
  REQUIRE_VALID_STATE ();
  REQUIRE (tracer, "can not disconnect zero tracer");
  bool res = internal->disconnect_proof_tracer (tracer);
  LOG_API_CALL_RETURNS ("disconnect proof tracer", res);
  return res;
}

disconnect_proof_tracer() [3/3]

bool CaDiCaL::Solver::disconnect_proof_tracer

(

Tracer *

tracer

)

Definition at line 1218 of file cadical_solver.cpp.

                                                    {
  LOG_API_CALL_BEGIN ("disconnect proof tracer");
  REQUIRE_VALID_STATE ();
  REQUIRE (tracer, "can not disconnect zero tracer");
  bool res = internal->disconnect_proof_tracer (tracer);
  LOG_API_CALL_RETURNS ("connect proof tracer", res);
  return res;
}

disconnect_terminator()

void CaDiCaL::Solver::disconnect_terminator

(

)

Definition at line 921 of file cadical_solver.cpp.

                                    {
  LOG_API_CALL_BEGIN ("disconnect_terminator");
  REQUIRE_VALID_STATE ();
#ifdef LOGGING
  if (external->terminator)
    LOG ("disconnecting previous terminator");
  else
    LOG ("ignoring to disconnect terminator (no previous one)");
#endif
  external->terminator = 0;
  LOG_API_CALL_END ("disconnect_terminator");
}

Here is the caller graph for this function:

failed()

bool CaDiCaL::Solver::failed

(

int

lit

)

Definition at line 850 of file cadical_solver.cpp.

                            {
  TRACE ("failed", lit);
  REQUIRE_VALID_STATE ();
  REQUIRE_VALID_LIT (lit);
  REQUIRE (state () == UNSATISFIED,
           "can only get failed assumptions in unsatisfied state");
  bool res = external->failed (lit);
  LOG_API_CALL_RETURNS ("failed", lit, res);
  CADICAL_assert (state () == UNSATISFIED);
  return res;
}

Here is the call graph for this function:

fixed()

int CaDiCaL::Solver::fixed

(

int

lit

)

const

Definition at line 873 of file cadical_solver.cpp.

                                {
  TRACE ("fixed", lit);
  REQUIRE_VALID_STATE ();
  REQUIRE_VALID_LIT (lit);
  int res = external->fixed (lit);
  LOG_API_CALL_RETURNS ("fixed", lit, res);
  return res;
}

flip()

bool CaDiCaL::Solver::flip

(

int

lit

)

Definition at line 824 of file cadical_solver.cpp.

                          {
  TRACE ("flip", lit);
  REQUIRE_VALID_STATE ();
  REQUIRE_VALID_LIT (lit);
  REQUIRE (state () == SATISFIED, "can only flip value in satisfied state");
  REQUIRE (!external->propagator,
           "can only flip when no external propagator is present");
  bool res = external->flip (lit);
  LOG_API_CALL_RETURNS ("flip", lit, res);
  CADICAL_assert (state () == SATISFIED);
  return res;
}

Here is the call graph for this function:

flippable()

bool CaDiCaL::Solver::flippable

(

int

lit

)

Definition at line 837 of file cadical_solver.cpp.

                               {
  TRACE ("flippable", lit);
  REQUIRE_VALID_STATE ();
  REQUIRE_VALID_LIT (lit);
  REQUIRE (state () == SATISFIED, "can only flip value in satisfied state");
  REQUIRE (!external->propagator,
           "can only flip when no external propagator is present");
  bool res = external->flippable (lit);
  LOG_API_CALL_RETURNS ("flippable", lit, res);
  CADICAL_assert (state () == SATISFIED);
  return res;
}

Here is the call graph for this function:

flush_proof_trace()

void CaDiCaL::Solver::flush_proof_trace

(

bool

print = false

)

Definition at line 1152 of file cadical_solver.cpp.

                                                                  {
  TRACE ("flush_proof_trace");
  REQUIRE_VALID_STATE ();
  REQUIRE (!internal->file_tracers.empty (), "proof is not traced");
  REQUIRE (!internal->file_tracers.back ()->closed (),
           "proof trace already closed");
  internal->flush_trace (print_statistics_unless_quiet);
  LOG_API_CALL_END ("flush_proof_trace");
}

Here is the caller graph for this function:

force_backtrack()

void CaDiCaL::Solver::force_backtrack

(

size_t

new_level

)

Definition at line 1494 of file cadical_solver.cpp.

                                              {
  TRACE ("force_backtrack", new_level);
  REQUIRE_VALID_OR_SOLVING_STATE ();
  external->force_backtrack (new_level);
}

freeze()

void CaDiCaL::Solver::freeze

(

int

lit

)

Definition at line 1095 of file cadical_solver.cpp.

                            {
  TRACE ("freeze", lit);
  REQUIRE_VALID_STATE ();
  REQUIRE_VALID_LIT (lit);
  external->freeze (lit);
  LOG_API_CALL_END ("freeze", lit);
}

frozen()

bool CaDiCaL::Solver::frozen

(

int

lit

)

const

Definition at line 1113 of file cadical_solver.cpp.

                                  {
  TRACE ("frozen", lit);
  REQUIRE_VALID_STATE ();
  REQUIRE_VALID_LIT (lit);
  bool res = external->frozen (lit);
  LOG_API_CALL_RETURNS ("frozen", lit, res);
  return res;
}

generate_cubes()

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

Definition at line 681 of file cadical_solver.cpp.

                                                                      {
  TRACE ("lookahead_cubes");
  REQUIRE_VALID_OR_SOLVING_STATE ();
  auto cubes = external->generate_cubes (depth, min_depth);
  TRACE ("lookahead_cubes");
 
  CubesWithStatus cubes2;
  cubes2.status = cubes.status;
  cubes2.cubes = cubes.cubes;
  return cubes2;
}

get()

int CaDiCaL::Solver::get

(

const char *

name

)

Definition at line 493 of file cadical_solver.cpp.

                                {
  REQUIRE_VALID_OR_SOLVING_STATE ();
  return internal->opts.get (arg);
}

implied()

void CaDiCaL::Solver::implied

(

std::vector< int > &

implicants

)

Definition at line 730 of file cadical_solver.cpp.

                                               {
  TRACE ("implied");
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == INCONCLUSIVE,
          "can only get implied literals only in unknown state");
  external->conclude_unknown ();
  external->implied (entrailed);
  if (tracing_nb_lidrup_env_var_method)
    flush_proof_trace (true);
  LOG_API_CALL_RETURNS ("implied", (int) entrailed.size ());
}

Here is the call graph for this function:

inconsistent()

bool CaDiCaL::Solver::inconsistent

(

)

Definition at line 647 of file cadical_solver.cpp.

{ return internal->unsat; }

irredundant()

int64_t CaDiCaL::Solver::irredundant

(

)

const

Definition at line 1085 of file cadical_solver.cpp.

                                   {
  TRACE ("irredundant");
  REQUIRE_VALID_STATE ();
  int64_t res = internal->irredundant ();
  LOG_API_CALL_RETURNS ("irredundant", res);
  return res;
}

is_decision()

bool CaDiCaL::Solver::is_decision

(

int

lit

)

Definition at line 1485 of file cadical_solver.cpp.

                                 {
  TRACE ("is_decision", lit);
  REQUIRE_VALID_OR_SOLVING_STATE ();
  REQUIRE_VALID_LIT (lit);
  bool res = external->is_decision (lit);
  LOG_API_CALL_RETURNS ("is_decision", lit, res);
  return res;
}

is_preprocessing_option()

bool CaDiCaL::Solver::is_preprocessing_option ( const char * name )

static

Definition at line 483 of file cadical_solver.cpp.

                                                      {
  return Options::is_preprocessing_option (name);
}

Here is the call graph for this function:

is_valid_configuration()

bool CaDiCaL::Solver::is_valid_configuration ( const char * name )

static

Definition at line 559 of file cadical_solver.cpp.

                                                     {
  return Config::has (name);
}

Here is the call graph for this function:

is_valid_limit()

bool CaDiCaL::Solver::is_valid_limit

(

const char *

arg

)

Definition at line 548 of file cadical_solver.cpp.

                                            {
  return Internal::is_valid_limit (arg);
}

Here is the call graph for this function:

is_valid_long_option()

bool CaDiCaL::Solver::is_valid_long_option ( const char * arg )

static

Definition at line 487 of file cadical_solver.cpp.

                                                  {
  string name;
  int tmp;
  return Options::parse_long_option (arg, name, tmp);
}

Here is the call graph for this function:

is_valid_option()

bool CaDiCaL::Solver::is_valid_option ( const char * name )

static

Definition at line 479 of file cadical_solver.cpp.

                                              {
  return Options::has (name);
}

Here is the call graph for this function:

limit()

bool CaDiCaL::Solver::limit	(	const char *	arg,
		int	val )

Definition at line 540 of file cadical_solver.cpp.

                                            {
  TRACE ("limit", arg, val);
  REQUIRE_VALID_STATE ();
  bool res = internal->limit (arg, val);
  LOG_API_CALL_END ("limit", arg, val, res);
  return res;
}

Here is the call graph for this function:

lookahead()

int CaDiCaL::Solver::lookahead

(

void

)

Definition at line 673 of file cadical_solver.cpp.

                       {
  TRACE ("lookahead");
  REQUIRE_VALID_OR_SOLVING_STATE ();
  int lit = external->lookahead ();
  TRACE ("lookahead");
  return lit;
}

melt()

void CaDiCaL::Solver::melt

(

int

lit

)

Definition at line 1103 of file cadical_solver.cpp.

                          {
  TRACE ("melt", lit);
  REQUIRE_VALID_STATE ();
  REQUIRE_VALID_LIT (lit);
  REQUIRE (external->frozen (lit),
           "can not melt completely melted literal '%d'", lit);
  external->melt (lit);
  LOG_API_CALL_END ("melt", lit);
}

optimize()

void CaDiCaL::Solver::optimize

(

int

val

)

Definition at line 533 of file cadical_solver.cpp.

                              {
  LOG_API_CALL_BEGIN ("optimize", arg);
  REQUIRE_VALID_STATE ();
  internal->opts.optimize (arg);
  LOG_API_CALL_END ("optimize", arg);
}

options()

void CaDiCaL::Solver::options

(

)

Definition at line 1335 of file cadical_solver.cpp.

                      {
  REQUIRE_VALID_STATE ();
  internal->opts.print ();
}

phase()

void CaDiCaL::Solver::phase

(

int

lit

)

Definition at line 882 of file cadical_solver.cpp.

                           {
  TRACE ("phase", lit);
  REQUIRE_VALID_OR_SOLVING_STATE ();
  REQUIRE_VALID_LIT (lit);
  external->phase (lit);
  LOG_API_CALL_END ("phase", lit);
}

prefix()

void CaDiCaL::Solver::prefix

(

const char *

verbose_message_prefix

)

Definition at line 552 of file cadical_solver.cpp.

                                    {
  LOG_API_CALL_BEGIN ("prefix", str);
  REQUIRE_VALID_OR_SOLVING_STATE ();
  internal->prefix = str;
  LOG_API_CALL_END ("prefix", str);
}

Here is the caller graph for this function:

propagate()

int CaDiCaL::Solver::propagate

(

)

Definition at line 713 of file cadical_solver.cpp.

                       {
  TRACE ("propagate_assumptions");
  REQUIRE_VALID_STATE ();
  transition_to_steady_state ();
  const int res = external->propagate_assumptions ();
  if (tracing_nb_lidrup_env_var_method)
    flush_proof_trace (true);
  LOG_API_CALL_RETURNS ("propagate_assumptions", res);
  if (res == 10)
    STATE (SATISFIED);
  else if (res == 20)
    STATE (UNSATISFIED);
  else
    STATE (INCONCLUSIVE);
  return res;
}

Here is the call graph for this function:

read_dimacs() [1/4]

const char * CaDiCaL::Solver::read_dimacs	(	const char *	path,
		int &	vars,
		int	strict,
		bool &	incremental,
		std::vector< int > &	cubes )

Here is the call graph for this function:

read_dimacs() [2/4]

const char * CaDiCaL::Solver::read_dimacs	(	const char *	path,
		int &	vars,
		int	strict = 1 )

Definition at line 1389 of file cadical_solver.cpp.

                                                                        {
  LOG_API_CALL_BEGIN ("read_dimacs", path);
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == CONFIGURING,
           "can only read DIMACS file right after initialization");
  File *file = File::read (internal, path);
  if (!file)
    return internal->error_message.init ("failed to read DIMACS file '%s'",
                                         path);
  const char *err = read_dimacs (file, vars, strict);
  delete file;
  LOG_API_CALL_RETURNS ("read_dimacs", path, err);
  return err;
}

Here is the call graph for this function:

read_dimacs() [3/4]

const char * CaDiCaL::Solver::read_dimacs	(	FILE *	file,
		const char *	name,
		int &	vars,
		int	strict,
		bool &	incremental,
		std::vector< int > &	cubes )

Here is the call graph for this function:

read_dimacs() [4/4]

const char * CaDiCaL::Solver::read_dimacs	(	FILE *	file,
		const char *	name,
		int &	vars,
		int	strict = 1 )

Definition at line 1375 of file cadical_solver.cpp.

                                                        {
  LOG_API_CALL_BEGIN ("read_dimacs", name);
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == CONFIGURING,
           "can only read DIMACS file right after initialization");
  File *file = File::read (internal, external_file, name);
  CADICAL_assert (file);
  const char *err = read_dimacs (file, vars, strict);
  delete file;
  LOG_API_CALL_RETURNS ("read_dimacs", name, err);
  return err;
}

Here is the call graph for this function:

Here is the caller graph for this function:

redundant()

int64_t CaDiCaL::Solver::redundant

(

)

const

Definition at line 1077 of file cadical_solver.cpp.

                                 {
  TRACE ("redundant");
  REQUIRE_VALID_STATE ();
  int64_t res = internal->redundant ();
  LOG_API_CALL_RETURNS ("redundant", res);
  return res;
}

remove_observed_var()

void CaDiCaL::Solver::remove_observed_var

(

int

var

)

Definition at line 1052 of file cadical_solver.cpp.

                                         {
  TRACE ("unobserve", idx);
  REQUIRE_VALID_STATE ();
  REQUIRE_VALID_LIT (idx);
  external->remove_observed_var (idx);
  LOG_API_CALL_END ("unobserve", idx);
}

reserve()

void CaDiCaL::Solver::reserve

(

int

min_max_var

)

Definition at line 440 of file cadical_solver.cpp.

                                     {
  TRACE ("reserve", min_max_var);
  REQUIRE_VALID_STATE ();
  transition_to_steady_state ();
  external->reset_extended ();
  external->init (min_max_var);
  LOG_API_CALL_END ("reserve", min_max_var);
}

reserve_difference()

int CaDiCaL::Solver::reserve_difference

(

int

number_of_vars

)

Definition at line 449 of file cadical_solver.cpp.

                                                  {
  TRACE ("reserve_difference", number_of_vars);
  REQUIRE_VALID_STATE ();
  transition_to_steady_state ();
  external->reset_extended ();
  int new_max_var = external->max_var + number_of_vars;
  external->init (new_max_var);
  LOG_API_CALL_END ("reserve_difference", number_of_vars);
  return new_max_var;
}

reset_assumptions()

void CaDiCaL::Solver::reset_assumptions

(

)

Definition at line 693 of file cadical_solver.cpp.

                                {
  TRACE ("reset_assumptions");
  REQUIRE_VALID_STATE ();
  transition_to_steady_state ();
  external->reset_assumptions ();
  external->reset_concluded ();
  LOG_API_CALL_END ("reset_assumptions");
}

reset_constraint()

void CaDiCaL::Solver::reset_constraint

(

)

Definition at line 702 of file cadical_solver.cpp.

                               {
  TRACE ("reset_constraint");
  REQUIRE_VALID_STATE ();
  transition_to_steady_state ();
  external->reset_constraint ();
  external->reset_concluded ();
  LOG_API_CALL_END ("reset_constraint");
}

reset_observed_vars()

void CaDiCaL::Solver::reset_observed_vars

(

)

Definition at line 1060 of file cadical_solver.cpp.

                                  {
  TRACE ("reset_observed_vars");
  REQUIRE_VALID_OR_SOLVING_STATE ();
  external->reset_observed_vars ();
  LOG_API_CALL_END ("reset_observed_vars");
}

resources()

void CaDiCaL::Solver::resources

(

)

Definition at line 1353 of file cadical_solver.cpp.

                        {
  if (state () == DELETING)
    return;
  TRACE ("resources");
  REQUIRE_VALID_OR_SOLVING_STATE ();
  internal->print_resource_usage ();
  LOG_API_CALL_END ("resources");
}

Here is the call graph for this function:

set()

bool CaDiCaL::Solver::set	(	const char *	name,
		int	val )

Definition at line 498 of file cadical_solver.cpp.

                                          {
  TRACE ("set", arg, val);
  REQUIRE_VALID_STATE ();
  if (strcmp (arg, "log") && strcmp (arg, "quiet") &&
      strcmp (arg, "report") && strcmp (arg, "verbose")) {
    REQUIRE (
        state () == CONFIGURING,
        "can only set option 'set (\"%s\", %d)' right after initialization",
        arg, val);
  }
  bool res = internal->opts.set (arg, val);
  LOG_API_CALL_END ("set", arg, val, res);
 
  return res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

set_long_option()

bool CaDiCaL::Solver::set_long_option

(

const char *

arg

)

Definition at line 514 of file cadical_solver.cpp.

                                             {
  LOG_API_CALL_BEGIN ("set", arg);
  REQUIRE_VALID_STATE ();
  REQUIRE (state () == CONFIGURING,
           "can only set option '%s' right after initialization", arg);
  bool res;
  if (arg[0] != '-' || arg[1] != '-')
    res = false;
  else {
    int val;
    string name;
    res = Options::parse_long_option (arg, name, val);
    if (res)
      set (name.c_str (), val);
  }
  LOG_API_CALL_END ("set", arg, res);
  return res;
}

Here is the call graph for this function:

signature()

const char * CaDiCaL::Solver::signature ( )

static

Definition at line 1333 of file cadical_solver.cpp.

{ return CaDiCaL::signature (); }

Here is the call graph for this function:

Here is the caller graph for this function:

simplify()

int CaDiCaL::Solver::simplify

(

int

rounds = 3

)

Definition at line 796 of file cadical_solver.cpp.

                                {
  TRACE ("simplify", rounds);
  REQUIRE_READY_STATE ();
  REQUIRE (rounds >= 0, "negative number of simplification rounds '%d'",
           rounds);
  internal->limit ("preprocessing", rounds);
  const int res = call_external_solve_and_check_results (true);
  LOG_API_CALL_RETURNS ("simplify", rounds, res);
  return res;
}

solve()

int CaDiCaL::Solver::solve

(

)

Definition at line 786 of file cadical_solver.cpp.

                   {
  TRACE ("solve");
  REQUIRE_READY_STATE ();
  const int res = call_external_solve_and_check_results (false);
  LOG_API_CALL_RETURNS ("solve", res);
  if (tracing_nb_lidrup_env_var_method)
    flush_proof_trace (true);
  return res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

state()

const State & CaDiCaL::Solver::state ( ) const

inline

Definition at line 529 of file cadical.hpp.

{ return _state; }

Here is the caller graph for this function:

statistics()

void CaDiCaL::Solver::statistics

(

)

Definition at line 1344 of file cadical_solver.cpp.

                         {
  if (state () == DELETING)
    return;
  TRACE ("stats");
  REQUIRE_VALID_OR_SOLVING_STATE ();
  internal->print_statistics ();
  LOG_API_CALL_END ("stats");
}

Here is the call graph for this function:

status()

int CaDiCaL::Solver::status ( ) const

inline

Definition at line 534 of file cadical.hpp.

                      {
    if (_state == SATISFIED)
      return 10;
    else if (_state == UNSATISFIED)
      return 20;
    else
      return 0;
  }

terminate()

void CaDiCaL::Solver::terminate

(

)

Definition at line 900 of file cadical_solver.cpp.

                        {
  LOG_API_CALL_BEGIN ("terminate");
  REQUIRE_VALID_OR_SOLVING_STATE ();
  external->terminate ();
  LOG_API_CALL_END ("terminate");
}

trace_proof() [1/2]

bool CaDiCaL::Solver::trace_proof

(

const char *

path

)

Definition at line 1138 of file cadical_solver.cpp.

                                          {
  TRACE ("trace_proof", path);
  REQUIRE_VALID_STATE ();
  REQUIRE (
      state () == CONFIGURING,
      "can only start proof tracing to '%s' right after initialization",
      path);
  File *internal_file = File::write (internal, path);
  bool res = (internal_file != 0);
  internal->trace (internal_file);
  LOG_API_CALL_RETURNS ("trace_proof", path, res);
  return res;
}

Here is the call graph for this function:

trace_proof() [2/2]

bool CaDiCaL::Solver::trace_proof	(	FILE *	file,
		const char *	name )

Definition at line 1124 of file cadical_solver.cpp.

                                                               {
  TRACE ("trace_proof", name);
  REQUIRE_VALID_STATE ();
  REQUIRE (
      state () == CONFIGURING,
      "can only start proof tracing to '%s' right after initialization",
      name);
  File *internal_file = File::write (internal, external_file, name);
  CADICAL_assert (internal_file);
  internal->trace (internal_file);
  LOG_API_CALL_RETURNS ("trace_proof", name, true);
  return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

traverse_clauses()

bool CaDiCaL::Solver::traverse_clauses

(

ClauseIterator &

it

)

const

Definition at line 1502 of file cadical_solver.cpp.

                                                       {
  LOG_API_CALL_BEGIN ("traverse_clauses");
  REQUIRE_VALID_STATE ();
  bool res = external->traverse_all_frozen_units_as_clauses (it) &&
             internal->traverse_clauses (it) &&
             internal->traverse_constraint (it);
  LOG_API_CALL_RETURNS ("traverse_clauses", res);
  return res;
}

Here is the caller graph for this function:

traverse_witnesses_backward()

bool CaDiCaL::Solver::traverse_witnesses_backward

(

WitnessIterator &

it

)

const

Definition at line 1512 of file cadical_solver.cpp.

                                                                   {
  LOG_API_CALL_BEGIN ("traverse_witnesses_backward");
  REQUIRE_VALID_STATE ();
  bool res = external->traverse_all_non_frozen_units_as_witnesses (it) &&
             external->traverse_witnesses_backward (it);
  LOG_API_CALL_RETURNS ("traverse_witnesses_backward", res);
  return res;
}

Here is the caller graph for this function:

traverse_witnesses_forward()

bool CaDiCaL::Solver::traverse_witnesses_forward

(

WitnessIterator &

it

)

const

Definition at line 1521 of file cadical_solver.cpp.

                                                                  {
  LOG_API_CALL_BEGIN ("traverse_witnesses_forward");
  REQUIRE_VALID_STATE ();
  bool res = external->traverse_witnesses_forward (it) &&
             external->traverse_all_non_frozen_units_as_witnesses (it);
  LOG_API_CALL_RETURNS ("traverse_witnesses_forward", res);
  return res;
}

Here is the caller graph for this function:

unphase()

void CaDiCaL::Solver::unphase

(

int

lit

)

Definition at line 890 of file cadical_solver.cpp.

                             {
  TRACE ("unphase", lit);
  REQUIRE_VALID_OR_SOLVING_STATE ();
  REQUIRE_VALID_LIT (lit);
  external->unphase (lit);
  LOG_API_CALL_END ("unphase", lit);
}

usage()

void CaDiCaL::Solver::usage ( )

static

Definition at line 1340 of file cadical_solver.cpp.

{ Options::usage (); }

Here is the call graph for this function:

val()

int CaDiCaL::Solver::val

(

int

lit

)

Definition at line 809 of file cadical_solver.cpp.

                        {
  TRACE ("val", lit);
  REQUIRE_VALID_STATE ();
  REQUIRE_VALID_LIT (lit);
  REQUIRE (state () == SATISFIED, "can only get value in satisfied state");
  if (!external->extended)
    external->extend ();
  external->conclude_sat ();
  int res = external->ival (lit);
  LOG_API_CALL_RETURNS ("val", lit, res);
  CADICAL_assert (state () == SATISFIED);
  CADICAL_assert (res == lit || res == -lit);
  return res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

vars()

int CaDiCaL::Solver::vars

(

)

Definition at line 432 of file cadical_solver.cpp.

                  {
  TRACE ("vars");
  REQUIRE_VALID_OR_SOLVING_STATE ();
  int res = external->max_var;
  LOG_API_CALL_RETURNS ("vars", res);
  return res;
}

Here is the caller graph for this function:

version()

const char * CaDiCaL::Solver::version ( )

static

Definition at line 1331 of file cadical_solver.cpp.

{ return CaDiCaL::version (); }

Here is the call graph for this function:

write_dimacs()

const char * CaDiCaL::Solver::write_dimacs	(	const char *	path,
		int	min_max_var = 0 )

Definition at line 1565 of file cadical_solver.cpp.

                                                                   {
  LOG_API_CALL_BEGIN ("write_dimacs", path, min_max_var);
  REQUIRE_VALID_STATE ();
#ifndef CADICAL_QUIET
  const double start = internal->time ();
#endif
  internal->restore_clauses ();
  ClauseCounter counter;
  (void) traverse_clauses (counter);
  LOG ("found maximal variable %d and %" PRId64 " clauses", counter.vars,
       counter.clauses);
  File *file = File::write (internal, path);
  const char *res = 0;
  if (file) {
    int actual_max_vars = max (min_max_var, counter.vars);
    MSG ("writing %s'p cnf %d %" PRId64 "'%s header", tout.green_code (),
         actual_max_vars, counter.clauses, tout.normal_code ());
    file->put ("p cnf ");
    file->put (actual_max_vars);
    file->put (' ');
    file->put (counter.clauses);
    file->put ('\n');
    ClauseWriter writer (file);
    if (!traverse_clauses (writer))
      res = internal->error_message.init (
          "writing to DIMACS file '%s' failed", path);
    delete file;
  } else
    res = internal->error_message.init (
        "failed to open DIMACS file '%s' for writing", path);
#ifndef CADICAL_QUIET
  if (!res) {
    const double end = internal->time ();
    MSG ("wrote %" PRId64 " clauses in %.2f seconds %s time",
         counter.clauses, end - start,
         internal->opts.realtime ? "real" : "process");
  }
#endif
  LOG_API_CALL_RETURNS ("write_dimacs", path, min_max_var, res);
  return res;
}

Here is the call graph for this function:

write_extension()

const char * CaDiCaL::Solver::write_extension

(

const char *

path

)

Definition at line 1636 of file cadical_solver.cpp.

                                                     {
  LOG_API_CALL_BEGIN ("write_extension", path);
  REQUIRE_VALID_STATE ();
  const char *res = 0;
#ifndef CADICAL_QUIET
  const double start = internal->time ();
#endif
  File *file = File::write (internal, path);
  WitnessWriter writer (file);
  if (file) {
    if (!traverse_witnesses_backward (writer))
      res = internal->error_message.init (
          "writing to DIMACS file '%s' failed", path);
    delete file;
  } else
    res = internal->error_message.init (
        "failed to open extension file '%s' for writing", path);
#ifndef CADICAL_QUIET
  if (!res) {
    const double end = internal->time ();
    MSG ("wrote %" PRId64 " witnesses in %.2f seconds %s time",
         writer.witnesses, end - start,
         internal->opts.realtime ? "real" : "process");
  }
#endif
  LOG_API_CALL_RETURNS ("write_extension", path, res);
  return res;
}

Here is the call graph for this function:

Friends And Related Symbol Documentation

App

friend class App

friend

Definition at line 1068 of file cadical.hpp.

DisconnectCall

friend struct DisconnectCall

friend

Definition at line 1163 of file cadical.hpp.

DumpCall

friend struct DumpCall

friend

Definition at line 1150 of file cadical.hpp.

LemmaCall

friend struct LemmaCall

friend

Definition at line 1161 of file cadical.hpp.

Mobical

friend class Mobical

friend

Definition at line 1069 of file cadical.hpp.

MockPropagator

friend class MockPropagator

friend

Definition at line 1164 of file cadical.hpp.

ObserveCall

friend struct ObserveCall

friend

Definition at line 1162 of file cadical.hpp.

Parser

friend class Parser

friend

Definition at line 1070 of file cadical.hpp.

Testing

friend class Testing

friend

Definition at line 1034 of file cadical.hpp.

---

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

• src/sat/cadical/cadical.hpp
• src/sat/cadical/cadical_solver.cpp