summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp40
-rw-r--r--src/smt/smt_engine.h7
-rw-r--r--src/theory/quantifiers/anti_skolem.cpp11
-rw-r--r--src/theory/quantifiers/anti_skolem.h3
-rw-r--r--src/theory/theory_engine.cpp2
5 files changed, 34 insertions, 29 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c9484dbf0..46469fb0d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -989,8 +989,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
d_propEngine(NULL),
d_proofManager(NULL),
d_definedFunctions(NULL),
- d_fmfRecFunctionsAbs(NULL),
- d_fmfRecFunctionsConcrete(NULL),
+ d_fmfRecFunctionsDefined(NULL),
d_assertionList(NULL),
d_assignments(NULL),
d_modelGlobalCommands(),
@@ -1059,8 +1058,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
if( options::fmfFunWellDefined() || options::fmfFunWellDefinedRelevant() ){
- d_fmfRecFunctionsAbs = new(true) TypeNodeMap(d_userContext);
- d_fmfRecFunctionsConcrete = new(true) NodeListMap(d_userContext);
+ d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext);
}
d_modelCommands = new(true) smt::CommandList(d_userContext);
}
@@ -1206,13 +1204,10 @@ SmtEngine::~SmtEngine() throw() {
d_definedFunctions->deleteSelf();
- if( d_fmfRecFunctionsAbs != NULL ){
- d_fmfRecFunctionsAbs->deleteSelf();
+ if( d_fmfRecFunctionsDefined != NULL ){
+ d_fmfRecFunctionsDefined->deleteSelf();
}
- if( d_fmfRecFunctionsConcrete != NULL ){
- d_fmfRecFunctionsConcrete->deleteSelf();
- }
-
+
delete d_theoryEngine;
d_theoryEngine = NULL;
delete d_propEngine;
@@ -3998,27 +3993,28 @@ void SmtEnginePrivate::processAssertions() {
if( options::fmfFunWellDefined() ){
quantifiers::FunDefFmf fdf;
//must carry over current definitions (for incremental)
- for( SmtEngine::TypeNodeMap::const_iterator fit = d_smt.d_fmfRecFunctionsAbs->begin(); fit != d_smt.d_fmfRecFunctionsAbs->end(); ++fit ){
- Node f = (*fit).first;
- TypeNode ft = (*fit).second;
+ for( context::CDList<Node>::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin();
+ fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) {
+ Node f = (*fit);
+ Assert( d_smt.d_fmfRecFunctionsAbs.find( f )!=d_smt.d_fmfRecFunctionsAbs.end() );
+ TypeNode ft = d_smt.d_fmfRecFunctionsAbs[f];
fdf.d_sorts[f] = ft;
- SmtEngine::NodeListMap::const_iterator fcit = d_smt.d_fmfRecFunctionsConcrete->find( f );
- Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete->end() );
- SmtEngine::NodeList* cl = (*fcit).second;
- for( SmtEngine::NodeList::const_iterator cit = cl->begin(); cit != cl->end(); ++cit ){
- fdf.d_input_arg_inj[f].push_back( *cit );
+ std::map< Node, std::vector< Node > >::iterator fcit = d_smt.d_fmfRecFunctionsConcrete.find( f );
+ Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete.end() );
+ for( unsigned j=0; j<fcit->second.size(); j++ ){
+ fdf.d_input_arg_inj[f].push_back( fcit->second[j] );
}
}
fdf.simplify( d_assertions.ref() );
//must store new definitions (for incremental)
for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
Node f = fdf.d_funcs[i];
- d_smt.d_fmfRecFunctionsAbs->insert( f, fdf.d_sorts[f] );
- SmtEngine::NodeList* cl = new(true) SmtEngine::NodeList( d_smt.d_userContext );
+ d_smt.d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
+ d_smt.d_fmfRecFunctionsConcrete[f].clear();
for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){
- cl->push_back( fdf.d_input_arg_inj[f][j] );
+ d_smt.d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] );
}
- d_smt.d_fmfRecFunctionsConcrete->insert( f, cl );
+ d_smt.d_fmfRecFunctionsDefined->push_back( f );
}
}
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 760c7c071..f1ce2e0e9 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -130,9 +130,7 @@ class CVC4_PUBLIC SmtEngine {
/** The type of our internal assignment set */
typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
/** The types for the recursive function definitions */
- typedef context::CDHashMap< Node, TypeNode, NodeHashFunction > TypeNodeMap;
typedef context::CDList<Node> NodeList;
- typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
/** Expr manager context */
context::Context* d_context;
@@ -157,8 +155,9 @@ class CVC4_PUBLIC SmtEngine {
/** An index of our defined functions */
DefinedFunctionMap* d_definedFunctions;
/** recursive function definition abstractions for --fmf-fun */
- TypeNodeMap* d_fmfRecFunctionsAbs;
- NodeListMap* d_fmfRecFunctionsConcrete;
+ std::map< Node, TypeNode > d_fmfRecFunctionsAbs;
+ std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete;
+ NodeList* d_fmfRecFunctionsDefined;
/**
* The assertion list (before any conversion) for supporting
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index 9ccba38cd..908aeecfd 100644
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -9,7 +9,7 @@
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Implementation of anti-skolemization
+ ** \brief Implementation of anti-skolemization, e.g.:
** ( forall x. P[ f( x ) ] ^ forall x. Q[ f( x ) ] ) => forall x. exists y. ( P[ y ] ^ Q[ y ] )
**/
@@ -75,6 +75,15 @@ bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Nod
}
}
+QuantAntiSkolem::CDSkQuantCache::~CDSkQuantCache() {
+ for(std::map< Node, CDSkQuantCache* >::iterator i = d_data.begin(), iend = d_data.end();
+ i != iend; ++i){
+ CDSkQuantCache* current = (*i).second;
+ Assert(current != NULL);
+ delete current;
+ }
+}
+
QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe)
: QuantifiersModule(qe) {
d_sqc = new CDSkQuantCache(qe->getUserContext());
diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
index 48205db9d..c996b171e 100644
--- a/src/theory/quantifiers/anti_skolem.h
+++ b/src/theory/quantifiers/anti_skolem.h
@@ -9,7 +9,7 @@
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief dynamic quantifiers splitting
+ ** \brief anti-skolemization
**/
#include "cvc4_private.h"
@@ -71,6 +71,7 @@ public:
class CDSkQuantCache {
public:
CDSkQuantCache( context::Context* c ) : d_valid( c, false ){}
+ ~CDSkQuantCache();
std::map< Node, CDSkQuantCache* > d_data;
context::CDO< bool > d_valid;
bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 );
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 9de8fa0dd..cf7611dab 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -739,7 +739,7 @@ void TheoryEngine::propagate(Theory::Effort effort) {
Node TheoryEngine::getNextDecisionRequest() {
// Definition of the statement that is to be run by every theory
- unsigned min_priority;
+ unsigned min_priority = 0;
Node dec;
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
#undef CVC4_FOR_EACH_THEORY_STATEMENT
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback