summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/term_database.cpp14
-rw-r--r--src/theory/quantifiers/term_database_sygus.cpp42
-rw-r--r--src/theory/quantifiers/term_database_sygus.h4
-rw-r--r--src/theory/quantifiers_engine.cpp19
4 files changed, 44 insertions, 35 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a3225e404..5db58067f 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -14,20 +14,12 @@
#include "theory/quantifiers/term_database.h"
-#include "expr/datatype.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
-#include "options/datatypes_options.h"
#include "options/uf_options.h"
-#include "theory/quantifiers/ce_guided_instantiation.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fun_def_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/rewrite_engine.h"
-#include "theory/quantifiers/theory_quantifiers.h"
-#include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/trigger.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
@@ -250,10 +242,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
d_ops.push_back(op);
d_op_map[op].push_back( n );
added.insert( n );
-
- if( d_quantEngine->getTermDatabaseSygus() ){
- d_quantEngine->getTermDatabaseSygus()->registerEvalTerm( n );
- }
}
}else{
setTermInactive( n );
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index f298e9711..d8d120eab 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -1912,32 +1912,38 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) {
void TermDbSygus::registerEvalTerm( Node n ) {
if( options::sygusDirectEval() ){
if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
- Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n
- << std::endl;
TypeNode tn = n[0].getType();
if( tn.isDatatype() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
if( dt.isSygus() ){
Node f = n.getOperator();
- Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl;
if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
- d_evals[n[0]].push_back( n );
- TypeNode tn = n[0].getType();
- Assert( tn.isDatatype() );
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Node var_list = Node::fromExpr( dt.getSygusVarList() );
- Assert( dt.isSygus() );
- d_eval_args[n[0]].push_back( std::vector< Node >() );
- bool isConst = true;
- for( unsigned j=1; j<n.getNumChildren(); j++ ){
- d_eval_args[n[0]].back().push_back( n[j] );
- if( !n[j].isConst() ){
- isConst = false;
+ if (d_eval_processed.find(n) == d_eval_processed.end())
+ {
+ Trace("sygus-eager")
+ << "TermDbSygus::eager: Register eval term : " << n
+ << std::endl;
+ d_eval_processed.insert(n);
+ d_evals[n[0]].push_back(n);
+ TypeNode tn = n[0].getType();
+ Assert(tn.isDatatype());
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Node var_list = Node::fromExpr(dt.getSygusVarList());
+ Assert(dt.isSygus());
+ d_eval_args[n[0]].push_back(std::vector<Node>());
+ bool isConst = true;
+ for (unsigned j = 1; j < n.getNumChildren(); j++)
+ {
+ d_eval_args[n[0]].back().push_back(n[j]);
+ if (!n[j].isConst())
+ {
+ isConst = false;
+ }
}
+ d_eval_args_const[n[0]].push_back(isConst);
+ Node a = getAnchor(n[0]);
+ d_subterms[a][n[0]] = true;
}
- d_eval_args_const[n[0]].push_back( isConst );
- Node a = getAnchor( n[0] );
- d_subterms[a][n[0]] = true;
}
}
}
diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index c819bc781..4786f053b 100644
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -17,6 +17,8 @@
#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
#define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
+#include <unordered_set>
+
#include "theory/quantifiers/sygus_explain.h"
#include "theory/quantifiers/term_database.h"
@@ -243,6 +245,8 @@ public: // for symmetry breaking
//for eager instantiation
// TODO (as part of #1235) move some of these functions to sygus_explain.h
private:
+ /** the set of evaluation terms we have already processed */
+ std::unordered_set<Node, NodeHashFunction> d_eval_processed;
std::map< Node, std::map< Node, bool > > d_subterms;
std::map< Node, std::vector< Node > > d_evals;
std::map< Node, std::vector< std::vector< Node > > > d_eval_args;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ac0de29e3..f6b920cda 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -854,10 +854,21 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
std::set< Node > added;
d_term_db->addTerm(n, added, withinQuant, withinInstClosure);
- //added contains also the Node that just have been asserted in this branch
- if( d_quant_rel ){
- for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
- if( !withinQuant ){
+ if (!withinQuant)
+ {
+ if (d_sygus_tdb)
+ {
+ d_sygus_tdb->registerEvalTerm(n);
+ }
+
+ // added contains also the Node that just have been asserted in this
+ // branch
+ if (d_quant_rel)
+ {
+ for (std::set<Node>::iterator i = added.begin(), end = added.end();
+ i != end;
+ i++)
+ {
d_quant_rel->setRelevance( i->getOperator(), 0 );
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback