summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/model_manager.cpp2
-rw-r--r--src/theory/quantifiers/fmf/model_builder.cpp2
-rw-r--r--src/theory/sort_inference.cpp3
-rw-r--r--src/theory/sort_inference.h7
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/theory_model.cpp16
-rw-r--r--src/theory/theory_model_builder.cpp17
-rw-r--r--src/theory/theory_model_builder.h10
-rw-r--r--src/theory/uf/ho_extension.cpp2
-rw-r--r--src/theory/uf/theory_uf.cpp23
-rw-r--r--src/theory/uf/theory_uf_rewriter.cpp10
-rw-r--r--src/theory/uf/theory_uf_rewriter.h3
12 files changed, 61 insertions, 36 deletions
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 9d25dd760..29c4bf169 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -59,7 +59,7 @@ void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
// not have a model builder
if (d_modelBuilder == nullptr)
{
- d_alocModelBuilder.reset(new TheoryEngineModelBuilder);
+ d_alocModelBuilder.reset(new TheoryEngineModelBuilder(d_env));
d_modelBuilder = d_alocModelBuilder.get();
}
// notice that the equality engine of the model has yet to be assigned.
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 1e78d103e..a331409f1 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -34,7 +34,7 @@ QModelBuilder::QModelBuilder(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr)
- : TheoryEngineModelBuilder(),
+ : TheoryEngineModelBuilder(qs.getEnv()),
d_addedLemmas(0),
d_triedLemmas(0),
d_qstate(qs),
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index cad545ca6..db2db9937 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -29,6 +29,7 @@
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/uf_options.h"
+#include "smt/env.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/rewriter.h"
@@ -880,7 +881,7 @@ bool SortInference::isMonotonic( TypeNode tn ) {
bool SortInference::isHandledApplyUf(Kind k) const
{
- return k == APPLY_UF && !options::ufHo();
+ return k == APPLY_UF && !d_env.getLogicInfo().isHigherOrder();
}
} // namespace theory
diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h
index 1dc7ff3c3..279be5e10 100644
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -25,6 +25,9 @@
#include "expr/type_node.h"
namespace cvc5 {
+
+class Env;
+
namespace theory {
/** sort inference
@@ -63,6 +66,8 @@ public:
};
private:
+ /** Reference to the env */
+ Env& d_env;
/** the id count for all subsorts we have allocated */
int d_sortCount;
UnionFind d_type_union_find;
@@ -106,7 +111,7 @@ private:
void reset();
public:
- SortInference() : d_sortCount(1) {}
+ SortInference(Env& env) : d_env(env), d_sortCount(1) {}
~SortInference(){}
/** initialize
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index db98b47fa..cd9445bb0 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -264,7 +264,7 @@ TheoryEngine::TheoryEngine(Env& env)
if (options::sortInference())
{
- d_sortInfer.reset(new SortInference);
+ d_sortInfer.reset(new SortInference(env));
}
d_true = NodeManager::currentNM()->mkConst<bool>(true);
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 02a837899..291cd1905 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -40,7 +40,7 @@ TheoryModel::TheoryModel(Env& env, std::string name, bool enableFuncModels)
d_enableFuncModels(enableFuncModels)
{
// must use function models when ufHo is enabled
- Assert(d_enableFuncModels || !options::ufHo());
+ Assert(d_enableFuncModels || !d_env.getLogicInfo().isHigherOrder());
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
}
@@ -52,7 +52,8 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee)
Assert(ee != nullptr);
d_equalityEngine = ee;
// The kinds we are treating as function application in congruence
- d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
+ d_equalityEngine->addFunctionKind(
+ kind::APPLY_UF, false, d_env.getLogicInfo().isHigherOrder());
d_equalityEngine->addFunctionKind(kind::HO_APPLY);
d_equalityEngine->addFunctionKind(kind::SELECT);
// d_equalityEngine->addFunctionKind(kind::STORE);
@@ -293,7 +294,8 @@ Node TheoryModel::getModelValue(TNode n) const
// return the representative of the term in the equality engine, if it exists
TypeNode t = ret.getType();
bool eeHasTerm;
- if (!options::ufHo() && (t.isFunction() || t.isPredicate()))
+ if (!d_env.getLogicInfo().isHigherOrder()
+ && (t.isFunction() || t.isPredicate()))
{
// functions are in the equality engine, but *not* as first-class members
// when higher-order is disabled. In this case, we cannot query
@@ -692,7 +694,8 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) {
Trace("model-builder") << " Assigning function (" << f << ") to (" << f_def << ")" << endl;
Assert(d_uf_models.find(f) == d_uf_models.end());
- if( options::ufHo() ){
+ if (d_env.getLogicInfo().isHigherOrder())
+ {
//we must rewrite the function value since the definition needs to be a constant value
f_def = Rewriter::rewrite( f_def );
Trace("model-builder-debug")
@@ -705,7 +708,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) {
d_uf_models[f] = f_def;
}
- if (options::ufHo() && d_equalityEngine->hasTerm(f))
+ if (d_env.getLogicInfo().isHigherOrder() && d_equalityEngine->hasTerm(f))
{
Trace("model-builder-debug") << " ...function is first-class member of equality engine" << std::endl;
// assign to representative if higher-order
@@ -740,7 +743,8 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() {
Assert(d_env.getTopLevelSubstitutions().apply(n) == n);
if( !hasAssignedFunctionDefinition( n ) ){
Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl;
- if( options::ufHo() ){
+ if (d_env.getLogicInfo().isHigherOrder())
+ {
// if in higher-order mode, assign function definitions modulo equality
Node r = getRepresentative( n );
std::map< Node, Node >::iterator itf = func_to_rep.find( r );
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index e43cb26c8..2acbe2388 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -21,6 +21,7 @@
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "options/uf_options.h"
+#include "smt/env.h"
#include "theory/rewriter.h"
#include "theory/uf/theory_uf_model.h"
@@ -31,6 +32,8 @@ using namespace cvc5::context;
namespace cvc5 {
namespace theory {
+TheoryEngineModelBuilder::TheoryEngineModelBuilder(Env& env) : d_env(env) {}
+
void TheoryEngineModelBuilder::Assigner::initialize(
TypeNode tn, TypeEnumeratorProperties* tep, const std::vector<Node>& aes)
{
@@ -64,8 +67,6 @@ Node TheoryEngineModelBuilder::Assigner::getNextAssignment()
return n;
}
-TheoryEngineModelBuilder::TheoryEngineModelBuilder() {}
-
Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
{
eq::EqClassIterator eqc_i = eq::EqClassIterator(r, m->d_equalityEngine);
@@ -129,7 +130,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n)
{
// selectors are always assignable (where we guarantee that they are not
// evaluatable here)
- if (!options::ufHo())
+ if (!d_env.getLogicInfo().isHigherOrder())
{
Assert(!n.getType().isFunction());
return true;
@@ -151,7 +152,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n)
else
{
// non-function variables, and fully applied functions
- if (!options::ufHo())
+ if (!d_env.getLogicInfo().isHigherOrder())
{
// no functions exist, all functions are fully applied
Assert(n.getKind() != kind::HO_APPLY);
@@ -1228,7 +1229,7 @@ bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m)
void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
{
- Assert(!options::ufHo());
+ Assert(!d_env.getLogicInfo().isHigherOrder());
uf::UfModelTree ufmt(f);
Node default_v;
for (size_t i = 0; i < m->d_uf_terms[f].size(); i++)
@@ -1273,7 +1274,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
{
- Assert(options::ufHo());
+ Assert(d_env.getLogicInfo().isHigherOrder());
TypeNode type = f.getType();
std::vector<TypeNode> argTypes = type.getArgTypes();
std::vector<Node> args;
@@ -1397,7 +1398,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
Trace("model-builder") << "Assigning function values..." << std::endl;
std::vector<Node> funcs_to_assign = m->getFunctionsToAssign();
- if (options::ufHo())
+ if (d_env.getLogicInfo().isHigherOrder())
{
// sort based on type size if higher-order
Trace("model-builder") << "Sort functions by type..." << std::endl;
@@ -1424,7 +1425,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
Trace("model-builder") << " Function #" << k << " is " << f << std::endl;
// std::map< Node, std::vector< Node > >::iterator itht =
// m->d_ho_uf_terms.find( f );
- if (!options::ufHo())
+ if (!d_env.getLogicInfo().isHigherOrder())
{
Trace("model-builder") << " Assign function value for " << f
<< " based on APPLY_UF" << std::endl;
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 195ba9e0f..71458a913 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -25,7 +25,7 @@
namespace cvc5 {
-class TheoryEngine;
+class Env;
namespace theory {
@@ -48,7 +48,7 @@ class TheoryEngineModelBuilder
typedef std::unordered_set<Node> NodeSet;
public:
- TheoryEngineModelBuilder();
+ TheoryEngineModelBuilder(Env& env);
virtual ~TheoryEngineModelBuilder() {}
/**
* Should be called only on models m after they have been prepared
@@ -207,8 +207,8 @@ class TheoryEngineModelBuilder
* Assign all unassigned functions in the model m (those returned by
* TheoryModel::getFunctionsToAssign),
* using the two functions above. Currently:
- * If ufHo is disabled, we call assignFunction for all functions.
- * If ufHo is enabled, we call assignHoFunction.
+ * If HO logic is disabled, we call assignFunction for all functions.
+ * If HO logic is enabled, we call assignHoFunction.
*/
void assignFunctions(TheoryModel* m);
@@ -315,6 +315,8 @@ class TheoryEngineModelBuilder
Node v,
std::map<Node, bool>& visited);
//---------------------------------end for debugging finite model finding
+ /** Reference to the env */
+ Env& d_env;
}; /* class TheoryEngineModelBuilder */
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 853ae719b..af2bf4a3b 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -436,7 +436,7 @@ bool HoExtension::collectModelInfoHo(TheoryModel* m,
for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it)
{
Node n = *it;
- // For model-building with ufHo, we require that APPLY_UF is always
+ // For model-building with higher-order, we require that APPLY_UF is always
// expanded to HO_APPLY. That is, we always expand to a fully applicative
// encoding during model construction.
if (!collectModelInfoHoTerm(n, m))
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 3525786d5..9c506f2ac 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -49,6 +49,7 @@ TheoryUF::TheoryUF(Env& env,
d_ho(nullptr),
d_functionsTerms(getSatContext()),
d_symb(getUserContext(), instanceName),
+ d_rewriter(env.getLogicInfo().isHigherOrder()),
d_state(env, valuation),
d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false),
d_notify(d_im, *this)
@@ -94,8 +95,9 @@ void TheoryUF::finishInit() {
d_thss.reset(new CardinalityExtension(d_state, d_im, this));
}
// The kinds we are treating as function application in congruence
- d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
- if (options::ufHo())
+ d_equalityEngine->addFunctionKind(
+ kind::APPLY_UF, false, getLogicInfo().isHigherOrder());
+ if (getLogicInfo().isHigherOrder())
{
d_equalityEngine->addFunctionKind(kind::HO_APPLY);
d_ho.reset(new HoExtension(d_state, d_im));
@@ -146,7 +148,7 @@ void TheoryUF::postCheck(Effort level)
// check with the higher-order extension at full effort
if (!d_state.isInConflict() && fullEffort(level))
{
- if (options::ufHo())
+ if (getLogicInfo().isHigherOrder())
{
d_ho->check();
}
@@ -169,7 +171,7 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
{
case kind::EQUAL:
{
- if (options::ufHo() && options::ufHoExt())
+ if (getLogicInfo().isHigherOrder() && options::ufHoExt())
{
if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction())
{
@@ -212,7 +214,8 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
Kind k = node.getKind();
if (k == kind::HO_APPLY)
{
- if( !options::ufHo() ){
+ if (!getLogicInfo().isHigherOrder())
+ {
std::stringstream ss;
ss << "Partial function applications are only supported with "
"higher-order logic. Try adding the logic prefix HO_.";
@@ -230,7 +233,8 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
{
// check for higher-order
// logic exception if higher-order is not enabled
- if (isHigherOrderType(node.getOperator().getType()) && !options::ufHo())
+ if (isHigherOrderType(node.getOperator().getType())
+ && !getLogicInfo().isHigherOrder())
{
std::stringstream ss;
ss << "UF received an application whose operator has higher-order type "
@@ -252,8 +256,8 @@ void TheoryUF::preRegisterTerm(TNode node)
}
// we always use APPLY_UF if not higher-order, HO_APPLY if higher-order
- //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() );
- Assert(node.getKind() != kind::HO_APPLY || options::ufHo());
+ Assert(node.getKind() != kind::HO_APPLY
+ || getLogicInfo().isHigherOrder());
Kind k = node.getKind();
switch (k)
@@ -314,7 +318,8 @@ TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); }
bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
{
- if( options::ufHo() ){
+ if (getLogicInfo().isHigherOrder())
+ {
// must add extensionality disequalities for all pairs of (non-disequal)
// function equivalence classes.
if (!d_ho->collectModelInfoHo(m, termSet))
diff --git a/src/theory/uf/theory_uf_rewriter.cpp b/src/theory/uf/theory_uf_rewriter.cpp
index 082fe349e..f4bedb4b8 100644
--- a/src/theory/uf/theory_uf_rewriter.cpp
+++ b/src/theory/uf/theory_uf_rewriter.cpp
@@ -16,7 +16,6 @@
#include "theory/uf/theory_uf_rewriter.h"
#include "expr/node_algorithm.h"
-#include "options/uf_options.h"
#include "theory/rewriter.h"
#include "theory/substitutions.h"
@@ -24,6 +23,11 @@ namespace cvc5 {
namespace theory {
namespace uf {
+TheoryUfRewriter::TheoryUfRewriter(bool isHigherOrder)
+ : d_isHigherOrder(isHigherOrder)
+{
+}
+
RewriteResponse TheoryUfRewriter::postRewrite(TNode node)
{
if (node.getKind() == kind::EQUAL)
@@ -56,7 +60,7 @@ RewriteResponse TheoryUfRewriter::postRewrite(TNode node)
Node ret;
// build capture-avoiding substitution since in HOL shadowing may have
// been introduced
- if (options::ufHo())
+ if (d_isHigherOrder)
{
std::vector<Node> vars;
std::vector<Node> subs;
@@ -119,7 +123,7 @@ RewriteResponse TheoryUfRewriter::postRewrite(TNode node)
// build capture-avoiding substitution since in HOL shadowing may have
// been introduced
- if (options::ufHo())
+ if (d_isHigherOrder)
{
Node arg = Rewriter::rewrite(node[1]);
Node var = node[0][0][0];
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 23576b7a1..dfa797f71 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -34,6 +34,7 @@ namespace uf {
class TheoryUfRewriter : public TheoryRewriter
{
public:
+ TheoryUfRewriter(bool isHigherOrder = false);
RewriteResponse postRewrite(TNode node) override;
RewriteResponse preRewrite(TNode node) override;
@@ -61,6 +62,8 @@ class TheoryUfRewriter : public TheoryRewriter
* Then, f and g can be used as APPLY_UF operators, but (ite C f g), (lambda x1. (f x1)) as well as the variable x above are not.
*/
static bool canUseAsApplyUfOperator(TNode n);
+ /** Is the logic higher-order? */
+ bool d_isHigherOrder;
}; /* class TheoryUfRewriter */
} // namespace uf
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback