Split out is_in_conflict solver capability
This is only provided by the prop_conv_solvert-based hierarchy at the moment and is quite specific to MiniSAT-based solvers. The functionality itself is used out-of-tree only (2LS).
This commit is contained in:
parent
b77b5b09d4
commit
ef366e5a7e
|
@ -0,0 +1,30 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Capability to check whether an expression is a reason for
|
||||
the solver returning UNSAT
|
||||
|
||||
Author: Peter Schrammel
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// Capability to check whether an expression is a reason for
|
||||
/// the solver returning UNSAT
|
||||
|
||||
#ifndef CPROVER_SOLVERS_CONFLICT_PROVIDER_H
|
||||
#define CPROVER_SOLVERS_CONFLICT_PROVIDER_H
|
||||
|
||||
class exprt;
|
||||
|
||||
class conflict_providert
|
||||
{
|
||||
public:
|
||||
/// Returns true if an expression is in the final conflict leading to UNSAT.
|
||||
/// The argument can be a Boolean expression or something more
|
||||
/// solver-specific, e.g. a `literal_exprt`.
|
||||
virtual bool is_in_conflict(const exprt &) const = 0;
|
||||
|
||||
virtual ~conflict_providert() = default;
|
||||
};
|
||||
|
||||
#endif // CPROVER_SOLVERS_CONFLICT_PROVIDER_H
|
|
@ -36,13 +36,6 @@ exprt prop_convt::handle(const exprt &expr)
|
|||
return literal_exprt(l);
|
||||
}
|
||||
|
||||
/// determine whether a variable is in the final conflict
|
||||
bool prop_convt::is_in_conflict(literalt) const
|
||||
{
|
||||
UNREACHABLE;
|
||||
return false;
|
||||
}
|
||||
|
||||
void prop_convt::set_assumptions(const bvt &)
|
||||
{
|
||||
UNREACHABLE;
|
||||
|
|
|
@ -46,10 +46,6 @@ public:
|
|||
virtual void set_assumptions(const bvt &_assumptions);
|
||||
virtual bool has_set_assumptions() const { return false; }
|
||||
virtual void set_all_frozen() {}
|
||||
|
||||
// returns true if an assumption is in the final conflict
|
||||
virtual bool is_in_conflict(literalt l) const;
|
||||
virtual bool has_is_in_conflict() const { return false; }
|
||||
};
|
||||
|
||||
#endif // CPROVER_SOLVERS_PROP_PROP_CONV_H
|
||||
|
|
|
@ -10,6 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include <algorithm>
|
||||
|
||||
bool prop_conv_solvert::is_in_conflict(const exprt &expr) const
|
||||
{
|
||||
return prop.is_in_conflict(to_literal_expr(expr).get_literal());
|
||||
}
|
||||
|
||||
bool prop_conv_solvert::literal(const symbol_exprt &expr, literalt &dest) const
|
||||
{
|
||||
PRECONDITION(expr.type().id() == ID_bool);
|
||||
|
|
|
@ -16,13 +16,17 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/message.h>
|
||||
#include <util/std_expr.h>
|
||||
|
||||
#include <solvers/conflict_provider.h>
|
||||
|
||||
#include "literal.h"
|
||||
#include "literal_expr.h"
|
||||
#include "prop.h"
|
||||
#include "prop_conv.h"
|
||||
#include "solver_resource_limits.h"
|
||||
|
||||
class prop_conv_solvert : public prop_convt, public solver_resource_limitst
|
||||
class prop_conv_solvert : public conflict_providert,
|
||||
public prop_convt,
|
||||
public solver_resource_limitst
|
||||
{
|
||||
public:
|
||||
prop_conv_solvert(propt &_prop, message_handlert &message_handler)
|
||||
|
@ -65,14 +69,7 @@ public:
|
|||
freeze_all = true;
|
||||
}
|
||||
literalt convert(const exprt &expr) override;
|
||||
bool is_in_conflict(literalt l) const override
|
||||
{
|
||||
return prop.is_in_conflict(l);
|
||||
}
|
||||
bool has_is_in_conflict() const override
|
||||
{
|
||||
return prop.has_is_in_conflict();
|
||||
}
|
||||
bool is_in_conflict(const exprt &expr) const override;
|
||||
|
||||
// get literal for expression, if available
|
||||
bool literal(const symbol_exprt &expr, literalt &literal) const;
|
||||
|
|
Loading…
Reference in New Issue