summaryrefslogtreecommitdiff
path: root/src/theory/fp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp')
-rw-r--r--src/theory/fp/fp_converter.cpp8
-rw-r--r--src/theory/fp/fp_converter.h33
-rw-r--r--src/theory/fp/theory_fp.cpp45
-rw-r--r--src/theory/fp/theory_fp.h75
4 files changed, 86 insertions, 75 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 85482bf6d..858710746 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -755,18 +755,20 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const
}
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
{
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 59e65c9e1..6688e8607 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -14,6 +14,8 @@
** 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"
@@ -26,7 +28,7 @@
#include "context/cdlist.h"
#include "expr/node.h"
#include "expr/node_builder.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
#include "theory/valuation.h"
#include "util/bitvector.h"
#include "util/floatingpoint_size.h"
@@ -49,10 +51,6 @@ namespace CVC4 {
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.
@@ -302,6 +300,20 @@ class floatingPointTypeInfo : public FloatingPointSize
*/
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;
@@ -338,17 +350,6 @@ class FpConverter
/* 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
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 0b15486e2..01fab92c8 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -23,6 +23,7 @@
#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"
@@ -108,7 +109,7 @@ TheoryFp::TheoryFp(context::Context* c,
: 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),
@@ -116,9 +117,9 @@ TheoryFp::TheoryFp(context::Context* c,
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
@@ -341,10 +342,10 @@ Node TheoryFp::abstractRealToFloat(Node node)
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();
@@ -353,7 +354,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
nm->mkFunctionType(args, node.getType()),
"floatingpoint_abstract_real_to_float",
NodeManager::SKOLEM_EXACT_NAME);
- realToFloatMap.insert(t, fun);
+ d_realToFloatMap.insert(t, fun);
}
else
{
@@ -361,7 +362,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
}
Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
- abstractionMap.insert(uf, node);
+ d_abstractionMap.insert(uf, node);
return uf;
}
@@ -373,10 +374,10 @@ Node TheoryFp::abstractFloatToReal(Node node)
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;
@@ -385,7 +386,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
nm->mkFunctionType(args, nm->realType()),
"floatingpoint_abstract_float_to_real",
NodeManager::SKOLEM_EXACT_NAME);
- floatToRealMap.insert(t, fun);
+ d_floatToRealMap.insert(t, fun);
}
else
{
@@ -393,7 +394,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
}
Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
- abstractionMap.insert(uf, node);
+ d_abstractionMap.insert(uf, node);
return uf;
}
@@ -737,9 +738,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
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")
@@ -748,11 +749,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
<< "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;
@@ -953,8 +954,8 @@ void TheoryFp::postCheck(Effort level)
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))
@@ -1016,7 +1017,7 @@ TrustNode TheoryFp::explain(TNode n)
}
Node TheoryFp::getModelValue(TNode var) {
- return d_conv.getValue(d_valuation, var);
+ return d_conv->getValue(d_valuation, var);
}
bool TheoryFp::collectModelInfo(TheoryModel* m,
@@ -1069,14 +1070,16 @@ bool TheoryFp::collectModelValues(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;
}
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 42c009893..fe91a39bd 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -24,7 +24,6 @@
#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"
@@ -33,7 +32,10 @@ namespace CVC4 {
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,
@@ -42,8 +44,9 @@ class TheoryFp : public Theory {
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
@@ -51,7 +54,7 @@ class TheoryFp : public Theory {
* documentation in Theory::needsEqualityEngine.
*/
bool needsEqualityEngine(EeSetupInfo& esi) override;
- /** finish initialization */
+ /** Finish initialization. */
void finishInit() override;
//--------------------------------- end initialization
@@ -77,8 +80,10 @@ class TheoryFp : public Theory {
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;
@@ -87,7 +92,20 @@ class TheoryFp : public Theory {
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;
@@ -108,14 +126,15 @@ class TheoryFp : public Theory {
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);
@@ -133,44 +152,30 @@ class TheoryFp : public Theory {
*/
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback