}
FpConverter::FpConverter(context::UserContext* user)
- :
+ : d_additionalAssertions(user)
#ifdef CVC4_USE_SYMFPU
+ ,
d_fpMap(user),
d_rmMap(user),
d_boolMap(user),
d_ubvMap(user),
- d_sbvMap(user),
+ d_sbvMap(user)
#endif
- d_additionalAssertions(user)
{
}
+FpConverter::~FpConverter() {}
+
#ifdef CVC4_USE_SYMFPU
Node FpConverter::ufToNode(const fpt &format, const uf &u) const
{
** Uses the symfpu library to convert from floating-point operations to
** bit-vectors and propositions allowing the theory to be solved by
** 'bit-blasting'.
+ **
+ ** !!! This header is not to be included in any other headers !!!
**/
#include "cvc4_private.h"
namespace theory {
namespace fp {
-typedef PairHashFunction<TypeNode, TypeNode, TypeNodeHashFunction,
- TypeNodeHashFunction>
- PairTypeNodeHashFunction;
-
/**
* This is a symfpu symbolic "back-end". It allows the library to be used to
* construct bit-vector expressions that compute floating-point operations.
*/
class FpConverter
{
+ public:
+ /** Constructor. */
+ FpConverter(context::UserContext*);
+ /** Destructor. */
+ ~FpConverter();
+
+ /** Adds a node to the conversion, returns the converted node */
+ Node convert(TNode);
+
+ /** Gives the node representing the value of a given variable */
+ Node getValue(Valuation&, TNode);
+
+ context::CDList<Node> d_additionalAssertions;
+
protected:
#ifdef CVC4_USE_SYMFPU
typedef symfpuSymbolic::traits traits;
/* Creates the relevant components for a variable */
uf buildComponents(TNode current);
#endif
-
- public:
- context::CDList<Node> d_additionalAssertions;
-
- FpConverter(context::UserContext *);
-
- /** Adds a node to the conversion, returns the converted node */
- Node convert(TNode);
-
- /** Gives the node representing the value of a given variable */
- Node getValue(Valuation &, TNode);
};
} // namespace fp
#include <vector>
#include "options/fp_options.h"
+#include "theory/fp/fp_converter.h"
#include "theory/fp/theory_fp_rewriter.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
: Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm),
d_notification(*this),
d_registeredTerms(u),
- d_conv(u),
+ d_conv(new FpConverter(u)),
d_expansionRequested(false),
d_conflictNode(c, Node::null()),
d_minMap(u),
d_toUBVMap(u),
d_toSBVMap(u),
d_toRealMap(u),
- realToFloatMap(u),
- floatToRealMap(u),
- abstractionMap(u),
+ d_realToFloatMap(u),
+ d_floatToRealMap(u),
+ d_abstractionMap(u),
d_state(c, u, valuation)
{
// indicate we are using the default theory state object
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
- ComparisonUFMap::const_iterator i(realToFloatMap.find(t));
+ ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t));
Node fun;
- if (i == realToFloatMap.end())
+ if (i == d_realToFloatMap.end())
{
std::vector<TypeNode> args(2);
args[0] = node[0].getType();
nm->mkFunctionType(args, node.getType()),
"floatingpoint_abstract_real_to_float",
NodeManager::SKOLEM_EXACT_NAME);
- realToFloatMap.insert(t, fun);
+ d_realToFloatMap.insert(t, fun);
}
else
{
}
Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
- abstractionMap.insert(uf, node);
+ d_abstractionMap.insert(uf, node);
return uf;
}
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
- ComparisonUFMap::const_iterator i(floatToRealMap.find(t));
+ ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t));
Node fun;
- if (i == floatToRealMap.end())
+ if (i == d_floatToRealMap.end())
{
std::vector<TypeNode> args(2);
args[0] = t;
nm->mkFunctionType(args, nm->realType()),
"floatingpoint_abstract_float_to_real",
NodeManager::SKOLEM_EXACT_NAME);
- floatToRealMap.insert(t, fun);
+ d_floatToRealMap.insert(t, fun);
}
else
{
}
Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
- abstractionMap.insert(uf, node);
+ d_abstractionMap.insert(uf, node);
return uf;
}
void TheoryFp::convertAndEquateTerm(TNode node) {
Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
- size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size();
+ size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size();
- Node converted(d_conv.convert(node));
+ Node converted(d_conv->convert(node));
if (converted != node) {
Debug("fp-convertTerm")
<< "TheoryFp::convertTerm(): after " << converted << std::endl;
}
- size_t newAdditionalAssertions = d_conv.d_additionalAssertions.size();
+ size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size();
Assert(oldAdditionalAssertions <= newAdditionalAssertions);
while (oldAdditionalAssertions < newAdditionalAssertions) {
- Node addA = d_conv.d_additionalAssertions[oldAdditionalAssertions];
+ Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions];
Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion "
<< addA << std::endl;
TheoryModel* m = getValuation().getModel();
bool lemmaAdded = false;
- for (abstractionMapType::const_iterator i = abstractionMap.begin();
- i != abstractionMap.end();
+ for (AbstractionMap::const_iterator i = d_abstractionMap.begin();
+ i != d_abstractionMap.end();
++i)
{
if (m->hasTerm((*i).first))
}
Node TheoryFp::getModelValue(TNode var) {
- return d_conv.getValue(d_valuation, var);
+ return d_conv->getValue(d_valuation, var);
}
bool TheoryFp::collectModelInfo(TheoryModel* m,
}
for (std::set<TNode>::const_iterator i(relevantVariables.begin());
- i != relevantVariables.end(); ++i) {
+ i != relevantVariables.end();
+ ++i)
+ {
TNode node = *i;
Trace("fp-collectModelInfo")
<< "TheoryFp::collectModelInfo(): relevantVariable " << node
<< std::endl;
- if (!m->assertEquality(node, d_conv.getValue(d_valuation, node), true))
+ if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true))
{
return false;
}
#include <utility>
#include "context/cdo.h"
-#include "theory/fp/fp_converter.h"
#include "theory/fp/theory_fp_rewriter.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
namespace theory {
namespace fp {
-class TheoryFp : public Theory {
+class FpConverter;
+
+class TheoryFp : public Theory
+{
public:
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
TheoryFp(context::Context* c,
Valuation valuation,
const LogicInfo& logicInfo,
ProofNodeManager* pnm = nullptr);
+
//--------------------------------- initialization
- /** get the official theory rewriter of this theory */
+ /** Get the official theory rewriter of this theory. */
TheoryRewriter* getTheoryRewriter() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* documentation in Theory::needsEqualityEngine.
*/
bool needsEqualityEngine(EeSetupInfo& esi) override;
- /** finish initialization */
+ /** Finish initialization. */
void finishInit() override;
//--------------------------------- end initialization
Node getModelValue(TNode var) override;
bool collectModelInfo(TheoryModel* m,
const std::set<Node>& relevantTerms) override;
- /** Collect model values in m based on the relevant terms given by
- * relevantTerms */
+ /**
+ * Collect model values in m based on the relevant terms given by
+ * relevantTerms.
+ */
bool collectModelValues(TheoryModel* m,
const std::set<Node>& relevantTerms) override;
TrustNode explain(TNode n) override;
protected:
- /** Equality engine */
+ using PairTypeNodeHashFunction = PairHashFunction<TypeNode,
+ TypeNode,
+ TypeNodeHashFunction,
+ TypeNodeHashFunction>;
+ /** Uninterpreted functions for undefined cases of non-total operators. */
+ using ComparisonUFMap =
+ context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>;
+ /** Uninterpreted functions for lazy handling of conversions. */
+ using ConversionUFMap = context::
+ CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>;
+ using ConversionAbstractionMap = ComparisonUFMap;
+ using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+
+ /** Equality engine. */
class NotifyClass : public eq::EqualityEngineNotify {
protected:
TheoryFp& d_theorySolver;
NotifyClass d_notification;
- /** General utility **/
+ /** General utility. */
void registerTerm(TNode node);
bool isRegistered(TNode node);
context::CDHashSet<Node, NodeHashFunction> d_registeredTerms;
- /** Bit-blasting conversion */
- FpConverter d_conv;
+ /** The word-blaster. Translates FP -> BV. */
+ std::unique_ptr<FpConverter> d_conv;
+
bool d_expansionRequested;
void convertAndEquateTerm(TNode node);
*/
void conflictEqConstantMerge(TNode t1, TNode t2);
- context::CDO<Node> d_conflictNode;
-
- typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>
- ComparisonUFMap;
-
- ComparisonUFMap d_minMap;
- ComparisonUFMap d_maxMap;
+ bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
Node minUF(Node);
Node maxUF(Node);
- typedef context::CDHashMap<std::pair<TypeNode, TypeNode>, Node,
- PairTypeNodeHashFunction>
- ConversionUFMap;
-
- ConversionUFMap d_toUBVMap;
- ConversionUFMap d_toSBVMap;
-
Node toUBVUF(Node);
Node toSBVUF(Node);
- ComparisonUFMap d_toRealMap;
-
Node toRealUF(Node);
- /** Uninterpretted functions for lazy handling of conversions */
- typedef ComparisonUFMap conversionAbstractionMap;
-
- conversionAbstractionMap realToFloatMap;
- conversionAbstractionMap floatToRealMap;
-
Node abstractRealToFloat(Node);
Node abstractFloatToReal(Node);
- typedef context::CDHashMap<Node, Node, NodeHashFunction> abstractionMapType;
- abstractionMapType abstractionMap; // abstract -> original
+ private:
+ context::CDO<Node> d_conflictNode;
- bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
+ ComparisonUFMap d_minMap;
+ ComparisonUFMap d_maxMap;
+ ConversionUFMap d_toUBVMap;
+ ConversionUFMap d_toSBVMap;
+ ComparisonUFMap d_toRealMap;
+ ConversionAbstractionMap d_realToFloatMap;
+ ConversionAbstractionMap d_floatToRealMap;
+ AbstractionMap d_abstractionMap; // abstract -> original
/** The theory rewriter for this theory. */
TheoryFpRewriter d_rewriter;
projects / cvc5.git / commitdiff